157 lines
3.8 KiB
Python
157 lines
3.8 KiB
Python
from z3 import DeclareSort
|
|
from z3 import Datatype
|
|
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 IntSort
|
|
from z3 import Solver
|
|
|
|
from functools import reduce
|
|
from typing import Any
|
|
from typing import List
|
|
|
|
axioms: List[Any] = []
|
|
|
|
Sig = Datatype('Sig')
|
|
Sig.declare("Person")
|
|
Sig.declare("Man")
|
|
Sig.declare("Woman")
|
|
Sig.declare("Barber")
|
|
Sig = Sig.create()
|
|
|
|
Type = DeclareSort('Type')
|
|
Instance = DeclareSort('Instance')
|
|
subtype = Function('subtype', Type, Type, BoolSort())
|
|
|
|
x, y, z = Consts('x, y, z', Type)
|
|
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 = Consts('a b', Instance)
|
|
typeOf = Function('typeOf', Instance, Type, BoolSort())
|
|
inClass = Function('inClass', Instance, Type, BoolSort())
|
|
hasSig = Function('hasSig', Instance, Sig, BoolSort())
|
|
s, o = Consts('s o', Sig)
|
|
instance_axioms = [
|
|
ForAll([a, s, o], Implies(And(hasSig(a, s), hasSig(a, o)), s == o)),
|
|
ForAll([a], Exists([s], hasSig(a, s))),
|
|
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), 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)
|
|
|
|
|
|
# abstract sig Person {shaves: set Man}
|
|
# sig Man, Woman extends Person{}
|
|
# one sig Barber in Person {} // must be 'in' not 'extends':
|
|
|
|
Man = Const("Man", Type)
|
|
Woman = Const("Woman", Type)
|
|
Person = Const("Person", Type)
|
|
ax = [
|
|
subtype(Person, Man),
|
|
subtype(Person, Woman),
|
|
|
|
Not(Exists([a], hasSig(a, Sig.Person))),
|
|
Not(Exists([a], typeOf(a, Person))),
|
|
ForAll([a], Implies(hasSig(a, Sig.Man), typeOf(a, Man))),
|
|
ForAll([a], Implies(hasSig(a, Sig.Woman), typeOf(a, Woman))),
|
|
ForAll([a], Implies(hasSig(a, Sig.Barber), inClass(a, Person))),
|
|
]
|
|
axioms.extend(ax)
|
|
|
|
|
|
shaves = Function('Person::shaves', Instance, Instance, BoolSort())
|
|
ax = [
|
|
ForAll([a, b], Implies(shaves(a, b),
|
|
And(inClass(a, Person), inClass(b, Man))))
|
|
|
|
]
|
|
axioms.extend(ax)
|
|
|
|
|
|
ax = [
|
|
# lone constraint
|
|
Exists(a, hasSig(a, Sig.Barber)),
|
|
# one constraint
|
|
ForAll([a, b], Implies(And(hasSig(a, Sig.Barber), hasSig(b, Sig.Barber)),
|
|
a == b)),
|
|
]
|
|
|
|
axioms.extend(ax)
|
|
|
|
# fact {
|
|
# Barber.shaves = {m: Man | m not in m.shaves}
|
|
# }
|
|
|
|
ax = [
|
|
ForAll(a, Implies(
|
|
hasSig(a, Sig.Barber),
|
|
ForAll(b,
|
|
Implies(
|
|
inClass(b, Man),
|
|
And(
|
|
shaves(a, b),
|
|
Not(shaves(b, b))
|
|
))))),
|
|
]
|
|
axioms.extend(ax)
|
|
|
|
ax = [
|
|
ForAll(a, Or(
|
|
hasSig(a, Sig.Man),
|
|
hasSig(a, Sig.Barber),
|
|
hasSig(a, Sig.Person),
|
|
hasSig(a, Sig.Woman),
|
|
))
|
|
]
|
|
axioms.extend(ax)
|
|
|
|
# run { }
|
|
|
|
inst1 = Const('inst1', Instance)
|
|
inst2 = Const('inst2', Instance)
|
|
|
|
ax = [
|
|
hasSig(inst1, Sig.Man),
|
|
ForAll(a, Or(a == inst1, a == inst2)),
|
|
ForAll(x, Or(x == Man, x == Woman, x == Person)),
|
|
]
|
|
axioms.extend(ax)
|
|
|
|
|
|
s = Solver()
|
|
|
|
|
|
for i, c in enumerate(axioms):
|
|
s.assert_and_track(c, str(i) + c.__str__())
|
|
|
|
s.assert_and_track(Distinct(inst1, inst2), "distinct")
|
|
#s.assert_and_track(ForAll([a], And(a < 2, a >= 0)), "maxsize")
|
|
|
|
|
|
print(s.check())
|
|
m = s.model()
|
|
g = Const("g", Sig)
|
|
test = Const("test", Type)
|