From 2aedaf315a3fca530322381a43525ac473fcae4c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 May 2018 16:32:38 +0100 Subject: [PATCH] fix removal bug, tune all-interval usage Signed-off-by: Nikolaj Bjorner --- examples/python/all_interval_series.py | 2 ++ src/sat/sat_params.pyg | 2 +- src/sat/sat_simplifier.cpp | 5 +++-- src/sat/sat_simplifier.h | 2 ++ src/sat/sat_solver.cpp | 15 ++++++++++++--- src/sat/sat_solver.h | 2 ++ 6 files changed, 22 insertions(+), 6 deletions(-) diff --git a/examples/python/all_interval_series.py b/examples/python/all_interval_series.py index 216941451..8269303d3 100644 --- a/examples/python/all_interval_series.py +++ b/examples/python/all_interval_series.py @@ -8,6 +8,8 @@ from __future__ import print_function from z3 import * import time +set_option("sat.gc.burst", False) # disable GC at every search. It is wasteful for these small queries. + def diff_at_j_is_i(xs, j, i): assert(0 <= j and j + 1 < len(xs)) assert(1 <= i and i < len(xs)) diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index ce40949da..dd840468e 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -28,7 +28,7 @@ def_module_params('sat', ('gc.increment', UINT, 500, 'increment to the garbage collection threshold'), ('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'), ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'), - ('gc.burst', BOOL, True, 'perform eager garbage collection during initialization'), + ('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'), ('minimize_lemmas', BOOL, True, 'minimize learned clauses'), diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 314b661ea..efdf8a39a 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -664,8 +664,9 @@ namespace sat { m_sub_todo.insert(it.curr()); } clause_use_list& cs = m_use_list.get(l); - for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) { + for (auto it = cs.mk_iterator(); !it.at_end(); ) { clause & c = it.curr(); + it.next(); remove_clause(c, l); } cs.reset(); @@ -2023,7 +2024,7 @@ namespace sat { m_new_cls.reset(); if (!resolve(c1, c2, pos_l, m_new_cls)) continue; - if (false && v == 27041) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n"); + if (false && v == 767) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n"); TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";); if (cleanup_clause(m_new_cls)) continue; // clause is already satisfied. diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index a777e07a4..3787b5894 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -219,6 +219,8 @@ namespace sat { simplifier(solver & s, params_ref const & p); ~simplifier(); + void init_search() { m_num_calls = 0; } + void insert_elim_todo(bool_var v) { m_elim_todo.insert(v); } void reset_todos() { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index c8173d1e7..c55383a57 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -524,8 +524,15 @@ namespace sat { } }; + bool solver::should_defrag() { + if (m_defrag_threshold > 0) --m_defrag_threshold; + return m_defrag_threshold == 0 && m_config.m_gc_defrag; + } + void solver::defrag_clauses() { + return; if (memory_pressure()) return; + pop(scope_lvl()); IF_VERBOSE(1, verbose_stream() << "(sat-defrag)\n"); clause_allocator& alloc = m_cls_allocator[!m_cls_allocator_idx]; ptr_vector new_clauses, new_learned; @@ -585,6 +592,8 @@ namespace sat { cls_allocator().finalize(); m_cls_allocator_idx = !m_cls_allocator_idx; + + reinit_assumptions(); } @@ -1576,6 +1585,7 @@ namespace sat { m_restart_threshold = m_config.m_restart_initial; m_luby_idx = 1; m_gc_threshold = m_config.m_gc_initial; + m_defrag_threshold = 2; m_restarts = 0; m_simplifications = 0; m_conflicts_since_init = 0; @@ -1590,6 +1600,7 @@ namespace sat { m_core.reset(); m_min_core_valid = false; m_min_core.reset(); + m_simplifier.init_search(); TRACE("sat", display(tout);); } @@ -1939,10 +1950,8 @@ namespace sat { break; } if (m_ext) m_ext->gc(); - if (gc > 0 && m_config.m_gc_defrag && !memory_pressure()) { - pop(scope_lvl()); + if (gc > 0 && should_defrag()) { defrag_clauses(); - reinit_assumptions(); } m_conflicts_since_gc = 0; m_gc_threshold += m_config.m_gc_increment; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 1c5e10616..b44c04604 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -230,6 +230,7 @@ namespace sat { inline void dealloc_clause(clause* c) { cls_allocator().del_clause(c); } struct cmp_activity; void defrag_clauses(); + bool should_defrag(); bool memory_pressure(); void del_clause(clause & c); clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned); @@ -392,6 +393,7 @@ namespace sat { unsigned m_luby_idx; unsigned m_conflicts_since_gc; unsigned m_gc_threshold; + unsigned m_defrag_threshold; unsigned m_num_checkpoints; double m_min_d_tk; unsigned m_next_simplify;