mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Fixes

Browse source
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-10-23 12:51:19 -07:00
parent ee6cfb8eef
commit 63545c1e7b
2 changed files with 6 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/sat/sat_simplifier.cpp
View file

@ -974,9 +974,9 @@ namespace sat {
void operator()() { void operator()() {
if (s.bce_enabled()) if (s.bce_enabled())
block_clauses(); block_clauses();
if (s.m_cce) if (s.cce_enabled())
cce(); cce();
if (s.m_bca) if (s.bca_enabled())
bca(); bca();
} }
@ -1176,7 +1176,7 @@ namespace sat {
is_tautology = add_cla(blocked); is_tautology = add_cla(blocked);
} }
while (m_covered_clause.size() > sz && !is_tautology); while (m_covered_clause.size() > sz && !is_tautology);
if (s.m_acce && !is_tautology) { if (s.acce_enabled() && !is_tautology) {
sz = m_covered_clause.size(); sz = m_covered_clause.size();
add_ala(); add_ala();
} }
@ -1338,11 +1338,9 @@ namespace sat {
} }
if (!found) { if (!found) {
IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";); IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";);
watched w(l2, false); watched w(l2, true);
w.set_blocked();
s.get_wlist(~l).push_back(w); s.get_wlist(~l).push_back(w);
w = watched(l, false); w = watched(l, true);
w.set_blocked();
s.get_wlist(~l2).push_back(w); s.get_wlist(~l2).push_back(w);
++s.m_num_bca; ++s.m_num_bca;
} }

2
src/sat/sat_simplifier_params.pyg
View file

@ -20,6 +20,6 @@ def_module_params(module_name='sat',
('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'), ('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'), ('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'),
('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'), ('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'),
('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'), ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),
('subsumption', BOOL, True, 'eliminate subsumed clauses'), ('subsumption', BOOL, True, 'eliminate subsumed clauses'),
('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)'))) ('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))