kdrag.printers.latex

Functions

to_latex(obj[, prec])

to_latex_expr(expr[, prec])

to_latex_goal(goal)

to_latex_proof(proof[, prec])

to_latex_proof_state(state)

to_latex_sort(sort)

update_notation()

Refresh notation from registered kdrag.notation operators.

Classes

Infix(symbol, precedence)

Prefix(symbol, precedence)

class kdrag.printers.latex.Infix(symbol: str, precedence: int)

Bases: object

Parameters:

  • symbol (str)

  • precedence (int)

precedence: int
symbol: str
class kdrag.printers.latex.Prefix(symbol: str, precedence: int)

Bases: object

Parameters:

  • symbol (str)

  • precedence (int)

precedence: int
symbol: str
kdrag.printers.latex.to_latex(obj: ExprRef | SortRef | Proof | Goal | ProofState, prec: int = 0) → str
>>> x = smt.Int("x")
>>> to_latex(x + 1)
'\\text{x} + 1'
>>> to_latex(smt.IntSort())
'\\mathsf{Int}'
>>> to_latex(kd.prove(x < x + 1))
'\\vdash \\text{x} < \\text{x} + 1'
>>> l = tactics.Lemma(x > 0)
>>> to_latex(l)
'\\begin{array}{ll} \\hline \\vdash & \\text{x} > 0 \\end{array}'
Parameters:
Return type:

str

