From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 4 Mar 2010 18:45:15 +0000 (+0000)
Subject: Adding phase-caching to minisat.
X-Git-Tag: cvc5-1.0.0~9205
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=45b7c76aba6ac71726fb2bf46c45ad7ce6bc8c99;p=cvc5.git

Adding phase-caching to minisat.
(A Lightweight Component Caching Scheme for Satisfiability Solvers <http://www.springerlink.com/content/y802q03263x84159/>)
---

diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index 771d79f62..dd5e1e667 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -394,9 +394,10 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
 void Solver::uncheckedEnqueue(Lit p, Clause* from)
 {
     assert(value(p) == l_Undef);
-    assigns [var(p)] = toInt(lbool(!sign(p)));  // <<== abstract but not uttermost effecient
-    level   [var(p)] = decisionLevel();
-    reason  [var(p)] = from;
+    assigns  [var(p)] = toInt(lbool(!sign(p)));  // <<== abstract but not uttermost effecient
+    level    [var(p)] = decisionLevel();
+    reason   [var(p)] = from;
+    polarity [var(p)] = sign(p);
     trail.push(p);
 }
 
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 1cd5d0bfe..2468990f2 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -109,6 +109,8 @@ class SatSolver {
       d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
       // Do not delete the satisfied clauses, just the learnt ones
       d_minisat->remove_satisfied = false;
+      // Make minisat reuse the literal values
+      d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
     }
 
     ~SatSolver() {