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

Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2013-06-07 12:21:06 +01:00
commit a88a15ac67
4 changed files with 41 additions and 18 deletions
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_
#include"sat_types.h"
#include"trace.h"
namespace sat {
@ -35,6 +36,7 @@ namespace sat {
#endif
public:
clause_use_list() {
STRACE("clause_use_list_bug", tout << "[cul_created] " << this << "\n";);
#ifdef LAZY_USE_LIST
m_size = 0;
#endif
@ -51,22 +53,33 @@ namespace sat {
bool empty() const { return size() == 0; }
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);
#ifdef LAZY_USE_LIST
m_size++;
#endif
}
void erase_not_removed(clause & c) {
STRACE("clause_use_list_bug", tout << "[cul_erase_not_removed] " << this << " " << &c << "\n";);
#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
m_clauses.erase(&c);
#endif
}
void erase(clause & c) {
STRACE("clause_use_list_bug", tout << "[cul_erase] " << this << " " << &c << "\n";);
#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
m_clauses.erase(&c);
#endif
@ -80,6 +93,7 @@ namespace sat {
}
bool check_invariant() const;
// iterate & compress
class iterator {
clause_vector & m_clauses;

27
src/sat/sat_simplifier.cpp
View file

@ -146,8 +146,11 @@ namespace sat {
m_need_cleanup = false;
m_use_list.init(s.num_vars());
init_visited();
if (learned)
bool learned_in_use_lists = false;
if (learned) {
register_clauses(s.m_learned);
learned_in_use_lists = true;
}
register_clauses(s.m_clauses);
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 (vars_eliminated) {
// 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());
TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
@ -187,8 +190,8 @@ namespace sat {
return;
}
cleanup_watches();
cleanup_clauses(s.m_learned, true, vars_eliminated);
cleanup_clauses(s.m_clauses, false, vars_eliminated);
cleanup_clauses(s.m_learned, true, vars_eliminated, learned_in_use_lists);
cleanup_clauses(s.m_clauses, false, vars_eliminated, true);
TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
CASSERT("sat_solver", s.check_invariant());
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 it2 = it;
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);
continue;
}
@ -516,7 +519,7 @@ namespace sat {
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;
unsigned sz = c.size();
unsigned j = 0;
@ -529,7 +532,11 @@ namespace sat {
break;
case l_false:
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;
case l_true:
r = true;
@ -611,7 +618,7 @@ namespace sat {
clause_use_list & occurs = m_use_list.get(l);
occurs.erase_not_removed(c);
m_sub_counter -= occurs.size()/2;
if (cleanup_clause(c)) {
if (cleanup_clause(c, true /* clause is in the use lists */)) {
// clause was satisfied
TRACE("elim_lit", tout << "clause was satisfied\n";);
remove_clause(c);
@ -805,7 +812,7 @@ namespace sat {
m_sub_counter--;
TRACE("subsumption", tout << "next: " << c << "\n";);
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);
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 back_subsumption0(clause & c1);
bool cleanup_clause(clause & c);
bool cleanup_clause(clause & c, bool in_use_list);
bool cleanup_clause(literal_vector & c);
void propagate_unit(literal l);
void elim_lit(clause & c, literal l);
@ -136,7 +136,7 @@ namespace sat {
void subsume();
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 was_eliminated(bool_var v) const;

8
src/tactic/core/ctx_simplify_tactic.cpp
View file

@ -21,7 +21,7 @@ Notes:
#include"goal_num_occurs.h"
#include"cooperate.h"
#include"ast_ll_pp.h"
#include"ast_smt2_pp.h"
#include"ast_pp.h"
struct ctx_simplify_tactic::imp {
struct cached_result {
@ -105,6 +105,7 @@ struct ctx_simplify_tactic::imp {
}
bool shared(expr * t) const {
TRACE("ctx_simplify_tactic_bug", tout << mk_pp(t, m) << "\n";);
return t->get_ref_count() > 1 && m_occs.get_num_occs(t) > 1;
}
@ -242,12 +243,13 @@ struct ctx_simplify_tactic::imp {
}
void assert_expr(expr * t, bool sign) {
expr * p = t;
if (m.is_not(t)) {
t = to_app(t)->get_arg(0);
sign = !sign;
}
bool mk_scope = true;
if (shared(t)) {
if (shared(t) || shared(p)) {
push();
mk_scope = false;
assert_eq_core(t, sign ? m.mk_false() : m.mk_true());
@ -457,7 +459,7 @@ struct ctx_simplify_tactic::imp {
if (visit.is_marked(s)) {
continue;
}
visit.mark(s, true);
visit.mark(s, true);
++sz;
for (unsigned i = 0; is_app(s) && i < to_app(s)->get_num_args(); ++i) {
todo.push_back(to_app(s)->get_arg(i));