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 issue https://z3.codeplex.com/workitem/38

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-06-06 13:20:43 -07:00
parent 110fa0b7fb
commit f4f1c63abb
3 changed files with 36 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/sat/sat_clause_use_list.h
View file

@ -20,6 +20,7 @@ Revision History:
#define _SAT_CLAUSE_USE_LIST_H_ #define _SAT_CLAUSE_USE_LIST_H_
#include"sat_types.h" #include"sat_types.h"
#include"trace.h"
namespace sat { namespace sat {
@ -35,6 +36,7 @@ namespace sat {
#endif #endif
public: public:
clause_use_list() { clause_use_list() {
STRACE("clause_use_list_bug", tout << "[cul_created] " << this << "\n";);
#ifdef LAZY_USE_LIST #ifdef LAZY_USE_LIST
m_size = 0; m_size = 0;
#endif #endif
@ -51,22 +53,33 @@ namespace sat {
bool empty() const { return size() == 0; } bool empty() const { return size() == 0; }
void insert(clause & c) { void insert(clause & c) {
SASSERT(!m_clauses.contains(&c)); SASSERT(!c.was_removed()); STRACE("clause_use_list_bug", tout << "[cul_insert] " << this << " " << &c << "\n";);
SASSERT(!m_clauses.contains(&c));
SASSERT(!c.was_removed());
m_clauses.push_back(&c); m_clauses.push_back(&c);
#ifdef LAZY_USE_LIST #ifdef LAZY_USE_LIST
m_size++; m_size++;
#endif #endif
} }
void erase_not_removed(clause & c) { void erase_not_removed(clause & c) {
STRACE("clause_use_list_bug", tout << "[cul_erase_not_removed] " << this << " " << &c << "\n";);
#ifdef LAZY_USE_LIST #ifdef LAZY_USE_LIST
SASSERT(m_clauses.contains(&c)); SASSERT(!c.was_removed()); m_clauses.erase(&c); m_size--; SASSERT(m_clauses.contains(&c));
SASSERT(!c.was_removed());
m_clauses.erase(&c);
m_size--;
#else #else
m_clauses.erase(&c); m_clauses.erase(&c);
#endif #endif
} }
void erase(clause & c) { void erase(clause & c) {
STRACE("clause_use_list_bug", tout << "[cul_erase] " << this << " " << &c << "\n";);
#ifdef LAZY_USE_LIST #ifdef LAZY_USE_LIST
SASSERT(m_clauses.contains(&c)); SASSERT(c.was_removed()); m_size--; SASSERT(m_clauses.contains(&c));
SASSERT(c.was_removed());
m_size--;
#else #else
m_clauses.erase(&c); m_clauses.erase(&c);
#endif #endif
@ -80,6 +93,7 @@ namespace sat {
} }
bool check_invariant() const; bool check_invariant() const;
// iterate & compress // iterate & compress
class iterator { class iterator {
clause_vector & m_clauses; clause_vector & m_clauses;

27
src/sat/sat_simplifier.cpp
View file

@ -146,8 +146,11 @@ namespace sat {
m_need_cleanup = false; m_need_cleanup = false;
m_use_list.init(s.num_vars()); m_use_list.init(s.num_vars());
init_visited(); init_visited();
if (learned) bool learned_in_use_lists = false;
if (learned) {
register_clauses(s.m_learned); register_clauses(s.m_learned);
learned_in_use_lists = true;
}
register_clauses(s.m_clauses); register_clauses(s.m_clauses);
if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls)) if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
@ -179,7 +182,7 @@ namespace sat {
if (!m_need_cleanup) { if (!m_need_cleanup) {
if (vars_eliminated) { if (vars_eliminated) {
// must remove learned clauses with eliminated variables // must remove learned clauses with eliminated variables
cleanup_clauses(s.m_learned, true, true); cleanup_clauses(s.m_learned, true, true, learned_in_use_lists);
} }
CASSERT("sat_solver", s.check_invariant()); CASSERT("sat_solver", s.check_invariant());
TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout);); TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
@ -187,8 +190,8 @@ namespace sat {
return; return;
} }
cleanup_watches(); cleanup_watches();
cleanup_clauses(s.m_learned, true, vars_eliminated); cleanup_clauses(s.m_learned, true, vars_eliminated, learned_in_use_lists);
cleanup_clauses(s.m_clauses, false, vars_eliminated); cleanup_clauses(s.m_clauses, false, vars_eliminated, true);
TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout);); TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
CASSERT("sat_solver", s.check_invariant()); CASSERT("sat_solver", s.check_invariant());
free_memory(); free_memory();
@ -221,7 +224,7 @@ namespace sat {
} }
} }
void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated) { void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) {
clause_vector::iterator it = cs.begin(); clause_vector::iterator it = cs.begin();
clause_vector::iterator it2 = it; clause_vector::iterator it2 = it;
clause_vector::iterator end = cs.end(); clause_vector::iterator end = cs.end();
@ -245,7 +248,7 @@ namespace sat {
} }
} }
if (cleanup_clause(c)) { if (cleanup_clause(c, in_use_lists)) {
s.del_clause(c); s.del_clause(c);
continue; continue;
} }
@ -516,7 +519,7 @@ namespace sat {
Return true if the clause is satisfied Return true if the clause is satisfied
*/ */
bool simplifier::cleanup_clause(clause & c) { bool simplifier::cleanup_clause(clause & c, bool in_use_list) {
bool r = false; bool r = false;
unsigned sz = c.size(); unsigned sz = c.size();
unsigned j = 0; unsigned j = 0;
@ -529,7 +532,11 @@ namespace sat {
break; break;
case l_false: case l_false:
m_need_cleanup = true; m_need_cleanup = true;
m_use_list.get(l).erase_not_removed(c); if (in_use_list && !c.frozen()) {
// Remark: if in_use_list is false, then the given clause was not added to the use lists.
// Remark: frozen clauses are not added to the use lists.
m_use_list.get(l).erase_not_removed(c);
}
break; break;
case l_true: case l_true:
r = true; r = true;
@ -611,7 +618,7 @@ namespace sat {
clause_use_list & occurs = m_use_list.get(l); clause_use_list & occurs = m_use_list.get(l);
occurs.erase_not_removed(c); occurs.erase_not_removed(c);
m_sub_counter -= occurs.size()/2; m_sub_counter -= occurs.size()/2;
if (cleanup_clause(c)) { if (cleanup_clause(c, true /* clause is in the use lists */)) {
// clause was satisfied // clause was satisfied
TRACE("elim_lit", tout << "clause was satisfied\n";); TRACE("elim_lit", tout << "clause was satisfied\n";);
remove_clause(c); remove_clause(c);
@ -805,7 +812,7 @@ namespace sat {
m_sub_counter--; m_sub_counter--;
TRACE("subsumption", tout << "next: " << c << "\n";); TRACE("subsumption", tout << "next: " << c << "\n";);
if (s.m_trail.size() > m_last_sub_trail_sz) { if (s.m_trail.size() > m_last_sub_trail_sz) {
if (cleanup_clause(c)) { if (cleanup_clause(c, true /* clause is in the use_lists */)) {
remove_clause(c); remove_clause(c);
continue; continue;
} }

4
src/sat/sat_simplifier.h
View file

@ -125,7 +125,7 @@ namespace sat {
void collect_subsumed0(clause const & c1, clause_vector & out); void collect_subsumed0(clause const & c1, clause_vector & out);
void back_subsumption0(clause & c1); void back_subsumption0(clause & c1);
bool cleanup_clause(clause & c); bool cleanup_clause(clause & c, bool in_use_list);
bool cleanup_clause(literal_vector & c); bool cleanup_clause(literal_vector & c);
void propagate_unit(literal l); void propagate_unit(literal l);
void elim_lit(clause & c, literal l); void elim_lit(clause & c, literal l);
@ -136,7 +136,7 @@ namespace sat {
void subsume(); void subsume();
void cleanup_watches(); void cleanup_watches();
void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated); void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists);
bool is_external(bool_var v) const; bool is_external(bool_var v) const;
bool was_eliminated(bool_var v) const; bool was_eliminated(bool_var v) const;