kdrag.printers.smtlib

In some cases, the default smtlib printers in z3 do not output reparseable SMT-LIB code for other solvers. Z3 has some extra features, and also identical names with different sorts may need to be mangled This module provides SMT-LIB printers for such cases.

Functions

`expr_to_smtlib`(expr)
`funcdecl_smtlib`(decl)
`mangle_decl_smtlib`(d)	Mangle a declaration to remove overloading
`smtlib_datatypes`(dts)

kdrag.printers.smtlib.expr_to_smtlib(expr: ExprRef)

Parameters:: expr (ExprRef)

kdrag.printers.smtlib.funcdecl_smtlib(decl: FuncDeclRef)

Parameters:: decl (FuncDeclRef)

kdrag.printers.smtlib.mangle_decl_smtlib(d: FuncDeclRef)

Mangle a declaration to remove overloading

Parameters:: d (FuncDeclRef)

kdrag.printers.smtlib.smtlib_datatypes(dts: list[DatatypeSortRef]) → str

Parameters:: dts (list[DatatypeSortRef])
Return type:: str