kdrag.printers.tptp.cnf_file

kdrag.printers.tptp.cnf_file(axioms: list[BoolRef], nnf=False) → str

Make a file out of a list of axioms in CNF format. Will recognize a single ForAll(, Or(Not(…))) layer. >>> x,y = smt.Ints(“x y”) >>> f = smt.Function(“f”, smt.IntSort(), smt.IntSort()) >>> cnf_file([smt.ForAll([x, y], smt.Or(x == y, f(x) <= f(y)))]) ‘cnf(0,axiom,(X = Y) | <=(f(X), f(Y))).’