kdrag.printers.latex.to_latex_expr(expr: ExprRef, prec: int = 0) → str
>>> x, y = smt.Ints("x y")
>>> to_latex(x)
'\\text{x}'
>>> to_latex(smt.IntVal(42))
'42'
>>> to_latex(smt.BoolVal(True))
'\\top'
>>> to_latex(smt.BoolVal(False))
'\\bot'
>>> to_latex(smt.RealVal(2))
'2'
>>> to_latex(smt.RealVal("3/2"))
'\\frac{3}{2}'
>>> to_latex(smt.RealVal("-3/2"))
'-\\frac{3}{2}'
>>> to_latex(smt.StringVal("a_b"))
'\\text{"a\\_b"}'
>>> to_latex(smt.FPVal(1.5, smt.Float32()))
'1.5'
>>> to_latex(smt.FPVal(float("inf"), smt.Float32()))
'+\\infty'
>>> to_latex(smt.RNE())
'\\mathsf{RNE}'
>>> to_latex(smt.CharVal(65))
'\\operatorname{char}(65)'
>>> to_latex((x + 1) * y)
'(\\text{x} + 1) \\cdot \\text{y}'
>>> to_latex(x - (y + 1))
'\\text{x} - (\\text{y} + 1)'
>>> to_latex(-x)
'-\\text{x}'
>>> to_latex(-(x + y))
'-(\\text{x} + \\text{y})'
>>> to_latex(x / (y + 1))
'\\text{x} / (\\text{y} + 1)'
>>> to_latex(x % (y + 1))
'\\text{x} \\bmod (\\text{y} + 1)'
>>> to_latex(smt.If(x < y, x + 1, y + 1))
'\\begin{cases} \\text{x} + 1 & \\text{if } \\text{x} < \\text{y} \\\\ \\text{y} + 1 & \\text{otherwise} \\end{cases}'
>>> to_latex(smt.If(x < 0, -x, smt.If(x == 0, 0, x + 1)))
'\\begin{cases} -\\text{x} & \\text{if } \\text{x} < 0 \\\\ 0 & \\text{if } \\text{x} = 0 \\\\ \\text{x} + 1 & \\text{otherwise} \\end{cases}'
>>> to_latex(smt.And(x < y, y <= x + 1))
'(\\text{x} < \\text{y}) \\wedge (\\text{y} \\leq \\text{x} + 1)'
>>> to_latex(smt.And(x > y, y >= x + 1))
'(\\text{x} > \\text{y}) \\wedge (\\text{y} \\geq \\text{x} + 1)'
>>> to_latex(smt.Or(x < y, y < x))
'(\\text{x} < \\text{y}) \\vee (\\text{y} < \\text{x})'
>>> to_latex(smt.Not(x < y))
'\\neg (\\text{x} < \\text{y})'
>>> to_latex(smt.Implies(smt.And(x < y, y < 10), x < 9))
'((\\text{x} < \\text{y}) \\wedge (\\text{y} < 10)) \\rightarrow (\\text{x} < 9)'
>>> to_latex(smt.ForAll([x, y], smt.Implies(x < y, x + 1 <= y)))
'\\forall \\text{x}, \\text{y}. (\\text{x} < \\text{y}) \\rightarrow (\\text{x} + 1 \\leq \\text{y})'
>>> to_latex(smt.Lambda([x], x + 1))
'\\lambda \\text{x}. \\text{x} + 1'
>>> to_latex(smt.Lambda([x, y], x < y))
'\\lambda \\text{x}, \\text{y}. \\text{x} < \\text{y}'
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort())
>>> to_latex(f(x + 1))
'\\text{f}(\\text{x} + 1)'
>>> namespaced = smt.Const("Foo.Bar.biz", smt.IntSort())
>>> to_latex(namespaced)
'\\text{biz}_{\\text{Foo.Bar}}'
>>> to_latex(smt.Const("x!127", smt.IntSort()))
'\\text{x}_{127}'
>>> to_latex(smt.Const("Foo.Bar.x!127", smt.IntSort()))
'\\text{x}_{127, \\text{Foo.Bar}}'
>>> g = smt.Function("Foo.Bar.g", smt.IntSort(), smt.IntSort())
>>> to_latex(g(x))
'\\text{g}_{\\text{Foo.Bar}}(\\text{x})'
>>> to_latex(kd.prove(x < x + 1))
'\\vdash \\text{x} < \\text{x} + 1'
>>> a, b = smt.BitVecs("a b", 8)
>>> to_latex(smt.BitVecVal(0xA, 8))
'\\texttt{0x0a}'
>>> to_latex(smt.BitVecVal(0xBEEF, 16))
'\\texttt{0xbeef}'
>>> to_latex(smt.Concat(a, b))
'\\text{a} \\mathbin{+\\!+} \\text{b}'
>>> to_latex(a + b)
'\\text{a} + \\text{b}'
>>> to_latex(a - b)
'\\text{a} - \\text{b}'
>>> to_latex(a * b)
'\\text{a} * \\text{b}'
>>> to_latex(smt.Extract(7, 4, a))
'\\text{a}[7:4]'
>>> to_latex(smt.Extract(3, 3, a))
'\\text{a}[3]'
>>> to_latex(smt.Extract(11, 4, smt.Concat(a, b)))
'(\\text{a} \\mathbin{+\\!+} \\text{b})[11:4]'
>>> to_latex(a & b)
'\\text{a} \\mathbin{\\&} \\text{b}'
>>> to_latex(a | b)
'\\text{a} \\mid \\text{b}'
>>> to_latex(a ^ b)
'\\text{a} \\oplus \\text{b}'
>>> to_latex(~a)
'\\sim \\text{a}'
>>> to_latex(a << 2)
'\\text{a} \\ll \\texttt{0x02}'
>>> to_latex(smt.LShR(a, 2))
'\\text{a} \\gg_u \\texttt{0x02}'
>>> to_latex(a >> 2)
'\\text{a} \\gg_s \\texttt{0x02}'
>>> to_latex(smt.ULT(a, b))
'\\text{a} <_u \\text{b}'
>>> to_latex(a < b)
'\\text{a} <_s \\text{b}'
>>> to_latex(smt.ZeroExt(4, a))
'\\operatorname{zext}_{4}(\\text{a})'
>>> to_latex(smt.SignExt(4, a))
'\\operatorname{sext}_{4}(\\text{a})'
>>> to_latex(smt.RotateLeft(a, 3))
'\\operatorname{rotl}(\\text{a}, \\texttt{0x03})'
>>> to_latex(smt.RotateRight(a, 3))
'\\operatorname{rotr}(\\text{a}, \\texttt{0x03})'
>>> A = smt.Array("A", smt.IntSort(), smt.BitVecSort(8))
>>> to_latex(A[x + 1])
'\\text{A}[\\text{x} + 1]'
>>> to_latex(smt.Store(A, x, a))
'\\text{A}[\\text{x} := \\text{a}]'
>>> to_latex(smt.Store(smt.Store(A, x, a), y, b))
'\\text{A}[\\text{x} := \\text{a}][\\text{y} := \\text{b}]'
>>> to_latex(smt.EmptySet(smt.IntSort()))
'\\emptyset'
>>> to_latex(smt.Unit(x))
'[\\text{x}]'
>>> to_latex(smt.Unit(x + 1))
'[\\text{x} + 1]'
>>> to_latex(smt.Concat(smt.Unit(x), smt.Unit(y)))
'[\\text{x}] \\mathbin{+\\!+} [\\text{y}]'
Parameters:

  • expr (ExprRef)

  • prec (int)

