mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 21:31:22 +00:00
Code Activity

fix quadratic behavior of extract_assumptions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-02 15:57:31 -07:00
parent ed0b2be618
commit 21cda27f5e
2 changed files with 16 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/sat/sat_solver.cpp
View file

@ -3523,6 +3523,7 @@ namespace sat {
bool solver::extract_assumptions(literal lit, index_set& s) { bool solver::extract_assumptions(literal lit, index_set& s) {
justification js = m_justification[lit.var()]; justification js = m_justification[lit.var()];
TRACE("sat", tout << lit << " " << js << "\n";); TRACE("sat", tout << lit << " " << js << "\n";);
bool all_found = true;
switch (js.get_kind()) { switch (js.get_kind()) {
case justification::NONE: case justification::NONE:
break; break;
@ -3540,8 +3541,12 @@ namespace sat {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset())); clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
for (unsigned i = 0; i < c.size(); ++i) { for (unsigned i = 0; i < c.size(); ++i) {
if (c[i] != lit) { if (c[i] != lit) {
if (!check_domain(lit, ~c[i])) return false; if (check_domain(lit, ~c[i]) && all_found) {
s |= m_antecedents.find(c[i].var()); s |= m_antecedents.find(c[i].var());
}
else {
all_found = false;
}
} }
} }
break; break;
@ -3551,8 +3556,12 @@ namespace sat {
literal_vector::iterator it = m_ext_antecedents.begin(); literal_vector::iterator it = m_ext_antecedents.begin();
literal_vector::iterator end = m_ext_antecedents.end(); literal_vector::iterator end = m_ext_antecedents.end();
for (; it != end; ++it) { for (; it != end; ++it) {
if (!check_domain(lit, *it)) return false; if (check_domain(lit, *it) && all_found) {
s |= m_antecedents.find(it->var()); s |= m_antecedents.find(it->var());
}
else {
all_found = false;
}
} }
break; break;
} }
@ -3561,7 +3570,7 @@ namespace sat {
break; break;
} }
TRACE("sat", display_index_set(tout << lit << ": " , s) << "\n";); TRACE("sat", display_index_set(tout << lit << ": " , s) << "\n";);
return true; return all_found;
} }
std::ostream& solver::display_index_set(std::ostream& out, index_set const& s) const { std::ostream& solver::display_index_set(std::ostream& out, index_set const& s) const {

3
src/test/cnf_backbones.cpp
View file

@ -246,13 +246,14 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
vector<sat::literal_vector> conseq; vector<sat::literal_vector> conseq;
sat::bool_var_vector vars; sat::bool_var_vector vars;
sat::literal_vector assumptions; sat::literal_vector assumptions;
unsigned num_vars = solver.num_vars();
if (p.get_bool("dimacs.core", false)) { if (p.get_bool("dimacs.core", false)) {
g_solver = &solver2; g_solver = &solver2;
vector<sat::literal_vector> tracking_clauses; vector<sat::literal_vector> tracking_clauses;
track_clauses(solver, solver2, assumptions, tracking_clauses); track_clauses(solver, solver2, assumptions, tracking_clauses);
} }
for (unsigned i = 1; i < g_solver->num_vars(); ++i) { for (unsigned i = 1; i < num_vars; ++i) {
vars.push_back(i); vars.push_back(i);
g_solver->set_external(i); g_solver->set_external(i);
} }