From 0833a9ee14d8a3ec665b28918084c30392552992 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 27 Sep 2017 07:15:06 -0700
Subject: [PATCH] n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/sat_lookahead.cpp | 41 +++++++++++++++++++++++++++++++++++----
src/sat/sat_lookahead.h | 2 +-
2 files changed, 38 insertions(+), 5 deletions(-)
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 66ad2afd7..ce205cc2f 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -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()];
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 78ec590b5..a3777ea44 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -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