diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 16:59:28 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 17:58:14 -0400 |
commit | 2dbe1f150d30f0fb0c8522f891104270ce09db4c (patch) | |
tree | 1305f3de890f4353c3b5695a93ab7e2419760617 /src/prop | |
parent | 4ec2c8eb8b8a50dc743119100767e101f19305f6 (diff) |
Unsat core infrastruture and API (SMT-LIB compliance to come).
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 4 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 4 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 28 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 28 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 32 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 38 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 6 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 8 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 26 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 9 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 3 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 3 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 2 |
14 files changed, 123 insertions, 70 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 2121d7366..498b31ce5 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -5,7 +5,7 @@ ** Major contributors: ** Minor contributors (to current version): ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -45,7 +45,7 @@ void BVMinisatSatSolver::setNotify(Notify* notify) { d_minisat->setNotify(d_minisatNotify); } -void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) { +void BVMinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { Debug("sat::minisat") << "Add clause " << clause <<"\n"; BVMinisat::vec<BVMinisat::Lit> minisat_clause; toMinisatClause(clause, minisat_clause); diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 0101c5d62..04f21e761 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -5,7 +5,7 @@ ** Major contributors: ** Minor contributors (to current version): ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -76,7 +76,7 @@ public: void setNotify(Notify* notify); - void addClause(SatClause& clause, bool removable); + void addClause(SatClause& clause, bool removable, uint64_t proof_id); SatValue propagate(); diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index e0697735f..0d133aa13 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -44,7 +44,6 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { - CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) : d_satSolver(satSolver), d_booleanVariables(context), @@ -52,6 +51,7 @@ CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Contex d_literalToNodeMap(context), d_fullLitToNodeMap(fullLitToNodeMap), d_registrar(registrar), + d_assertionTable(context), d_removable(false) { } @@ -74,7 +74,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) { Dump("clauses") << AssertCommand(Expr(n.toExpr())); } } - d_satSolver->addClause(c, d_removable); + d_satSolver->addClause(c, d_removable, d_proofId); } void CnfStream::assertClause(TNode node, SatLiteral a) { @@ -104,9 +104,9 @@ bool CnfStream::hasLiteral(TNode n) const { } void TseitinCnfStream::ensureLiteral(TNode n) { - - // These are not removable + // These are not removable and have no proof ID d_removable = false; + d_proofId = uint64_t(-1); Debug("cnf") << "ensureLiteral(" << n << ")" << endl; if(hasLiteral(n)) { @@ -188,9 +188,12 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister // If a theory literal, we pre-register it if (preRegister) { - bool backup = d_removable; + // In case we are re-entered due to lemmas, save our state + bool backupRemovable = d_removable; + uint64_t backupProofId= d_proofId; d_registrar->preRegister(node); - d_removable = backup; + d_removable = backupRemovable; + d_proofId = backupProofId; } // Here, you can have it @@ -642,9 +645,20 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) { // At the top level we must ensure that all clauses that are asserted are // not unit, except for the direct assertions. This allows us to remove the // clauses later when they are not needed anymore (lemmas for example). -void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated) { +void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from) { Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; d_removable = removable; + if(options::proof() || options::unsatCores()) { + // Encode the assertion ID in the proof_id to store with generated clauses. + uint64_t assertionTableIndex = d_assertionTable.size(); + Assert((uint64_t(proof_id) & 0xffffffff00000000) == 0 && (assertionTableIndex & 0xffffffff00000000) == 0, "proof_id/table_index collision"); + d_proofId = assertionTableIndex | (uint64_t(proof_id) << 32); + d_assertionTable.push_back(from.isNull() ? node : from); + Debug("cores") << "cnf ix " << assertionTableIndex << " asst " << node << " proof_id " << proof_id << " from " << from << endl; + } else { + // We aren't producing proofs or unsat cores; use an invalid proof id. + d_proofId = uint64_t(-1); + } convertAndAssert(node, negated); } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 266362ef5..b76051279 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -28,6 +28,7 @@ #include "expr/node.h" #include "prop/theory_proxy.h" #include "prop/registrar.h" +#include "proof/proof_manager.h" #include "context/cdlist.h" #include "context/cdinsert_hashmap.h" @@ -36,7 +37,6 @@ namespace CVC4 { namespace prop { - class PropEngine; /** @@ -77,6 +77,9 @@ protected: /** The "registrar" for pre-registration of terms */ Registrar* d_registrar; + /** A table of assertions, used for regenerating proofs. */ + context::CDList<Node> d_assertionTable; + /** * How many literals were already mapped at the top-level when we * tried to convertAndAssert() something. This @@ -104,10 +107,18 @@ protected: } /** + * A reference into the assertion table, used to map clauses back to + * their "original" input assertion/lemma. This variable is manipulated + * by the top-level convertAndAssert(). This is needed in proofs-enabled + * runs, to justify where the SAT solver's clauses came from. + */ + uint64_t d_proofId; + + /** * Are we asserting a removable clause (true) or a permanent clause (false). * This is set at the beginning of convertAndAssert so that it doesn't - * need to be passed on over the stack. Only pure clauses can be asserted as - * removable. + * need to be passed on over the stack. Only pure clauses can be asserted + * as removable. */ bool d_removable; @@ -190,7 +201,7 @@ public: * @param removable whether the sat solver can choose to remove the clauses * @param negated whether we are asserting the node negated */ - virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0; + virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()) = 0; /** * Get the node that is represented by the given SatLiteral. @@ -223,6 +234,13 @@ public: SatLiteral getLiteral(TNode node); /** + * Get the assertion with a given ID. (Used for reconstructing proofs.) + */ + TNode getAssertion(uint64_t id) { + return d_assertionTable[id]; + } + + /** * Returns the Boolean variables from the input problem. */ void getBooleanVariables(std::vector<TNode>& outputVariables) const; @@ -258,7 +276,7 @@ public: * @param removable is this something that can be erased * @param negated true if negated */ - void convertAndAssert(TNode node, bool removable, bool negated); + void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()); /** * Constructs the stream to use the given sat solver. diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index b0d710d66..5403b992e 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -135,8 +135,8 @@ 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); ) - PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT); ) + PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT, uint64_t(-1)); ) + PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT, uint64_t(-1)); ) } @@ -263,7 +263,7 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); - PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ); + PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA, (uint64_t(RULE_CONFLICT) << 32)); ); 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 +271,7 @@ CRef Solver::reason(Var x) { return real_reason; } -bool Solver::addClause_(vec<Lit>& ps, bool removable) +bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) { if (!ok) return false; @@ -321,6 +321,8 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) 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); } else { // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { @@ -329,7 +331,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) // 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( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT, proof_id); ) PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); ) return ok = false; } @@ -351,7 +353,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) attachClause(cr); if(PROOF_ON()) { - PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); ) + PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT, proof_id); ) if(ps.size() == falseLiteralsCount) { PROOF( ProofManager::getSatProof()->finalizeProof(cr); ) return ok = false; @@ -364,11 +366,12 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) if(assigns[var(ps[0])] == l_Undef) { assert(assigns[var(ps[0])] != l_False); uncheckedEnqueue(ps[0], cr); - PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } ); + 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); } ); 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( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT, proof_id); ); PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); ) } else { PROOF( ProofManager::getSatProof()->finalizeProof(confl); ); @@ -842,7 +845,7 @@ CRef Solver::propagate(TheoryCheckType type) propagateTheory(); // If there are lemmas (or conflicts) update them if (lemmas.size() > 0) { - confl = updateLemmas(); + confl = updateLemmas(); } } else { // Even though in conflict, we still need to discharge the lemmas @@ -891,7 +894,7 @@ void Solver::propagateTheory() { proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl); vec<Lit> explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); - addClause(explanation, true); + addClause(explanation, true, 0); } } } @@ -1645,6 +1648,8 @@ CRef Solver::updateLemmas() { // 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; @@ -1659,7 +1664,7 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ); + PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA, proof_id); ); if (removable) { clauses_removable.push(lemma_ref); } else { @@ -1667,7 +1672,7 @@ CRef Solver::updateLemmas() { } attachClause(lemma_ref); } else { - PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); ); + PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA, proof_id); ); } // If the lemma is propagating enqueue its literal (or set the conflict) @@ -1681,7 +1686,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]); ); + PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT, proof_id); ); } } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; @@ -1694,6 +1699,7 @@ CRef Solver::updateLemmas() { // Clear the lemmas lemmas.clear(); lemmas_removable.clear(); + lemmas_proof_id.clear(); if (conflict != CRef_Undef) { theoryConflict = true; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 7831f211b..2d70cfeef 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -37,12 +37,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "expr/command.h" namespace CVC4 { -class SatProof; - -namespace prop { - class TheoryProxy; -}/* CVC4::prop namespace */ + class SatProof; + namespace prop { + class TheoryProxy; + }/* CVC4::prop namespace */ }/* CVC4 namespace */ namespace Minisat { @@ -85,6 +84,9 @@ protected: /** Is the lemma removable */ vec<bool> lemmas_removable; + /** Proof IDs for lemmas */ + vec<uint64_t> lemmas_proof_id; + /** Do a another check if FULL_EFFORT was the last one */ bool recheck; @@ -154,12 +156,14 @@ public: void push (); void pop (); - bool addClause (const vec<Lit>& ps, bool removable); // Add a clause to the solver. + // 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); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, bool removable); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver. - bool addClause_( vec<Lit>& ps, bool removable); // Add a clause to the solver without making superflous internal copy. Will + 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 // change the passed vector 'ps'. // Solving: @@ -489,11 +493,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) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); } -inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable); } -inline bool Solver::addClause (Lit p, bool removable) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); } -inline bool Solver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); } -inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); } +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::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/minisat.cpp b/src/prop/minisat/minisat.cpp index 4a192d0d2..b50c1c09f 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -149,10 +149,10 @@ void MinisatSatSolver::setupOptions() { d_minisat->restart_inc = options::satRestartInc(); } -void MinisatSatSolver::addClause(SatClause& clause, bool removable) { +void MinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { Minisat::vec<Minisat::Lit> minisat_clause; toMinisatClause(clause, minisat_clause); - d_minisat->addClause(minisat_clause, removable); + d_minisat->addClause(minisat_clause, removable, proof_id); } SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) { @@ -228,7 +228,7 @@ void MinisatSatSolver::push() { d_minisat->push(); } -void MinisatSatSolver::pop(){ +void MinisatSatSolver::pop() { d_minisat->pop(); } diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index b37371d98..3992f1adb 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -53,7 +53,7 @@ public: static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause); void initialize(context::Context* context, TheoryProxy* theoryProxy); - void addClause(SatClause& clause, bool removable); + void addClause(SatClause& clause, bool removable, uint64_t proof_id); SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase); SatVariable trueVar() { return d_minisat->trueVar(); } diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 6dcdb76c7..71e747f72 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -159,7 +159,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) -bool SimpSolver::addClause_(vec<Lit>& ps, bool removable) +bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) { #ifndef NDEBUG if (use_simplification) { @@ -173,7 +173,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable) if (use_rcheck && implied(ps)) return true; - if (!Solver::addClause_(ps, removable)) + if (!Solver::addClause_(ps, removable, proof_id)) return false; if (use_simplification && clauses_persistent.size() == nclauses + 1){ @@ -545,7 +545,7 @@ bool SimpSolver::eliminateVar(Var v) 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)) { + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable, uint64_t(-1))) { return false; } } @@ -585,7 +585,7 @@ bool SimpSolver::substitute(Var v, Lit x) removeClause(cls[i]); - if (!addClause_(subst_clause, c.removable())) { + if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) { return ok = false; } } diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 878d799a5..041309546 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -47,12 +47,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); - bool addEmptyClause(bool removable); // Add the empty clause to the solver. - bool addClause (Lit p, bool removable); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, bool removable); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver. - bool addClause_(vec<Lit>& ps, bool removable); + 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 substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). // Variable mode: @@ -182,11 +182,15 @@ inline void SimpSolver::updateElimHeap(Var v) { elim_heap.update(v); } -inline bool SimpSolver::addClause (const vec<Lit>& ps, bool removable) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); } -inline bool SimpSolver::addEmptyClause(bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable); } -inline bool SimpSolver::addClause (Lit p, bool removable) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); } -inline bool SimpSolver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); } -inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); } +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 void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 82c0bae1a..a02e40e32 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -25,6 +25,7 @@ #include "decision/options.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" +#include "proof/proof_manager.h" #include "util/cvc4_assert.h" #include "options/options.h" #include "smt/options.h" @@ -109,15 +110,15 @@ void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable - d_cnfStream->convertAndAssert(node, false, false); + d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN); } -void PropEngine::assertLemma(TNode node, bool negated, bool removable) { +void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; - // Assert as removable - d_cnfStream->convertAndAssert(node, removable, negated); + // Assert as (possibly) removable + d_cnfStream->convertAndAssert(node, removable, negated, rule, from); } void PropEngine::requirePhase(TNode n, bool phase) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index a5132e3da..ed022a64f 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -25,6 +25,7 @@ #include "options/options.h" #include "util/result.h" #include "smt/modal_exception.h" +#include "proof/proof_manager.h" #include <sys/time.h> namespace CVC4 { @@ -199,7 +200,7 @@ public: * @param removable whether this lemma can be quietly removed based * on an activity heuristic (or not) */ - void assertLemma(TNode node, bool negated, bool removable); + void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null()); /** * If ever n is decided upon, it must be in the given phase. This diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 8e7e53474..e3b0f3449 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -24,6 +24,7 @@ #include "util/statistics_registry.h" #include "context/cdlist.h" #include "prop/sat_solver_types.h" +#include "expr/node.h" namespace CVC4 { namespace prop { @@ -38,7 +39,7 @@ public: virtual ~SatSolver() { } /** Assert a clause in the solver. */ - virtual void addClause(SatClause& clause, bool removable) = 0; + virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0; /** * Create a new boolean variable in the solver. diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 67325cb18..2bcd48099 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -122,7 +122,7 @@ void TheoryProxy::notifyRestart() { if(lemmaCount % 1 == 0) { Debug("shared") << "=) " << asNode << std::endl; } - d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true); + d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID); } else { Debug("shared") << "=(" << asNode << std::endl; } |