kdrag.parsers.microlean.parse

kdrag.parsers.microlean.parse(s: str, globals=None) → ExprRef

Parse a logical expression into an SMT expression.

>>> parse("x + 1", {"x": smt.Int("x")})
x + 1
>>> x, y = smt.Ints("x y")
>>> assert parse("forall (x y : Int), x + 1 = 0 -> x = -1").eq( smt.ForAll([x, y], x + 1 == 0, x == -1))
>>> a = smt.Real("a")
>>> assert parse("exists (a : Real), a * a = 2").eq(smt.Exists([a], a * a == 2))
>>> parse("fun (x : Int -> Int) => x 1 = 2")
Lambda(x, x[1] == 2)
>>> parse("fun (x : Int -> Int -> Int) => x 1 3 = 2")
Lambda(x, x[1][3] == 2)
>>> parse("f 3 2", {"f": smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort())})
f(3, 2)
>>> parse("fun (x : Int) (y : Real) => x + y > 0")
Lambda([x, y], ToReal(x) + y > 0)
>>> parse(r"forall (x : Int), x >= 0 /\ x < 10")
ForAll(x, And(x >= 0, x < 10))
>>> parse(r"forall (x : Int), x >= 0 && x < 10 -> x < 20")
ForAll(x, Implies(And(x >= 0, x < 10), x < 20))
>>> parse(r"exists (x : (BitVec 32) -> BitVec 8), x 8 = 5")
Exists(x, x[8] == 5)
>>> parse("fun x y (z : Int) => x + y + z", {"x": smt.Int("x"), "y": smt.Int("y")})
Lambda([x, y, z], x + y + z)
>>> parse("fun (x : 'a) => x").sort()
Array(a, a)
>>> parse("true")
True
>>> parse("[true, false]")
Concat(Unit(True), Unit(False))
>>> q = smt.Const("x", smt.TupleSort("pair", [smt.IntSort(), smt.BoolSort()])[0])
>>> parse("q.project1", {"q": q})
project1(x)
>>> parse("{x : Int | x > 0}")
Lambda(x, x > 0)
>>> parse("if true && false then 1 + 1 else 0")
If(And(True, False), 2, 0)

Parameters:

s (str)

Return type:

ExprRef