From: Dejan Jovanović 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 ) --- 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& 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() {