Return type:

str

kdrag.printers.latex.to_latex_goal(goal: Goal) → str
>>> x = smt.Int("x")
>>> g = tactics.Goal(sig=[x], ctx=[x > 0, x < 10], goal=x == 5)
>>> to_latex_goal(g)
'\\begin{array}{ll} \\text{fix} & \\text{x} : \\mathsf{Int} \\\\ h_{0} & \\text{x} > 0 \\\\ h_{1} & \\text{x} < 10 \\\\ \\hline \\vdash & \\text{x} = 5 \\end{array}'
>>> to_latex_goal(tactics.Goal.empty())
'\\text{Nothing to do!}'
Parameters:

goal (Goal)

Return type:

str

kdrag.printers.latex.to_latex_proof(proof: Proof, prec: int = 0) → str
Parameters:

  • proof (Proof)

  • prec (int)

Return type:

str

kdrag.printers.latex.to_latex_proof_state(state: ProofState) → str
Parameters:

state (ProofState)

Return type:

str

kdrag.printers.latex.to_latex_sort(sort: SortRef) → str
>>> to_latex_sort(smt.BoolSort())
'\\mathsf{Bool}'
>>> to_latex_sort(smt.IntSort())
'\\mathsf{Int}'
>>> to_latex_sort(smt.RealSort())
'\\mathsf{Real}'
>>> to_latex_sort(smt.BitVecSort(8))
'\\mathsf{BV}_{8}'
>>> to_latex_sort(smt.SeqSort(smt.IntSort()))
'\\mathsf{Seq}(\\mathsf{Int})'
>>> to_latex_sort(smt.ArraySort(smt.IntSort(), smt.BoolSort()))
'\\mathsf{Int} \\to \\mathsf{Bool}'
>>> to_latex_sort(smt.ArraySort(smt.BitVecSort(8), smt.ArraySort(smt.IntSort(), smt.BoolSort())))
'\\mathsf{BV}_{8} \\to (\\mathsf{Int} \\to \\mathsf{Bool})'
>>> to_latex_sort(kd.TupleSort(smt.IntSort(), smt.BoolSort()))
'\\langle \\mathsf{Int}, \\mathsf{Bool} \\rangle'
Parameters:

sort (SortRef)

Return type:

str

kdrag.printers.latex.update_notation() → None

Refresh notation from registered kdrag.notation operators.

Only unary and binary FuncDeclRef methods are added. Call this after importing a theory that registers new notation-backed function declarations.

>>> from kdrag.theories import real
>>> update_notation()
>>> f, g = smt.Consts("f g", real.RFun)
>>> to_latex(f + g)
'\\text{f} + \\text{g}'
>>> from kdrag.theories.real import vec2
>>> update_notation()
>>> u = smt.Const("u", vec2.Vec2)
>>> to_latex(-u)
'-\\text{u}'
Return type:

None