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

n/a

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-27 07:15:06 -07:00
parent 3a832e5b24
commit 0833a9ee14
2 changed files with 38 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/sat/sat_lookahead.cpp
View file

@ -1086,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();
@ -1113,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) {
@ -1130,7 +1130,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);
}
@ -1497,6 +1497,39 @@ namespace sat {
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 sz = m_nary_count[(~l).index()];

2
src/sat/sat_lookahead.h
View file

@ -435,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