mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

pass qhead

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-01 16:54:22 -07:00
parent 8ba78081ec
commit 48e37b0e16
2 changed files with 35 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

73
src/smt/smt_context.cpp
View file

@ -74,7 +74,6 @@ namespace smt {
m_unsat_proof(m), m_unsat_proof(m),
m_unknown("unknown"), m_unknown("unknown"),
m_unsat_core(m), m_unsat_core(m),
m_th_case_split_qhead(0),
#ifdef Z3DEBUG #ifdef Z3DEBUG
m_trail_enabled(true), m_trail_enabled(true),
#endif #endif
@ -340,7 +339,6 @@ namespace smt {
bool context::bcp() { bool context::bcp() {
SASSERT(!inconsistent()); SASSERT(!inconsistent());
m_th_case_split_qhead = m_qhead;
while (m_qhead < m_assigned_literals.size()) { while (m_qhead < m_assigned_literals.size()) {
if (get_cancel_flag()) { if (get_cancel_flag()) {
return true; return true;
@ -1770,7 +1768,7 @@ namespace smt {
unsigned qhead = m_qhead; unsigned qhead = m_qhead;
if (!bcp()) if (!bcp())
return false; return false;
if (!propagate_th_case_split()) if (!propagate_th_case_split(qhead))
return false; return false;
if (get_cancel_flag()) { if (get_cancel_flag()) {
m_qhead = qhead; m_qhead = qhead;
@ -2979,16 +2977,13 @@ namespace smt {
TRACE("theory_case_split", display_literals_verbose(tout << "theory case split: ", num_lits, lits); tout << std::endl;); TRACE("theory_case_split", display_literals_verbose(tout << "theory case split: ", num_lits, lits); tout << std::endl;);
// If we don't use the theory case split heuristic, // If we don't use the theory case split heuristic,
// for each pair of literals (l1, l2) we add the clause (~l1 OR ~l2) // for each pair of literals (l1, l2) we add the clause (~l1 OR ~l2)
// to enforce the condition that more than one literal can't be // to enforce the condition that at most one literal can be assigned 'true'.
// assigned 'true' simultaneously.
if (!m_fparams.m_theory_case_split) { if (!m_fparams.m_theory_case_split) {
for (unsigned i = 0; i < num_lits; ++i) { for (unsigned i = 0; i < num_lits; ++i) {
for (unsigned j = i+1; j < num_lits; ++j) { for (unsigned j = i+1; j < num_lits; ++j) {
literal l1 = lits[i]; literal l1 = lits[i];
literal l2 = lits[j]; literal l2 = lits[j];
literal excl[2] = {~l1, ~l2}; mk_clause(~l1, ~l2, (justification*) 0);
justification * j_excl = 0;
mk_clause(2, excl, j_excl);
} }
} }
} else { } else {
@ -3010,11 +3005,11 @@ namespace smt {
m_literal2casesplitsets[l.index()].push_back(new_case_split); m_literal2casesplitsets[l.index()].push_back(new_case_split);
} }
TRACE("theory_case_split", tout << "tracking case split literal set { "; TRACE("theory_case_split", tout << "tracking case split literal set { ";
for (unsigned i = 0; i < num_lits; ++i) { for (unsigned i = 0; i < num_lits; ++i) {
tout << lits[i].index() << " "; tout << lits[i].index() << " ";
} }
tout << "}" << std::endl; tout << "}" << std::endl;
); );
} }
} }
@ -3027,7 +3022,7 @@ namespace smt {
} }
} }
bool context::propagate_th_case_split() { bool context::propagate_th_case_split(unsigned qhead) {
if (m_all_th_case_split_literals.empty()) if (m_all_th_case_split_literals.empty())
return true; return true;
@ -3035,34 +3030,34 @@ namespace smt {
// not counting any literals that get assigned by this method // not counting any literals that get assigned by this method
// this relies on bcp() to give us its old m_qhead and therefore // this relies on bcp() to give us its old m_qhead and therefore
// bcp() should always be called before this method // bcp() should always be called before this method
unsigned assigned_literal_idx = m_th_case_split_qhead;
unsigned assigned_literal_end = m_assigned_literals.size(); unsigned assigned_literal_end = m_assigned_literals.size();
while(assigned_literal_idx < assigned_literal_end) { for (; qhead < assigned_literal_end; ++qhead) {
literal l = m_assigned_literals[assigned_literal_idx]; literal l = m_assigned_literals[qhead];
TRACE("theory_case_split", tout << "check literal " << l.index() << std::endl; display_literal_verbose(tout, l); tout << std::endl;); TRACE("theory_case_split", tout << "check literal " << l.index() << std::endl; display_literal_verbose(tout, l); tout << std::endl;);
++assigned_literal_idx;
// check if this literal participates in any theory case split // check if this literal participates in any theory case split
if (m_all_th_case_split_literals.contains(l.index())) { if (!m_all_th_case_split_literals.contains(l.index())) {
TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;); continue;
// now find the sets of literals which contain l }
vector<literal_vector> const& case_split_sets = m_literal2casesplitsets[l.index()]; TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;);
for (vector<literal_vector>::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) { // now find the sets of literals which contain l
literal_vector case_split_set = *it; vector<literal_vector> const& case_split_sets = m_literal2casesplitsets[l.index()];
TRACE("theory_case_split", tout << "found case split set { "; for (vector<literal_vector>::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) {
for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) { literal_vector case_split_set = *it;
tout << set_it->index() << " "; TRACE("theory_case_split", tout << "found case split set { ";
} for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
tout << "}" << std::endl;); tout << set_it->index() << " ";
for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) { }
literal l2 = *set_it; tout << "}" << std::endl;);
if (l2 != l) { for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
b_justification js(l); literal l2 = *set_it;
TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m_manager, m_bool_var2expr.c_ptr());); if (l2 != l) {
assign(~l2, js); b_justification js(l);
if (inconsistent()) { TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m_manager, m_bool_var2expr.c_ptr()););
TRACE("theory_case_split", tout << "conflict detected!" << std::endl;); assign(~l2, js);
return false; if (inconsistent()) {
} TRACE("theory_case_split", tout << "conflict detected!" << std::endl;);
return false;
} }
} }
} }

3
src/smt/smt_context.h
View file

@ -234,7 +234,6 @@ namespace smt {
uint_set m_all_th_case_split_literals; uint_set m_all_th_case_split_literals;
vector<literal_vector> m_th_case_split_sets; vector<literal_vector> m_th_case_split_sets;
u_map< vector<literal_vector> > m_literal2casesplitsets; // returns the case split literal sets that a literal participates in u_map< vector<literal_vector> > m_literal2casesplitsets; // returns the case split literal sets that a literal participates in
unsigned m_th_case_split_qhead;
// ----------------------------------- // -----------------------------------
// //
@ -844,7 +843,7 @@ namespace smt {
// helper function for trail // helper function for trail
void undo_th_case_split(literal l); void undo_th_case_split(literal l);
bool propagate_th_case_split(); bool propagate_th_case_split(unsigned qhead);
bool_var mk_bool_var(expr * n); bool_var mk_bool_var(expr * n);