kdrag.solvers.expr_to_cnf

kdrag.solvers.expr_to_cnf(expr: BoolRef) → str

Print in CNF format. Will recognize a single ForAll(, Or(Not(…))) layer.

>>> x = smt.Int("x")
>>> y = smt.Int("y")
>>> expr_to_cnf(smt.ForAll([x, y], smt.Or(x == y, x + 1 <= y)))
'(X = Y) | <=(+(X, 1), Y)'