kdrag.solvers.egglog

Functions

mangle_name(name)
z3_to_egglog(e[, vars])	a simple sexpr traversal, but we wrap 0-arity constants in parens and vars in no parens to match egglog's syntax

Classes

EgglogSolver([debug])

class kdrag.solvers.egglog.EgglogSolver(debug=False)

Bases: object

add(thm: Proof | BoolRef | list[BoolRef | Proof])

>>> s = EgglogSolver()
>>> x, y = smt.Ints("x y")
>>> add = smt.Function("add", smt.IntSort(), smt.IntSort(), smt.IntSort())
>>> s.add(smt.ForAll([x, y], add(x,y) == add(y, x)))
>>> res = s.run(5)

>>> s = EgglogSolver()
>>> V = smt.DeclareSort("V")
>>> x, y, z = smt.Consts("x y z", V)
>>> edge = smt.Function("edge", V, V, smt.BoolSort())
>>> path = smt.Function("path", V, V, smt.BoolSort())
>>> s.add(smt.ForAll([x, y], edge(x,y), path(x,y)))
>>> s.add(smt.ForAll([x, y, z], path(x,y), edge(y,z), path(x,z)))
>>> s.add(edge(x,y))
>>> s.add(edge(y,z))
>>> _ = s.run(10)
>>> _ = s.run_cmd("(print-function path 100)")

Parameters:

thm (Proof | BoolRef | list[BoolRef | Proof])

extract(goal: ExprRef)

Parameters:

goal (ExprRef)

let(name, expr)

predefined_names = ['=', '=>', 'and', 'or', 'not', 'true', 'false']

print_decl(decl: FuncDeclRef, n: int)

Parameters:

• decl (FuncDeclRef)

• n (int)

run(n)

run_cmd(cmd: str)

Parameters:

cmd (str)

kdrag.solvers.egglog.mangle_name(name)

kdrag.solvers.egglog.z3_to_egglog(e: ExprRef, vars=[])

a simple sexpr traversal, but we wrap 0-arity constants in parens and vars in no parens to match egglog’s syntax

Parameters:

e (ExprRef)