kdrag.printers.tptp

Functions

expr_to_cnf(expr)	Print in CNF format.
expr_to_tptp(expr[, env, format, theories, ...])	Pretty print expr as TPTP
mangle_decl(d[, env])	Mangle a declaration to a tptp name.
sort_to_tptp(sort)	Pretty print sort as tptp

kdrag.printers.tptp.expr_to_cnf(expr: BoolRef) → str

Print in CNF format. Will recognize a single ForAll(, Or(Not(…))) layer.

>>> x = smt.Int("x")
>>> y = smt.Int("y")
>>> expr_to_cnf(smt.ForAll([x, y], smt.Or(x == y, x + 1 <= y)))
'(X = Y) | <=(+(X, 1), Y)'

Parameters:

expr (BoolRef)

Return type:

str

kdrag.printers.tptp.expr_to_tptp(expr: ExprRef, env=None, format='thf', theories=True, no_mangle=None) → str

Pretty print expr as TPTP

>>> x,y = smt.Ints("x y")
>>> expr_to_tptp(smt.ForAll([x,y], smt.Implies(x < y, x + 1 <= y)))
'(![X...:$int, Y...:$int] : ($less(X...,Y...) => $lesseq($sum(X...,1),Y...))'

Parameters:

expr (ExprRef)

Return type:

str

kdrag.printers.tptp.mangle_decl(d: FuncDeclRef, env=[])

Mangle a declaration to a tptp name. SMTLib supports type based overloading, TPTP does not.

Parameters:

d (FuncDeclRef)

kdrag.printers.tptp.sort_to_tptp(sort: SortRef)

Pretty print sort as tptp

>>> sort_to_tptp(smt.IntSort())
'$int'
>>> sort_to_tptp(smt.ArraySort(smt.IntSort(), smt.BoolSort()))
'($int > $o)'

Parameters:

sort (SortRef)