a couple test scripts that translate Alloy into Z3 by hand

barber.py

@@ -0,0 +1,112 @@
+from z3 import DeclareSort
+from z3 import Distinct
+from z3 import Const
+from z3 import Consts
+from z3 import Function
+from z3 import ForAll
+from z3 import Exists
+from z3 import Implies
+from z3 import And
+from z3 import Or
+from z3 import Xor
+from z3 import Not
+from z3 import BoolSort
+from z3 import Solver
+
+from typing import Any
+from typing import List
+
+axioms: List[Any] = []
+
+Sig = DeclareSort('Sig')
+Instance = DeclareSort('Instance')
+subtype = Function('subtype', Sig, Sig, BoolSort())
+
+x, y, z = Consts('x, y, z', Sig)
+inheritance_axioms = [
+    ForAll(x, subtype(x, x)),
+    ForAll([x, y, z], Implies(And(subtype(x, y), subtype(y, z)),
+                              subtype(x, z))),
+    ForAll([x, y], Implies(And(subtype(x, y), subtype(y, x)),
+                           x == y)),
+    ForAll([x, y, z], Implies(And(subtype(x, y), subtype(x, z)),
+                              Or(subtype(y, z), subtype(z, y)))),
+]
+
+a, b, c = Consts('a b c', Instance)
+typeOf = Function('typeOf', Instance, Sig)
+inClass = Function('inClass', Instance, Sig, BoolSort())
+instance_axioms = [
+    ForAll([a, x, y], Implies(And(typeOf(a) == x, typeOf(a) == y), x == y)),
+    ForAll([a, x], Implies(typeOf(a) == x, inClass(a, x))),
+    ForAll([a, x, y], Implies(And(inClass(a, x), subtype(y, x)),
+                              inClass(a, y))),
+]
+
+axioms.extend(inheritance_axioms)
+axioms.extend(instance_axioms)
+
+# sig Man {shaves: set Man}
+# one sig Barber extends Man {}
+
+
+Man = Const('Man', Sig)
+shaves = Function('Man::shaves', Instance, Instance, BoolSort())
+ax = [
+    ForAll([a, b], Implies(shaves(a, b),
+                           And(inClass(a, Man), inClass(b, Man))))
+
+]
+axioms.extend(ax)
+
+Barber = Const('Barber', Sig)
+
+ax = [
+    subtype(Barber, Man),
+    # lone constraint
+    Exists([a], typeOf(a) == Barber),
+    # one constraint
+    ForAll([a, b], Implies(And(typeOf(a) == Barber, typeOf(b) == Barber),
+                           a == b)),
+]
+axioms.extend(ax)
+
+# fact {
+#   Barber.shaves = {m: Man | m not in m.shaves}
+# }
+
+ax = [
+    ForAll([a], Implies(
+        typeOf(a) == Barber,
+        ForAll([b],
+               Implies(
+                   inClass(b, Man),
+                   And(
+                       shaves(a, b),
+                       Not(shaves(b, b))
+                   ))))),
+]
+axioms.extend(ax)
+
+ax = [
+    ForAll([a], Xor(
+        typeOf(a) == Barber,
+        typeOf(a) == Man,
+    ))
+]
+axioms.extend(ax)
+
+# run { }
+
+inst1 = Const('inst1', Instance)
+inst2 = Const('inst2', Instance)
+
+
+s = Solver()
+
+for c in axioms:
+    s.assert_and_track(c, c.__str__())
+
+s.add(Distinct(inst1, inst2))
+
+print(s.check())

fp.py

@@ -0,0 +1,34 @@
+from z3 import *
+
+Sig = DeclareSort("Sig")
+Instance = DeclareSort("Instance")
+
+Object = Const('Object', Sig)
+Farmer, Fox, Chicken, Grain = Consts('Farmer Fox Chicken, Grain', Sig)
+IsType = Function('IsType', Sig, Sig, BoolSort())
+fp.register_relation(IsType)
+
+fp = Fixedpoint()
+
+fp.fact(IsType(Object, Object))
+fp.fact(IsType(Farmer, Object))
+fp.fact(IsType(Fox, Object))
+fp.fact(IsType(Chicken, Object))
+fp.fact(IsType(Grain, Object))
+
+Eats = Function("Eats", Sig, Sig, BoolSort())
+fp.register_relation(Eats)
+
+def genEats(x, y):
+    fp.rule(Eats(x, y), IsType(x, Object), IsType(y, Object))
+
+genEats(Fox, Chicken)
+genEats(Chicken, Grain)
+
+State = Const("State", Sig)
+Near = Const("State::Near", Sig, Sig, BoolSort())
+fp.register_relation(Near)
+Far = Const("State::Far", Sig, Sig, BoolSort())
+fp.register_relation(Far)
+
+fp.rule(Near())

test.py

@@ -0,0 +1,84 @@
+from z3 import *
+from z3 import Solver
+# A = DeclareSort('A')
+# x, y = Consts('x y', A)
+# f = Function('f', A, A)
+
+# s = Solver()
+# s.add(f(f(x)) == x, f(x) == y, x != y)
+
+# print(s.check())
+# m = s.model()
+# print(m)
+# print("interpretation assigned to A:")
+# print(m[A])
+
+
+Type     = DeclareSort('Type')
+subtype  = Function('subtype', Type, Type, BoolSort())
+root     = Const('root', Type)
+
+x, y, z  = Consts('x y z', Type)
+
+Instance = DeclareSort('Instance')
+typeOf = Function('type', Instance, Type)
+instance_of = Function('instance_of', Instance, Type, BoolSort())
+
+a, b, c = Consts('a b c', Instance)
+instance_axioms = [
+    ForAll(a, Exists(x, typeOf(a) == x)),
+    ForAll([a, x, y], Implies(And(typeOf(a) == x, typeOf(a) == y), x == y)),
+    ForAll([a, x], Implies(typeOf(a) == x, instance_of(a, x))),
+    ForAll([a, x, y], Implies(And(instance_of(a, x), subtype(y, x)), instance_of(a, y))),
+]
+
+axioms = [
+    ForAll(x, subtype(x, x)),
+    ForAll([x, y, z], Implies(And(subtype(x, y), subtype(y, z)),
+                              subtype(x, z))),
+    ForAll([x, y], Implies(And(subtype(x, y), subtype(y, x)),
+                           x == y)),
+    ForAll([x, y, z], Implies(And(subtype(x, y), subtype(x, z)),
+                              Or(subtype(y, z), subtype(z, y)))),
+    ForAll(x, subtype(root, x)),
+]
+
+
+class Foo:
+    def __init__(self, str_reason):
+        self.reason = str_reason
+
+
+myType = Const('myType', Type)
+myInstance = Const('myInst', Instance)
+myOtherType = Const('otherType', Type)
+
+# fp = Fixedpoint()
+# fp.register_relation(type)
+# fp.register_relation(instance_of)
+# fp.register_relation(subtype)
+# fp.declare_var(myType, myInstance, myOtherType, root)
+
+# fp.get_answer()
+
+s = Solver()
+for ax in axioms + instance_axioms:
+    s.assert_and_track(ax, ax.__str__())
+
+checks = [
+    typeOf(myInstance) == myType,
+    typeOf(a) == myOtherType,
+    subtype(myType, myOtherType),
+]
+
+for c in checks:
+    s.assert_and_track(c, c.__str__())
+print( s )
+print( s.check() )
+print( "Interpretation for Type:")
+# print(s.model()[Type])
+# print( "Interpretation for Instance:")
+# print(s.model()[Instance])
+# print("Model:")
+# print(s.model())
+# print(s.statistics())