mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt
This commit is contained in:
Nikolaj Bjorner
commit
41ac4ff308
2 changed files with 143 additions and 99 deletions
|
|
@ -317,7 +317,7 @@ namespace sat {
|
|||
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_clause_literals) {
|
||||
for (unsigned l_idx : m_nary_literals) {
|
||||
literal l = to_literal(l_idx);
|
||||
if (first) {
|
||||
// skip the first entry, the length indicator.
|
||||
|
|
@ -385,7 +385,7 @@ namespace sat {
|
|||
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_clause_literals) {
|
||||
for (unsigned l_idx : m_nary_literals) {
|
||||
literal l = to_literal(l_idx);
|
||||
if (first) {
|
||||
// skip the first entry, the length indicator.
|
||||
|
|
@ -484,18 +484,18 @@ namespace sat {
|
|||
if (sz-- == 0) break;
|
||||
sum += (literal_occs(b.m_u) + literal_occs(b.m_v)) / 8.0;
|
||||
}
|
||||
sz = m_clause_count[(~l).index()];
|
||||
for (unsigned idx : m_clauses[(~l).index()]) {
|
||||
sz = m_nary_count[(~l).index()];
|
||||
for (unsigned idx : m_nary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
literal lit;
|
||||
unsigned j = idx;
|
||||
double to_add = 0;
|
||||
while ((lit = to_literal(m_clause_literals[++j])) != null_literal) {
|
||||
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
|
||||
if (!is_fixed(lit) && lit != ~l) {
|
||||
to_add += literal_occs(lit);
|
||||
}
|
||||
}
|
||||
unsigned len = m_clause_literals[idx];
|
||||
unsigned len = m_nary_literals[idx];
|
||||
sum += pow(0.5, len) * to_add / len;
|
||||
}
|
||||
#else
|
||||
|
|
@ -551,10 +551,10 @@ namespace sat {
|
|||
}
|
||||
#ifdef NEW_CLAUSE
|
||||
sum += 0.25 * m_ternary_count[(~l).index()];
|
||||
unsigned sz = m_clause_count[(~l).index()];
|
||||
for (unsigned cls_idx : m_clauses[(~l).index()]) {
|
||||
unsigned sz = m_nary_count[(~l).index()];
|
||||
for (unsigned cls_idx : m_nary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
sum += pow(0.5, m_clause_literals[cls_idx]);
|
||||
sum += pow(0.5, m_nary_literals[cls_idx]);
|
||||
}
|
||||
#else
|
||||
watch_list& wlist = m_watches[l.index()];
|
||||
|
|
@ -973,10 +973,11 @@ namespace sat {
|
|||
}
|
||||
|
||||
|
||||
#ifndef NEW_CLAUSE
|
||||
|
||||
// ------------------------------------
|
||||
// clause management
|
||||
|
||||
#ifndef NEW_CLAUSE
|
||||
void lookahead::attach_clause(clause& c) {
|
||||
if (c.size() == 3) {
|
||||
attach_ternary(c[0], c[1], c[2]);
|
||||
|
|
@ -1036,6 +1037,15 @@ namespace sat {
|
|||
#ifndef NEW_CLAUSE
|
||||
m_full_watches.push_back(clause_vector());
|
||||
m_full_watches.push_back(clause_vector());
|
||||
#else
|
||||
m_ternary.push_back(svector<binary()>);
|
||||
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_count.push_back(0);
|
||||
m_nary_count.push_back(0);
|
||||
#endif
|
||||
m_bstamp.push_back(0);
|
||||
m_bstamp.push_back(0);
|
||||
|
|
@ -1076,8 +1086,8 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
copy_clauses(m_s.m_clauses);
|
||||
copy_clauses(m_s.m_learned);
|
||||
copy_clauses(m_s.m_clauses, false);
|
||||
copy_clauses(m_s.m_learned, true);
|
||||
|
||||
// copy units
|
||||
unsigned trail_sz = m_s.init_trail_size();
|
||||
|
|
@ -1103,7 +1113,7 @@ namespace sat {
|
|||
TRACE("sat", m_s.display(tout); display(tout););
|
||||
}
|
||||
|
||||
void lookahead::copy_clauses(clause_vector const& clauses) {
|
||||
void lookahead::copy_clauses(clause_vector const& clauses, bool learned) {
|
||||
// copy clauses
|
||||
#ifdef NEW_CLAUSE
|
||||
for (clause* cp : clauses) {
|
||||
|
|
@ -1121,7 +1131,7 @@ namespace sat {
|
|||
case 1: assign(c[0]); break;
|
||||
case 2: add_binary(c[0],c[1]); break;
|
||||
case 3: add_ternary(c[0],c[1],c[2]); break;
|
||||
default: add_clause(c); break;
|
||||
default: if (!learned) add_clause(c); break;
|
||||
}
|
||||
if (m_s.m_config.m_drat) m_drat.add(c, false);
|
||||
}
|
||||
|
|
@ -1184,8 +1194,6 @@ namespace sat {
|
|||
TRACE("sat", tout << "inserting free var v" << l.var() << "\n";);
|
||||
m_freevars.insert(l.var());
|
||||
}
|
||||
m_trail.shrink(old_sz); // reset assignment.
|
||||
m_trail_lim.pop_back();
|
||||
|
||||
m_num_tc1 = m_num_tc1_lim.back();
|
||||
m_num_tc1_lim.pop_back();
|
||||
|
|
@ -1213,6 +1221,9 @@ namespace sat {
|
|||
}
|
||||
#endif
|
||||
|
||||
m_trail.shrink(old_sz); // reset assignment.
|
||||
m_trail_lim.pop_back();
|
||||
|
||||
// remove local binary clauses
|
||||
old_sz = m_binary_trail_lim.back();
|
||||
for (unsigned i = m_binary_trail.size(); i > old_sz; ) {
|
||||
|
|
@ -1358,15 +1369,13 @@ namespace sat {
|
|||
|
||||
void lookahead::propagate_ternary(literal l) {
|
||||
unsigned sz = m_ternary_count[(~l).index()];
|
||||
svector<binary> const& negs = m_ternary[(~l).index()];
|
||||
|
||||
switch (m_search_mode) {
|
||||
case lookahead_mode::searching: {
|
||||
|
||||
// ternary clauses where l is negative become binary
|
||||
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
binary const& b = negs[i];
|
||||
for (binary const& b : m_ternary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
// this could create a conflict from propagation, but we complete the transaction.
|
||||
literal l1 = b.m_u;
|
||||
literal l2 = b.m_v;
|
||||
|
|
@ -1375,18 +1384,17 @@ namespace sat {
|
|||
try_add_binary(l1, l2);
|
||||
break;
|
||||
default:
|
||||
// propagated or tautology.
|
||||
// propagated or tautology or conflict
|
||||
break;
|
||||
}
|
||||
remove_ternary(l1, l2, l);
|
||||
remove_ternary(l2, l, l1);
|
||||
}
|
||||
sz = m_ternary_count[l.index()];
|
||||
svector<binary> const& poss = m_ternary[l.index()];
|
||||
|
||||
|
||||
sz = m_ternary_count[l.index()];
|
||||
// ternary clauses where l is positive are tautologies
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
binary const& b = poss[i];
|
||||
for (binary const& b : m_ternary[l.index()]) {
|
||||
if (sz-- == 0) break;
|
||||
remove_ternary(b.m_u, b.m_v, l);
|
||||
remove_ternary(b.m_v, l, b.m_u);
|
||||
}
|
||||
|
|
@ -1394,8 +1402,8 @@ namespace sat {
|
|||
}
|
||||
case lookahead_mode::lookahead1:
|
||||
// this could create a conflict from propagation, but we complete the loop.
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
binary const& b = negs[i];
|
||||
for (binary const& b : m_ternary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
literal l1 = b.m_u;
|
||||
literal l2 = b.m_v;
|
||||
switch (propagate_ternary(l1, l2)) {
|
||||
|
|
@ -1409,8 +1417,8 @@ namespace sat {
|
|||
break;
|
||||
case lookahead2:
|
||||
// this could create a conflict from propagation, but we complete the loop.
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
binary const& b = negs[i];
|
||||
for (binary const& b : m_ternary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
propagate_ternary(b.m_u, b.m_v);
|
||||
}
|
||||
break;
|
||||
|
|
@ -1435,7 +1443,7 @@ namespace sat {
|
|||
void lookahead::restore_ternary(literal l) {
|
||||
unsigned sz = m_ternary_count[(~l).index()];
|
||||
for (binary const& b : m_ternary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
if (sz-- == 0) break;
|
||||
m_ternary_count[b.m_u.index()]++;
|
||||
m_ternary_count[b.m_v.index()]++;
|
||||
}
|
||||
|
|
@ -1459,7 +1467,7 @@ namespace sat {
|
|||
lookahead_literal_occs_fun literal_occs_fn(*this);
|
||||
m_lookahead_reward += m_s.m_ext->get_reward(l, it->get_ext_constraint_idx(), literal_occs_fn);
|
||||
}
|
||||
if (m_inconsistent) {
|
||||
if (inconsistent()) {
|
||||
if (!keep) ++it;
|
||||
}
|
||||
else if (keep) {
|
||||
|
|
@ -1479,26 +1487,59 @@ namespace sat {
|
|||
void lookahead::add_clause(clause const& c) {
|
||||
unsigned sz = c.size();
|
||||
SASSERT(sz > 3);
|
||||
unsigned idx = m_clause_literals.size();
|
||||
m_clause_literals.push_back(sz);
|
||||
unsigned idx = m_nary_literals.size();
|
||||
m_nary_literals.push_back(sz);
|
||||
for (literal l : c) {
|
||||
m_clause_literals.push_back(l.index());
|
||||
m_clause_count[l.index()]++;
|
||||
m_clauses[l.index()].push_back(idx);
|
||||
m_nary_literals.push_back(l.index());
|
||||
m_nary_count[l.index()]++;
|
||||
m_nary[l.index()].push_back(idx);
|
||||
SASSERT(m_nary_count[l.index()] == m_nary[l.index()].size());
|
||||
}
|
||||
m_clause_literals.push_back(null_literal.index());
|
||||
m_nary_literals.push_back(null_literal.index());
|
||||
}
|
||||
|
||||
#if 0
|
||||
// split large clauses into smaller ones to avoid overhead during propagation.
|
||||
|
||||
void lookahead::add_clause(unsigned sz, literal const * lits) {
|
||||
if (sz > 6) {
|
||||
bool_var v = m_s.mk_var(false);
|
||||
++m_num_vars;
|
||||
init_var(v);
|
||||
literal lit(v, false);
|
||||
unsigned mid = sz / 2;
|
||||
literal_vector lits1(mid, lits);
|
||||
lits1.push_back(lit);
|
||||
add_clause(lits1.size(), lits1.c_ptr());
|
||||
lit.neg();
|
||||
literal_vector lits2(sz - mid, lits + mid);
|
||||
lits2.push_back(lit);
|
||||
add_clause(lits2.size(), lits2.c_ptr());
|
||||
}
|
||||
else {
|
||||
unsigned idx = m_nary_literals.size();
|
||||
m_nary_literals.push_back(sz);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
literal l = lits[i];
|
||||
m_nary_literals.push_back(l.index());
|
||||
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());
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
void lookahead::propagate_clauses_searching(literal l) {
|
||||
// clauses where l is negative
|
||||
unsigned_vector const& nclauses = m_clauses[(~l).index()];
|
||||
unsigned sz = m_clause_count[(~l).index()];
|
||||
unsigned sz = m_nary_count[(~l).index()];
|
||||
literal lit;
|
||||
SASSERT(m_search_mode == lookahead_mode::searching);
|
||||
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
unsigned idx = nclauses[i];
|
||||
unsigned len = --m_clause_literals[idx];
|
||||
for (unsigned idx : m_nary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
unsigned len = --m_nary_literals[idx];
|
||||
if (len <= 1) continue; // already processed
|
||||
// find the two unassigned literals, if any
|
||||
if (len == 2) {
|
||||
|
|
@ -1506,7 +1547,7 @@ namespace sat {
|
|||
literal l2 = null_literal;
|
||||
unsigned j = idx;
|
||||
bool found_true = false;
|
||||
while ((lit = to_literal(m_clause_literals[++j])) != null_literal) {
|
||||
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
|
||||
if (!is_fixed(lit)) {
|
||||
if (l1 == null_literal) {
|
||||
l1 = lit;
|
||||
|
|
@ -1518,7 +1559,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
else if (is_true(lit)) {
|
||||
// can't swap with idx. std::swap(m_clause_literals[j], m_clause_literals[idx]);
|
||||
// can't swap with idx. std::swap(m_nary_literals[j], m_nary_literals[idx]);
|
||||
found_true = true;
|
||||
break;
|
||||
}
|
||||
|
|
@ -1529,7 +1570,7 @@ namespace sat {
|
|||
else if (l1 == null_literal) {
|
||||
set_conflict();
|
||||
for (++i; i < sz; ++i) {
|
||||
--m_clause_literals[nclauses[i]];
|
||||
--m_nary_literals[nclauses[i]];
|
||||
}
|
||||
}
|
||||
else if (l2 == null_literal) {
|
||||
|
|
@ -1548,29 +1589,28 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
// clauses where l is positive:
|
||||
unsigned_vector const& pclauses = m_clauses[l.index()];
|
||||
sz = m_clause_count[l.index()];
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
remove_clause_at(l, pclauses[i]);
|
||||
sz = m_nary_count[l.index()];
|
||||
for (unsigned idx : m_nary[l.index())) {
|
||||
if (sz-- == 0) break;
|
||||
remove_clause_at(l, idx);
|
||||
}
|
||||
}
|
||||
|
||||
void lookahead::propagate_clauses_lookahead(literal l) {
|
||||
// clauses where l is negative
|
||||
unsigned_vector const& nclauses = m_clauses[(~l).index()];
|
||||
unsigned sz = m_clause_count[(~l).index()];
|
||||
unsigned sz = m_nary_count[(~l).index()];
|
||||
literal lit;
|
||||
SASSERT(m_search_mode == lookahead_mode::lookahead1 ||
|
||||
m_search_mode == lookahead_mode::lookahead2);
|
||||
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
unsigned idx = nclauses[i];
|
||||
|
||||
for (unsigned idx : m_nary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
literal l1 = null_literal;
|
||||
literal l2 = null_literal;
|
||||
unsigned j = idx;
|
||||
bool found_true = false;
|
||||
unsigned nonfixed = 0;
|
||||
while ((lit = to_literal(m_clause_literals[++j])) != null_literal) {
|
||||
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
|
||||
if (!is_fixed(lit)) {
|
||||
++nonfixed;
|
||||
if (l1 == null_literal) {
|
||||
|
|
@ -1599,12 +1639,13 @@ namespace sat {
|
|||
continue;
|
||||
}
|
||||
else {
|
||||
SASSERT (m_search_mode == lookahead_mode::lookahead1);
|
||||
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_clause_literals[++j])) != null_literal) {
|
||||
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
|
||||
if (!is_fixed(lit)) {
|
||||
to_add += literal_occs(lit);
|
||||
}
|
||||
|
|
@ -1634,7 +1675,7 @@ namespace sat {
|
|||
void lookahead::remove_clause_at(literal l, unsigned clause_idx) {
|
||||
unsigned j = clause_idx;
|
||||
literal lit;
|
||||
while ((lit = to_literal(m_clause_literals[++j])) != null_literal) {
|
||||
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
|
||||
if (lit != l) {
|
||||
remove_clause(lit, clause_idx);
|
||||
}
|
||||
|
|
@ -1642,8 +1683,8 @@ namespace sat {
|
|||
}
|
||||
|
||||
void lookahead::remove_clause(literal l, unsigned clause_idx) {
|
||||
unsigned_vector& pclauses = m_clauses[l.index()];
|
||||
unsigned sz = m_clause_count[l.index()]--;
|
||||
unsigned_vector& pclauses = m_nary[l.index()];
|
||||
unsigned sz = m_nary_count[l.index()]--;
|
||||
for (unsigned i = sz; i > 0; ) {
|
||||
--i;
|
||||
if (clause_idx == pclauses[i]) {
|
||||
|
|
@ -1658,22 +1699,25 @@ namespace sat {
|
|||
SASSERT(m_search_mode == lookahead_mode::searching);
|
||||
|
||||
// increase the length of clauses where l is negative
|
||||
unsigned_vector const& nclauses = m_clauses[(~l).index()];
|
||||
unsigned sz = m_clause_count[(~l).index()];
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
++m_clause_literals[nclauses[i]];
|
||||
unsigned sz = m_nary_count[(~l).index()];
|
||||
for (unsigned idx : m_nary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
++m_nary_literals[idx];
|
||||
}
|
||||
|
||||
// add idx back to clause list where l is positive
|
||||
unsigned_vector const& pclauses = m_clauses[l.index()];
|
||||
sz = m_clause_count[l.index()];
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
unsigned idx = pclauses[i];
|
||||
unsigned j = idx;
|
||||
// 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_clause_literals[++j])) != null_literal) {
|
||||
while ((lit = to_literal(m_nary_literals[++j])) != null_literal) {
|
||||
if (lit != l) {
|
||||
m_clause_count[lit.index()]++;
|
||||
SASSERT(m_nary[lit.index()] == pclauses[i]);
|
||||
m_nary_count[lit.index()]++;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1905,8 +1949,8 @@ namespace sat {
|
|||
double lookahead::literal_occs(literal l) {
|
||||
double result = m_binary[l.index()].size();
|
||||
#ifdef NEW_CLAUSE
|
||||
unsigned_vector const& nclauses = m_clauses[(~l).index()];
|
||||
result += m_clause_count[(~l).index()];
|
||||
unsigned_vector const& nclauses = m_nary[(~l).index()];
|
||||
result += m_nary_count[(~l).index()];
|
||||
result += m_ternary_count[(~l).index()];
|
||||
#else
|
||||
for (clause const* c : m_full_watches[l.index()]) {
|
||||
|
|
@ -2117,7 +2161,7 @@ namespace sat {
|
|||
#ifdef NEW_CLAUSE
|
||||
TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()]
|
||||
<< " "
|
||||
<< (!m_binary[l.index()].empty() || m_clause_count[l.index()] != 0) << "\n";);
|
||||
<< (!m_binary[l.index()].empty() || m_nary_count[l.index()] != 0) << "\n";);
|
||||
#endif
|
||||
reset_lookahead_reward();
|
||||
assign(l);
|
||||
|
|
@ -2379,20 +2423,6 @@ namespace sat {
|
|||
std::ostream& lookahead::display_clauses(std::ostream& out) const {
|
||||
#ifdef NEW_CLAUSE
|
||||
bool first = true;
|
||||
for (unsigned l_idx : m_clause_literals) {
|
||||
literal l = to_literal(l_idx);
|
||||
if (first) {
|
||||
// skip the first entry, the length indicator.
|
||||
first = false;
|
||||
}
|
||||
else if (l == null_literal) {
|
||||
first = true;
|
||||
out << "\n";
|
||||
}
|
||||
else {
|
||||
out << l << " ";
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned idx = 0; idx < m_ternary.size(); ++idx) {
|
||||
literal lit = to_literal(idx);
|
||||
|
|
@ -2405,6 +2435,22 @@ 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 << " ";
|
||||
}
|
||||
}
|
||||
|
||||
#else
|
||||
for (unsigned i = 0; i < m_clauses.size(); ++i) {
|
||||
out << *m_clauses[i] << "\n";
|
||||
|
|
@ -2414,8 +2460,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
std::ostream& lookahead::display_values(std::ostream& out) const {
|
||||
for (unsigned i = 0; i < m_trail.size(); ++i) {
|
||||
literal l = m_trail[i];
|
||||
for (literal l : m_trail) {
|
||||
out << l << "\n";
|
||||
}
|
||||
return out;
|
||||
|
|
|
|||
|
|
@ -153,15 +153,14 @@ namespace sat {
|
|||
|
||||
#ifdef NEW_CLAUSE
|
||||
// specialized clause managemet uses ternary clauses and dedicated clause data-structure.
|
||||
// this will replace m_clauses below
|
||||
// this replaces m_clauses below
|
||||
vector<svector<binary>> m_ternary; // lit |-> vector of ternary clauses
|
||||
unsigned_vector m_ternary_count; // lit |-> current number of active ternary clauses for lit
|
||||
unsigned_vector m_ternary_trail_lim; // limit for ternary vectors.
|
||||
unsigned_vector m_ternary_count; // lit |-> current number of active ternary clauses for lit
|
||||
|
||||
vector<unsigned_vector> m_clauses; // lit |-> vector of clause_id
|
||||
unsigned_vector m_clause_count; // lit |-> number of valid clause_id in m_clauses2[lit]
|
||||
unsigned_vector m_clause_literals; // the actual literals, clauses start at offset clause_id,
|
||||
// the first entry is the current length, clauses are separated by a null_literal
|
||||
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
|
||||
|
||||
|
||||
#endif
|
||||
|
|
@ -436,7 +435,7 @@ namespace sat {
|
|||
|
||||
void init_var(bool_var v);
|
||||
void init();
|
||||
void copy_clauses(clause_vector const& clauses);
|
||||
void copy_clauses(clause_vector const& clauses, bool learned);
|
||||
|
||||
// ------------------------------------
|
||||
// search
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue