diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /src/prop/minisat | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 132 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 61 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 37 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 41 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 5 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 12 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 30 |
7 files changed, 211 insertions, 107 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 4c431a9b1..f4489c4be 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -25,6 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/output.h" #include "options/prop_options.h" #include "proof/proof_manager.h" +#include "proof/sat_proof_implementation.h" #include "proof/sat_proof.h" #include "prop/minisat/core/Solver.h" #include "prop/minisat/minisat.h" @@ -32,6 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/theory_proxy.h" #include "smt_util/command.h" + using namespace CVC4::prop; namespace CVC4 { @@ -40,7 +42,6 @@ namespace Minisat { //================================================================================================= // Options: - static const char* _cat = "CORE"; static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false)); @@ -55,6 +56,10 @@ static IntOption opt_restart_first (_cat, "rfirst", "The base resta static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false)); static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); +//================================================================================================= +// Proof declarations +CRef Solver::TCRef_Undef = CRef_Undef; +CRef Solver::TCRef_Lazy = CRef_Lazy; class ScopedBool { bool& watch; @@ -135,8 +140,12 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, // Assert the constants uncheckedEnqueue(mkLit(varTrue, false)); uncheckedEnqueue(mkLit(varFalse, true)); - PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT, uint64_t(-1)); ) - PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT, uint64_t(-1)); ) + // FIXME: these should be axioms I believe + PROOF + ( + ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false)); + ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true)); + ); } @@ -217,7 +226,9 @@ CRef Solver::reason(Var x) { // Get the explanation from the theory SatClause explanation_cl; - proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl); + // FIXME: at some point return a tag with the theory that spawned you + proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), + explanation_cl); vec<Lit> explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); @@ -263,7 +274,12 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); - PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA, (uint64_t(RULE_CONFLICT) << 32)); ); + // FIXME: at some point will need more information about where this explanation + // came from (ie. the theory/sharing) + PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); + ProofManager::getCnfProof()->registerConvertedClause(id, true); + // no need to pop current assertion as this is not converted to cnf + ); vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); @@ -271,7 +287,7 @@ CRef Solver::reason(Var x) { return real_reason; } -bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) +bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) { if (!ok) return false; @@ -289,11 +305,13 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) clauseLevel = std::max(clauseLevel, intro_level(var(ps[i]))); // Tautologies are ignored if (ps[i] == ~p) { + id = ClauseIdUndef; // Clause can be ignored return true; } // Clauses with 0-level true literals are also ignored if (value(ps[i]) == l_True && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { + id = ClauseIdUndef; return true; } // Ignore repeated literals @@ -321,8 +339,19 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) lemmas.push(); ps.copyTo(lemmas.last()); lemmas_removable.push(removable); - Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl; - lemmas_proof_id.push(proof_id); + 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); } else { // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { @@ -331,7 +360,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) // construct the clause below to give to the proof manager // as the final conflict. if(falseLiteralsCount == 1) { - PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT, proof_id); ) + PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); ) PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); ) return ok = false; } @@ -353,7 +382,9 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) attachClause(cr); if(PROOF_ON()) { - PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT, proof_id); ) + PROOF( + id = ProofManager::getSatProof()->registerClause(cr, INPUT); + ) if(ps.size() == falseLiteralsCount) { PROOF( ProofManager::getSatProof()->finalizeProof(cr); ) return ok = false; @@ -366,12 +397,16 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_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, proof id " << proof_id << std::endl; - PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT, proof_id); } ); + Debug("cores") << "i'm registering a unit clause, input" << std::endl; + PROOF( + if(ps.size() == 1) { + id = ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); + } + ); CRef confl = propagate(CHECK_WITHOUT_THEORY); if(! (ok = (confl == CRef_Undef)) ) { if(ca[confl].size() == 1) { - PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT, proof_id); ); + PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); ); PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); ) } else { PROOF( ProofManager::getSatProof()->finalizeProof(confl); ); @@ -604,7 +639,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ Lit q = c[j]; - if (!seen[var(q)] && level(var(q)) > 0){ + if (!seen[var(q)] && level(var(q)) > 0) { varBumpActivity(var(q)); seen[var(q)] = 1; if (level(var(q)) >= decisionLevel()) @@ -646,7 +681,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) uint32_t abstract_level = 0; for (i = 1; i < out_learnt.size(); i++) abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) - + for (i = j = 1; i < out_learnt.size(); i++) { if (reason(var(out_learnt[i])) == CRef_Undef) { out_learnt[j++] = out_learnt[i]; @@ -901,7 +936,8 @@ void Solver::propagateTheory() { proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl); vec<Lit> explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); - addClause(explanation, true, 0); + ClauseId id; // FIXME: mark it as explanation here somehow? + addClause(explanation, true, id); } } } @@ -1159,8 +1195,17 @@ lbool Solver::search(int nof_conflicts) attachClause(cr); claBumpActivity(ca[cr]); uncheckedEnqueue(learnt_clause[0], cr); - - PROOF( ProofManager::getSatProof()->endResChain(cr); ) + PROOF( + ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT); + PSTATS( + __gnu_cxx::hash_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); + ); } varDecayActivity(); @@ -1650,14 +1695,14 @@ CRef Solver::updateLemmas() { // Last index in the trail int backtrack_index = trail.size(); + PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size());); + // Attach all the clauses and enqueue all the propagations for (int i = 0; i < lemmas.size(); ++ i) { // The current lemma vec<Lit>& lemma = lemmas[i]; bool removable = lemmas_removable[i]; - uint64_t proof_id = lemmas_proof_id[i]; - Debug("cores") << "pulled lemma proof id " << proof_id << " " << (proof_id & 0xffffffff) << std::endl; // Attach it if non-unit CRef lemma_ref = CRef_Undef; @@ -1672,7 +1717,15 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA, proof_id); ); + PROOF + ( + TNode cnf_assertion = lemmas_cnf_assertion[i].first; + TNode cnf_def = lemmas_cnf_assertion[i].second; + + ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); + ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); + ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); + ); if (removable) { clauses_removable.push(lemma_ref); } else { @@ -1680,7 +1733,15 @@ CRef Solver::updateLemmas() { } attachClause(lemma_ref); } else { - PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA, proof_id); ); + PROOF + ( + Node cnf_assertion = lemmas_cnf_assertion[i].first; + Node cnf_def = lemmas_cnf_assertion[i].second; + + ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); + ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); + ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); + ); } // If the lemma is propagating enqueue its literal (or set the conflict) @@ -1694,7 +1755,7 @@ 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, proof_id); ); + PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); ); } } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; @@ -1704,10 +1765,11 @@ CRef Solver::updateLemmas() { } } + PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size());); // Clear the lemmas lemmas.clear(); + lemmas_cnf_assertion.clear(); lemmas_removable.clear(); - lemmas_proof_id.clear(); if (conflict != CRef_Undef) { theoryConflict = true; @@ -1718,6 +1780,28 @@ CRef Solver::updateLemmas() { return conflict; } +void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy) +{ + + // FIXME what is this CRef_lazy + if (cr == CRef_Lazy) return; + + CRef old = cr; // save the old reference + Clause& c = operator[](cr); + if (c.reloced()) { cr = c.relocation(); return; } + + cr = to.alloc(c.level(), c, c.removable()); + c.relocate(cr); + if (proxy) { + proxy->updateCRef(old, cr); + } + // Copy extra data-fields: + // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) + to[cr].mark(c.mark()); + if (to[cr].removable()) to[cr].activity() = c.activity(); + else if (to[cr].has_extra()) to[cr].calcAbstraction(); +} + inline bool Solver::withinBudget(uint64_t ammount) const { Assert (proxy); // spendResource sets async_interrupt or throws UnsafeInterruptException diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 3be6b1b22..a239eba72 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -37,13 +37,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace CVC4 { - class SatProof; +template <class Solver> class TSatProof; - namespace prop { - class TheoryProxy; - }/* CVC4::prop namespace */ +namespace prop { + class TheoryProxy; +}/* CVC4::prop namespace */ }/* CVC4 namespace */ +typedef unsigned ClauseId; + namespace CVC4 { namespace Minisat { @@ -54,7 +56,18 @@ class Solver { /** The only two CVC4 entry points to the private solver data */ friend class CVC4::prop::TheoryProxy; - friend class CVC4::SatProof; + friend class CVC4::TSatProof<Minisat::Solver>; + +public: + static CRef TCRef_Undef; + static CRef TCRef_Lazy; + + typedef Var TVar; + typedef Lit TLit; + typedef Clause TClause; + typedef CRef TCRef; + typedef vec<Lit> TLitVec; + protected: /** The pointer to the proxy that provides interfaces to the SMT engine */ @@ -85,8 +98,8 @@ protected: /** Is the lemma removable */ vec<bool> lemmas_removable; - /** Proof IDs for lemmas */ - vec<uint64_t> lemmas_proof_id; + /** Nodes being converted to CNF */ + std::vector< std::pair<CVC4::Node, CVC4::Node > >lemmas_cnf_assertion; /** Do a another check if FULL_EFFORT was the last one */ bool recheck; @@ -157,14 +170,14 @@ public: void push (); void pop (); - // CVC4 adds the "proof_id" here to refer to the input assertion/lemma - // that produced this clause - bool addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id); // Add a clause to the solver. - bool addEmptyClause(bool removable); // Add the empty clause, making the solver contradictory. - bool addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver. - bool addClause_( vec<Lit>& ps, bool removable, uint64_t proof_id); // Add a clause to the solver without making superflous internal copy. Will + // addClause returns the ClauseId corresponding to the clause added in the + // reference parameter id. + bool addClause (const vec<Lit>& ps, bool removable, ClauseId& id); // Add a clause to the solver. + bool addEmptyClause(bool removable); // Add the empty clause, making the solver contradictory. + bool addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the 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); // Add a clause to the solver without making superflous internal copy. Will // change the passed vector 'ps'. // Solving: @@ -495,15 +508,15 @@ inline void Solver::checkGarbage(double gf){ // NOTE: enqueue does not set the ok flag! (only public methods do) inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } -inline bool Solver::addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id) - { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); } -inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable, uint64_t(-1)); } -inline bool Solver::addClause (Lit p, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); } -inline bool Solver::addClause (Lit p, Lit q, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); } -inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); } +inline bool Solver::addClause (const vec<Lit>& ps, bool removable, ClauseId& id) + { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); } +inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); ClauseId tmp; return addClause_(add_tmp, removable, tmp); } +inline bool Solver::addClause (Lit p, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); } +inline bool Solver::addClause (Lit p, Lit q, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); } +inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); } inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); } inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); flipped.push(false); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } } diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index b0d78242c..116a39a49 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -169,20 +169,22 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) { } -} /* Minisat */ -} - +class Solver; - -namespace CVC4 { class ProofProxyAbstract { public: virtual ~ProofProxyAbstract() {} virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0; }; -} + +} /* namespace CVC4::Minisat */ +} /* namespace CVC4 */ +namespace CVC4 { +template <class Solver> class ProofProxy; +typedef ProofProxy<CVC4::Minisat::Solver> CoreProofProxy; +} namespace CVC4 { namespace Minisat{ @@ -305,27 +307,8 @@ class ClauseAllocator : public RegionAllocator<uint32_t> RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra())); } - void reloc(CRef& cr, ClauseAllocator& to, CVC4::ProofProxyAbstract* proxy = NULL) - { - - // FIXME what is this CRef_lazy - if (cr == CRef_Lazy) return; - - CRef old = cr; // save the old reference - Clause& c = operator[](cr); - if (c.reloced()) { cr = c.relocation(); return; } - - cr = to.alloc(c.level(), c, c.removable()); - c.relocate(cr); - if (proxy) { - proxy->updateCRef(old, cr); - } - // Copy extra data-fields: - // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) - to[cr].mark(c.mark()); - if (to[cr].removable()) to[cr].activity() = c.activity(); - else if (to[cr].has_extra()) to[cr].calcAbstraction(); - } + void reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy = NULL); + // Implementation moved to Solver.cc. }; diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index ce5c1eb92..739d9087a 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -23,6 +23,7 @@ #include "options/prop_options.h" #include "options/smt_options.h" #include "prop/minisat/simp/SimpSolver.h" +#include "proof/sat_proof.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -94,14 +95,6 @@ void MinisatSatSolver::toMinisatClause(SatClause& clause, Assert(clause.size() == (unsigned)minisat_clause.size()); } -void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause, - SatClause& sat_clause) { - for (int i = 0; i < clause.size(); ++i) { - sat_clause.push_back(toSatLiteral(clause[i])); - } - Assert((unsigned)clause.size() == sat_clause.size()); -} - void MinisatSatSolver::toSatClause(const Minisat::Clause& clause, SatClause& sat_clause) { for (int i = 0; i < clause.size(); ++i) { @@ -149,10 +142,18 @@ void MinisatSatSolver::setupOptions() { d_minisat->restart_inc = options::satRestartInc(); } -void MinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { +ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { Minisat::vec<Minisat::Lit> minisat_clause; toMinisatClause(clause, minisat_clause); - d_minisat->addClause(minisat_clause, removable, proof_id); + ClauseId clause_id = ClauseIdError; + // FIXME: This relies on the invariant that when ok() is false + // the SAT solver does not add the clause (which is what Minisat currently does) + if (!ok()) { + return ClauseIdUndef; + } + d_minisat->addClause(minisat_clause, removable, clause_id); + PROOF( Assert (clause_id != ClauseIdError);); + return clause_id; } SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) { @@ -182,6 +183,9 @@ SatValue MinisatSatSolver::solve() { return toSatLiteralValue(d_minisat->solve()); } +bool MinisatSatSolver::ok() const { + return d_minisat->okay(); +} void MinisatSatSolver::interrupt() { d_minisat->interrupt(); @@ -280,3 +284,20 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ } /* namespace CVC4::prop */ } /* namespace CVC4 */ + + +namespace CVC4 { +template<> +prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) { + return prop::MinisatSatSolver::toSatLiteral(lit); +} + +template<> +void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl, + prop::SatClause& sat_cl) { + prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl); +} + +} /* namespace CVC4 */ + + diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index f279b3a5b..535ce1a47 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -40,11 +40,10 @@ public: //(Commented because not in use) static bool tobool(SatValue val); static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause); - static void toSatClause (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause); static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause); void initialize(context::Context* context, TheoryProxy* theoryProxy); - void addClause(SatClause& clause, bool removable, uint64_t proof_id); + ClauseId addClause(SatClause& clause, bool removable); SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase); SatVariable trueVar() { return d_minisat->trueVar(); } @@ -53,6 +52,8 @@ public: SatValue solve(); SatValue solve(long unsigned int&); + bool ok() const; + void interrupt(); SatValue value(SatLiteral l); diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 235c97e8f..5bdaea950 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -160,7 +160,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) -bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) +bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) { #ifndef NDEBUG if (use_simplification) { @@ -174,7 +174,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) if (use_rcheck && implied(ps)) return true; - if (!Solver::addClause_(ps, removable, proof_id)) + if (!Solver::addClause_(ps, removable, id)) return false; if (use_simplification && clauses_persistent.size() == nclauses + 1){ @@ -541,12 +541,14 @@ bool SimpSolver::eliminateVar(Var v) for (int i = 0; i < cls.size(); i++) removeClause(cls[i]); + ClauseId id = ClauseIdUndef; // Produce clauses in cross product: vec<Lit>& resolvent = add_tmp; for (int i = 0; i < pos.size(); i++) for (int j = 0; j < neg.size(); j++) { bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable(); - if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable, uint64_t(-1))) { + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && + !addClause_(resolvent, removable, id)) { return false; } } @@ -585,8 +587,8 @@ bool SimpSolver::substitute(Var v, Lit x) } removeClause(cls[i]); - - if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) { + ClauseId id = ClauseIdUndef; + if (!addClause_(subst_clause, c.removable(), id)) { return ok = false; } } diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 0c5062726..a19bec1ef 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -48,12 +48,12 @@ class SimpSolver : public Solver { // Problem specification: // Var newVar (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); - bool addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id); - bool addEmptyClause(bool removable, uint64_t proof_id); // Add the empty clause to the solver. - bool addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver. - bool addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id); + bool addClause (const vec<Lit>& ps, bool removable, ClauseId& id); + bool addEmptyClause(bool removable); // Add the empty clause to the solver. + bool addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the 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). // Variable mode: @@ -183,15 +183,15 @@ inline void SimpSolver::updateElimHeap(Var v) { elim_heap.update(v); } -inline bool SimpSolver::addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id) - { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); } -inline bool SimpSolver::addEmptyClause(bool removable, uint64_t proof_id) { add_tmp.clear(); return addClause_(add_tmp, removable, proof_id); } -inline bool SimpSolver::addClause (Lit p, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); } -inline bool SimpSolver::addClause (Lit p, Lit q, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); } -inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); } +inline bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id) +{ ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); } +inline bool SimpSolver::addEmptyClause(bool removable) { add_tmp.clear(); ClauseId id=-1; return addClause_(add_tmp, removable, id); } +inline bool SimpSolver::addClause (Lit p, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); } +inline bool SimpSolver::addClause (Lit p, Lit q, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); } +inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } // the solver can always return unknown due to resource limiting |