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: BaseSolver

a = a

add(thm: ExprRef)

Parameters:: thm (ExprRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

thm (BoolRef)
name (str)

b = b

c = c

check()

check_tptp_status(res)

extract(goal: ExprRef)

Parameters:: goal (ExprRef)

k = k

let(name, expr)

m = m

n = n

predefined = [And, Or, Not, Implies, -, +, *, ==, <=]

predefined_names = ['=']

predefined_sorts = ['Int', 'Real', 'Bool']

proof() → object

Return type:: object

res: subprocess.CompletedProcess | None

run(n)

run_cmd(cmd: str)

Parameters:: cmd (str)

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

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)