kdrag.solvers.scryer.from_scryer

kdrag.solvers.scryer.from_scryer(term: Term, decls: dict[str, FuncDeclRef]) → tuple[list[ExprRef], ExprRef]

Translate a scryer term to a z3 expression.

>>> x,y = smt.Ints("x y")
>>> decls = {"f": smt.Function("f", smt.IntSort(), smt.IntSort())}
>>> from_scryer(Compound("f", [Var("x")]), decls)
([x], f(x))
>>> from_scryer(Compound("=", [Compound("f", [Var("x")]), Var("y")]), decls)
([x, y], f(x) == y)

Parameters:

term (Term)
decls (dict[str, FuncDeclRef])

Return type:

tuple[list[ExprRef], ExprRef]