34 lines
836 B
Python
34 lines
836 B
Python
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())
|