Open SundermannC opened 12 months ago
DIMACS is a standard format for specifying boolean formulas in CNF. It is used by most modern solvers. Exporting UVL models as DIMACS could be very helpful. There should be options in Z3 to export (at least some) formulas to DIMACS.
DIMACS is a standard format for specifying boolean formulas in CNF. It is used by most modern solvers. Exporting UVL models as DIMACS could be very helpful. There should be options in Z3 to export (at least some) formulas to DIMACS.