mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-15 07:15:26 +00:00
Code Activity

expose xor solver separate from cardinality solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-25 16:29:46 -08:00
parent 4e85a6e8fd
commit 388b025d9e
3 changed files with 9 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_params.pyg
View file

@ -26,6 +26,6 @@ def_module_params('sat',
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
('drat.check', BOOL, False, 'build up internal proof and check'), ('drat.check', BOOL, False, 'build up internal proof and check'),
('cardinality.solver', BOOL, False, 'use cardinality/xor solver'), ('cardinality.solver', BOOL, False, 'use cardinality solver'),
('cliff', UINT, 0, 'my favorite parameter'), ('xor.solver', BOOL, False, 'use xor solver'),
)) ))

2
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -217,7 +217,7 @@ public:
sat_params p1(p); sat_params p1(p);
m_params.set_bool("elim_vars", false); m_params.set_bool("elim_vars", false);
m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver()); m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver());
m_params.set_bool("cardinality_solver", p1.cardinality_solver()); m_params.set_bool("xor_solver", p1.xor_solver());
m_solver.updt_params(m_params); m_solver.updt_params(m_params);
m_optimize_model = m_params.get_bool("optimize_model", false); m_optimize_model = m_params.get_bool("optimize_model", false);

12
src/sat/tactic/goal2sat.cpp
View file

@ -65,7 +65,7 @@ struct goal2sat::imp {
expr_ref_vector m_trail; expr_ref_vector m_trail;
expr_ref_vector m_interpreted_atoms; expr_ref_vector m_interpreted_atoms;
bool m_default_external; bool m_default_external;
bool m_cardinality_solver; bool m_xor_solver;
imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external): imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
m(_m), m(_m),
@ -82,9 +82,9 @@ struct goal2sat::imp {
} }
void updt_params(params_ref const & p) { void updt_params(params_ref const & p) {
m_ite_extra = p.get_bool("ite_extra", true); m_ite_extra = p.get_bool("ite_extra", true);
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_cardinality_solver = p.get_bool("cardinality_solver", false); m_xor_solver = p.get_bool("xor_solver", false);
} }
void throw_op_not_handled(std::string const& s) { void throw_op_not_handled(std::string const& s) {
@ -560,7 +560,7 @@ struct goal2sat::imp {
unsigned get_num_args(app* t) { unsigned get_num_args(app* t) {
if (m.is_iff(t) && m_cardinality_solver) { if (m.is_iff(t) && m_xor_solver) {
unsigned n = 2; unsigned n = 2;
while (m.is_iff(t->get_arg(1))) { while (m.is_iff(t->get_arg(1))) {
++n; ++n;
@ -574,7 +574,7 @@ struct goal2sat::imp {
} }
expr* get_arg(app* t, unsigned idx) { expr* get_arg(app* t, unsigned idx) {
if (m.is_iff(t) && m_cardinality_solver) { if (m.is_iff(t) && m_xor_solver) {
while (idx >= 1) { while (idx >= 1) {
SASSERT(m.is_iff(t)); SASSERT(m.is_iff(t));
t = to_app(t->get_arg(1)); t = to_app(t->get_arg(1));