mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add parameter to force sat-cleaning on initialization and on simplification phases
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f14a2b9a7c
commit
f5fea8ae30
|
@ -152,6 +152,8 @@ namespace sat {
|
|||
m_gc_burst = p.gc_burst();
|
||||
m_gc_defrag = p.gc_defrag();
|
||||
|
||||
m_force_cleanup = p.force_cleanup();
|
||||
|
||||
m_minimize_lemmas = p.minimize_lemmas();
|
||||
m_core_minimize = p.core_minimize();
|
||||
m_core_minimize_partial = p.core_minimize_partial();
|
||||
|
|
|
@ -136,6 +136,8 @@ namespace sat {
|
|||
bool m_gc_burst;
|
||||
bool m_gc_defrag;
|
||||
|
||||
bool m_force_cleanup;
|
||||
|
||||
|
||||
bool m_minimize_lemmas;
|
||||
bool m_dyn_sub_res;
|
||||
|
|
|
@ -31,6 +31,7 @@ def_module_params('sat',
|
|||
('gc.burst', BOOL, False, 'perform eager garbage collection during initialization'),
|
||||
('gc.defrag', BOOL, True, 'defragment clauses when garbage collecting'),
|
||||
('simplify.delay', UINT, 0, 'set initial delay of simplification by a conflict count'),
|
||||
('force_cleanup', BOOL, False, 'force cleanup to remove tautologies and simplify clauses'),
|
||||
('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
|
||||
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
|
||||
('core.minimize', BOOL, False, 'minimize computed core'),
|
||||
|
|
|
@ -1086,7 +1086,7 @@ namespace sat {
|
|||
init_assumptions(num_lits, lits);
|
||||
propagate(false);
|
||||
if (check_inconsistent()) return l_false;
|
||||
cleanup();
|
||||
cleanup(m_config.m_force_cleanup);
|
||||
|
||||
if (m_config.m_unit_walk) {
|
||||
return do_unit_walk();
|
||||
|
@ -1458,7 +1458,7 @@ namespace sat {
|
|||
if (should_restart())
|
||||
return l_undef;
|
||||
if (at_base_lvl()) {
|
||||
cleanup(); // cleaner may propagate frozen clauses
|
||||
cleanup(false); // cleaner may propagate frozen clauses
|
||||
if (inconsistent()) {
|
||||
TRACE("sat", tout << "conflict at level 0\n";);
|
||||
return l_false;
|
||||
|
@ -1654,7 +1654,7 @@ namespace sat {
|
|||
|
||||
SASSERT(at_base_lvl());
|
||||
|
||||
m_cleaner();
|
||||
m_cleaner(m_config.m_force_cleanup);
|
||||
CASSERT("sat_simplify_bug", check_invariant());
|
||||
|
||||
m_scc();
|
||||
|
@ -3695,10 +3695,10 @@ namespace sat {
|
|||
// Simplification
|
||||
//
|
||||
// -----------------------
|
||||
void solver::cleanup() {
|
||||
void solver::cleanup(bool force) {
|
||||
if (!at_base_lvl() || inconsistent())
|
||||
return;
|
||||
if (m_cleaner() && m_ext)
|
||||
if (m_cleaner(force) && m_ext)
|
||||
m_ext->clauses_modifed();
|
||||
}
|
||||
|
||||
|
|
|
@ -549,7 +549,7 @@ namespace sat {
|
|||
//
|
||||
// -----------------------
|
||||
public:
|
||||
void cleanup();
|
||||
void cleanup(bool force);
|
||||
void simplify(bool learned = true);
|
||||
void asymmetric_branching();
|
||||
unsigned scc_bin();
|
||||
|
|
Loading…
Reference in a new issue