kdrag.printers.latex.to_latex_expr

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