kdrag.solvers.prolog

Functions

get_vars(e)
interp(t)
interp_pred(t)
interp_term(t)
prolog(vs0, goals, rules0)	A small prolog interpreter.
run_string(s)	Run a Prolog-like string and return the results.

kdrag.solvers.prolog.get_vars(e: ExprRef) → list[ExprRef]

Parameters:

e (ExprRef)

Return type:

list[ExprRef]

kdrag.solvers.prolog.interp(t: Tree) → tuple[list[BoolRef | QuantifierRef], list[tuple[list[ExprRef], list[BoolRef]]]]

Parameters:

t (Tree)

Return type:

tuple[list[BoolRef | QuantifierRef], list[tuple[list[ExprRef], list[BoolRef]]]]

kdrag.solvers.prolog.interp_pred(t: Tree) → BoolRef

Parameters:

t (Tree)

Return type:

BoolRef

kdrag.solvers.prolog.interp_term(t: Tree) → ExprRef

Parameters:

t (Tree)

Return type:

ExprRef

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

kdrag.solvers.prolog.run_string(s: str)

Run a Prolog-like string and return the results.

>>> run_string("plus(z, Y, Y). plus(s(X), Y, s(Z)) :- plus(X, Y, Z). ?- plus(X, Y, s(z)).")
[([], {Y: s(z), X: z}), ([], {X: s(z), Y: z})]

Parameters:

s (str)