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

adding option to selectively enable bcd

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-29 22:15:24 -07:00
parent 60d7872cc8
commit 83a0611cb9
4 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_bceq.cpp
View file

@ -428,6 +428,8 @@ namespace sat {
void bceq::operator()() { void bceq::operator()() {
if (!m_solver.m_config.m_bcd) return;
flet<bool> _disable_bcd(m_solver.m_config.m_bcd, false);
use_list ul; use_list ul;
solver s(m_solver.m_params, 0); solver s(m_solver.m_params, 0);
m_use_list = &ul; m_use_list = &ul;

1
src/sat/sat_config.cpp
View file

@ -107,6 +107,7 @@ namespace sat {
m_minimize_core = p.minimize_core(); m_minimize_core = p.minimize_core();
m_minimize_core_partial = p.minimize_core_partial(); m_minimize_core_partial = p.minimize_core_partial();
m_optimize_model = p.optimize_model(); m_optimize_model = p.optimize_model();
m_bcd = p.bcd();
m_dyn_sub_res = p.dyn_sub_res(); m_dyn_sub_res = p.dyn_sub_res();
} }

1
src/sat/sat_config.h
View file

@ -71,6 +71,7 @@ namespace sat {
bool m_minimize_core; bool m_minimize_core;
bool m_minimize_core_partial; bool m_minimize_core_partial;
bool m_optimize_model; bool m_optimize_model;
bool m_bcd;
symbol m_always_true; symbol m_always_true;

1
src/sat/sat_params.pyg
View file

@ -21,4 +21,5 @@ def_module_params('sat',
('minimize_core', BOOL, False, 'minimize computed core'), ('minimize_core', BOOL, False, 'minimize computed core'),
('minimize_core_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('minimize_core_partial', BOOL, False, 'apply partial (cheap) core minimization'),
('optimize_model', BOOL, False, 'enable optimization of soft constraints'), ('optimize_model', BOOL, False, 'enable optimization of soft constraints'),
('bcd', BOOL, False, 'enable blocked clause decomposition for equality extraction'),
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'))) ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))