diff options
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 313 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 64 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 2 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 98 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 2 |
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: // |