kdrag.theories.sexp

Functions

Quote(e)	Quote an expression as an s-expression.
Truth(pf)	https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem
Unquote(sexp)	Interpret an s-expression as an expression.
of_sexp(sexp)
parse(s)	Parse a string as an s-expression.

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)))
")

Parameters:

e (ExprRef)

Return type:

tuple[ExprRef, Proof, Proof]

kdrag.theories.sexp.Truth(pf: Proof) → tuple[ExprRef, Proof, Proof, Proof]

https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem

>>> p = kd.prove(smt.BoolVal(True))
>>> Truth(p)
(Sexp("(declare-fun F (Bool) Bool) (assert (F true)) "),
|= truth(Sexp("(declare-fun F (Bool) Bool) (assert (F true)) ")),
|= has_interp(Sexp("(declare-fun F (Bool) Bool) (assert (F true)) "),  True),
|= interp(Sexp("(declare-fun F (Bool) Bool) (assert (F true)) ")) == True)

Parameters:

pf (Proof)

Return type:

tuple[ExprRef, Proof, Proof, Proof]

kdrag.theories.sexp.Unquote(sexp: ExprRef) → tuple[ExprRef, Proof, Proof]

Interpret an s-expression as an expression.

>>> x = smt.Int("x")
>>> q, hi1, i1 = Quote(x + 1)
>>> e, hi2, i2 = Unquote(q)
>>> e
x + 1
>>> assert hi1.thm.eq(hi2.thm) and i1.thm.eq(i2.thm)

Parameters:

sexp (ExprRef)

Return type:

tuple[ExprRef, Proof, Proof]

kdrag.theories.sexp.of_sexp(sexp: Sexp) → ExprRef

>>> of_sexp(['a', ['b', 'c']])
List(Concat(Unit(Atom("a")),
            Unit(List(Concat(Unit(Atom("b")),
                             Unit(Atom("c")))))))

Parameters:

sexp (Sexp)

Return type:

ExprRef

kdrag.theories.sexp.parse(s: str) → ExprRef

Parse a string as an s-expression.

>>> parse("(a b (c d))")
List(Unit(List(Concat(Unit(Atom("a")),
                    Concat(Unit(Atom("b")),
                            Unit(List(Concat(Unit(Atom("c")),
                                    Unit(Atom("d"))))))))))

Parameters:

s (str)

Return type:

ExprRef