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/core | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'src/prop/minisat/core')
-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 |
3 files changed, 155 insertions, 75 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. }; |