mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-02-19 11:32:18 -08:00
commit 0cf5af121a
3 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_params.pyg
View file

@ -26,4 +26,5 @@ 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, True, 'use cardinality solver'),
)) ))

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

@ -82,9 +82,7 @@ public:
m_num_scopes(0), m_num_scopes(0),
m_dep_core(m), m_dep_core(m),
m_unknown("no reason given") { m_unknown("no reason given") {
m_params.set_bool("elim_vars", false); updt_params(p);
sat_params p1(m_params);
m_solver.updt_params(m_params);
init_preprocess(); init_preprocess();
} }
@ -218,8 +216,10 @@ public:
m_params.append(p); m_params.append(p);
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_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);
} }
virtual void collect_statistics(statistics & st) const { virtual void collect_statistics(statistics & st) const {
if (m_preprocess) m_preprocess->collect_statistics(st); if (m_preprocess) m_preprocess->collect_statistics(st);