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

fix bug in tracking levels of variables: levels are not cleared, only truth assignment

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-02 14:10:07 -07:00
parent 48e37b0e16
commit ed0b2be618
2 changed files with 41 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/opt/wmax.cpp
View file

@ -61,13 +61,12 @@ namespace opt {
return is_sat; return is_sat;
} }
m_upper = m_lower; m_upper = m_lower;
bool was_sat = false;
expr_ref_vector asms(m); expr_ref_vector asms(m);
vector<expr_ref_vector> cores; vector<expr_ref_vector> cores;
obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end(); obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
for (; it != end; ++it) { for (; it != end; ++it) {
expr* c = assert_weighted(wth(), it->m_key, it->m_value); assert_weighted(wth(), it->m_key, it->m_value);
if (!is_true(it->m_key)) { if (!is_true(it->m_key)) {
m_upper += it->m_value; m_upper += it->m_value;
} }
@ -97,7 +96,6 @@ namespace opt {
expr_ref fml = wth().mk_block(); expr_ref fml = wth().mk_block();
//DEBUG_CODE(verify_cores(cores);); //DEBUG_CODE(verify_cores(cores););
s().assert_expr(fml); s().assert_expr(fml);
was_sat = true;
} }
else { else {
//DEBUG_CODE(verify_cores(cores);); //DEBUG_CODE(verify_cores(cores););

77
src/sat/sat_solver.cpp
View file

@ -3141,42 +3141,42 @@ namespace sat {
// //
// ----------------------- // -----------------------
static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) { static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) {
for (unsigned i = 0; i < lambda.size(); ++i) { for (unsigned i = 0; i < lambda.size(); ++i) {
if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) { if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) {
lambda[i] = lambda.back(); lambda[i] = lambda.back();
lambda.pop_back(); lambda.pop_back();
--i;
}
}
}
// Algorithm 7: Corebased Algorithm with Chunking
static void back_remove(sat::literal_vector& lits, sat::literal l) {
for (unsigned i = lits.size(); i > 0; ) {
--i; --i;
if (lits[i] == l) {
lits[i] = lits.back();
lits.pop_back();
return;
}
} }
UNREACHABLE();
} }
}
// Algorithm 7: Corebased Algorithm with Chunking
static void back_remove(sat::literal_vector& lits, sat::literal l) {
for (unsigned i = lits.size(); i > 0; ) {
--i;
if (lits[i] == l) {
lits[i] = lits.back();
lits.pop_back();
return;
}
}
std::cout << "UNREACHABLE\n";
}
static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, vector<sat::literal_vector>& conseq) { static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, vector<sat::literal_vector>& conseq) {
for (unsigned i = 0; i < gamma.size(); ++i) { for (unsigned i = 0; i < gamma.size(); ++i) {
sat::literal nlit = ~gamma[i]; sat::literal nlit = ~gamma[i];
sat::literal_vector asms1(asms); sat::literal_vector asms1(asms);
asms1.push_back(nlit); asms1.push_back(nlit);
lbool r = s.check(asms1.size(), asms1.c_ptr()); lbool r = s.check(asms1.size(), asms1.c_ptr());
if (r == l_false) { if (r == l_false) {
conseq.push_back(s.get_core()); conseq.push_back(s.get_core());
}
} }
} }
}
static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) { static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
sat::literal_vector lambda; sat::literal_vector lambda;
for (unsigned i = 0; i < vars.size(); i++) { for (unsigned i = 0; i < vars.size(); i++) {
@ -3259,9 +3259,12 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
} }
} }
// is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100); if (false && asms.empty()) {
is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100);
is_sat = get_consequences(asms, lits, conseq); }
else {
is_sat = get_consequences(asms, lits, conseq);
}
set_model(mdl); set_model(mdl);
return is_sat; return is_sat;
} }
@ -3390,8 +3393,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
literal lit = *it; literal lit = *it;
if (value(lit) != l_undef) { if (value(lit) != l_undef) {
++num_fixed; ++num_fixed;
if (lvl(lit) <= 1) { if (lvl(lit) <= 1 && value(lit) == l_true) {
SASSERT(value(lit) == l_true);
extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq); extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
} }
continue; continue;
@ -3498,8 +3500,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end(); literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end();
for (; it != end; ++it) { for (; it != end; ++it) {
literal lit = *it; literal lit = *it;
if (lvl(lit) <= 1) { TRACE("sat", tout << "extract: " << lit << " " << value(lit) << " " << lvl(lit) << "\n";);
SASSERT(value(lit) == l_true);
if (lvl(lit) <= 1 && value(lit) == l_true) {
extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq); extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
} }
} }
@ -3508,8 +3511,8 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
bool solver::check_domain(literal lit, literal lit2) { bool solver::check_domain(literal lit, literal lit2) {
if (!m_antecedents.contains(lit2.var())) { if (!m_antecedents.contains(lit2.var())) {
SASSERT(value(lit2) == l_true); SASSERT(value(lit2) == l_true);
SASSERT(m_todo_antecedents.empty() || m_todo_antecedents.back() != lit2);
m_todo_antecedents.push_back(lit2); m_todo_antecedents.push_back(lit2);
TRACE("sat", tout << "todo: " << lit2 << " " << value(lit2) << "\n";);
return false; return false;
} }
else { else {