summaryrefslogtreecommitdiff
path: root/src/prop/minisat
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/minisat')
-rw-r--r--src/prop/minisat/core/Solver.cc313
-rw-r--r--src/prop/minisat/core/Solver.h6
-rw-r--r--src/prop/minisat/core/SolverTypes.h64
-rw-r--r--src/prop/minisat/minisat.cpp2
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc98
-rw-r--r--src/prop/minisat/simp/SimpSolver.h2
6 files changed, 294 insertions, 191 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index f56f6a447..311224a03 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -30,6 +30,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "options/prop_options.h"
#include "options/smt_options.h"
#include "proof/clause_id.h"
+#include "proof/cnf_proof.h"
#include "proof/proof_manager.h"
#include "proof/sat_proof.h"
#include "proof/sat_proof_implementation.h"
@@ -217,7 +218,10 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy,
propagation_budget(-1),
asynch_interrupt(false)
{
- PROOF(ProofManager::currentPM()->initSatProof(this);)
+ if (options::unsatCores())
+ {
+ ProofManager::currentPM()->initSatProof(this);
+ }
// Create the constant variables
varTrue = newVar(true, false, false);
@@ -227,11 +231,11 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy,
uncheckedEnqueue(mkLit(varTrue, false));
uncheckedEnqueue(mkLit(varFalse, true));
// FIXME: these should be axioms I believe
- PROOF
- (
- ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
- ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
- );
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
+ ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
+ }
}
@@ -390,15 +394,20 @@ CRef Solver::reason(Var x) {
// FIXME: at some point will need more information about where this explanation
// came from (ie. the theory/sharing)
Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl;
- PROOF(ClauseId id = ProofManager::getSatProof()->registerClause(
- real_reason, THEORY_LEMMA);
- ProofManager::getCnfProof()->registerConvertedClause(id, true);
- // explainPropagation() pushes the explanation on the assertion stack
- // in CnfProof, so we need to pop it here. This is important because
- // reason() may be called indirectly while adding a clause, which can
- // lead to a wrong assertion being associated with the clause being
- // added (see issue #2137).
- ProofManager::getCnfProof()->popCurrentAssertion(););
+ if (options::unsatCores())
+ {
+ ClauseId id = ProofManager::getSatProof()->registerClause(real_reason,
+ THEORY_LEMMA);
+ // map id to assertion, which may be required if looking for
+ // lemmas in unsat core
+ ProofManager::getCnfProof()->registerConvertedClause(id);
+ // explainPropagation() pushes the explanation on the assertion stack
+ // in CnfProof, so we need to pop it here. This is important because
+ // reason() may be called indirectly while adding a clause, which can
+ // lead to a wrong assertion being associated with the clause being
+ // added (see issue #2137).
+ ProofManager::getCnfProof()->popCurrentAssertion();
+ }
vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
clauses_removable.push(real_reason);
attachClause(real_reason);
@@ -441,9 +450,13 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
}
// If a literal is false at 0 level (both sat and user level) we also ignore it
if (value(ps[i]) == l_False) {
- if (!PROOF_ON() && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) {
+ if (!options::unsatCores() && level(var(ps[i])) == 0
+ && user_level(var(ps[i])) == 0)
+ {
continue;
- } else {
+ }
+ else
+ {
// If we decide to keep it, we count it into the false literals
falseLiteralsCount ++;
}
@@ -467,34 +480,46 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
lemmas.push();
ps.copyTo(lemmas.last());
lemmas_removable.push(removable);
- PROOF(
- // Store the expression being converted to CNF until
- // the clause is actually created
- Node assertion = ProofManager::getCnfProof()->getCurrentAssertion();
- Node def = ProofManager::getCnfProof()->getCurrentDefinition();
- lemmas_cnf_assertion.push_back(std::make_pair(assertion, def));
- id = ClauseIdUndef;
- );
- // does it have to always be a lemma?
- // PROOF(id = ProofManager::getSatProof()->registerUnitClause(ps[0], THEORY_LEMMA););
- // PROOF(id = ProofManager::getSatProof()->registerTheoryLemma(ps););
- // Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
- // lemmas_proof_id.push(proof_id);
+ if (options::unsatCores())
+ {
+ // Store the expression being converted to CNF until
+ // the clause is actually created
+ lemmas_cnf_assertion.push_back(
+ ProofManager::getCnfProof()->getCurrentAssertion());
+ id = ClauseIdUndef;
+ }
} else {
assert(decisionLevel() == 0);
// If all false, we're in conflict
if (ps.size() == falseLiteralsCount) {
- if(PROOF_ON()) {
+ if (options::unsatCores())
+ {
// Take care of false units here; otherwise, we need to
// construct the clause below to give to the proof manager
// as the final conflict.
if(falseLiteralsCount == 1) {
- PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); )
- PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); )
+ if (options::unsatCores())
+ {
+ ClauseKind ck =
+ ProofManager::getCnfProof()->getCurrentAssertionKind()
+ ? INPUT
+ : THEORY_LEMMA;
+ id = ProofManager::getSatProof()->storeUnitConflict(ps[0], ck);
+ // map id to assertion, which may be required if looking for
+ // lemmas in unsat core
+ if (ck == THEORY_LEMMA)
+ {
+ ProofManager::getCnfProof()->registerConvertedClause(id);
+ }
+ ProofManager::getSatProof()->finalizeProof(
+ CVC4::Minisat::CRef_Lazy);
+ }
return ok = false;
}
- } else {
+ }
+ else
+ {
return ok = false;
}
}
@@ -509,14 +534,23 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
cr = ca.alloc(clauseLevel, ps, false);
clauses_persistent.push(cr);
- attachClause(cr);
-
- if(PROOF_ON()) {
- PROOF(
- id = ProofManager::getSatProof()->registerClause(cr, INPUT);
- )
- if(ps.size() == falseLiteralsCount) {
- PROOF( ProofManager::getSatProof()->finalizeProof(cr); )
+ attachClause(cr);
+
+ if (options::unsatCores())
+ {
+ ClauseKind ck = ProofManager::getCnfProof()->getCurrentAssertionKind()
+ ? INPUT
+ : THEORY_LEMMA;
+ id = ProofManager::getSatProof()->registerClause(cr, ck);
+ // map id to assertion, which may be required if looking for
+ // lemmas in unsat core
+ if (ck == THEORY_LEMMA)
+ {
+ ProofManager::getCnfProof()->registerConvertedClause(id);
+ }
+ if (ps.size() == falseLiteralsCount)
+ {
+ ProofManager::getSatProof()->finalizeProof(cr);
return ok = false;
}
}
@@ -527,15 +561,25 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
if(assigns[var(ps[0])] == l_Undef) {
assert(assigns[var(ps[0])] != l_False);
uncheckedEnqueue(ps[0], cr);
- Debug("cores") << "i'm registering a unit clause, input" << std::endl;
- PROOF(
- if(ps.size() == 1) {
- id = ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT);
- }
- );
+ Debug("cores") << "i'm registering a unit clause, maybe input"
+ << std::endl;
+ if (options::unsatCores() && ps.size() == 1)
+ {
+ ClauseKind ck =
+ ProofManager::getCnfProof()->getCurrentAssertionKind()
+ ? INPUT
+ : THEORY_LEMMA;
+ id = ProofManager::getSatProof()->registerUnitClause(ps[0], ck);
+ // map id to assertion, which may be required if looking for
+ // lemmas in unsat core
+ if (ck == THEORY_LEMMA)
+ {
+ ProofManager::getCnfProof()->registerConvertedClause(id);
+ }
+ }
CRef confl = propagate(CHECK_WITHOUT_THEORY);
if(! (ok = (confl == CRef_Undef)) ) {
- if (PROOF_ON())
+ if (options::unsatCores())
{
if (ca[confl].size() == 1)
{
@@ -552,7 +596,10 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
}
return ok;
} else {
- PROOF(id = ClauseIdUndef;);
+ if (options::unsatCores())
+ {
+ id = ClauseIdUndef;
+ }
return ok;
}
}
@@ -575,7 +622,10 @@ void Solver::attachClause(CRef cr) {
void Solver::detachClause(CRef cr, bool strict) {
const Clause& c = ca[cr];
- PROOF( ProofManager::getSatProof()->markDeleted(cr); );
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->markDeleted(cr);
+ }
Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
assert(c.size() > 1);
@@ -826,7 +876,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
int max_resolution_level = 0; // Maximal level of the resolved clauses
- PROOF( ProofManager::getSatProof()->startResChain(confl); )
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->startResChain(confl);
+ }
do{
assert(confl != CRef_Undef); // (otherwise should be UIP)
@@ -867,9 +920,9 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
}
// FIXME: can we do it lazily if we actually need the proof?
- if (level(var(q)) == 0)
+ if (options::unsatCores() && level(var(q)) == 0)
{
- PROOF(ProofManager::getSatProof()->resolveOutUnit(q);)
+ ProofManager::getSatProof()->resolveOutUnit(q);
}
}
}
@@ -881,8 +934,9 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
seen[var(p)] = 0;
pathC--;
- if ( pathC > 0 && confl != CRef_Undef ) {
- PROOF( ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); )
+ if (options::unsatCores() && pathC > 0 && confl != CRef_Undef)
+ {
+ ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
}
}while (pathC > 0);
@@ -905,7 +959,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
// Literal is not redundant
out_learnt[j++] = out_learnt[i];
} else {
- PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); )
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
+ }
// Literal is redundant, to be safe, mark the level as current assertion level
// TODO: maybe optimize
max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i])));
@@ -1169,7 +1226,10 @@ void Solver::propagateTheory() {
addClause(explanation, true, id);
// explainPropagation() pushes the explanation on the assertion
// stack in CnfProof, so we need to pop it here.
- PROOF(ProofManager::getCnfProof()->popCurrentAssertion();)
+ if (options::unsatCores())
+ {
+ ProofManager::getCnfProof()->popCurrentAssertion();
+ }
}
}
}
@@ -1310,9 +1370,10 @@ void Solver::removeSatisfied(vec<CRef>& cs)
for (i = j = 0; i < cs.size(); i++){
Clause& c = ca[cs[i]];
if (satisfied(c)) {
- if (locked(c)) {
+ if (options::unsatCores() && locked(c))
+ {
// store a resolution of the literal c propagated
- PROOF( ProofManager::getSatProof()->storeUnitResolution(c[0]); )
+ ProofManager::getSatProof()->storeUnitResolution(c[0]);
}
removeClause(cs[i]);
}
@@ -1412,8 +1473,11 @@ lbool Solver::search(int nof_conflicts)
conflicts++; conflictC++;
if (decisionLevel() == 0) {
- PROOF( ProofManager::getSatProof()->finalizeProof(confl); )
- return l_False;
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->finalizeProof(confl);
+ }
+ return l_False;
}
// Analyze the conflict
@@ -1425,8 +1489,10 @@ lbool Solver::search(int nof_conflicts)
if (learnt_clause.size() == 1) {
uncheckedEnqueue(learnt_clause[0]);
- PROOF( ProofManager::getSatProof()->endResChain(learnt_clause[0]); )
-
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->endResChain(learnt_clause[0]);
+ }
} else {
CRef cr =
ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
@@ -1436,15 +1502,12 @@ lbool Solver::search(int nof_conflicts)
attachClause(cr);
claBumpActivity(ca[cr]);
uncheckedEnqueue(learnt_clause[0], cr);
- PROOF(ClauseId id =
- ProofManager::getSatProof()->registerClause(cr, LEARNT);
- PSTATS(std::unordered_set<int> cl_levels;
- for (int i = 0; i < learnt_clause.size(); ++i) {
- cl_levels.insert(level(var(learnt_clause[i])));
- } ProofManager::getSatProof()
- ->storeClauseGlue(id, cl_levels.size());)
- ProofManager::getSatProof()
- ->endResChain(id););
+ if (options::unsatCores())
+ {
+ ClauseId id =
+ ProofManager::getSatProof()->registerClause(cr, LEARNT);
+ ProofManager::getSatProof()->endResChain(id);
+ }
}
varDecayActivity();
@@ -1469,25 +1532,33 @@ lbool Solver::search(int nof_conflicts)
}
} else {
-
- // If this was a final check, we are satisfiable
- if (check_type == CHECK_FINAL) {
- bool decisionEngineDone = d_proxy->isDecisionEngineDone();
- // Unless a lemma has added more stuff to the queues
- if (!decisionEngineDone &&
- (!order_heap.empty() || qhead < trail.size()) ) {
- check_type = CHECK_WITH_THEORY;
- continue;
- } else if (recheck) {
- // There some additional stuff added, so we go for another full-check
- continue;
- } else {
- // Yes, we're truly satisfiable
- return l_True;
- }
- } else if (check_type == CHECK_FINAL_FAKE) {
+ // If this was a final check, we are satisfiable
+ if (check_type == CHECK_FINAL)
+ {
+ bool decisionEngineDone = d_proxy->isDecisionEngineDone();
+ // Unless a lemma has added more stuff to the queues
+ if (!decisionEngineDone
+ && (!order_heap.empty() || qhead < trail.size()))
+ {
check_type = CHECK_WITH_THEORY;
+ continue;
+ }
+ else if (recheck)
+ {
+ // There some additional stuff added, so we go for another
+ // full-check
+ continue;
}
+ else
+ {
+ // Yes, we're truly satisfiable
+ return l_True;
+ }
+ }
+ else if (check_type == CHECK_FINAL_FAKE)
+ {
+ check_type = CHECK_WITH_THEORY;
+ }
if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
|| !withinBudget(ResourceManager::Resource::SatConflictStep))
@@ -1744,7 +1815,10 @@ void Solver::relocAll(ClauseAllocator& to)
// printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
vec<Watcher>& ws = watches[p];
for (int j = 0; j < ws.size(); j++)
- ca.reloc(ws[j].cref, to, NULLPROOF(ProofManager::getSatProof()));
+ ca.reloc(ws[j].cref,
+ to,
+ CVC4::options::unsatCores() ? ProofManager::getSatProof()
+ : nullptr);
}
// All reasons:
@@ -1753,22 +1827,31 @@ void Solver::relocAll(ClauseAllocator& to)
Var v = var(trail[i]);
if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
- ca.reloc(
- vardata[v].d_reason, to, NULLPROOF(ProofManager::getSatProof()));
+ ca.reloc(vardata[v].d_reason,
+ to,
+ CVC4::options::unsatCores() ? ProofManager::getSatProof()
+ : nullptr);
}
// All learnt:
//
for (int i = 0; i < clauses_removable.size(); i++)
ca.reloc(
- clauses_removable[i], to, NULLPROOF(ProofManager::getSatProof()));
+ clauses_removable[i],
+ to,
+ CVC4::options::unsatCores() ? ProofManager::getSatProof() : nullptr);
// All original:
//
for (int i = 0; i < clauses_persistent.size(); i++)
ca.reloc(
- clauses_persistent[i], to, NULLPROOF(ProofManager::getSatProof()));
+ clauses_persistent[i],
+ to,
+ CVC4::options::unsatCores() ? ProofManager::getSatProof() : nullptr);
- PROOF(ProofManager::getSatProof()->finishUpdateCRef();)
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->finishUpdateCRef();
+ }
}
@@ -1874,7 +1957,7 @@ CRef Solver::updateLemmas() {
// If it's an empty lemma, we have a conflict at zero level
if (lemma.size() == 0) {
- Assert(!PROOF_ON());
+ Assert(!options::unsatCores());
conflict = CRef_Lazy;
backtrackLevel = 0;
Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
@@ -1904,7 +1987,8 @@ CRef Solver::updateLemmas() {
// Last index in the trail
int backtrack_index = trail.size();
- PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size()););
+ Assert(!options::unsatCores()
+ || lemmas.size() == (int)lemmas_cnf_assertion.size());
// Attach all the clauses and enqueue all the propagations
for (int j = 0; j < lemmas.size(); ++j)
@@ -1928,15 +2012,16 @@ CRef Solver::updateLemmas() {
}
lemma_ref = ca.alloc(clauseLevel, lemma, removable);
- PROOF(TNode cnf_assertion = lemmas_cnf_assertion[j].first;
- TNode cnf_def = lemmas_cnf_assertion[j].second;
-
- Debug("pf::sat")
- << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
- ClauseId id = ProofManager::getSatProof()->registerClause(
- lemma_ref, THEORY_LEMMA);
- ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
- ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def););
+ if (options::unsatCores())
+ {
+ TNode cnf_assertion = lemmas_cnf_assertion[j];
+
+ Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)"
+ << std::endl;
+ ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref,
+ THEORY_LEMMA);
+ ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
+ }
if (removable) {
clauses_removable.push(lemma_ref);
} else {
@@ -1948,17 +2033,15 @@ CRef Solver::updateLemmas() {
// If the lemma is propagating enqueue its literal (or set the conflict)
if (conflict == CRef_Undef && value(lemma[0]) != l_True) {
if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) {
- if (PROOF_ON() && lemma.size() == 1)
+ if (options::unsatCores() && lemma.size() == 1)
{
- Node cnf_assertion = lemmas_cnf_assertion[j].first;
- Node cnf_def = lemmas_cnf_assertion[j].second;
+ Node cnf_assertion = lemmas_cnf_assertion[j];
Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) "
<< cnf_assertion << value(lemma[0]) << std::endl;
ClauseId id = ProofManager::getSatProof()->registerUnitClause(
lemma[0], THEORY_LEMMA);
ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
- ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
}
if (value(lemma[0]) == l_False) {
@@ -1969,7 +2052,10 @@ CRef Solver::updateLemmas() {
} else {
Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
conflict = CRef_Lazy;
- PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); );
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
+ }
}
} else {
Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
@@ -1979,7 +2065,8 @@ CRef Solver::updateLemmas() {
}
}
- PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size()););
+ Assert(!options::unsatCores()
+ || lemmas.size() == (int)lemmas_cnf_assertion.size());
// Clear the lemmas
lemmas.clear();
lemmas_cnf_assertion.clear();
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 508947456..a5f3664e8 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -63,7 +63,7 @@ public:
typedef Var TVar;
typedef Lit TLit;
- typedef Clause TClause;
+ typedef Clause TClause;
typedef CRef TCRef;
typedef vec<Lit> TLitVec;
@@ -98,7 +98,7 @@ public:
vec<bool> lemmas_removable;
/** Nodes being converted to CNF */
- std::vector<std::pair<CVC4::Node, CVC4::Node> > lemmas_cnf_assertion;
+ std::vector<CVC4::Node> lemmas_cnf_assertion;
/** Do a another check if FULL_EFFORT was the last one */
bool recheck;
@@ -203,7 +203,7 @@ public:
lbool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions.
bool okay () const; // FALSE means solver is in a conflicting state
- void toDimacs ();
+ void toDimacs();
void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format.
void toDimacs (const char *file, const vec<Lit>& assumps);
void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max);
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index bbd6e17a2..b30d97aee 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -73,9 +73,14 @@ inline bool sign (Lit p) { return p.x & 1; }
inline int var (Lit p) { return p.x >> 1; }
// Mapping Literals to and from compact integers suitable for array indexing:
-inline int toInt (Var v) { return v; }
-inline int toInt (Lit p) { return p.x; }
-inline Lit toLit (int i) { Lit p; p.x = i; return p; }
+inline int toInt(Var v) { return v; }
+inline int toInt(Lit p) { return p.x; }
+inline Lit toLit(int i)
+{
+ Lit p;
+ p.x = i;
+ return p;
+}
//const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants.
//const Lit lit_Error = mkLit(var_Undef, true ); // }
@@ -83,20 +88,19 @@ inline Lit toLit (int i) { Lit p; p.x = i; return p; }
const Lit lit_Undef = { -2 }; // }- Useful special constants.
const Lit lit_Error = { -1 }; // }
-
//=================================================================================================
// Lifted booleans:
//
-// NOTE: this implementation is optimized for the case when comparisons between values are mostly
-// between one variable and one constant. Some care had to be taken to make sure that gcc
-// does enough constant propagation to produce sensible code, and this appears to be somewhat
-// fragile unfortunately.
+// NOTE: this implementation is optimized for the case when comparisons between
+// values are mostly
+// between one variable and one constant. Some care had to be taken to
+// make sure that gcc does enough constant propagation to produce sensible
+// code, and this appears to be somewhat fragile unfortunately.
/*
- This is to avoid multiple definitions of l_True, l_False and l_Undef if using multiple copies of
- Minisat.
- IMPORTANT: if we you change the value of the constants so that it is not the same in all copies
- of Minisat this breaks!
+ This is to avoid multiple definitions of l_True, l_False and l_Undef if using
+ multiple copies of Minisat. IMPORTANT: if we you change the value of the
+ constants so that it is not the same in all copies of Minisat this breaks!
*/
#ifndef l_True
@@ -124,10 +128,12 @@ public:
bool operator != (lbool b) const { return !(*this == b); }
lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
- lbool operator && (lbool b) const {
- uint8_t sel = (this->value << 1) | (b.value << 3);
- uint8_t v = (0xF7F755F4 >> sel) & 3;
- return lbool(v); }
+ lbool operator&&(lbool b) const
+ {
+ uint8_t sel = (this->value << 1) | (b.value << 3);
+ uint8_t v = (0xF7F755F4 >> sel) & 3;
+ return lbool(v);
+ }
lbool operator || (lbool b) const {
uint8_t sel = (this->value << 1) | (b.value << 3);
@@ -163,7 +169,7 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::vec<Minisat::Lit>&
}
inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
- std::string val_str;
+ std::string val_str;
if( val == l_False ) {
val_str = "0";
} else if (val == l_True ) {
@@ -208,14 +214,14 @@ class Clause {
header.size = ps.size();
header.level = level;
- for (int i = 0; i < ps.size(); i++)
- data[i].lit = ps[i];
+ for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i];
if (header.has_extra){
if (header.removable)
- data[header.size].act = 0;
- else
- calcAbstraction(); }
+ data[header.size].act = 0;
+ else
+ calcAbstraction();
+ }
}
public:
@@ -321,7 +327,7 @@ class OccLists
public:
OccLists(const Deleted& d) : deleted(d) {}
-
+
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
void resizeTo (const Idx& idx);
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
@@ -394,13 +400,12 @@ class CMap
typedef Map<CRef, T, CRefHash> HashTable;
HashTable map;
-
+
public:
// Size-operations:
void clear () { map.clear(); }
int size () const { return map.elems(); }
-
// Insert/Remove/Test mapping:
void insert (CRef cr, const T& t){ map.insert(cr, t); }
void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
@@ -423,15 +428,14 @@ class CMap
printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
};
-
/*_________________________________________________________________________________________________
|
| subsumes : (other : const Clause&) -> Lit
-|
+|
| Description:
-| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
-| by subsumption resolution.
-|
+| Checks if clause subsumes 'other', and at the same time, if it can be
+used to simplify 'other' | by subsumption resolution.
+|
| Result:
| lit_Error - No subsumption or simplification
| lit_Undef - Clause subsumes 'other'
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index a4d2dce8a..25353e416 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -154,7 +154,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
return ClauseIdUndef;
}
d_minisat->addClause(minisat_clause, removable, clause_id);
- PROOF(Assert(clause_id != ClauseIdError););
+ Assert(!CVC4::options::unsatCores() || clause_id != ClauseIdError);
return clause_id;
}
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index a101a0c2d..0ec8981ca 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "prop/minisat/simp/SimpSolver.h"
#include "options/prop_options.h"
+#include "options/smt_options.h"
#include "proof/clause_id.h"
-#include "proof/proof.h"
#include "prop/minisat/mtl/Sort.h"
#include "prop/minisat/utils/System.h"
@@ -47,25 +47,30 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
//=================================================================================================
// Constructor/Destructor:
-
-SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental) :
- Solver(proxy, context, enableIncremental)
- , grow (opt_grow)
- , clause_lim (opt_clause_lim)
- , subsumption_lim (opt_subsumption_lim)
- , simp_garbage_frac (opt_simp_garbage_frac)
- , use_asymm (opt_use_asymm)
- , use_rcheck (opt_use_rcheck)
- , use_elim (options::minisatUseElim() && !enableIncremental)
- , merges (0)
- , asymm_lits (0)
- , eliminated_vars (0)
- , elimorder (1)
- , use_simplification (!enableIncremental && !PROOF_ON()) // TODO: turn off simplifications if proofs are on initially
- , occurs (ClauseDeleted(ca))
- , elim_heap (ElimLt(n_occ))
- , bwdsub_assigns (0)
- , n_touched (0)
+SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy,
+ CVC4::context::Context* context,
+ bool enableIncremental)
+ : Solver(proxy, context, enableIncremental),
+ grow(opt_grow),
+ clause_lim(opt_clause_lim),
+ subsumption_lim(opt_subsumption_lim),
+ simp_garbage_frac(opt_simp_garbage_frac),
+ use_asymm(opt_use_asymm),
+ use_rcheck(opt_use_rcheck),
+ use_elim(options::minisatUseElim() && !enableIncremental),
+ merges(0),
+ asymm_lits(0),
+ eliminated_vars(0),
+ elimorder(1),
+ use_simplification(
+ !enableIncremental
+ && !options::unsatCores()) // TODO: turn off simplifications if
+ // proofs are on initially
+ ,
+ occurs(ClauseDeleted(ca)),
+ elim_heap(ElimLt(n_occ)),
+ bwdsub_assigns(0),
+ n_touched(0)
{
if(options::minisatUseElim() &&
options::minisatUseElim.wasSetByUser() &&
@@ -117,8 +122,8 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister
lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
{
if (options::minisatDumpDimacs()) {
- toDimacs();
- return l_Undef;
+ toDimacs();
+ return l_Undef;
}
assert(decisionLevel() == 0);
@@ -525,7 +530,7 @@ bool SimpSolver::eliminateVar(Var v)
for (int i = 0; i < cls.size(); i++)
(find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
- // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
+ // Check whether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
// clause must exceed the limit on the maximal clause size (if it is set):
//
int cnt = 0;
@@ -533,9 +538,10 @@ bool SimpSolver::eliminateVar(Var v)
for (int i = 0; i < pos.size(); i++)
for (int j = 0; j < neg.size(); j++)
- if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) &&
- (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
- return true;
+ if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
+ && (++cnt > cls.size() + grow
+ || (clause_lim != -1 && clause_size > clause_lim)))
+ return true;
// Delete and store old clauses:
eliminated[v] = true;
@@ -552,10 +558,9 @@ bool SimpSolver::eliminateVar(Var v)
mkElimClause(elimclauses, ~mkLit(v));
}
- for (int i = 0; i < cls.size(); i++)
- removeClause(cls[i]);
+ for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
- ClauseId id = ClauseIdUndef;
+ ClauseId id = ClauseIdUndef;
// Produce clauses in cross product:
vec<Lit>& resolvent = add_tmp;
for (int i = 0; i < pos.size(); i++)
@@ -569,7 +574,7 @@ bool SimpSolver::eliminateVar(Var v)
// Free occurs list for this variable:
occurs[v].clear(true);
-
+
// Free watchers lists for this variable, if possible:
if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
@@ -589,7 +594,7 @@ bool SimpSolver::substitute(Var v, Lit x)
eliminated[v] = true;
setDecisionVar(v, false);
const vec<CRef>& cls = occurs.lookup(v);
-
+
vec<Lit>& subst_clause = add_tmp;
for (int i = 0; i < cls.size(); i++){
Clause& c = ca[cls[i]];
@@ -641,9 +646,12 @@ bool SimpSolver::eliminate(bool turn_off_elim)
gatherTouchedClauses();
// printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
- if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
- !backwardSubsumptionCheck(true)){
- ok = false; goto cleanup; }
+ if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
+ && !backwardSubsumptionCheck(true))
+ {
+ ok = false;
+ goto cleanup;
+ }
// Empty elim_heap and return immediately on user-interrupt:
if (asynch_interrupt){
@@ -656,7 +664,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
// printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
for (int cnt = 0; !elim_heap.empty(); cnt++){
Var elim = elim_heap.removeMin();
-
+
if (asynch_interrupt) break;
if (isEliminated(elim) || value(elim) != l_Undef) continue;
@@ -706,8 +714,10 @@ bool SimpSolver::eliminate(bool turn_off_elim)
}
if (verbosity >= 1 && elimclauses.size() > 0)
- printf("| Eliminated clauses: %10.2f Mb |\n",
- double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
+ printf(
+ "| Eliminated clauses: %10.2f Mb "
+ " |\n",
+ double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024));
return ok;
}
@@ -744,11 +754,11 @@ void SimpSolver::relocAll(ClauseAllocator& to)
//
for (int i = 0; i < subsumption_queue.size(); i++)
ca.reloc(subsumption_queue[i], to);
- // TODO reloc now takes the proof form the core solver
+ // TODO reloc now takes the proof form the core solver
// Temporary clause:
//
ca.reloc(bwdsub_tmpunit, to);
- // TODO reloc now takes the proof form the core solver
+ // TODO reloc now takes the proof form the core solver
}
@@ -756,15 +766,17 @@ void SimpSolver::garbageCollect()
{
// Initialize the next region to a size corresponding to the estimated utilization degree. This
// is not precise but should avoid some unnecessary reallocations for the new region:
- ClauseAllocator to(ca.size() - ca.wasted());
+ ClauseAllocator to(ca.size() - ca.wasted());
cleanUpClauses();
to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
relocAll(to);
Solver::relocAll(to);
if (verbosity >= 2)
- printf("| Garbage collection: %12d bytes => %12d bytes |\n",
- ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+ printf(
+ "| Garbage collection: %12d bytes => %12d bytes |\n",
+ ca.size() * ClauseAllocator::Unit_Size,
+ to.size() * ClauseAllocator::Unit_Size);
to.moveTo(ca);
- // TODO: proof.finalizeUpdateId();
+ // TODO: proof.finalizeUpdateId();
}
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 335075f09..c13ee5583 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -55,7 +55,7 @@ class SimpSolver : public Solver {
bool addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solver.
bool addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver.
bool addClause_(vec<Lit>& ps, bool removable, ClauseId& id);
- bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction).
+ bool substitute(Var v, Lit x); // Replace all occurrences of v with x (may cause a contradiction).
// Variable mode:
//
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback