mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

ensure that bca takes also lemmas into account

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-27 15:40:25 -07:00
parent 0919fd4075
commit 829c140087
21 changed files with 384 additions and 149 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/cmd_context/cmd_context.cpp
View file

@ -1776,6 +1776,7 @@ void cmd_context::validate_model() {
continue;
}
TRACE("model_validate", model_smt2_pp(tout, *this, *(md.get()), 0););
IF_VERBOSE(10, verbose_stream() << "model check failed on: " << mk_pp(a, m()) << "\n";);
invalid_model = true;
}
}

1
src/sat/sat_asymm_branch.cpp
View file

@ -115,6 +115,7 @@ namespace sat {
}
bool asymm_branch::process(clause & c) {
if (c.is_blocked()) return true;
TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";);
SASSERT(s.scope_lvl() == 0);
SASSERT(s.m_qhead == s.m_trail.size());

28
src/sat/sat_clause.cpp
View file

@ -60,15 +60,15 @@ namespace sat {
}
bool clause::contains(literal l) const {
for (unsigned i = 0; i < m_size; i++)
if (m_lits[i] == l)
for (literal l2 : *this)
if (l2 == l)
return true;
return false;
}
bool clause::contains(bool_var v) const {
for (unsigned i = 0; i < m_size; i++)
if (m_lits[i].var() == v)
for (literal l : *this)
if (l.var() == v)
return true;
return false;
}
@ -87,8 +87,7 @@ namespace sat {
}
bool clause::satisfied_by(model const & m) const {
for (unsigned i = 0; i < m_size; i++) {
literal l = m_lits[i];
for (literal l : *this) {
if (l.sign()) {
if (m[l.var()] == l_false)
return true;
@ -197,14 +196,13 @@ namespace sat {
if (c.was_removed()) out << "x";
if (c.strengthened()) out << "+";
if (c.is_learned()) out << "*";
if (c.is_blocked()) out << "b";
return out;
}
std::ostream & operator<<(std::ostream & out, clause_vector const & cs) {
clause_vector::const_iterator it = cs.begin();
clause_vector::const_iterator end = cs.end();
for (; it != end; ++it) {
out << *(*it) << "\n";
for (clause *cp : cs) {
out << *cp << "\n";
}
return out;
}
@ -226,12 +224,12 @@ namespace sat {
}
std::ostream & operator<<(std::ostream & out, clause_wrapper const & c) {
out << "(";
for (unsigned i = 0; i < c.size(); i++) {
if (i > 0) out << " ";
out << c[i];
if (c.is_binary()) {
out << "(" << c[0] << " " << c[1] << ")";
}
else {
out << c.get_clause()->id() << ": " << *c.get_clause();
}
out << ")";
return out;
}

10
src/sat/sat_clause.h
View file

@ -33,6 +33,10 @@ namespace sat {
class clause_allocator;
class clause;
std::ostream & operator<<(std::ostream & out, clause const & c);
class clause {
friend class clause_allocator;
friend class tmp_clause;
@ -61,8 +65,8 @@ namespace sat {
literal & operator[](unsigned idx) { SASSERT(idx < m_size); return m_lits[idx]; }
literal const & operator[](unsigned idx) const { SASSERT(idx < m_size); return m_lits[idx]; }
bool is_learned() const { return m_learned; }
void unset_learned() { SASSERT(is_learned()); m_learned = false; }
void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; mark_strengthened(); } }
void unset_learned() { if (id() == 642277) std::cout << "unlearn " << *this << "\n"; SASSERT(is_learned()); m_learned = false; }
void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; mark_strengthened(); if (id() == 642277) std::cout << "shrink " << *this << "\n"; } }
bool strengthened() const { return m_strengthened; }
void mark_strengthened() { m_strengthened = true; update_approx(); }
void unmark_strengthened() { m_strengthened = false; }
@ -101,7 +105,6 @@ namespace sat {
void set_reinit_stack(bool f) { m_reinit_stack = f; }
};
std::ostream & operator<<(std::ostream & out, clause const & c);
std::ostream & operator<<(std::ostream & out, clause_vector const & cs);
class bin_clause {
@ -180,6 +183,7 @@ namespace sat {
bool contains(literal l) const;
bool contains(bool_var v) const;
clause * get_clause() const { SASSERT(!is_binary()); return m_cls; }
bool was_removed() const { return !is_binary() && get_clause()->was_removed(); }
};
typedef svector<clause_wrapper> clause_wrapper_vector;

3
src/sat/sat_cleaner.cpp
View file

@ -137,7 +137,8 @@ namespace sat {
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
if (new_sz == 2) {
TRACE("cleanup_bug", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
s.mk_bin_clause(c[0], c[1], c.is_learned());
if (!c.is_blocked())
s.mk_bin_clause(c[0], c[1], c.is_learned());
s.del_clause(c);
}
else {

5
src/sat/sat_config.cpp
View file

@ -146,9 +146,10 @@ namespace sat {
m_minimize_lemmas = p.minimize_lemmas();
m_core_minimize = p.core_minimize();
m_core_minimize_partial = p.core_minimize_partial();
m_drat_check = p.drat_check();
m_drat_check_unsat = p.drat_check_unsat();
m_drat_check_sat = p.drat_check_sat();
m_drat_file = p.drat_file();
m_drat = (m_drat_check || m_drat_file != symbol("")) && p.threads() == 1;
m_drat = (m_drat_check_unsat || m_drat_file != symbol("") || m_drat_check_sat) && p.threads() == 1;
m_dyn_sub_res = p.dyn_sub_res();
// Parameters used in Liang, Ganesh, Poupart, Czarnecki AAAI 2016.

3
src/sat/sat_config.h
View file

@ -105,7 +105,8 @@ namespace sat {
bool m_core_minimize_partial;
bool m_drat;
symbol m_drat_file;
bool m_drat_check;
bool m_drat_check_unsat;
bool m_drat_check_sat;
bool m_dimacs_display;
bool m_dimacs_inprocess_display;

42
src/sat/sat_drat.cpp
View file

@ -27,7 +27,10 @@ namespace sat {
drat::drat(solver& s):
s(s),
m_out(0),
m_inconsistent(false)
m_inconsistent(false),
m_check_unsat(false),
m_check_sat(false),
m_check(false)
{
if (s.m_config.m_drat && s.m_config.m_drat_file != symbol()) {
m_out = alloc(std::ofstream, s.m_config.m_drat_file.str().c_str());
@ -44,6 +47,12 @@ namespace sat {
}
}
void drat::updt_config() {
m_check_unsat = s.m_config.m_drat_check_unsat;
m_check_sat = s.m_config.m_drat_check_sat;
m_check = m_check_unsat || m_check_sat;
}
std::ostream& operator<<(std::ostream& out, drat::status st) {
switch (st) {
case drat::status::learned: return out << "l";
@ -88,7 +97,7 @@ namespace sat {
}
void drat::append(literal l, status st) {
IF_VERBOSE(10, trace(verbose_stream(), 1, &l, st););
IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st););
if (st == status::learned) {
verify(1, &l);
}
@ -100,7 +109,7 @@ namespace sat {
void drat::append(literal l1, literal l2, status st) {
literal lits[2] = { l1, l2 };
IF_VERBOSE(10, trace(verbose_stream(), 2, lits, st););
IF_VERBOSE(20, trace(verbose_stream(), 2, lits, st););
if (st == status::deleted) {
// noop
// don't record binary as deleted.
@ -131,7 +140,7 @@ namespace sat {
void drat::append(clause& c, status st) {
unsigned n = c.size();
IF_VERBOSE(10, trace(verbose_stream(), n, c.begin(), st););
IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st););
if (st == status::learned) {
verify(n, c.begin());
@ -270,7 +279,7 @@ namespace sat {
}
void drat::verify(unsigned n, literal const* c) {
if (!is_drup(n, c) && !is_drat(n, c)) {
if (m_check_unsat && !is_drup(n, c) && !is_drat(n, c)) {
std::cout << "Verification failed\n";
UNREACHABLE();
//display(std::cout);
@ -412,7 +421,7 @@ namespace sat {
void drat::add() {
if (m_out) (*m_out) << "0\n";
if (s.m_config.m_drat_check) {
if (m_check_unsat) {
SASSERT(m_inconsistent);
}
}
@ -420,7 +429,7 @@ namespace sat {
declare(l);
status st = get_status(learned);
if (m_out) dump(1, &l, st);
if (s.m_config.m_drat_check) append(l, st);
if (m_check) append(l, st);
}
void drat::add(literal l1, literal l2, bool learned) {
declare(l1);
@ -428,17 +437,17 @@ namespace sat {
literal ls[2] = {l1, l2};
status st = get_status(learned);
if (m_out) dump(2, ls, st);
if (s.m_config.m_drat_check) append(l1, l2, st);
if (m_check) append(l1, l2, st);
}
void drat::add(clause& c, bool learned) {
TRACE("sat", tout << "add: " << c << "\n";);
for (unsigned i = 0; i < c.size(); ++i) declare(c[i]);
status st = get_status(learned);
if (m_out) dump(c.size(), c.begin(), st);
if (s.m_config.m_drat_check) append(c, get_status(learned));
if (m_check_unsat) append(c, get_status(learned));
}
void drat::add(literal_vector const& lits, svector<premise> const& premises) {
if (s.m_config.m_drat_check) {
if (m_check) {
switch (lits.size()) {
case 0: add(); break;
case 1: append(lits[0], status::external); break;
@ -453,7 +462,7 @@ namespace sat {
void drat::add(literal_vector const& c) {
for (unsigned i = 0; i < c.size(); ++i) declare(c[i]);
if (m_out) dump(c.size(), c.begin(), status::learned);
if (s.m_config.m_drat_check) {
if (m_check) {
switch (c.size()) {
case 0: add(); break;
case 1: append(c[0], status::learned); break;
@ -469,20 +478,25 @@ namespace sat {
void drat::del(literal l) {
if (m_out) dump(1, &l, status::deleted);
if (s.m_config.m_drat_check) append(l, status::deleted);
if (m_check_unsat) append(l, status::deleted);
}
void drat::del(literal l1, literal l2) {
literal ls[2] = {l1, l2};
if (m_out) dump(2, ls, status::deleted);
if (s.m_config.m_drat_check)
if (m_check)
append(l1, l2, status::deleted);
}
void drat::del(clause& c) {
TRACE("sat", tout << "del: " << c << "\n";);
if (m_out) dump(c.size(), c.begin(), status::deleted);
if (s.m_config.m_drat_check) {
if (m_check) {
clause* c1 = s.m_cls_allocator.mk_clause(c.size(), c.begin(), c.is_learned());
append(*c1, status::deleted);
}
}
void drat::check_model(model const& m) {
std::cout << "check model on " << m_proof.size() << "\n";
}
}

5
src/sat/sat_drat.h
View file

@ -52,6 +52,7 @@ namespace sat {
vector<watch> m_watches;
svector<lbool> m_assignment;
bool m_inconsistent;
bool m_check_unsat, m_check_sat, m_check;
void dump(unsigned n, literal const* c, status st);
void append(literal l, status st);
@ -78,6 +79,8 @@ namespace sat {
public:
drat(solver& s);
~drat();
void updt_config();
void add();
void add(literal l, bool learned);
void add(literal l1, literal l2, bool learned);
@ -89,6 +92,8 @@ namespace sat {
void del(literal l);
void del(literal l1, literal l2);
void del(clause& c);
void check_model(model const& m);
};
};

4
src/sat/sat_lookahead.h
View file

@ -246,8 +246,8 @@ namespace sat {
inline bool is_true(literal l) const { return is_true_at(l, m_level); }
inline void set_true(literal l) { m_stamp[l.var()] = m_level + l.sign(); }
inline void set_undef(literal l) { m_stamp[l.var()] = 0; }
inline unsigned get_level(literal l) const { return m_stamp[l.var()] & UINT_MAX - 1; }
void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); }
inline unsigned get_level(literal l) const { return m_stamp[l.var()] & ~0x1; }
void set_level(literal d, literal s) { m_stamp[d.var()] = get_level(s) + d.sign(); }
lbool value(literal l) const { return is_undef(l) ? l_undef : is_true(l) ? l_true : l_false; }
// set the level within a scope of the search.

138
src/sat/sat_model_converter.cpp
View file

@ -18,11 +18,12 @@ Revision History:
--*/
#include "sat/sat_model_converter.h"
#include "sat/sat_clause.h"
#include "sat/sat_solver.h"
#include "util/trace.h"
namespace sat {
model_converter::model_converter() {
model_converter::model_converter(): m_solver(nullptr) {
}
model_converter::~model_converter() {
@ -50,7 +51,6 @@ namespace sat {
}
if (!sat) {
m[lit.var()] = lit.sign() ? l_false : l_true;
// if (lit.var() == 258007) std::cout << "flip " << lit << " " << m[lit.var()] << " @ " << i << " of " << c << " from overall size " << sz << "\n";
}
}
}
@ -58,6 +58,8 @@ namespace sat {
void model_converter::operator()(model & m) const {
vector<entry>::const_iterator begin = m_entries.begin();
vector<entry>::const_iterator it = m_entries.end();
bool first = true;
VERIFY(!m_solver || m_solver->check_clauses(m));
while (it != begin) {
--it;
SASSERT(it->get_kind() != ELIM_VAR || m[it->var()] == l_undef);
@ -70,14 +72,18 @@ namespace sat {
for (literal l : it->m_clauses) {
if (l == null_literal) {
// end of clause
elim_stack* s = it->m_elim_stack[index];
elim_stack* st = it->m_elim_stack[index];
if (!sat) {
m[it->var()] = var_sign ? l_false : l_true;
}
if (s) {
process_stack(m, clause, s->stack());
if (st) {
process_stack(m, clause, st->stack());
}
sat = false;
if (first && m_solver && !m_solver->check_clauses(m)) {
display(std::cout, *it) << "\n";
first = false;
}
++index;
clause.reset();
continue;
@ -95,8 +101,12 @@ namespace sat {
else if (!sat && v != it->var() && m[v] == l_undef) {
// clause can be satisfied by assigning v.
m[v] = sign ? l_false : l_true;
// if (v == 258007) std::cout << "set undef " << v << " to " << m[v] << " in " << clause << "\n";
// if (first) std::cout << "set: " << l << "\n";
sat = true;
if (first && m_solver && !m_solver->check_clauses(m)) {
display(std::cout, *it) << "\n";;
first = false;
}
}
}
DEBUG_CODE({
@ -217,10 +227,12 @@ namespace sat {
it2++;
for (; it2 != end; ++it2) {
SASSERT(it2->var() != it->var());
if (it2->var() == it->var()) return false;
for (literal l : it2->m_clauses) {
CTRACE("sat_model_converter", l.var() == it->var(), tout << "var: " << it->var() << "\n"; display(tout););
SASSERT(l.var() != it->var());
SASSERT(l == null_literal || l.var() < num_vars);
if (it2->var() == it->var()) return false;
}
}
}
@ -229,31 +241,105 @@ namespace sat {
}
void model_converter::display(std::ostream & out) const {
out << "(sat::model-converter";
out << "(sat::model-converter\n";
bool first = true;
for (auto & entry : m_entries) {
out << "\n (" << (entry.get_kind() == ELIM_VAR ? "elim" : "blocked") << " " << entry.var();
bool start = true;
for (literal l : entry.m_clauses) {
if (start) {
out << "\n (";
start = false;
}
else {
if (l != null_literal)
out << " ";
}
if (l == null_literal) {
out << ")";
start = true;
continue;
}
out << l;
}
out << ")";
if (first) first = false; else out << "\n";
display(out, entry);
}
out << ")\n";
}
std::ostream& model_converter::display(std::ostream& out, entry const& entry) const {
out << " (";
switch (entry.get_kind()) {
case ELIM_VAR: out << "elim"; break;
case BLOCK_LIT: out << "blocked"; break;
case CCE: out << "cce"; break;
case ACCE: out << "acce"; break;
}
out << " " << entry.var();
bool start = true;
unsigned index = 0;
for (literal l : entry.m_clauses) {
if (start) {
out << "\n (";
start = false;
}
else {
if (l != null_literal)
out << " ";
}
if (l == null_literal) {
out << ")";
start = true;
elim_stack* st = entry.m_elim_stack[index];
if (st) {
elim_stackv const& stack = st->stack();
unsigned sz = stack.size();
for (unsigned i = sz; i-- > 0; ) {
out << "\n " << stack[i].first << " " << stack[i].second;
}
}
++index;
continue;
}
out << l;
}
out << ")";
for (literal l : entry.m_clauses) {
if (l != null_literal) {
if (m_solver && m_solver->was_eliminated(l.var())) out << "\neliminated: " << l;
}
}
return out;
}
void model_converter::validate_is_blocked(entry const& e, clause const& c) {
if (c.is_blocked() || c.is_learned()) return;
unsigned index = 0;
literal lit = null_literal;
bool_var v = e.var();
for (literal l : c) {
if (l.var() == v) {
lit = l;
break;
}
}
if (lit == null_literal) return;
bool sat = false;
for (literal l : e.m_clauses) {
if (l == null_literal) {
if (!sat) {
display(std::cout << "clause is not blocked\n", e) << "\n";
std::cout << c << "\n";
}
sat = false;
elim_stack* st = e.m_elim_stack[index];
if (st) {
elim_stackv const& stack = st->stack();
unsigned sz = stack.size();
for (unsigned i = sz; i-- > 0; ) {
// verify ...
}
}
++index;
continue;
}
if (sat) {
continue;
}
if (l.var() == v) {
sat = l == lit;
}
else {
sat = c.contains(~l);
}
}
}
void model_converter::copy(model_converter const & src) {
reset();
m_entries.append(src.m_entries);

15
src/sat/sat_model_converter.h
View file

@ -36,6 +36,9 @@ namespace sat {
This is a low-level model_converter. Given a mapping from bool_var to expr,
it can be converted into a general Z3 model_converter
*/
class solver;
class model_converter {
public:
@ -55,11 +58,11 @@ namespace sat {
elim_stackv const& stack() const { return m_stack; }
};
enum kind { ELIM_VAR = 0, BLOCK_LIT };
enum kind { ELIM_VAR = 0, BLOCK_LIT, CCE, ACCE };
class entry {
friend class model_converter;
unsigned m_var:31;
unsigned m_kind:1;
unsigned m_var:30;
unsigned m_kind:2;
literal_vector m_clauses; // the different clauses are separated by null_literal
sref_vector<elim_stack> m_elim_stack;
entry(kind k, bool_var v):m_var(v), m_kind(k) {}
@ -75,12 +78,18 @@ namespace sat {
};
private:
vector<entry> m_entries;
solver const* m_solver;
void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const;
std::ostream& display(std::ostream & out, entry const& entry) const;
void validate_is_blocked(entry const& e, clause const& c);
public:
model_converter();
~model_converter();
void set_solver(solver const* s) { m_solver = s; }
void operator()(model & m) const;
model_converter& operator=(model_converter const& other);

3
src/sat/sat_params.pyg
View file

@ -28,7 +28,8 @@ def_module_params('sat',
('threads', UINT, 1, 'number of parallel threads to use'),
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
('drat.check', BOOL, False, 'build up internal proof and check'),
('drat.check_unsat', BOOL, False, 'build up internal proof and check'),
('drat.check_sat', BOOL, False, 'build up internal trace, check satisfying model'),
('cardinality.solver', BOOL, False, 'use cardinality solver'),
('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'),
('xor.solver', BOOL, False, 'use xor solver'),

4
src/sat/sat_scc.cpp
View file

@ -107,7 +107,7 @@ namespace sat {
frame & fr = frames.back();
unsigned l_idx = fr.m_lidx;
if (!fr.m_first) {
SASSERT(fr.m_it->is_binary_clause());
SASSERT(fr.m_it->is_binary_unblocked_clause());
// after visiting child
literal l2 = fr.m_it->get_literal();
unsigned l2_idx = l2.index();
@ -118,7 +118,7 @@ namespace sat {
}
fr.m_first = false;
while (fr.m_it != fr.m_end) {
if (!fr.m_it->is_binary_clause()) {
if (!fr.m_it->is_binary_unblocked_clause()) {
fr.m_it++;
continue;
}

157
src/sat/sat_simplifier.cpp
View file

@ -201,18 +201,19 @@ namespace sat {
CASSERT("sat_solver", s.check_invariant());
m_need_cleanup = false;
m_use_list.init(s.num_vars());
m_learned_in_use_lists = false;
m_learned_in_use_lists = learned;
if (learned) {
register_clauses(s.m_learned);
m_learned_in_use_lists = true;
}
register_clauses(s.m_clauses);
if (!learned && (bce_enabled() || bca_enabled()))
if (bce_enabled() || abce_enabled() || bca_enabled()) {
elim_blocked_clauses();
}
if (!learned)
if (!learned) {
m_num_calls++;
}
m_sub_counter = m_subsumption_limit;
m_elim_counter = m_res_limit;
@ -457,7 +458,7 @@ namespace sat {
literal_vector::iterator l_it = m_bs_ls.begin();
for (; it != end; ++it, ++l_it) {
clause & c2 = *(*it);
if (!c2.was_removed() && *l_it == null_literal) {
if (!c2.was_removed() && !c1.is_blocked() && *l_it == null_literal) {
// c2 was subsumed
if (c1.is_learned() && !c2.is_learned())
c1.unset_learned();
@ -713,7 +714,7 @@ namespace sat {
// should not traverse wlist using iterators, since back_subsumption1 may add new binary clauses there
for (unsigned j = 0; j < wlist.size(); j++) {
watched w = wlist[j];
if (w.is_binary_clause()) {
if (w.is_binary_unblocked_clause()) {
literal l2 = w.get_literal();
if (l.index() < l2.index()) {
m_dummy.set(l, l2, w.is_learned());
@ -959,8 +960,10 @@ namespace sat {
void operator()() {
if (s.bce_enabled())
block_clauses();
if (s.abce_enabled())
cce<false>();
if (s.cce_enabled())
cce();
cce<true>();
if (s.bca_enabled())
bca();
}
@ -1053,21 +1056,22 @@ namespace sat {
for (watched & w : s.get_wlist(l)) {
// when adding a blocked clause, then all non-learned clauses have to be considered for the
// resolution intersection.
bool process_bin = adding ? (w.is_binary_clause() && !w.is_learned()) : w.is_binary_unblocked_clause();
bool process_bin = adding ? w.is_binary_clause() : w.is_binary_unblocked_clause();
if (process_bin) {
literal lit = w.get_literal();
if (s.is_marked(~lit) && lit != ~l) continue;
if (s.is_marked(~lit) && lit != ~l) {
continue; // tautology
}
if (!first || s.is_marked(lit)) {
inter.reset();
return false;
return false; // intersection is empty or does not add anything new.
}
first = false;
inter.push_back(lit);
}
}
clause_use_list & neg_occs = s.m_use_list.get(~l);
clause_use_list::iterator it = neg_occs.mk_iterator();
for (; !it.at_end(); it.next()) {
for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
bool tautology = false;
clause & c = it.curr();
if (c.is_blocked() && !adding) continue;
@ -1098,6 +1102,30 @@ namespace sat {
return first;
}
bool check_abce_tautology(literal l) {
if (!process_var(l.var())) return false;
for (watched & w : s.get_wlist(l)) {
if (w.is_binary_unblocked_clause()) {
literal lit = w.get_literal();
if (!s.is_marked(~lit) || lit == ~l) return false;
}
}
clause_use_list & neg_occs = s.m_use_list.get(~l);
for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
clause & c = it.curr();
if (c.is_blocked()) continue;
bool tautology = false;
for (literal lit : c) {
if (s.is_marked(~lit) && lit != ~l) {
tautology = true;
break;
}
}
if (!tautology) return false;
}
return true;
}
/*
* C \/ l l \/ lit
* -------------------
@ -1146,59 +1174,101 @@ namespace sat {
return false;
}
bool cla(literal& blocked) {
bool above_threshold(unsigned sz0) const {
return sz0 * 10 < m_covered_clause.size();
}
template<bool use_ri>
bool cla(literal& blocked, model_converter::kind& k) {
bool is_tautology = false;
for (literal l : m_covered_clause) s.mark_visited(l);
unsigned num_iterations = 0, sz;
m_elim_stack.reset();
m_ala_qhead = 0;
k = model_converter::CCE;
unsigned sz0 = m_covered_clause.size();
/*
* For blocked clause elimination with asymmetric literal addition (ABCE)
* it suffices to check if one of the original
* literals in the clause is blocked modulo the additional literals added to the clause.
* So we record sz0, the original set of literals in the clause, mark additional literals,
* and then check if any of the first sz0 literals are blocked.
*/
if (s.abce_enabled() && !use_ri) {
add_ala();
for (unsigned i = 0; i < sz0; ++i) {
if (check_abce_tautology(m_covered_clause[i])) {
blocked = m_covered_clause[i];
is_tautology = true;
break;
}
}
k = model_converter::BLOCK_LIT; // actually ABCE
for (literal l : m_covered_clause) s.unmark_visited(l);
m_covered_clause.shrink(sz0);
return is_tautology;
}
/*
* For CCE we add the resolution intersection while checking if the clause becomes a tautology.
* For ACCE, in addition, we add literals.
*/
do {
do {
if (above_threshold(sz0)) break;
++num_iterations;
sz = m_covered_clause.size();
is_tautology = add_cla(blocked);
}
while (m_covered_clause.size() > sz && !is_tautology);
if (above_threshold(sz0)) break;
if (s.acce_enabled() && !is_tautology) {
sz = m_covered_clause.size();
add_ala();
k = model_converter::ACCE;
}
}
while (m_covered_clause.size() > sz && !is_tautology);
// if (is_tautology) std::cout << num_iterations << " " << m_covered_clause.size() << " " << sz0 << " " << is_tautology << " " << m_elim_stack.size() << "\n";
for (literal l : m_covered_clause) s.unmark_visited(l);
// if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n";
return is_tautology;
return is_tautology && !above_threshold(sz0);
}
// perform covered clause elimination.
// first extract the covered literal addition (CLA).
// then check whether the CLA is blocked.
bool cce(clause& c, literal& blocked) {
template<bool use_ri>
bool cce(clause& c, literal& blocked, model_converter::kind& k) {
m_covered_clause.reset();
for (literal l : c) m_covered_clause.push_back(l);
return cla(blocked);
return cla<use_ri>(blocked, k);
}
bool cce(literal l1, literal l2, literal& blocked) {
template<bool use_ri>
bool cce(literal l1, literal l2, literal& blocked, model_converter::kind& k) {
m_covered_clause.reset();
m_covered_clause.push_back(l1);
m_covered_clause.push_back(l2);
return cla(blocked);
return cla<use_ri>(blocked, k);
}
template<bool use_ri>
void cce() {
insert_queue();
cce_clauses();
cce_binary();
cce_clauses<use_ri>();
cce_binary<use_ri>();
}
template<bool use_ri>
void cce_binary() {
while (!m_queue.empty() && m_counter >= 0) {
s.checkpoint();
process_cce_binary(m_queue.next());
process_cce_binary<use_ri>(m_queue.next());
}
}
template<bool use_ri>
void process_cce_binary(literal l) {
literal blocked = null_literal;
watch_list & wlist = s.get_wlist(~l);
@ -1206,15 +1276,15 @@ namespace sat {
watch_list::iterator it = wlist.begin();
watch_list::iterator it2 = it;
watch_list::iterator end = wlist.end();
model_converter::kind k;
for (; it != end; ++it) {
if (!it->is_binary_clause() || it->is_blocked()) {
INC();
continue;
}
literal l2 = it->get_literal();
if (cce(l, l2, blocked)) {
block_covered_binary(it, l, blocked);
if (cce<use_ri>(l, l2, blocked, k)) {
block_covered_binary(it, l, blocked, k);
s.m_num_covered_clauses++;
}
else {
@ -1225,13 +1295,15 @@ namespace sat {
}
template<bool use_ri>
void cce_clauses() {
m_to_remove.reset();
literal blocked;
model_converter::kind k;
for (clause* cp : s.s.m_clauses) {
clause& c = *cp;
if (!c.was_removed() && !c.is_blocked() && cce(c, blocked)) {
block_covered_clause(c, blocked);
if (!c.was_removed() && !c.is_blocked() && cce<use_ri>(c, blocked, k)) {
block_covered_clause(c, blocked, k);
s.m_num_covered_clauses++;
}
}
@ -1242,10 +1314,10 @@ namespace sat {
}
void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry) {
void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) {
TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
if (new_entry == 0)
new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
new_entry = &(mc.mk(k, l.var()));
m_to_remove.push_back(&c);
for (literal lit : c) {
if (lit != l && process_var(lit.var())) {
@ -1255,19 +1327,19 @@ namespace sat {
}
void block_clause(clause& c, literal l, model_converter::entry *& new_entry) {
prepare_block_clause(c, l, new_entry);
prepare_block_clause(c, l, new_entry, model_converter::BLOCK_LIT);
mc.insert(*new_entry, c);
}
void block_covered_clause(clause& c, literal l) {
void block_covered_clause(clause& c, literal l, model_converter::kind k) {
model_converter::entry * new_entry = 0;
prepare_block_clause(c, l, new_entry);
prepare_block_clause(c, l, new_entry, k);
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
}
void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry) {
void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) {
if (new_entry == 0)
new_entry = &(mc.mk(model_converter::BLOCK_LIT, blocked.var()));
new_entry = &(mc.mk(k, blocked.var()));
literal l2 = it->get_literal();
TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";);
if (s.m_retain_blocked_clauses && !it->is_learned()) {
@ -1281,13 +1353,13 @@ namespace sat {
}
void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
prepare_block_binary(it, l, l, new_entry);
prepare_block_binary(it, l, l, new_entry, model_converter::BLOCK_LIT);
mc.insert(*new_entry, l, it->get_literal());
}
void block_covered_binary(watch_list::iterator it, literal l, literal blocked) {
void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::kind k) {
model_converter::entry * new_entry = 0;
prepare_block_binary(it, l, blocked, new_entry);
prepare_block_binary(it, l, blocked, new_entry, k);
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
}
@ -1375,10 +1447,12 @@ namespace sat {
stopwatch m_watch;
unsigned m_num_blocked_clauses;
unsigned m_num_covered_clauses;
unsigned m_num_added_clauses;
blocked_cls_report(simplifier & s):
m_simplifier(s),
m_num_blocked_clauses(s.m_num_blocked_clauses),
m_num_covered_clauses(s.m_num_covered_clauses) {
m_num_covered_clauses(s.m_num_covered_clauses),
m_num_added_clauses(s.m_num_bca) {
m_watch.start();
}
@ -1389,6 +1463,8 @@ namespace sat {
<< (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses)
<< " :elim-covered-clauses "
<< (m_simplifier.m_num_covered_clauses - m_num_covered_clauses)
<< " :added-clauses "
<< (m_simplifier.m_num_bca - m_num_added_clauses)
<< mem_stat()
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
}
@ -1456,8 +1532,7 @@ namespace sat {
*/
void simplifier::collect_clauses(literal l, clause_wrapper_vector & r, bool include_blocked) {
clause_use_list const & cs = m_use_list.get(l);
clause_use_list::iterator it = cs.mk_iterator();
for (; !it.at_end(); it.next()) {
for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
if (!it.curr().is_blocked() || include_blocked) {
r.push_back(clause_wrapper(it.curr()));
SASSERT(r.back().size() == it.curr().size());
@ -1703,6 +1778,7 @@ namespace sat {
else
s.m_stats.m_mk_clause++;
clause * new_c = s.m_cls_allocator.mk_clause(m_new_cls.size(), m_new_cls.c_ptr(), false);
if (s.m_config.m_drat) s.m_drat.add(*new_c, true);
s.m_clauses.push_back(new_c);
m_use_list.insert(*new_c);
@ -1769,6 +1845,7 @@ namespace sat {
m_cce = p.cce();
m_acce = p.acce();
m_bca = p.bca();
m_bce_delay = p.bce_delay();
m_elim_blocked_clauses = p.elim_blocked_clauses();
m_elim_blocked_clauses_at = p.elim_blocked_clauses_at();
m_retain_blocked_clauses = p.retain_blocked_clauses();

11
src/sat/sat_simplifier.h
View file

@ -71,9 +71,11 @@ namespace sat {
int m_elim_counter;
// config
bool m_abce; // block clauses using asymmetric added literals
bool m_cce; // covered clause elimination
bool m_acce; // cce with asymetric literal addition
bool m_bca; // blocked (binary) clause addition.
unsigned m_bce_delay;
bool m_elim_blocked_clauses;
unsigned m_elim_blocked_clauses_at;
bool m_retain_blocked_clauses;
@ -169,10 +171,11 @@ namespace sat {
struct blocked_clause_elim;
void elim_blocked_clauses();
bool bce_enabled() const { return m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls || cce_enabled(); }
bool acce_enabled() const { return m_acce; }
bool cce_enabled() const { return m_cce || acce_enabled(); }
bool bca_enabled() const { return m_bca; }
bool bce_enabled() const { return !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls || cce_enabled()); }
bool acce_enabled() const { return !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_acce; }
bool cce_enabled() const { return !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled()); }
bool abce_enabled() const { return !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce; }
bool bca_enabled() const { return m_bca && m_learned_in_use_lists; }
bool elim_vars_bdd_enabled() const { return m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay; }
bool elim_vars_enabled() const { return m_elim_vars; }

2
src/sat/sat_simplifier_params.pyg
View file

@ -2,10 +2,12 @@ def_module_params(module_name='sat',
class_name='sat_simplifier_params',
export=True,
params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'),
('abce', BOOL, BOOL, False, 'eliminate blocked clauses using asymmmetric literals'),
('cce', BOOL, False, 'eliminate covered clauses'),
('acce', BOOL, False, 'eliminate covered clauses using asymmetric added literals'),
('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'),
('bca', BOOL, False, 'blocked clause addition - add blocked binary clauses'),
('bce_delay', UINT, 0, 'delay eliminate blocked clauses until simplification round'),
('retain_blocked_clauses', BOOL, False, 'retain blocked clauses for propagation, hide them from variable elimination'),
('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'),
('resolution.limit', UINT, 500000000, 'approx. maximum number of literals visited during variable elimination'),

77
src/sat/sat_solver.cpp
View file

@ -23,14 +23,11 @@ Revision History:
#include "util/luby.h"
#include "util/trace.h"
#include "util/max_cliques.h"
#include "util/gparams.h"
// define to update glue during propagation
#define UPDATE_GLUE
// define to create a copy of the solver before starting the search
// useful for checking models
// #define CLONE_BEFORE_SOLVING
namespace sat {
solver::solver(params_ref const & p, reslimit& l):
@ -734,15 +731,13 @@ namespace sat {
case watched::CLAUSE: {
if (value(it->get_blocked_literal()) == l_true) {
TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n";
clause_offset cls_off = it->get_clause_offset();
clause & c = *(m_cls_allocator.get_clause(cls_off));
tout << c << "\n";);
tout << get_clause(it) << "\n";);
*it2 = *it;
it2++;
break;
}
clause_offset cls_off = it->get_clause_offset();
clause & c = *(m_cls_allocator.get_clause(cls_off));
clause & c = get_clause(cls_off);
TRACE("propagate_clause_bug", tout << "processing... " << c << "\nwas_removed: " << c.was_removed() << "\n";);
if (c[0] == not_l)
std::swap(c[0], c[1]);
@ -886,12 +881,10 @@ namespace sat {
return check_par(num_lits, lits);
}
flet<bool> _searching(m_searching, true);
#ifdef CLONE_BEFORE_SOLVING
if (m_mc.empty()) {
m_clone = alloc(solver, m_params);
SASSERT(m_clone);
if (m_mc.empty() && gparams::get().get_bool("model_validate", false)) {
m_clone = alloc(solver, m_params, m_rlimit);
m_clone->copy(*this);
}
#endif
try {
init_search();
if (inconsistent()) return l_false;
@ -1548,30 +1541,40 @@ namespace sat {
m_model[v] = value(v);
}
TRACE("sat_mc_bug", m_mc.display(tout););
m_mc(m_model);
TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);
// #ifndef _EXTERNAL_RELEASE
IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";);
if (!check_model(m_model)) {
if (!check_clauses(m_model)) {
UNREACHABLE();
throw solver_exception("check model failed");
}
if (m_config.m_drat) m_drat.check_model(m_model);
// m_mc.set_solver(this);
m_mc(m_model);
if (!check_clauses(m_model)) {
std::cout << "failure checking clauses on transformed model\n";
UNREACHABLE();
throw solver_exception("check model failed");
}
TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);
if (m_clone) {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model (on original set of clauses)\"\n";);
if (!m_clone->check_model(m_model))
throw solver_exception("check model failed (for cloned solver)");
}
// #endif
}
bool solver::check_model(model const & m) const {
bool solver::check_clauses(model const& m) const {
bool ok = true;
for (clause const* cp : m_clauses) {
clause const & c = *cp;
if (!c.satisfied_by(m) && !c.is_blocked()) {
IF_VERBOSE(0, verbose_stream() << "model check failed: " << c << "\n";);
IF_VERBOSE(0, verbose_stream() << "failed clause " << c.id() << ": " << c << "\n";);
TRACE("sat", tout << "failed: " << c << "\n";
tout << "assumptions: " << m_assumptions << "\n";
tout << "trail: " << m_trail << "\n";
@ -1612,10 +1615,16 @@ namespace sat {
ok = false;
}
}
return ok;
}
bool solver::check_model(model const & m) const {
bool ok = check_clauses(m);
if (ok && !m_mc.check_model(m)) {
ok = false;
TRACE("sat", tout << "model: " << m << "\n"; m_mc.display(tout););
}
IF_VERBOSE(1, verbose_stream() << "model check " << (ok?"OK":"failed") << "\n";);
return ok;
}
@ -2034,7 +2043,7 @@ namespace sat {
process_antecedent(~(js.get_literal2()), num_marks);
break;
case justification::CLAUSE: {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
clause & c = get_clause(js);
unsigned i = 0;
if (consequent != null_literal) {
SASSERT(c[0] == consequent || c[1] == consequent);
@ -2153,7 +2162,7 @@ namespace sat {
process_antecedent_for_unsat_core(~(js.get_literal2()));
break;
case justification::CLAUSE: {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
clause & c = get_clause(js);
unsigned i = 0;
if (consequent != null_literal) {
SASSERT(c[0] == consequent || c[1] == consequent);
@ -2497,7 +2506,7 @@ namespace sat {
}
break;
case justification::CLAUSE: {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
clause & c = get_clause(js);
unsigned i = 0;
if (c[0].var() == var) {
i = 1;
@ -2624,8 +2633,7 @@ namespace sat {
unsigned sz = m_lemma.size();
SASSERT(!is_marked(m_lemma[0].var()));
mark(m_lemma[0].var());
for (unsigned i = m_lemma.size(); i > 0; ) {
--i;
for (unsigned i = m_lemma.size(); i-- > 0; ) {
justification js = m_justification[m_lemma[i].var()];
switch (js.get_kind()) {
case justification::NONE:
@ -2638,9 +2646,9 @@ namespace sat {
update_lrb_reasoned(js.get_literal2());
break;
case justification::CLAUSE: {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
for (unsigned i = 0; i < c.size(); ++i) {
update_lrb_reasoned(c[i]);
clause & c = get_clause(js);
for (literal l : c) {
update_lrb_reasoned(l);
}
break;
}
@ -3045,6 +3053,7 @@ namespace sat {
m_scc.updt_params(p);
m_rand.set_seed(m_config.m_random_seed);
m_step_size = m_config.m_step_size_init;
m_drat.updt_config();
}
void solver::collect_param_descrs(param_descrs & d) {
@ -3199,7 +3208,7 @@ namespace sat {
std::ostream& solver::display_justification(std::ostream & out, justification const& js) const {
out << js;
if (js.is_clause()) {
out << *(m_cls_allocator.get_clause(js.get_clause_offset()));
out << get_clause(js);
}
else if (js.is_ext_justification() && m_ext) {
m_ext->display_justification(out << " ", js.get_ext_justification_idx());
@ -3845,11 +3854,11 @@ namespace sat {
s |= m_antecedents.find(js.get_literal2().var());
break;
case justification::CLAUSE: {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
for (unsigned i = 0; i < c.size(); ++i) {
if (c[i] != lit) {
if (check_domain(lit, ~c[i]) && all_found) {
s |= m_antecedents.find(c[i].var());
clause & c = get_clause(js);
for (literal l : c) {
if (l != lit) {
if (check_domain(lit, ~l) && all_found) {
s |= m_antecedents.find(l.var());
}
else {
all_found = false;

15
src/sat/sat_solver.h
View file

@ -366,6 +366,7 @@ namespace sat {
model_converter const & get_model_converter() const { return m_mc; }
void set_model(model const& mdl);
char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
bool check_clauses(model const& m) const;
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
lbool cube(bool_var_vector const& vars, literal_vector& lits);
@ -442,6 +443,20 @@ namespace sat {
justification const & jst = m_justification[l0.var()];
return !jst.is_clause() || m_cls_allocator.get_clause(jst.get_clause_offset()) != &c;
}
clause& get_clause(watch_list::iterator it) const {
SASSERT(it->get_kind() == watched::CLAUSE);
return get_clause(it->get_clause_offset());
}
clause& get_clause(justification const& j) const {
SASSERT(j.is_clause());
return get_clause(j.get_clause_offset());
}
clause& get_clause(clause_offset cls_off) const {
return *(m_cls_allocator.get_clause(cls_off));
}
// -----------------------
//

8
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -180,7 +180,13 @@ public:
m_internalized_converted = false;
init_reason_unknown();
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
try {
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
}
catch (z3_exception& ex) {
IF_VERBOSE(10, verbose_stream() << "exception: " << ex.msg() << "\n";);
r = l_undef;
}
if (r == l_undef && m_solver.get_config().m_dimacs_display) {
for (auto const& kv : m_map) {
std::cout << "c " << kv.m_value << " " << mk_pp(kv.m_key, m) << "\n";

1
src/sat/tactic/goal2sat.cpp
View file

@ -896,6 +896,7 @@ struct sat2goal::imp {
public:
sat_model_converter(ast_manager & m, sat::solver const & s):m_var2expr(m) {
m_mc.copy(s.get_model_converter());
m_mc.set_solver(&s);
m_fmc = alloc(filter_model_converter, m);
}