kdrag.theories.sexp.Quote

kdrag.theories.sexp.Quote(e: ExprRef) → tuple[ExprRef, Proof, Proof]

Quote an expression as an s-expression.

>>> x = smt.Int("x")
>>> sexp, _ ,_ = Quote(x + 1)
>>> sexp
Sexp("(declare-fun F (Int) Bool)
(declare-fun x () Int)
(assert (F (+ x 1)))
")