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

fix #2416 exposed bugs: unsat-core extraction in combination with chronological backracking, equivalence elimination in combination with PB constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-25 18:55:44 -07:00
parent 8a0d79251e
commit 53aded3198
4 changed files with 14 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/maxres.cpp
View file

@ -133,7 +133,7 @@ public:
m_max_core_size(3),
m_maximize_assignment(false),
m_max_correction_set_size(3),
m_pivot_on_cs(true)
m_pivot_on_cs(true)
{
switch(st) {
case s_primal:

4
src/sat/ba_solver.cpp
View file

@ -2085,7 +2085,6 @@ namespace sat {
\brief return true to keep watching literal.
*/
bool ba_solver::propagate(literal l, ext_constraint_idx idx) {
TRACE("ba", tout << l << "\n";);
SASSERT(value(l) == l_true);
constraint& c = index2constraint(idx);
if (c.lit() != null_literal && l.var() == c.lit().var()) {
@ -2813,7 +2812,7 @@ namespace sat {
// literal is assigned to false.
unsigned sz = c.size();
unsigned bound = c.k();
TRACE("ba", tout << "assign: " << c.lit() << ": " << ~alit << "@" << lvl(~alit) << "\n";);
TRACE("ba", tout << "assign: " << c.lit() << ": " << ~alit << "@" << lvl(~alit) << " " << c << "\n";);
SASSERT(0 < bound && bound <= sz);
if (bound == sz) {
@ -3242,7 +3241,6 @@ namespace sat {
// pre-condition is that the literals, except c.lit(), in c are unwatched.
if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n";
// IF_VERBOSE(0, verbose_stream() << c << "\n";);
m_weights.resize(2*s().num_vars(), 0);
for (literal l : c) {
++m_weights[l.index()];

3
src/sat/sat_elim_eqs.cpp
View file

@ -230,7 +230,8 @@ namespace sat {
literal l(v, false);
literal r = roots[v];
SASSERT(v != r.var());
bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r);
bool set_root = m_solver.set_root(l, r);
bool root_ok = !m_solver.is_external(v) || set_root;
if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) {
// cannot really eliminate v, since we have to notify extension of future assignments
m_solver.mk_bin_clause(~l, r, false);

24
src/sat/sat_solver.cpp
View file

@ -301,8 +301,10 @@ namespace sat {
clause* solver::mk_clause(unsigned num_lits, literal * lits, bool learned) {
m_model_is_current = false;
DEBUG_CODE({
for (unsigned i = 0; i < num_lits; i++)
SASSERT(m_eliminated[lits[i].var()] == false);
for (unsigned i = 0; i < num_lits; i++) {
CTRACE("sat", m_eliminated[lits[i].var()], tout << lits[i] << " was eliminated\n";);
SASSERT(m_eliminated[lits[i].var()] == false);
}
});
if (m_user_scope_literals.empty()) {
@ -2908,26 +2910,20 @@ namespace sat {
justification js = m_conflict;
int init_sz = init_trail_size();
while (true) {
process_consequent_for_unsat_core(consequent, js);
while (idx >= 0) {
literal l = m_trail[idx];
if (is_marked(l.var()))
while (idx >= init_sz) {
consequent = m_trail[idx];
if (is_marked(consequent.var()) && lvl(consequent) == m_conflict_lvl)
break;
idx--;
}
if (idx < 0) {
if (idx < init_sz) {
break;
}
consequent = m_trail[idx];
if (lvl(consequent) < m_conflict_lvl) {
TRACE("sat", tout << consequent << " at level " << lvl(consequent) << "\n";);
break;
}
bool_var c_var = consequent.var();
SASSERT(lvl(consequent) == m_conflict_lvl);
js = m_justification[c_var];
js = m_justification[consequent.var()];
idx--;
}
reset_unmark(old_size);