commit 68d8cd408991e5532c2fce399d0154e578ab6ba5 Author: Barak Michener Date: Sat Aug 8 14:08:57 2020 -0700 a couple test scripts that translate Alloy into Z3 by hand diff --git a/barber.py b/barber.py new file mode 100644 index 0000000..a084711 --- /dev/null +++ b/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()) diff --git a/fp.py b/fp.py new file mode 100644 index 0000000..03d5525 --- /dev/null +++ b/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()) diff --git a/test.py b/test.py new file mode 100644 index 0000000..e5639e8 --- /dev/null +++ b/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())