kdrag.solvers.scryer

Functions

from_scryer(term, decls)	Translate a scryer term to a z3 expression.
in_term(term, tags)
subterms(term)
to_scryer_str(expr)
to_term(vs, expr)

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]

kdrag.solvers.scryer.in_term(term: Term, tags: set[Term]) → set[Term]

Parameters:

• term (Term)

• tags (set[Term])

Return type:

set[Term]

kdrag.solvers.scryer.subterms(term: Term) → set[Term]

Parameters:

term (Term)

Return type:

set[Term]

kdrag.solvers.scryer.to_scryer_str(expr: BoolRef) → str

Parameters:

expr (BoolRef)

Return type:

str

kdrag.solvers.scryer.to_term(vs: list[ExprRef], expr: ExprRef) → Term

>>> x,y = smt.Ints("x y")
>>> str(to_term([], x + y))
'+(x, y)'

Parameters:

• vs (list[ExprRef])

• expr (ExprRef)

Return type:

Term