mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt

Browse source
This commit is contained in:
Miguel Neves 2017-10-12 15:34:56 -07:00
commit bdce957ac8
83 changed files with 2596 additions and 1126 deletions
Download patch file Download diff file Expand all files Collapse all files

569
src/sat/ba_solver.cpp
View file

File diff suppressed because it is too large Load diff

18
src/sat/ba_solver.h
View file

@ -79,7 +79,7 @@ namespace sat {
void set_size(unsigned sz) { SASSERT(sz <= m_size); m_size = sz; }
void update_literal(literal l) { m_lit = l; }
bool was_removed() const { return m_removed; }
void remove() { m_removed = true; }
void set_removed() { m_removed = true; }
void nullify_literal() { m_lit = null_literal; }
unsigned glue() const { return m_glue; }
void set_glue(unsigned g) { m_glue = g; }
@ -199,7 +199,7 @@ namespace sat {
svector<uint64> m_coeffs;
uint64 m_k;
void reset(uint64 k) { m_lits.reset(); m_coeffs.reset(); m_k = k; }
void push(literal l, unsigned c) { m_lits.push_back(l); m_coeffs.push_back(c); }
void push(literal l, uint64 c) { m_lits.push_back(l); m_coeffs.push_back(c); }
};
solver* m_solver;
@ -286,7 +286,7 @@ namespace sat {
void cleanup_constraints();
void cleanup_constraints(ptr_vector<constraint>& cs, bool learned);
void ensure_external(constraint const& c);
void remove_constraint(constraint& c);
void remove_constraint(constraint& c, char const* reason);
// constraints
constraint& index2constraint(size_t idx) const { return *reinterpret_cast<constraint*>(idx); }
@ -304,6 +304,7 @@ namespace sat {
void nullify_tracking_literal(constraint& c);
void set_conflict(constraint& c, literal lit);
void assign(constraint& c, literal lit);
bool assigned_above(literal above, literal below);
void get_antecedents(literal l, constraint const& c, literal_vector & r);
bool validate_conflict(constraint const& c) const;
bool validate_unit_propagation(constraint const& c, literal alit) const;
@ -368,7 +369,7 @@ namespace sat {
inline watch_list const& get_wlist(literal l) const { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }
inline void assign(literal l, justification j) { if (m_lookahead) m_lookahead->assign(l); else m_solver->assign(l, j); }
inline void set_conflict(justification j, literal l) { if (m_lookahead) m_lookahead->set_conflict(); else m_solver->set_conflict(j, l); }
inline config const& get_config() const { return m_solver->get_config(); }
inline config const& get_config() const { return m_lookahead ? m_lookahead->get_config() : m_solver->get_config(); }
inline void drat_add(literal_vector const& c, svector<drat::premise> const& premises) { m_solver->m_drat.add(c, premises); }
@ -402,8 +403,13 @@ namespace sat {
bool validate_watch_literals() const;
bool validate_watch_literal(literal lit) const;
bool validate_watched_constraint(constraint const& c) const;
bool validate_watch(pb const& p) const;
bool validate_watch(pb const& p, literal alit) const;
bool is_watching(literal lit, constraint const& c) const;
literal translate_to_sat(solver& s, u_map<bool_var>& translation, ineq const& pb);
literal translate_to_sat(solver& s, u_map<bool_var>& translation, ineq& a, ineq& b);
literal translate_to_sat(solver& s, u_map<bool_var>& translation, literal lit);
ineq negate(ineq const& a) const;
void push_lit(literal_vector& lits, literal lit);
ineq m_A, m_B, m_C;
void active2pb(ineq& p);
@ -422,6 +428,7 @@ namespace sat {
constraint* add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
constraint* add_xor(literal l, literal_vector const& lits, bool learned);
void copy_core(ba_solver* result);
public:
ba_solver();
virtual ~ba_solver();
@ -447,6 +454,7 @@ namespace sat {
virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const;
virtual void collect_statistics(statistics& st) const;
virtual extension* copy(solver* s);
virtual extension* copy(lookahead* s);
virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes);
virtual void pop_reinit();
virtual void gc();

3
src/sat/sat_drat.cpp
View file

@ -272,7 +272,8 @@ namespace sat {
void drat::verify(unsigned n, literal const* c) {
if (!is_drup(n, c) && !is_drat(n, c)) {
std::cout << "Verification failed\n";
display(std::cout);
UNREACHABLE();
//display(std::cout);
TRACE("sat",
tout << literal_vector(n, c) << "\n";
display(tout);

59
src/sat/sat_elim_eqs.cpp
View file

@ -96,17 +96,18 @@ namespace sat {
if (!c.frozen())
m_solver.detach_clause(c);
// apply substitution
for (i = 0; i < sz; i++) {
SASSERT(!m_solver.was_eliminated(c[i].var()));
for (i = 0; i < sz; i++) {
c[i] = norm(roots, c[i]);
VERIFY(!m_solver.was_eliminated(c[i].var()));
}
std::sort(c.begin(), c.end());
for (literal l : c) VERIFY(l == norm(roots, l));
TRACE("sats", tout << "after normalization/sorting: " << c << "\n"; tout.flush(););
DEBUG_CODE({
for (unsigned i = 0; i < sz; i++) {
CTRACE("sats", c[i] != norm(roots, c[i]), tout << c[i] << " " << norm(roots, c[i]) << "\n"; tout.flush(););
SASSERT(c[i] == norm(roots, c[i]));
} });
for (literal l : c) {
CTRACE("sat", l != norm(roots, l), tout << l << " " << norm(roots, l) << "\n"; tout.flush(););
SASSERT(l == norm(roots, l));
} });
// remove duplicates, and check if it is a tautology
literal l_prev = null_literal;
unsigned j = 0;
@ -122,13 +123,11 @@ namespace sat {
break; // clause was satisfied
if (val == l_false)
continue; // skip
if (i != j) {
std::swap(c[i], c[j]);
}
c[j] = l;
j++;
}
if (i < sz) {
// clause is a tautology or was simplified
// clause is a tautology or was simplified to true
m_solver.del_clause(c);
continue;
}
@ -164,10 +163,7 @@ namespace sat {
else
c.update_approx();
DEBUG_CODE({
for (unsigned i = 0; i < j; i++) {
SASSERT(c[i] == norm(roots, c[i]));
} });
DEBUG_CODE(for (literal l : c) VERIFY(l == norm(roots, l)););
*it2 = *it;
it2++;
@ -187,7 +183,6 @@ namespace sat {
literal r = roots[v];
SASSERT(v != r.var());
if (m_solver.is_external(v) && !m_solver.set_root(l, r)) {
std::cout << "skip: " << l << " == " << r << "\n";
// cannot really eliminate v, since we have to notify extension of future assignments
m_solver.mk_bin_clause(~l, r, false);
m_solver.mk_bin_clause(l, ~r, false);
@ -199,29 +194,33 @@ namespace sat {
mc.insert(e, ~l, r);
mc.insert(e, l, ~r);
}
m_solver.flush_roots();
}
m_solver.flush_roots();
}
bool elim_eqs::check_clauses(literal_vector const & roots) const {
clause_vector * vs[2] = { &m_solver.m_clauses, &m_solver.m_learned };
for (unsigned i = 0; i < 2; i++) {
clause_vector & cs = *(vs[i]);
clause_vector::iterator it = cs.begin();
clause_vector::iterator end = cs.end();
for (; it != end; ++it) {
clause & c = *(*it);
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++) {
CTRACE("elim_eqs_bug", m_solver.was_eliminated(c[i].var()), tout << "lit: " << c[i] << " " << norm(roots, c[i]) << "\n";
tout << c << "\n";);
SASSERT(!m_solver.was_eliminated(c[i].var()));
}
bool elim_eqs::check_clause(clause const& c, literal_vector const& roots) const {
for (literal l : c) {
CTRACE("elim_eqs_bug", m_solver.was_eliminated(l.var()), tout << "lit: " << l << " " << norm(roots, l) << "\n";
tout << c << "\n";);
if (m_solver.was_eliminated(l.var())) {
IF_VERBOSE(0, verbose_stream() << c << " contains eliminated literal " << l << " " << norm(roots, l) << "\n";);
UNREACHABLE();
}
}
return true;
}
bool elim_eqs::check_clauses(literal_vector const & roots) const {
for (clause * cp : m_solver.m_clauses)
if (!check_clause(*cp, roots))
return false;
for (clause * cp : m_solver.m_learned)
if (!check_clause(*cp, roots))
return false;
return true;
}
void elim_eqs::operator()(literal_vector const & roots, bool_var_vector const & to_elim) {
cleanup_bin_watches(roots);
TRACE("elim_eqs", tout << "after bin cleanup\n"; m_solver.display(tout););

1
src/sat/sat_elim_eqs.h
View file

@ -30,6 +30,7 @@ namespace sat {
void cleanup_clauses(literal_vector const & roots, clause_vector & cs);
void cleanup_bin_watches(literal_vector const & roots);
bool check_clauses(literal_vector const & roots) const;
bool check_clause(clause const& c, literal_vector const& roots) const;
public:
elim_eqs(solver & s);
void operator()(literal_vector const & roots, bool_var_vector const & to_elim);

1
src/sat/sat_extension.h
View file

@ -71,6 +71,7 @@ namespace sat {
virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0;
virtual void collect_statistics(statistics& st) const = 0;
virtual extension* copy(solver* s) = 0;
virtual extension* copy(lookahead* s) = 0;
virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) = 0;
virtual void gc() = 0;
virtual void pop_reinit() = 0;

236
src/sat/sat_lookahead.cpp
View file

@ -92,7 +92,7 @@ namespace sat {
// TRACE("sat", display(tout << "Delete " << to_literal(idx) << "\n"););
literal_vector & lits = m_binary[idx];
SASSERT(!lits.empty());
literal l = lits.back();
literal l = lits.back();
lits.pop_back();
SASSERT(!m_binary[(~l).index()].empty());
IF_VERBOSE(0, if (m_binary[(~l).index()].back() != ~to_literal(idx)) verbose_stream() << "pop bad literal: " << idx << " " << (~l).index() << "\n";);
@ -112,7 +112,6 @@ namespace sat {
}
}
void lookahead::inc_bstamp() {
++m_bstamp_id;
if (m_bstamp_id == 0) {
@ -120,6 +119,7 @@ namespace sat {
m_bstamp.fill(0);
}
}
void lookahead::inc_istamp() {
++m_istamp_id;
if (m_istamp_id == 0) {
@ -204,13 +204,13 @@ namespace sat {
void lookahead::pre_select() {
IF_VERBOSE(10, verbose_stream() << "freevars: " << m_freevars.size() << "\n";);
m_lookahead.reset();
for (bool_var x : m_freevars) { // tree lookahead may leave some literals fixed in lower truth levels
for (bool_var x : m_freevars) { // tree lookahead leaves literals fixed in lower truth levels
literal l(x, false);
set_undef(l);
set_undef(~l);
}
//printf("m_freevars.size() = %d\n", m_freevars.size());
if (select(scope_lvl())) {
get_scc();
if (inconsistent()) return;
@ -276,6 +276,7 @@ namespace sat {
sift_down(0, i);
}
}
SASSERT(validate_heap_sort());
}
void lookahead::heapify() {
@ -299,6 +300,17 @@ namespace sat {
if (i > j) m_candidates[i] = c;
}
/**
* \brief validate that the result of heap sort sorts the candidates
* in descending order of their rating.
*/
bool lookahead::validate_heap_sort() {
for (unsigned i = 0; i + 1 < m_candidates.size(); ++i)
if (m_candidates[i].m_rating < m_candidates[i + 1].m_rating)
return false;
return true;
}
double lookahead::init_candidates(unsigned level, bool newbies) {
m_candidates.reset();
double sum = 0;
@ -328,25 +340,14 @@ namespace sat {
}
bool lookahead::is_unsat() const {
bool all_false = true;
bool first = true;
// check if there is a clause whose literals are false.
// every clause is terminated by a null-literal.
for (unsigned l_idx : m_nary_literals) {
literal l = to_literal(l_idx);
if (first) {
// skip the first entry, the length indicator.
first = false;
}
else if (l == null_literal) {
// when reaching the end of a clause check if all entries are false
if (all_false) return true;
all_false = true;
first = true;
}
else {
for (nary* n : m_nary_clauses) {
bool all_false = true;
for (literal l : *n) {
all_false &= is_false(l);
}
if (all_false) return true;
}
// check if there is a ternary whose literals are false.
for (unsigned idx = 0; idx < m_ternary.size(); ++idx) {
@ -382,24 +383,14 @@ namespace sat {
}
}
}
bool no_true = true;
bool first = true;
// check if there is a clause whose literals are false.
// every clause is terminated by a null-literal.
for (unsigned l_idx : m_nary_literals) {
literal l = to_literal(l_idx);
if (first) {
// skip the first entry, the length indicator.
first = false;
}
else if (l == null_literal) {
if (no_true) return false;
no_true = true;
first = true;
}
else {
for (nary * n : m_nary_clauses) {
bool no_true = true;
for (literal l : *n) {
no_true &= !is_true(l);
}
if (no_true) return false;
}
// check if there is a ternary whose literals are false.
for (unsigned idx = 0; idx < m_ternary.size(); ++idx) {
@ -476,17 +467,15 @@ namespace sat {
sum += (literal_occs(b.m_u) + literal_occs(b.m_v)) / 8.0;
}
sz = m_nary_count[(~l).index()];
for (unsigned idx : m_nary[(~l).index()]) {
for (nary * n : m_nary[(~l).index()]) {
if (sz-- == 0) break;
literal lit;
unsigned j = idx;
double to_add = 0;
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
for (literal lit : *n) {
if (!is_fixed(lit) && lit != ~l) {
to_add += literal_occs(lit);
}
}
unsigned len = m_nary_literals[idx];
unsigned len = n->size();
sum += pow(0.5, len) * to_add / len;
}
return sum;
@ -507,9 +496,9 @@ namespace sat {
}
sum += 0.25 * m_ternary_count[(~l).index()];
unsigned sz = m_nary_count[(~l).index()];
for (unsigned cls_idx : m_nary[(~l).index()]) {
for (nary * n : m_nary[(~l).index()]) {
if (sz-- == 0) break;
sum += pow(0.5, m_nary_literals[cls_idx]);
sum += pow(0.5, n->size());
}
return sum;
}
@ -616,18 +605,18 @@ namespace sat {
void lookahead::init_arcs(literal l) {
literal_vector lits;
literal_vector const& succ = m_binary[l.index()];
for (unsigned i = 0; i < succ.size(); ++i) {
literal u = succ[i];
for (literal u : succ) {
SASSERT(u != l);
// l => u
if (u.index() > l.index() && is_stamped(u)) {
add_arc(~l, ~u);
add_arc( u, l);
}
}
for (auto w : m_watches[l.index()]) {
if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) {
if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) {
for (literal u : lits) {
if (u.index() > l.index() && is_stamped(u)) {
if (u.index() > (~l).index() && is_stamped(u)) {
add_arc(~l, ~u);
add_arc( u, l);
}
@ -901,8 +890,8 @@ namespace sat {
m_ternary.push_back(svector<binary>());
m_ternary_count.push_back(0);
m_ternary_count.push_back(0);
m_nary.push_back(unsigned_vector());
m_nary.push_back(unsigned_vector());
m_nary.push_back(ptr_vector<nary>());
m_nary.push_back(ptr_vector<nary>());
m_nary_count.push_back(0);
m_nary_count.push_back(0);
m_bstamp.push_back(0);
@ -958,14 +947,8 @@ namespace sat {
}
}
// copy externals:
for (unsigned idx = 0; idx < m_s.m_watches.size(); ++idx) {
watch_list const& wl = m_s.m_watches[idx];
for (watched const& w : wl) {
if (w.is_ext_constraint()) {
m_watches[idx].push_back(w);
}
}
if (m_s.m_ext) {
m_ext = m_s.m_ext->copy(this);
}
propagate();
m_qhead = m_trail.size();
@ -1328,17 +1311,14 @@ namespace sat {
// new n-ary clause managment
void lookahead::add_clause(clause const& c) {
unsigned sz = c.size();
SASSERT(sz > 3);
unsigned idx = m_nary_literals.size();
m_nary_literals.push_back(sz);
SASSERT(c.size() > 3);
void * mem = m_allocator.allocate(nary::get_obj_size(c.size()));
nary * n = new (mem) nary(c.size(), c.begin());
m_nary_clauses.push_back(n);
for (literal l : c) {
m_nary_literals.push_back(l.index());
m_nary[l.index()].push_back(n);
m_nary_count[l.index()]++;
m_nary[l.index()].push_back(idx);
SASSERT(m_nary_count[l.index()] == m_nary[l.index()].size());
}
m_nary_literals.push_back(null_literal.index());
}
@ -1347,18 +1327,17 @@ namespace sat {
unsigned sz = m_nary_count[(~l).index()];
literal lit;
SASSERT(m_search_mode == lookahead_mode::searching);
for (unsigned idx : m_nary[(~l).index()]) {
for (nary * n : m_nary[(~l).index()]) {
if (sz-- == 0) break;
unsigned len = --m_nary_literals[idx];
unsigned len = n->dec_size();
if (m_inconsistent) continue;
if (len <= 1) continue; // already processed
// find the two unassigned literals, if any
if (len == 2) {
literal l1 = null_literal;
literal l2 = null_literal;
unsigned j = idx;
bool found_true = false;
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
for (literal lit : *n) {
if (!is_fixed(lit)) {
if (l1 == null_literal) {
l1 = lit;
@ -1370,7 +1349,7 @@ namespace sat {
}
}
else if (is_true(lit)) {
// can't swap with idx. std::swap(m_nary_literals[j], m_nary_literals[idx]);
n->set_head(lit);
found_true = true;
break;
}
@ -1398,9 +1377,9 @@ namespace sat {
}
// clauses where l is positive:
sz = m_nary_count[l.index()];
for (unsigned idx : m_nary[l.index()]) {
for (nary* n : m_nary[l.index()]) {
if (sz-- == 0) break;
remove_clause_at(l, idx);
remove_clause_at(l, *n);
}
}
@ -1411,14 +1390,17 @@ namespace sat {
SASSERT(m_search_mode == lookahead_mode::lookahead1 ||
m_search_mode == lookahead_mode::lookahead2);
for (unsigned idx : m_nary[(~l).index()]) {
for (nary* n : m_nary[(~l).index()]) {
if (sz-- == 0) break;
if (is_true(n->get_head())) {
continue;
}
literal l1 = null_literal;
literal l2 = null_literal;
unsigned j = idx;
bool found_true = false;
bool skip_clause = false;
unsigned nonfixed = 0;
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
for (literal lit : *n) {
if (!is_fixed(lit)) {
++nonfixed;
if (l1 == null_literal) {
@ -1427,14 +1409,19 @@ namespace sat {
else if (l2 == null_literal) {
l2 = lit;
}
else if (m_search_mode == lookahead_mode::lookahead2) {
skip_clause = true;
break;
}
}
else if (is_true(lit)) {
found_true = true;
n->set_head(lit);
skip_clause = true;
break;
}
}
if (found_true) {
// skip, the clause will be removed when propagating on 'lit'
if (skip_clause) {
// skip, the clause
}
else if (l1 == null_literal) {
set_conflict();
@ -1443,20 +1430,16 @@ namespace sat {
else if (l2 == null_literal) {
propagated(l1);
}
else if (m_search_mode == lookahead_mode::lookahead2) {
continue;
}
else {
SASSERT(nonfixed >= 2);
SASSERT(m_search_mode == lookahead_mode::lookahead1);
switch (m_config.m_reward_type) {
case heule_schur_reward: {
j = idx;
double to_add = 0;
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
for (literal lit : *n) {
if (!is_fixed(lit)) {
to_add += literal_occs(lit);
}
}
}
m_lookahead_reward += pow(0.5, nonfixed) * to_add / nonfixed;
break;
@ -1464,9 +1447,6 @@ namespace sat {
case heule_unit_reward:
m_lookahead_reward += pow(0.5, nonfixed);
break;
case march_cu_reward:
m_lookahead_reward += 3.3 * pow(0.5, nonfixed - 2);
break;
case ternary_reward:
if (nonfixed == 2) {
m_lookahead_reward += (*m_heur)[l1.index()] * (*m_heur)[l2.index()];
@ -1482,23 +1462,20 @@ namespace sat {
}
}
void lookahead::remove_clause_at(literal l, unsigned clause_idx) {
unsigned j = clause_idx;
literal lit;
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
void lookahead::remove_clause_at(literal l, nary& n) {
for (literal lit : n) {
if (lit != l) {
remove_clause(lit, clause_idx);
remove_clause(lit, n);
}
}
}
void lookahead::remove_clause(literal l, unsigned clause_idx) {
unsigned_vector& pclauses = m_nary[l.index()];
void lookahead::remove_clause(literal l, nary& n) {
ptr_vector<nary>& pclauses = m_nary[l.index()];
unsigned sz = m_nary_count[l.index()]--;
for (unsigned i = sz; i > 0; ) {
--i;
if (clause_idx == pclauses[i]) {
if (&n == pclauses[i]) {
std::swap(pclauses[i], pclauses[sz-1]);
return;
}
@ -1508,33 +1485,29 @@ namespace sat {
void lookahead::restore_clauses(literal l) {
SASSERT(m_search_mode == lookahead_mode::searching);
// increase the length of clauses where l is negative
unsigned sz = m_nary_count[(~l).index()];
for (unsigned idx : m_nary[(~l).index()]) {
for (nary* n : m_nary[(~l).index()]) {
if (sz-- == 0) break;
++m_nary_literals[idx];
n->inc_size();
}
// add idx back to clause list where l is positive
// add them back in the same order as they were inserted
// in this way we can check that the clauses are the same.
sz = m_nary_count[l.index()];
unsigned_vector const& pclauses = m_nary[l.index()];
for (unsigned i = sz; i > 0; ) {
--i;
unsigned j = pclauses[i];
literal lit;
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
ptr_vector<nary>& pclauses = m_nary[l.index()];
for (unsigned i = sz; i-- > 0; ) {
for (literal lit : *pclauses[i]) {
if (lit != l) {
SASSERT(m_nary[lit.index()][m_nary_count[lit.index()]] == pclauses[i]);
m_nary_count[lit.index()]++;
}
}
}
}
}
void lookahead::propagate_clauses(literal l) {
SASSERT(is_true(l));
propagate_ternary(l);
switch (m_search_mode) {
case lookahead_mode::searching:
@ -1545,9 +1518,7 @@ namespace sat {
break;
}
propagate_external(l);
}
}
void lookahead::update_binary_clause_reward(literal l1, literal l2) {
SASSERT(!is_false(l1));
@ -1610,7 +1581,6 @@ namespace sat {
// FIXME: counts occurences of ~l; misleading
double lookahead::literal_occs(literal l) {
double result = m_binary[l.index()].size();
//unsigned_vector const& nclauses = m_nary[(~l).index()];
result += literal_big_occs(l);
return result;
}
@ -1651,12 +1621,18 @@ namespace sat {
TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n"););
}
#define CHECK_FAILED_LITERAL 0
void lookahead::compute_lookahead_reward() {
TRACE("sat", display_lookahead(tout); );
m_delta_decrease = pow(m_config.m_delta_rho, 1.0 / (double)m_lookahead.size());
unsigned base = 2;
bool change = true;
literal last_changed = null_literal;
#if CHECK_FAILED_LITERAL
unsigned_vector assigns;
literal_vector assigns_lits;
#endif
while (change && !inconsistent()) {
change = false;
for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) {
@ -1677,7 +1653,6 @@ namespace sat {
reset_lookahead_reward(lit);
unsigned num_units = push_lookahead1(lit, level);
update_lookahead_reward(lit, level);
unsigned old_trail_sz = m_trail.size();
unsigned dl_lvl = level;
num_units += do_double(lit, dl_lvl);
if (dl_lvl > level) {
@ -1688,6 +1663,10 @@ namespace sat {
if (unsat) {
TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";);
lookahead_backtrack();
#if CHECK_FAILED_LITERAL
assigns.push_back(m_trail.size());
assigns_lits.push_back(~lit);
#endif
assign(~lit);
propagate();
change = true;
@ -1701,6 +1680,12 @@ namespace sat {
base += 2 * m_lookahead.size();
}
lookahead_backtrack();
#if CHECK_FAILED_LITERAL
for (unsigned i = 0; i < assigns.size(); ++i) {
std::cout << "check trail: " << m_trail[assigns[i]] << " " << assigns_lits[i] << "\n";
VERIFY(m_trail[assigns[i]] == assigns_lits[i]);
}
#endif
TRACE("sat", display_lookahead(tout); );
}
@ -1754,7 +1739,7 @@ namespace sat {
return false;
#if 0
// no propagations are allowed to reduce clauses.
for (clause * cp : m_full_watches[l.index()]) {
for (nary * cp : m_nary[(~l).index()]) {
clause& c = *cp;
unsigned sz = c.size();
bool found = false;
@ -1993,8 +1978,10 @@ namespace sat {
lbool lookahead::cube() {
literal_vector lits;
bool_var_vector vars;
for (bool_var v : m_freevars) vars.push_back(v);
while (true) {
lbool result = cube(lits);
lbool result = cube(vars, lits);
if (lits.empty() || result != l_undef) {
return l_undef;
}
@ -2003,8 +1990,13 @@ namespace sat {
return l_undef;
}
lbool lookahead::cube(literal_vector& lits) {
lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits) {
scoped_ext _scoped_ext(*this);
lits.reset();
m_select_lookahead_vars.reset();
for (auto v : vars) {
m_select_lookahead_vars.insert(v);
}
bool is_first = m_cube_state.m_first;
if (is_first) {
init_search();
@ -2111,20 +2103,9 @@ namespace sat {
}
}
for (unsigned l_idx : m_nary_literals) {
literal l = to_literal(l_idx);
if (first) {
// the first entry is a length indicator of non-false literals.
out << l_idx << ": ";
first = false;
}
else if (l == null_literal) {
first = true;
out << "\n";
}
else {
out << l << " ";
}
for (nary * n : m_nary_clauses) {
for (literal l : *n) out << l << " ";
out << "\n";
}
return out;
@ -2219,6 +2200,7 @@ namespace sat {
\brief simplify set of clauses by extracting units from a lookahead at base level.
*/
void lookahead::simplify() {
scoped_ext _scoped_ext(*this);
SASSERT(m_prefix == 0);
SASSERT(m_watches.empty());
m_search_mode = lookahead_mode::searching;

61
src/sat/sat_lookahead.h
View file

@ -20,6 +20,7 @@ Notes:
#ifndef _SAT_LOOKAHEAD_H_
#define _SAT_LOOKAHEAD_H_
// #define OLD_NARY 0
#include "sat_elim_eqs.h"
@ -89,8 +90,7 @@ namespace sat {
m_min_cutoff = 30;
m_preselect = false;
m_level_cand = 600;
//m_delta_rho = (double)0.25;
m_delta_rho = (double)0.5;
m_delta_rho = (double)0.25;
m_dl_max_iterations = 2;
m_tc1_limit = 10000000;
m_reward_type = ternary_reward;
@ -132,6 +132,36 @@ namespace sat {
literal m_u, m_v;
};
class nary {
unsigned m_size; // number of non-false literals
size_t m_obj_size; // object size (counting all literals)
literal m_head; // head literal
literal m_literals[0]; // list of literals, put any true literal in head.
size_t num_lits() const {
return (m_obj_size - sizeof(nary)) / sizeof(literal);
}
public:
static size_t get_obj_size(unsigned sz) { return sizeof(nary) + sz * sizeof(literal); }
size_t obj_size() const { return m_obj_size; }
nary(unsigned sz, literal const* lits):
m_size(sz),
m_obj_size(get_obj_size(sz)) {
for (unsigned i = 0; i < sz; ++i) m_literals[i] = lits[i];
m_head = lits[0];
}
unsigned size() const { return m_size; }
unsigned dec_size() { SASSERT(m_size > 0); return --m_size; }
void inc_size() { SASSERT(m_size < num_lits()); ++m_size; }
literal get_head() const { return m_head; }
void set_head(literal l) { m_head = l; }
literal operator[](unsigned i) { SASSERT(i < num_lits()); return m_literals[i]; }
literal const* begin() const { return m_literals; }
literal const* end() const { return m_literals + num_lits(); }
// swap the true literal to the head.
// void swap(unsigned i, unsigned j) { SASSERT(i < num_lits() && j < num_lits()); std::swap(m_literals[i], m_literals[j]); }
};
struct cube_state {
bool m_first;
svector<bool> m_is_decision;
@ -164,10 +194,10 @@ namespace sat {
vector<svector<binary>> m_ternary; // lit |-> vector of ternary clauses
unsigned_vector m_ternary_count; // lit |-> current number of active ternary clauses for lit
vector<unsigned_vector> m_nary; // lit |-> vector of clause_id
unsigned_vector m_nary_count; // lit |-> number of valid clause_id in m_clauses2[lit]
unsigned_vector m_nary_literals; // the actual literals, clauses start at offset clause_id,
// the first entry is the current length, clauses are separated by a null_literal
small_object_allocator m_allocator;
vector<ptr_vector<nary>> m_nary; // lit |-> vector of nary clauses
ptr_vector<nary> m_nary_clauses; // vector of all nary clauses
unsigned_vector m_nary_count; // lit |-> number of valid clause_id in m_nary[lit]
unsigned m_num_tc1;
unsigned_vector m_num_tc1_lim;
@ -196,6 +226,7 @@ namespace sat {
stats m_stats;
model m_model;
cube_state m_cube_state;
scoped_ptr<extension> m_ext;
// ---------------------------------------
// truth values
@ -293,10 +324,10 @@ namespace sat {
double get_rating(bool_var v) const { return m_rating[v]; }
double get_rating(literal l) const { return get_rating(l.var()); }
bool select(unsigned level);
//void sift_up(unsigned j);
void heap_sort();
void heapify();
void heapify();
void sift_down(unsigned j, unsigned sz);
bool validate_heap_sort();
double init_candidates(unsigned level, bool newbies);
std::ostream& display_candidates(std::ostream& out) const;
bool is_unsat() const;
@ -419,15 +450,15 @@ namespace sat {
void propagate_clauses_searching(literal l);
void propagate_clauses_lookahead(literal l);
void restore_clauses(literal l);
void remove_clause(literal l, unsigned clause_idx);
void remove_clause_at(literal l, unsigned clause_idx);
void remove_clause(literal l, nary& n);
void remove_clause_at(literal l, nary& n);
// ------------------------------------
// initialization
void init_var(bool_var v);
void init();
void copy_clauses(clause_vector const& clauses, bool learned);
nary * copy_clause(clause const& c);
// ------------------------------------
// search
@ -510,6 +541,9 @@ namespace sat {
~lookahead() {
m_s.rlimit().pop_child();
for (nary* n : m_nary_clauses) {
m_allocator.deallocate(n->obj_size(), n);
}
}
@ -524,9 +558,10 @@ namespace sat {
If cut-depth != 0, then it is used to control the depth of cuts.
Otherwise, cut-fraction gives an adaptive threshold for creating cuts.
*/
lbool cube();
lbool cube(literal_vector& lits);
lbool cube(bool_var_vector const& vars, literal_vector& lits);
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
/**
@ -557,6 +592,8 @@ namespace sat {
double literal_occs(literal l);
double literal_big_occs(literal l);
sat::config const& get_config() const { return m_s.get_config(); }
};
}

29
src/sat/sat_solver.cpp
View file

@ -162,6 +162,7 @@ namespace sat {
m_user_scope_literals.append(src.m_user_scope_literals);
m_mc = src.m_mc;
m_stats.m_units = init_trail_size();
}
// -----------------------
@ -837,11 +838,11 @@ namespace sat {
return lh.select_lookahead(assumptions, vars);
}
lbool solver::cube(literal_vector& lits) {
lbool solver::cube(bool_var_vector const& vars, literal_vector& lits) {
if (!m_cuber) {
m_cuber = alloc(lookahead, *this);
}
lbool result = m_cuber->cube(lits);
lbool result = m_cuber->cube(vars, lits);
if (result == l_false) {
dealloc(m_cuber);
m_cuber = nullptr;
@ -858,6 +859,7 @@ namespace sat {
lbool solver::check(unsigned num_lits, literal const* lits) {
init_reason_unknown();
pop_to_base_level();
m_stats.m_units = init_trail_size();
IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
SASSERT(at_base_lvl());
if (m_config.m_dimacs_display) {
@ -1468,11 +1470,14 @@ namespace sat {
lh.simplify();
lh.collect_statistics(m_aux_stats);
}
#if 0
// Buggy
{
lookahead lh(*this);
lh.scc();
lh.collect_statistics(m_aux_stats);
}
#endif
}
@ -2823,6 +2828,7 @@ namespace sat {
pop(num_scopes);
exchange_par();
reinit_assumptions();
m_stats.m_units = init_trail_size();
}
void solver::pop(unsigned num_scopes) {
@ -3048,7 +3054,6 @@ namespace sat {
m_probing.updt_params(p);
m_scc.updt_params(p);
m_rand.set_seed(m_config.m_random_seed);
m_step_size = m_config.m_step_size_init;
}
@ -4032,25 +4037,11 @@ namespace sat {
st.update("minimized lits", m_minimized_lits);
st.update("dyn subsumption resolution", m_dyn_sub_res);
st.update("blocked correction sets", m_blocked_corr_sets);
st.update("units", m_units);
}
void stats::reset() {
m_mk_var = 0;
m_mk_bin_clause = 0;
m_mk_ter_clause = 0;
m_mk_clause = 0;
m_conflict = 0;
m_propagate = 0;
m_bin_propagate = 0;
m_ter_propagate = 0;
m_decision = 0;
m_restart = 0;
m_gc_clause = 0;
m_del_clause = 0;
m_minimized_lits = 0;
m_dyn_sub_res = 0;
m_non_learned_generation = 0;
m_blocked_corr_sets = 0;
memset(this, 0, sizeof(*this));
}
void mk_stat::display(std::ostream & out) const {

3
src/sat/sat_solver.h
View file

@ -67,6 +67,7 @@ namespace sat {
unsigned m_dyn_sub_res;
unsigned m_non_learned_generation;
unsigned m_blocked_corr_sets;
unsigned m_units;
stats() { reset(); }
void reset();
void collect_statistics(statistics & st) const;
@ -364,7 +365,7 @@ namespace sat {
char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
lbool cube(literal_vector& lits);
lbool cube(bool_var_vector const& vars, literal_vector& lits);
protected:
unsigned m_conflicts_since_init;

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

@ -353,8 +353,12 @@ public:
m_internalized = true;
}
convert_internalized();
sat::bool_var_vector vars;
for (auto& kv : m_map) {
vars.push_back(kv.m_value);
}
sat::literal_vector lits;
lbool result = m_solver.cube(lits);
lbool result = m_solver.cube(vars, lits);
if (result == l_false || lits.empty()) {
return expr_ref(m.mk_false(), m);
}

8
src/sat/sat_watched.h
View file

@ -109,10 +109,10 @@ namespace sat {
bool operator!=(watched const & w) const { return !operator==(w); }
};
COMPILE_TIME_ASSERT(0 <= watched::BINARY && watched::BINARY <= 3);
COMPILE_TIME_ASSERT(0 <= watched::TERNARY && watched::TERNARY <= 3);
COMPILE_TIME_ASSERT(0 <= watched::CLAUSE && watched::CLAUSE <= 3);
COMPILE_TIME_ASSERT(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3);
static_assert(0 <= watched::BINARY && watched::BINARY <= 3, "");
static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, "");
static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, "");
static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, "");
struct watched_lt {
bool operator()(watched const & w1, watched const & w2) const {

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

@ -120,7 +120,7 @@ struct goal2sat::imp {
sat::bool_var mk_true() {
if (m_true == sat::null_bool_var) {
// create fake variable to represent true;
m_true = m_solver.mk_var();
m_true = m_solver.mk_var(false);
mk_clause(sat::literal(m_true, false)); // v is true
}
return m_true;