mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

add shortcuts for unit assertions, conflicts

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-11 10:56:36 -08:00
parent d73b7267e3
commit 93ee05648e
17 changed files with 55 additions and 94 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/ba_solver.cpp
View file

@ -4140,6 +4140,10 @@ namespace sat {
return out << index2constraint(idx);
}
std::ostream& ba_solver::display_constraint(std::ostream& out, ext_constraint_idx idx) const {
return out << index2constraint(idx);
}
void ba_solver::display(std::ostream& out, constraint const& c, bool values) const {
switch (c.tag()) {
case card_t: display(out, c.to_card(), values); break;

1
src/sat/ba_solver.h
View file

@ -547,6 +547,7 @@ namespace sat {
void flush_roots() override;
std::ostream& display(std::ostream& out) const override;
std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override;
std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override;
void collect_statistics(statistics& st) const override;
extension* copy(solver* s) override;
extension* copy(lookahead* s, bool learned) override;

6
src/sat/sat_asymm_branch.cpp
View file

@ -367,7 +367,7 @@ namespace sat {
bool asymm_branch::propagate_literal(clause const& c, literal l) {
SASSERT(!s.inconsistent());
TRACE("asymm_branch_detail", tout << "assigning: " << l << "\n";);
s.assign(l, justification());
s.assign_scoped(l);
s.propagate_core(false); // must not use propagate(), since check_missed_propagation may fail for c
return s.inconsistent();
}
@ -423,11 +423,11 @@ namespace sat {
switch (new_sz) {
case 0:
s.set_conflict(justification());
s.set_conflict();
return false;
case 1:
TRACE("asymm_branch", tout << "produced unit clause: " << c[0] << "\n";);
s.assign(c[0], justification());
s.assign_unit(c[0]);
s.propagate_core(false);
scoped_d.del_clause();
return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.

2
src/sat/sat_big.cpp
View file

@ -199,7 +199,7 @@ namespace sat {
s.add_ate(~u, v);
if (find_binary_watch(wlist, ~v)) {
IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n");
s.assign(~u, justification());
s.assign_unit(~u);
}
// could turn non-learned non-binary tautology into learned binary.
s.get_wlist(~v).erase(watched(~u, w.is_learned()));

4
src/sat/sat_cleaner.cpp
View file

@ -119,11 +119,11 @@ namespace sat {
s.display_watches(tout););
switch (new_sz) {
case 0:
s.set_conflict(justification());
s.set_conflict();
s.del_clause(c);
break;
case 1:
s.assign(c[0], justification());
s.assign_unit(c[0]);
s.del_clause(c);
break;
case 2:

6
src/sat/sat_elim_eqs.cpp
View file

@ -53,7 +53,7 @@ namespace sat {
literal l2 = it->get_literal();
literal r2 = norm(roots, l2);
if (r1 == r2) {
m_solver.assign(r1, justification());
m_solver.assign_unit(r1);
if (m_solver.inconsistent())
return;
// consume unit
@ -179,7 +179,7 @@ namespace sat {
switch (j) {
case 0:
m_solver.set_conflict(justification());
m_solver.set_conflict();
for (; it != end; ++it) {
*it2 = *it;
it2++;
@ -187,7 +187,7 @@ namespace sat {
cs.set_end(it2);
return;
case 1:
m_solver.assign(c[0], justification());
m_solver.assign_unit(c[0]);
drat_delete_clause();
c.set_removed(true);
m_solver.del_clause(c);

2
src/sat/sat_elim_vars.cpp
View file

@ -169,7 +169,7 @@ namespace sat{
switch (c.size()) {
case 0:
s.set_conflict(justification());
s.set_conflict();
break;
case 1:
simp.propagate_unit(c[0]);

1
src/sat/sat_extension.h
View file

@ -70,6 +70,7 @@ namespace sat {
virtual lbool get_phase(bool_var v) = 0;
virtual std::ostream& display(std::ostream& out) const = 0;
virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0;
virtual std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const = 0;
virtual void collect_statistics(statistics& st) const = 0;
virtual extension* copy(solver* s) = 0;
virtual extension* copy(lookahead* s, bool learned) = 0;

2
src/sat/sat_lookahead.cpp
View file

@ -2463,7 +2463,7 @@ namespace sat {
for (unsigned i = 0; i < m_watches.size(); ++i) {
watch_list const& wl = m_watches[i];
if (!wl.empty()) {
sat::display_watch_list(out << to_literal(i) << " -> ", dummy_allocator, wl);
sat::display_watch_list(out << to_literal(i) << " -> ", dummy_allocator, wl, nullptr);
out << "\n";
}
}

12
src/sat/sat_probing.cpp
View file

@ -69,7 +69,7 @@ namespace sat {
s.m_drat.add(l, lit, true);
s.m_drat.add(~l, lit, true);
}
s.assign(lit, justification());
s.assign_scoped(lit);
m_num_assigned++;
}
}
@ -77,14 +77,14 @@ namespace sat {
else {
m_to_assert.reset();
s.push();
s.assign(l, justification());
s.assign_scoped(l);
m_counter--;
unsigned old_tr_sz = s.m_trail.size();
s.propagate(false);
if (s.inconsistent()) {
// ~l must be true
s.pop(1);
s.assign(~l, justification());
s.assign_scoped(~l);
s.propagate(false);
return false;
}
@ -104,7 +104,7 @@ namespace sat {
s.m_drat.add(l, lit, true);
s.m_drat.add(~l, lit, true);
}
s.assign(lit, justification());
s.assign_scoped(lit);
m_num_assigned++;
}
}
@ -119,13 +119,13 @@ namespace sat {
m_counter--;
s.push();
literal l(v, false);
s.assign(l, justification());
s.assign_scoped(l);
unsigned old_tr_sz = s.m_trail.size();
s.propagate(false);
if (s.inconsistent()) {
// ~l must be true
s.pop(1);
s.assign(~l, justification());
s.assign_scoped(~l);
s.propagate(false);
m_num_assigned++;
return;

8
src/sat/sat_scc.cpp
View file

@ -47,18 +47,22 @@ namespace sat {
stopwatch m_watch;
unsigned m_num_elim;
unsigned m_num_elim_bin;
unsigned m_trail_size;
report(scc & c):
m_scc(c),
m_num_elim(c.m_num_elim),
m_num_elim_bin(c.m_num_elim_bin) {
m_num_elim_bin(c.m_num_elim_bin),
m_trail_size(c.m_solver.init_trail_size()) {
m_watch.start();
}
~report() {
m_watch.stop();
unsigned elim_bin = m_scc.m_num_elim_bin - m_num_elim_bin;
unsigned num_units = m_scc.m_solver.init_trail_size() - m_trail_size;
IF_VERBOSE(2,
verbose_stream() << " (sat-scc :elim-vars " << (m_scc.m_num_elim - m_num_elim);
if (elim_bin > 0) verbose_stream() << " :elim-bin " << elim_bin;
if (num_units > 0) verbose_stream() << " :units " << num_units;
verbose_stream() << m_watch << ")\n";);
}
};
@ -177,7 +181,7 @@ namespace sat {
l2_idx = s[j];
j--;
if (to_literal(l2_idx) == ~l) {
m_solver.set_conflict(justification());
m_solver.set_conflict();
return 0;
}
if (m_solver.is_external(to_literal(l2_idx).var())) {

76
src/sat/sat_simplifier.cpp
View file

@ -335,14 +335,14 @@ namespace sat {
unsigned sz = c.size();
switch(sz) {
case 0:
s.set_conflict(justification());
s.set_conflict();
for (; it != end; ++it, ++it2) {
*it2 = *it;
}
cs.set_end(it2);
return;
case 1:
s.assign(c[0], justification());
s.assign_unit(c[0]);
c.restore(sz0);
s.del_clause(c);
break;
@ -473,8 +473,9 @@ namespace sat {
clause & c2 = *(*it);
if (!c2.was_removed() && *l_it == null_literal) {
// c2 was subsumed
if (c1.is_learned() && !c2.is_learned())
if (c1.is_learned() && !c2.is_learned()) {
s.set_learned(c1, false);
}
TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
remove_clause(c2);
m_num_subsumed++;
@ -646,7 +647,7 @@ namespace sat {
inline void simplifier::propagate_unit(literal l) {
unsigned old_trail_sz = s.m_trail.size();
s.assign(l, justification());
s.assign_scoped(l);
s.propagate_core(false); // must not use propagate(), since s.m_clauses is not in a consistent state.
if (s.inconsistent())
return;
@ -696,7 +697,7 @@ namespace sat {
switch (sz) {
case 0:
TRACE("elim_lit", tout << "clause is empty\n";);
s.set_conflict(justification());
s.set_conflict();
break;
case 1:
TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";);
@ -893,7 +894,7 @@ namespace sat {
unsigned sz = c.size();
switch (sz) {
case 0:
s.set_conflict(justification());
s.set_conflict();
return;
case 1:
c.restore(sz0);
@ -1164,7 +1165,6 @@ namespace sat {
if (m_intersection.empty() && !first) {
m_tautology.shrink(tsz);
}
// if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";);
return first;
}
@ -1222,8 +1222,6 @@ namespace sat {
RI literals.
*/
void minimize_covered_clause(unsigned idx) {
// IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause
// << " @ " << idx << "\n" << "tautology: " << m_tautology << "\n";);
literal _blocked = m_covered_clause[idx];
for (literal l : m_tautology) VERIFY(s.is_marked(l));
for (literal l : m_covered_clause) s.unmark_visited(l);
@ -1234,14 +1232,6 @@ namespace sat {
if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit);
if (s.is_marked(lit)) idx = i;
}
if (false && _blocked.var() == 8074) {
IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n";
verbose_stream() << "tautology: " << m_tautology << "\n";
verbose_stream() << "index: " << idx << "\n";
for (unsigned i = idx; i > 0; --i) {
m_covered_antecedent[i].display(verbose_stream(), m_covered_clause[i]);
});
}
for (unsigned i = idx; i > 0; --i) {
literal lit = m_covered_clause[i];
//s.mark_visited(lit);
@ -1285,10 +1275,6 @@ namespace sat {
// unsigned sz0 = m_covered_clause.size();
m_covered_clause.resize(j);
VERIFY(j >= m_clause.size());
if (false && _blocked.var() == 16774) {
IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n");
}
// IF_VERBOSE(0, verbose_stream() << "reduced from size " << sz0 << " to " << m_covered_clause << "\n" << m_clause << "\n";);
}
/*
@ -1385,7 +1371,6 @@ namespace sat {
}
bool above_threshold(unsigned sz0) const {
// if (sz0 * 400 < m_covered_clause.size()) IF_VERBOSE(0, verbose_stream() << "above threshold " << sz0 << " " << m_covered_clause.size() << "\n";);
return sz0 * 400 < m_covered_clause.size();
}
@ -1608,15 +1593,6 @@ namespace sat {
}
void block_covered_clause(clause& c, literal l, model_converter::kind k) {
if (false) {
IF_VERBOSE(0, verbose_stream() << "blocked: " << l << " @ " << c << " :covered " << m_covered_clause << "\n";
s.m_use_list.display(verbose_stream() << "use " << l << ":", l);
s.m_use_list.display(verbose_stream() << "use " << ~l << ":", ~l);
s.s.display_watch_list(verbose_stream() << ~l << ": ", s.get_wlist(l)) << "\n";
s.s.display_watch_list(verbose_stream() << l << ": ", s.get_wlist(~l)) << "\n";
);
}
TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
SASSERT(!s.is_external(l));
model_converter::entry& new_entry = m_mc.mk(k, l.var());
@ -1875,36 +1851,7 @@ namespace sat {
}
void simplifier::add_non_learned_binary_clause(literal l1, literal l2) {
#if 0
if ((l1.var() == 2039 || l2.var() == 2039) &&
(l1.var() == 27042 || l2.var() == 27042)) {
IF_VERBOSE(1, verbose_stream() << "add_bin: " << l1 << " " << l2 << "\n");
}
#endif
#if 0
watched* w;
watch_list & wlist1 = get_wlist(~l1);
watch_list & wlist2 = get_wlist(~l2);
w = find_binary_watch(wlist1, l2);
if (w) {
if (w->is_learned())
w->set_learned(false);
}
else {
wlist1.push_back(watched(l2, false));
}
w = find_binary_watch(wlist2, l1);
if (w) {
if (w->is_learned())
w->set_learned(false);
}
else {
wlist2.push_back(watched(l1, false));
}
#else
s.mk_bin_clause(l1, l2, false);
#endif
}
/**
@ -2027,13 +1974,6 @@ namespace sat {
m_elim_counter -= num_pos * num_neg + before_lits;
if (false) {
literal l(v, false);
IF_VERBOSE(0,
verbose_stream() << "elim: " << l << "\n";
s.display_watch_list(verbose_stream() << ~l << ": ", get_wlist(l)) << "\n";
s.display_watch_list(verbose_stream() << l << ": ", get_wlist(~l)) << "\n";);
}
// eliminate variable
++s.m_stats.m_elim_var_res;
VERIFY(!is_external(v));
@ -2054,7 +1994,7 @@ namespace sat {
}
switch (m_new_cls.size()) {
case 0:
s.set_conflict(justification());
s.set_conflict();
break;
case 1:
propagate_unit(m_new_cls[0]);

5
src/sat/sat_solver.cpp
View file

@ -2356,7 +2356,7 @@ namespace sat {
}
m_conflict_lvl = get_max_lvl(m_not_l, m_conflict);
TRACE("sat", tout << "conflict detected at level " << m_conflict_lvl << " for ";
TRACE("sat_verbose", tout << "conflict detected at level " << m_conflict_lvl << " for ";
if (m_not_l == literal()) tout << "null literal\n";
else tout << m_not_l << "\n";);
@ -2970,7 +2970,6 @@ namespace sat {
for (; i < sz; i++) {
literal l = m_lemma[i];
if (implied_by_marked(l)) {
TRACE("sat", tout << "drop: " << l << "\n";);
m_unmark.push_back(l.var());
}
else {
@ -3720,7 +3719,7 @@ namespace sat {
}
std::ostream& solver::display_watch_list(std::ostream& out, watch_list const& wl) const {
return sat::display_watch_list(out, cls_allocator(), wl);
return sat::display_watch_list(out, cls_allocator(), wl, m_ext.get());
}
void solver::display_assignment(std::ostream & out) const {

3
src/sat/sat_solver.h
View file

@ -314,8 +314,11 @@ namespace sat {
}
}
void assign_core(literal l, unsigned lvl, justification jst);
void assign_unit(literal l) { assign(l, justification()); }
void assign_scoped(literal l) { assign(l, justification()); }
void set_conflict(justification c, literal not_l);
void set_conflict(justification c) { set_conflict(c, null_literal); }
void set_conflict() { set_conflict(justification()); }
lbool status(clause const & c) const;
clause_offset get_offset(clause const & c) const { return cls_allocator().get_offset(&c); }
void checkpoint() {

10
src/sat/sat_watched.cpp
View file

@ -18,6 +18,7 @@ Revision History:
--*/
#include "sat/sat_watched.h"
#include "sat/sat_clause.h"
#include "sat/sat_extension.h"
namespace sat {
@ -96,7 +97,7 @@ namespace sat {
}
std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist) {
std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist, extension* ext) {
bool first = true;
for (watched const& w : wlist) {
if (first)
@ -116,7 +117,12 @@ namespace sat {
out << "(" << w.get_blocked_literal() << " " << *(ca.get_clause(w.get_clause_offset())) << ")";
break;
case watched::EXT_CONSTRAINT:
out << "ext: " << w.get_ext_constraint_idx();
if (ext) {
ext->display_constraint(out, w.get_ext_constraint_idx());
}
else {
out << "ext: " << w.get_ext_constraint_idx();
}
break;
default:
UNREACHABLE();

5
src/sat/sat_watched.h
View file

@ -35,6 +35,9 @@ namespace sat {
Remark: there are no clause objects for binary clauses.
*/
class extension;
class watched {
public:
enum kind {
@ -138,7 +141,7 @@ namespace sat {
void set_ternary_learned(watch_list& wlist, literal l1, literal l2, bool learned);
class clause_allocator;
std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist);
std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist, extension* ext);
void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist);
};

2
src/smt/theory_bv.cpp
View file

@ -448,7 +448,7 @@ namespace smt {
}
unsigned act = m_eq_activity[hash_u_u(v1, v2) & 0xFF]++;
if (act < 255) {
if ((act & 0xFF) != 0xFF) {
return;
}
++m_stats.m_num_eq_dynamic;