diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 40 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 239 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 5 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 12 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 1 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 8 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 5 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 5 |
9 files changed, 20 insertions, 301 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 0fb4a59b5..f8a34ec42 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -22,9 +22,6 @@ #include "expr/node.h" #include "options/bv_options.h" #include "proof/clause_id.h" -#include "proof/cnf_proof.h" -#include "proof/proof_manager.h" -#include "proof/sat_proof.h" #include "prop/minisat/minisat.h" #include "prop/prop_engine.h" #include "prop/theory_proxy.h" @@ -54,7 +51,6 @@ CnfStream::CnfStream(SatSolver* satSolver, d_flitPolicy(flpol), d_registrar(registrar), d_name(name), - d_cnfProof(nullptr), d_removable(false), d_resourceManager(rm) { @@ -86,10 +82,6 @@ bool CnfStream::assertClause(TNode node, SatClause& c) ClauseId clauseId = d_satSolver->addClause(c, d_removable); - if (d_cnfProof && clauseId != ClauseIdUndef) - { - d_cnfProof->registerConvertedClause(clauseId); - } return clauseId != ClauseIdUndef; } @@ -159,27 +151,11 @@ void CnfStream::ensureLiteral(TNode n) // If we were called with something other than a theory atom (or // Boolean variable), we get a SatLiteral that is definitionally // equal to it. - // - // We are setting the current assertion to be null. This is because `toCNF` - // may add clauses to the SAT solver and we look up the current assertion - // in that case. Setting it to null ensures that the assertion stack is - // non-empty and that we are not associating a bogus assertion with the - // clause. This should be ok because we use the mapping back to assertions - // for clauses from input assertions only. - if (d_cnfProof) - { - d_cnfProof->pushCurrentAssertion(Node::null()); - } // These are not removable and have no proof ID d_removable = false; SatLiteral lit = toCNF(n, false); - if (d_cnfProof) - { - d_cnfProof->popCurrentAssertion(); - } - // Store backward-mappings // These may already exist d_literalToNodeMap.insert_safe(lit, n); @@ -239,7 +215,6 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister if (preRegister) { // In case we are re-entered due to lemmas, save our state bool backupRemovable = d_removable; - // Should be fine since cnfProof current assertion is stack based. d_registrar->preRegister(node); d_removable = backupRemovable; } @@ -277,11 +252,6 @@ bool CnfStream::isNotifyFormula(TNode node) const return d_notifyFormulas.find(node) != d_notifyFormulas.end(); } -void CnfStream::setProof(CnfProof* proof) { - Assert(d_cnfProof == NULL); - d_cnfProof = proof; -} - SatLiteral CnfStream::convertAtom(TNode node) { Trace("cnf") << "convertAtom(" << node << ")\n"; @@ -737,17 +707,7 @@ void CnfStream::convertAndAssert(TNode node, << ", negated = " << (negated ? "true" : "false") << ", removable = " << (removable ? "true" : "false") << ")\n"; d_removable = removable; - - if (d_cnfProof) - { - d_cnfProof->pushCurrentAssertion(negated ? node.notNode() : (Node)node, - input); - } convertAndAssert(node, negated); - if (d_cnfProof) - { - d_cnfProof->popCurrentAssertion(); - } } void CnfStream::convertAndAssert(TNode node, bool negated) diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 9901fb18b..264e26777 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -30,7 +30,6 @@ #include "context/cdinsert_hashmap.h" #include "context/cdlist.h" #include "expr/node.h" -#include "proof/proof_manager.h" #include "prop/proof_cnf_stream.h" #include "prop/registrar.h" #include "prop/sat_solver_types.h" @@ -164,8 +163,6 @@ class CnfStream { /** Retrieves map from literals to nodes. */ const CnfStream::LiteralToNodeMap& getNodeCache() const; - void setProof(CnfProof* proof); - protected: /** * Same as above, except that uses the saved d_removable flag. It calls the @@ -243,9 +240,6 @@ class CnfStream { /** The name of this CNF stream*/ std::string d_name; - /** Pointer to the proof corresponding to this CnfStream */ - CnfProof* d_cnfProof; - /** * 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 diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 971fb95d2..41019d58e 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -31,10 +31,6 @@ 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" #include "prop/minisat/minisat.h" #include "prop/minisat/mtl/Sort.h" #include "prop/theory_proxy.h" @@ -228,10 +224,6 @@ Solver::Solver(cvc5::prop::TheoryProxy* proxy, d_pfManager.reset( new SatProofManager(this, proxy->getCnfStream(), userContext, pnm)); } - else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::currentPM()->initSatProof(this); - } // Create the constant variables varTrue = newVar(true, false, false); @@ -240,12 +232,6 @@ Solver::Solver(cvc5::prop::TheoryProxy* proxy, // Assert the constants uncheckedEnqueue(mkLit(varTrue, false)); uncheckedEnqueue(mkLit(varFalse, true)); - // FIXME: these should be axioms I believe - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false)); - ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true)); - } } @@ -423,24 +409,6 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); - // FIXME: at some point will need more information about where this explanation - // came from (ie. the theory/sharing) - Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" - << std::endl; - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - 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); @@ -514,14 +482,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) lemmas.push(); ps.copyTo(lemmas.last()); lemmas_removable.push(removable); - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - // 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); @@ -533,22 +493,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) // construct the clause below to give to the proof manager // as the final conflict. if(falseLiteralsCount == 1) { - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - 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( - cvc5::Minisat::CRef_Lazy); - } if (needProof()) { d_pfManager->finalizeProof(ps[0], true); @@ -576,26 +520,8 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) if (options::unsatCores() || needProof()) { - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - 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) { - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getSatProof()->finalizeProof(cr); - } if (needProof()) { d_pfManager->finalizeProof(ca[cr], true); @@ -614,20 +540,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) << std::endl; if (ps.size() == 1) { - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - 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); - } - } // We need to do this so that the closedness check, if being done, // goes through when we have unit assumptions whose literal has // already been registered, as the ProofCnfStream will not register @@ -640,20 +552,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) } CRef confl = propagate(CHECK_WITHOUT_THEORY); if(! (ok = (confl == CRef_Undef)) ) { - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - if (ca[confl].size() == 1) - { - id = ProofManager::getSatProof()->storeUnitConflict( - ca[confl][0], LEARNT); - ProofManager::getSatProof()->finalizeProof( - cvc5::Minisat::CRef_Lazy); - } - else - { - ProofManager::getSatProof()->finalizeProof(confl); - } - } if (needProof()) { if (ca[confl].size() == 1) @@ -668,10 +566,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) } return ok; } else { - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - id = ClauseIdUndef; - } return ok; } } @@ -715,10 +609,6 @@ void Solver::detachClause(CRef cr, bool strict) { Debug("minisat") << "\n"; } Assert(c.size() > 1); - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getSatProof()->markDeleted(cr); - } if (strict){ remove(watches[~c[0]], Watcher(cr, c[1])); @@ -997,10 +887,6 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) int max_resolution_level = 0; // Maximal level of the resolved clauses - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getSatProof()->startResChain(confl); - } if (needProof()) { d_pfManager->startResChain(ca[confl]); @@ -1059,17 +945,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 (level(var(q)) == 0 && needProof()) { - if (options::unsatCoresMode() - == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getSatProof()->resolveOutUnit(q); - } - if (needProof()) - { - d_pfManager->addResolutionStep(q); - } + d_pfManager->addResolutionStep(q); } } } @@ -1082,19 +960,12 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) seen[var(p)] = 0; pathC--; - if (pathC > 0 && confl != CRef_Undef) + if (pathC > 0 && confl != CRef_Undef && needProof()) { - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); - } - if (needProof()) - { - d_pfManager->addResolutionStep(ca[confl], p); - } + d_pfManager->addResolutionStep(ca[confl], p); } - }while (pathC > 0); + } while (pathC > 0); out_learnt[0] = ~p; if (Debug.isOn("newproof::sat")) { @@ -1124,11 +995,6 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) // Literal is not redundant out_learnt[j++] = out_learnt[i]; } else { - if (options::unsatCoresMode() - == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); - } if (needProof()) { Debug("newproof::sat") @@ -1419,12 +1285,6 @@ void Solver::propagateTheory() { MinisatSatSolver::toMinisatClause(explanation_cl, explanation); ClauseId id; // FIXME: mark it as explanation here somehow? addClause(explanation, true, id); - // explainPropagation() pushes the explanation on the assertion - // stack in CnfProof, so we need to pop it here. - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getCnfProof()->popCurrentAssertion(); - } } } } @@ -1565,12 +1425,6 @@ void Solver::removeSatisfied(vec<CRef>& cs) for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; if (satisfied(c)) { - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF - && locked(c)) - { - // store a resolution of the literal c propagated - ProofManager::getSatProof()->storeUnitResolution(c[0]); - } removeClause(cs[i]); } else @@ -1673,10 +1527,6 @@ lbool Solver::search(int nof_conflicts) if (decisionLevel() == 0) { - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getSatProof()->finalizeProof(confl); - } if (needProof()) { if (confl == CRef_Lazy) @@ -1700,10 +1550,6 @@ lbool Solver::search(int nof_conflicts) if (learnt_clause.size() == 1) { uncheckedEnqueue(learnt_clause[0]); - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getSatProof()->endResChain(learnt_clause[0]); - } if (needProof()) { d_pfManager->endResChain(learnt_clause[0]); @@ -1718,11 +1564,6 @@ lbool Solver::search(int nof_conflicts) attachClause(cr); claBumpActivity(ca[cr]); uncheckedEnqueue(learnt_clause[0], cr); - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT); - ProofManager::getSatProof()->endResChain(id); - } if (needProof()) { d_pfManager->endResChain(ca[cr]); @@ -2059,12 +1900,7 @@ void Solver::relocAll(ClauseAllocator& to) vec<Watcher>& ws = watches[p]; for (int j = 0; j < ws.size(); j++) { - ca.reloc(ws[j].cref, - to, - options::unsatCoresMode() - == options::UnsatCoresMode::OLD_PROOF - ? ProofManager::getSatProof() - : nullptr); + ca.reloc(ws[j].cref, to); } } @@ -2076,37 +1912,20 @@ void Solver::relocAll(ClauseAllocator& to) if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) { - ca.reloc( - vardata[v].d_reason, - to, - options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF - ? ProofManager::getSatProof() - : nullptr); + ca.reloc(vardata[v].d_reason, to); } } // All learnt: // for (int i = 0; i < clauses_removable.size(); i++) { - ca.reloc(clauses_removable[i], - to, - options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF - ? ProofManager::getSatProof() - : nullptr); + ca.reloc(clauses_removable[i], to); } // All original: // for (int i = 0; i < clauses_persistent.size(); i++) { - ca.reloc(clauses_persistent[i], - to, - options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF - ? ProofManager::getSatProof() - : nullptr); - } - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getSatProof()->finishUpdateCRef(); + ca.reloc(clauses_persistent[i], to); } } @@ -2249,9 +2068,6 @@ CRef Solver::updateLemmas() { // Last index in the trail int backtrack_index = trail.size(); - Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF - || lemmas.size() == static_cast<int>(lemmas_cnf_assertion.size())); - // Attach all the clauses and enqueue all the propagations for (int j = 0; j < lemmas.size(); ++j) { @@ -2274,16 +2090,6 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - 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 { @@ -2295,17 +2101,6 @@ 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 (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF - && lemma.size() == 1) - { - Node cnf_assertion = lemmas_cnf_assertion[j]; - - Trace("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); - } Trace("pf::sat") << "Solver::updateLemmas: unit theory lemma: " << lemma[0] << std::endl; if (value(lemma[0]) == l_False) { @@ -2316,10 +2111,6 @@ CRef Solver::updateLemmas() { } else { Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl; conflict = CRef_Lazy; - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); - } if (needProof()) { d_pfManager->storeUnitConflict(lemma[0]); @@ -2334,11 +2125,8 @@ CRef Solver::updateLemmas() { } } - Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF - || lemmas.size() == static_cast<int>(lemmas_cnf_assertion.size())); // Clear the lemmas lemmas.clear(); - lemmas_cnf_assertion.clear(); lemmas_removable.clear(); if (conflict != CRef_Undef) { @@ -2350,24 +2138,17 @@ CRef Solver::updateLemmas() { return conflict; } -void ClauseAllocator::reloc(CRef& cr, - ClauseAllocator& to, - cvc5::TSatProof<Solver>* proof) +void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to) { Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl; // 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 (proof) - { - proof->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()); diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index f4aa04e4d..bed637904 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -39,7 +39,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "util/resource_manager.h" namespace cvc5 { -template <class Solver> class TSatProof; namespace prop { class PropEngine; @@ -58,7 +57,6 @@ class Solver { friend class cvc5::prop::PropEngine; friend class cvc5::prop::TheoryProxy; friend class cvc5::prop::SatProofManager; - friend class cvc5::TSatProof<Minisat::Solver>; public: static CRef TCRef_Undef; @@ -103,9 +101,6 @@ class Solver { /** Is the lemma removable */ vec<bool> lemmas_removable; - /** Nodes being converted to CNF */ - std::vector<cvc5::Node> lemmas_cnf_assertion; - /** Do a another check if FULL_EFFORT was the last one */ bool recheck; diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 312d0b6de..405d97a56 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -33,14 +33,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace cvc5 { namespace Minisat { -class Solver; -} -template <class Solver> -class TSatProof; -} // namespace cvc5 -namespace cvc5 { -namespace Minisat { +class Solver; //================================================================================================= // Variables, literals, lifted booleans, clauses: @@ -320,9 +314,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t> RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra())); } - void reloc(CRef& cr, - ClauseAllocator& to, - cvc5::TSatProof<Solver>* proof = NULL); + void reloc(CRef& cr, ClauseAllocator& to); // Implementation moved to Solver.cc. }; diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 293e7175b..4adbbe7f7 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -22,7 +22,6 @@ #include "options/prop_options.h" #include "options/smt_options.h" #include "proof/clause_id.h" -#include "proof/sat_proof.h" #include "prop/minisat/simp/SimpSolver.h" #include "util/statistics_stats.h" diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 0e6ca28b8..15ef5cacb 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -22,6 +22,14 @@ #include "util/statistics_registry.h" namespace cvc5 { + +template <class Solver> +prop::SatLiteral toSatLiteral(typename Solver::TLit lit); + +template <class Solver> +void toSatClause(const typename Solver::TClause& minisat_cl, + prop::SatClause& sat_cl); + namespace prop { class MinisatSatSolver : public CDCLTSatSolverInterface diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index b71c728e7..bcf75b43a 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -29,7 +29,6 @@ #include "options/options.h" #include "options/proof_options.h" #include "options/smt_options.h" -#include "proof/proof_manager.h" #include "prop/cnf_stream.h" #include "prop/minisat/minisat.h" #include "prop/prop_proof_manager.h" @@ -132,10 +131,6 @@ PropEngine::PropEngine(TheoryEngine* te, d_ppm.reset( new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get())); } - else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext); - } } void PropEngine::finishInit() diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index b764695cc..605c75a14 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -21,7 +21,6 @@ #include "decision/decision_engine.h" #include "options/decision_options.h" #include "options/smt_options.h" -#include "proof/cnf_proof.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/skolem_def_manager.h" @@ -105,10 +104,6 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { || tte.getGenerator()); d_propEngine->getProofCnfStream()->convertPropagation(tte); } - else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); - } Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl; explanation.push_back(l); |