kdrag.printers.tptp.expr_to_tptp

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