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())