mirror of
https://github.com/Z3Prover/z3
synced 2025-10-26 17:29:21 +00:00
426306376f
* split sat2goal out of goal2sat These two classes need different things out of the sat::solver class, and separating them makes it easier to fiddle with their dependencies independently. I also fiddled with some headers to make it possible to include sat_solver_core.h instead of sat_solver.h. * limit solver_core methods to those needed by goal2sat And switch sat2goal and sat_tactic over to relying on the derived sat::solver class instead. There were no other uses of solver_core. I'm hoping this makes it feasible to reuse goal2sat's CNF conversion from places like the tseitin-cnf tactic, so they can be unified into a single implementation. |
||
|---|---|---|
| .. | ||
| CMakeLists.txt | ||
| datalog_frontend.cpp | ||
| datalog_frontend.h | ||
| dimacs_frontend.cpp | ||
| dimacs_frontend.h | ||
| drat_frontend.cpp | ||
| drat_frontend.h | ||
| lp_frontend.cpp | ||
| lp_frontend.h | ||
| main.cpp | ||
| opt_frontend.cpp | ||
| opt_frontend.h | ||
| options.h | ||
| smtlib_frontend.cpp | ||
| smtlib_frontend.h | ||
| z3_log_frontend.cpp | ||
| z3_log_frontend.h | ||