mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove cache reset that causes crash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
030868d8de
commit
b3e5fade32
|
@ -48,14 +48,10 @@ void ast_translation::reset_cache() {
|
|||
void ast_translation::cache(ast * s, ast * t) {
|
||||
SASSERT(!m_cache.contains(s));
|
||||
if (s->get_ref_count() > 1) {
|
||||
if (m_insert_count > (1 << 17)) {
|
||||
reset_cache();
|
||||
m_insert_count = 0;
|
||||
}
|
||||
m_cache.insert(s, t);
|
||||
++m_insert_count;
|
||||
m_from_manager.inc_ref(s);
|
||||
m_to_manager.inc_ref(t);
|
||||
m_cache.insert(s, t);
|
||||
++m_insert_count;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -55,9 +55,11 @@ namespace sat {
|
|||
~report() {
|
||||
m_watch.stop();
|
||||
IF_VERBOSE(SAT_VB_LVL,
|
||||
verbose_stream() << " (sat-asymm-branch :elim-literals "
|
||||
<< (m_asymm_branch.m_elim_literals - m_elim_literals)
|
||||
<< " :elim-learned-literals " << (m_asymm_branch.m_elim_learned_literals - m_elim_learned_literals)
|
||||
unsigned num_learned = (m_asymm_branch.m_elim_learned_literals - m_elim_learned_literals);
|
||||
unsigned num_total = (m_asymm_branch.m_elim_literals - m_elim_literals);
|
||||
verbose_stream()
|
||||
<< " (sat-asymm-branch :elim-literals " << (num_total - num_learned)
|
||||
<< " :elim-learned-literals " << num_learned
|
||||
<< " :hidden-tautologies " << (m_asymm_branch.m_hidden_tautologies - m_hidden_tautologies)
|
||||
<< " :cost " << m_asymm_branch.m_counter
|
||||
<< mem_stat()
|
||||
|
@ -76,12 +78,15 @@ namespace sat {
|
|||
s.propagate(false);
|
||||
if (s.m_inconsistent)
|
||||
break;
|
||||
std::cout << "elim: " << m_elim_literals - elim << "\n";
|
||||
if (m_elim_literals == elim)
|
||||
unsigned num_elim = m_elim_literals - elim;
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";);
|
||||
if (num_elim == 0)
|
||||
break;
|
||||
}
|
||||
std::cout << "elim-literals: " << m_elim_literals - elim0 << "\n";
|
||||
std::cout << "elim-learned-literals: " << m_elim_learned_literals - eliml0 << "\n";
|
||||
if (num_elim > 1000)
|
||||
i = 0;
|
||||
}
|
||||
IF_VERBOSE(1, if (m_elim_learned_literals > eliml0)
|
||||
verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";);
|
||||
return m_elim_literals > elim0;
|
||||
}
|
||||
|
||||
|
@ -128,6 +133,16 @@ namespace sat {
|
|||
throw ex;
|
||||
}
|
||||
}
|
||||
|
||||
void asymm_branch::operator()(big& big) {
|
||||
s.propagate(false);
|
||||
if (s.m_inconsistent)
|
||||
return;
|
||||
report rpt(*this);
|
||||
svector<char> saved_phase(s.m_phase);
|
||||
process(&big);
|
||||
s.m_phase = saved_phase;
|
||||
}
|
||||
|
||||
void asymm_branch::operator()(bool force) {
|
||||
++m_calls;
|
||||
|
@ -244,7 +259,6 @@ namespace sat {
|
|||
lemma[j++] = l;
|
||||
}
|
||||
}
|
||||
// std::cout << lemma.size() << " -> " << j << "\n";
|
||||
lemma.shrink(j);
|
||||
}
|
||||
}
|
||||
|
@ -347,8 +361,7 @@ namespace sat {
|
|||
break;
|
||||
}
|
||||
}
|
||||
new_sz = j;
|
||||
// std::cout << "cleanup: " << c.id() << ": " << literal_vector(new_sz, c.begin()) << " delta: " << (c.size() - new_sz) << " " << skip_idx << " " << new_sz << "\n";
|
||||
new_sz = j;
|
||||
return re_attach(scoped_d, c, new_sz);
|
||||
}
|
||||
|
||||
|
@ -386,7 +399,7 @@ namespace sat {
|
|||
bool asymm_branch::process_sampled(big& big, clause & c) {
|
||||
scoped_detach scoped_d(s, c);
|
||||
sort(big, c);
|
||||
#if 0
|
||||
#if 1
|
||||
if (uhte(big, c)) {
|
||||
++m_hidden_tautologies;
|
||||
scoped_d.del_clause();
|
||||
|
|
|
@ -87,6 +87,8 @@ namespace sat {
|
|||
|
||||
void operator()(bool force = false);
|
||||
|
||||
void operator()(big& big);
|
||||
|
||||
void updt_params(params_ref const & p);
|
||||
static void collect_param_descrs(param_descrs & d);
|
||||
|
||||
|
|
|
@ -24,12 +24,8 @@ namespace sat {
|
|||
big::big() {}
|
||||
|
||||
void big::init_big(solver& s, bool learned) {
|
||||
m_num_vars = s.num_vars();
|
||||
init_adding_edges(s.num_vars());
|
||||
unsigned num_lits = m_num_vars * 2;
|
||||
m_dag.reset();
|
||||
m_roots.reset();
|
||||
m_dag.resize(num_lits, 0);
|
||||
m_roots.resize(num_lits, true);
|
||||
literal_vector lits;
|
||||
SASSERT(num_lits == m_dag.size() && num_lits == m_roots.size());
|
||||
for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
|
||||
|
@ -44,11 +40,31 @@ namespace sat {
|
|||
edges.push_back(v);
|
||||
}
|
||||
}
|
||||
}
|
||||
done_adding_edges();
|
||||
}
|
||||
|
||||
void big::init_adding_edges(unsigned num_vars) {
|
||||
m_num_vars = num_vars;
|
||||
unsigned num_lits = m_num_vars * 2;
|
||||
m_dag.reset();
|
||||
m_roots.reset();
|
||||
m_dag.resize(num_lits, 0);
|
||||
m_roots.resize(num_lits, true);
|
||||
}
|
||||
|
||||
void big::add_edge(literal u, literal v) {
|
||||
m_dag[u.index()].push_back(v);
|
||||
}
|
||||
|
||||
void big::done_adding_edges() {
|
||||
for (auto& edges : m_dag) {
|
||||
shuffle<literal>(edges.size(), edges.c_ptr(), m_rand);
|
||||
}
|
||||
init_dfs_num(learned);
|
||||
init_dfs_num();
|
||||
}
|
||||
|
||||
|
||||
struct big::pframe {
|
||||
literal m_parent;
|
||||
literal m_child;
|
||||
|
@ -58,7 +74,7 @@ namespace sat {
|
|||
literal parent() const { return m_parent; }
|
||||
};
|
||||
|
||||
void big::init_dfs_num(bool learned) {
|
||||
void big::init_dfs_num() {
|
||||
unsigned num_lits = m_num_vars * 2;
|
||||
m_left.reset();
|
||||
m_right.reset();
|
||||
|
|
|
@ -34,13 +34,24 @@ namespace sat {
|
|||
svector<int> m_left, m_right;
|
||||
literal_vector m_root, m_parent;
|
||||
|
||||
void init_dfs_num(bool learned);
|
||||
void init_dfs_num();
|
||||
struct pframe;
|
||||
|
||||
public:
|
||||
|
||||
big();
|
||||
/**
|
||||
\brief initialize a BIG from a solver.
|
||||
*/
|
||||
void init_big(solver& s, bool learned);
|
||||
|
||||
/**
|
||||
\brief initialize a BIG externally by adding implications.
|
||||
*/
|
||||
void init_adding_edges(unsigned num_vars);
|
||||
void add_edge(literal u, literal v);
|
||||
void done_adding_edges();
|
||||
|
||||
void ensure_big(solver& s, bool learned) { if (m_left.empty()) init_big(s, learned); }
|
||||
int get_left(literal l) const { return m_left[l.index()]; }
|
||||
int get_right(literal l) const { return m_right[l.index()]; }
|
||||
|
@ -49,6 +60,7 @@ namespace sat {
|
|||
bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; }
|
||||
bool connected(literal u, literal v) const { return reaches(u, v) || reaches(~v, ~u); }
|
||||
void display(std::ostream& out) const;
|
||||
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
@ -74,6 +74,7 @@ namespace sat {
|
|||
m_local_search_threads = p.local_search_threads();
|
||||
m_lookahead_simplify = p.lookahead_simplify();
|
||||
m_lookahead_simplify_bca = p.lookahead_simplify_bca();
|
||||
m_lookahead_simplify_asymm_branch = p.lookahead_simplify_asymm_branch();
|
||||
if (p.lookahead_reward() == symbol("heule_schur"))
|
||||
m_lookahead_reward = heule_schur_reward;
|
||||
else if (p.lookahead_reward() == symbol("heuleu"))
|
||||
|
|
|
@ -92,6 +92,7 @@ namespace sat {
|
|||
bool m_local_search;
|
||||
bool m_lookahead_simplify;
|
||||
bool m_lookahead_simplify_bca;
|
||||
bool m_lookahead_simplify_asymm_branch;
|
||||
cutoff_t m_lookahead_cube_cutoff;
|
||||
double m_lookahead_cube_fraction;
|
||||
unsigned m_lookahead_cube_depth;
|
||||
|
|
|
@ -2308,14 +2308,42 @@ namespace sat {
|
|||
elim_eqs elim(m_s);
|
||||
elim(roots, to_elim);
|
||||
|
||||
if (get_config().m_lookahead_simplify_asymm_branch) {
|
||||
big_asymm_branch();
|
||||
}
|
||||
if (get_config().m_lookahead_simplify_bca) {
|
||||
add_hyper_binary();
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
m_lookahead.reset();
|
||||
}
|
||||
|
||||
/**
|
||||
\brief extract binary implication graph from learned binary clauses and use it
|
||||
for strengthening clauses.
|
||||
*/
|
||||
|
||||
void lookahead::big_asymm_branch() {
|
||||
unsigned num_lits = m_s.num_vars() * 2;
|
||||
unsigned idx = 0;
|
||||
big big;
|
||||
big.init_adding_edges(m_s.num_vars());
|
||||
for (auto const& lits : m_binary) {
|
||||
literal u = get_parent(to_literal(idx++));
|
||||
if (u == null_literal) continue;
|
||||
for (literal v : lits) {
|
||||
v = get_parent(v);
|
||||
if (v != null_literal)
|
||||
big.add_edge(u, v);
|
||||
}
|
||||
}
|
||||
big.done_adding_edges();
|
||||
asymm_branch ab(m_s, m_s.m_params);
|
||||
ab(big);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief reduction based on binary implication graph
|
||||
*/
|
||||
|
|
|
@ -555,6 +555,8 @@ namespace sat {
|
|||
|
||||
void add_hyper_binary();
|
||||
|
||||
void big_asymm_branch();
|
||||
|
||||
double psat_heur();
|
||||
|
||||
public:
|
||||
|
|
|
@ -49,6 +49,7 @@ def_module_params('sat',
|
|||
('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
|
||||
('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
|
||||
('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'),
|
||||
('lookahead_simplify.asymm_branch', BOOL, False, 'apply asymmetric branch simplification with lookahead simplifier'),
|
||||
('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),
|
||||
('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')))
|
||||
|
||||
|
|
Loading…
Reference in a new issue