kdrag.solvers.prolog.prolog

kdrag.solvers.prolog.prolog(vs0: list[ExprRef], goals: list[BoolRef], rules0: Sequence[Rule | QuantifierRef | BoolRef])

A small prolog interpreter. THis is a generator of solutions consisting of variable list, substitution pairs.

>>> import kdrag.theories.nat as nat
>>> x,y,z = smt.Consts("x y z", nat.Nat)
>>> plus = smt.Function("plus", nat.Nat, nat.Nat, nat.Nat, smt.BoolSort())
>>> rules = [        kd.QForAll([y], plus(nat.Z, y, y)),        kd.QForAll([x,y,z], smt.Implies(            plus(x, y, z),            plus(nat.S(x), y, nat.S(z))        ))]
>>> list(prolog([x,y], [plus(x, y, nat.S(nat.Z))], rules))
[([], {y: S(Z), x: Z}), ([], {x: S(Z), y: Z})]

Parameters:

• vs0 (list[ExprRef])

• goals (list[BoolRef])

• rules0 (Sequence[Rule | QuantifierRef | BoolRef])