From: Haniel Barbosa Date: Thu, 20 May 2021 18:29:32 +0000 (-0300) Subject: Remove old unsat cores (#6581) X-Git-Tag: cvc5-1.0.0~1722 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a0644780130dd0ed86a9486e29aa326b3fe5d804;p=cvc5.git Remove old unsat cores (#6581) This commit removes the remaining old proof code and the code to produce unsat cores based on it. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 083bce687..5362baad8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -137,14 +137,8 @@ libcvc5_add_sources( printer/tptp/tptp_printer.cpp printer/tptp/tptp_printer.h proof/clause_id.h - proof/cnf_proof.cpp - proof/cnf_proof.h proof/dot/dot_printer.cpp proof/dot/dot_printer.h - proof/proof_manager.cpp - proof/proof_manager.h - proof/sat_proof.h - proof/sat_proof_implementation.h proof/unsat_core.cpp proof/unsat_core.h prop/bv_sat_solver_notify.h diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index ddffe8c12..880bbe0fb 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -200,9 +200,6 @@ name = "SMT Layer" [[option.mode.OFF]] name = "off" help = "Do not produce unsat cores." -[[option.mode.OLD_PROOF]] - name = "old-proof" - help = "Produce unsat cores from old proof infrastructure." [[option.mode.SAT_PROOF]] name = "sat-proof" help = "Produce unsat cores from SAT and preprocessing proofs." diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index beb8d75af..2f3a49ac2 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -19,7 +19,6 @@ #include "expr/node_manager.h" #include "options/smt_options.h" #include "expr/lazy_proof.h" -#include "proof/proof_manager.h" #include "smt/preprocess_proof_generator.h" #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" @@ -103,10 +102,6 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen) { d_pppg->notifyPreprocessed(d_nodes[i], n, pgen); } - else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::currentPM()->addDependence(n, d_nodes[i]); - } d_nodes[i] = n; } @@ -204,10 +199,6 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg) d_pppg->notifyNewAssert(newConjr, lcp); } } - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]); - } d_nodes[i] = newConjr; Assert(theory::Rewriter::rewrite(newConjr) == newConjr); } diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp index 8c97aabc7..44dafefcb 100644 --- a/src/preprocessing/passes/fun_def_fmf.cpp +++ b/src/preprocessing/passes/fun_def_fmf.cpp @@ -21,7 +21,6 @@ #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" -#include "proof/proof_manager.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 2b25098af..dc47c9c8e 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -21,7 +21,6 @@ #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" -#include "proof/proof_manager.h" #include "prop/prop_engine.h" #include "theory/rewriter.h" #include "theory/theory_preprocessor.h" @@ -61,12 +60,6 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) { imap[assertions->size()] = newSkolems[j]; assertions->pushBackTrusted(newAsserts[j]); - // new assertions have a dependence on the node (old pf architecture) - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::currentPM()->addDependence(newAsserts[j].getProven(), - assertion); - } } } for (unsigned i = 0, size = assertions->size(); i < size; ++i) diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index f2724932f..e0a57ae5b 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -115,7 +115,6 @@ ITESimp::Statistics::Statistics() bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) { - Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF); bool result = true; bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic(); if (simpDidALotOfWork) diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index fe515ed59..f27ff836a 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -188,7 +188,6 @@ PreprocessingPassResult MipLibTrick::applyInternal( Assert(assertionsToPreprocess->getRealAssertionsEnd() == assertionsToPreprocess->size()); Assert(!options::incrementalSolving()); - Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF); context::Context fakeContext; TheoryEngine* te = d_preprocContext->getTheoryEngine(); diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index d88e901d7..921442f0e 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -69,12 +69,6 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext) PreprocessingPassResult NonClausalSimp::applyInternal( AssertionPipeline* assertionsToPreprocess) { - Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF - || isProofEnabled()) - << "Unsat cores with non-clausal simp only supported with new proofs. " - "Cores mode is " - << options::unsatCoresMode() << "\n"; - d_preprocContext->spendResource(Resource::PreprocessStep); theory::booleans::CircuitPropagator* propagator = diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 90a4b8240..1eb21cd96 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -20,7 +20,6 @@ #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" -#include "proof/proof_manager.h" #include "prop/prop_engine.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" @@ -58,12 +57,6 @@ PreprocessingPassResult TheoryPreprocess::applyInternal( { imap[assertions->size()] = newSkolems[j]; assertions->pushBackTrusted(newAsserts[j]); - // new assertions have a dependence on the node (old pf architecture) - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - ProofManager::currentPM()->addDependence(newAsserts[j].getProven(), - assertion); - } } } diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp deleted file mode 100644 index 867977a29..000000000 --- a/src/proof/cnf_proof.cpp +++ /dev/null @@ -1,117 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Liana Hadarean, Andres Noetzli, Haniel Barbosa - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include "proof/cnf_proof.h" - -#include "proof/clause_id.h" -#include "proof/proof_manager.h" -#include "prop/cnf_stream.h" -#include "prop/minisat/minisat.h" -#include "prop/sat_solver_types.h" - -namespace cvc5 { - -CnfProof::CnfProof(prop::CnfStream* stream, - context::Context* ctx, - const std::string& name) - : d_cnfStream(stream) - , d_clauseToAssertion(ctx) - , d_currentAssertionStack() - , d_cnfDeps() - , d_name(name) -{ - // Setting the proof object for the CnfStream - d_cnfStream->setProof(this); -} - -CnfProof::~CnfProof() {} - -Node CnfProof::getAssertionForClause(ClauseId clause) { - ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause); - Assert(it != d_clauseToAssertion.end() && !(*it).second.isNull()); - return (*it).second; -} - -void CnfProof::registerConvertedClause(ClauseId clause) -{ - Assert(clause != ClauseIdUndef && clause != ClauseIdError - && clause != ClauseIdEmpty); - Node current_assertion = getCurrentAssertion(); - - Debug("proof:cnf") << "CnfProof::registerConvertedClause " << clause - << " assertion = " << current_assertion << std::endl; - - setClauseAssertion(clause, current_assertion); -} - -void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { - Debug("proof:cnf") << "CnfProof::setClauseAssertion " - << clause << " assertion " << expr << std::endl; - // We can add the same clause from different assertions. In this - // case we keep the first assertion. For example asserting a /\ b - // and then b /\ c where b is an atom, would assert b twice (note - // that since b is top level, it is not cached by the CnfStream) - // - // Note: If the current assertion associated with the clause is null, we - // update it because it means that it was previously added the clause without - // associating it with an assertion. - const auto& it = d_clauseToAssertion.find(clause); - if (it != d_clauseToAssertion.end() && (*it).second != Node::null()) - { - return; - } - - d_clauseToAssertion.insert(clause, expr); -} - -void CnfProof::pushCurrentAssertion(Node assertion, bool isInput) -{ - Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " << assertion - << std::endl; - - d_currentAssertionStack.push_back(std::pair(assertion, isInput)); - - Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " - << "new stack size = " << d_currentAssertionStack.size() - << std::endl; -} - -void CnfProof::popCurrentAssertion() { - Assert(d_currentAssertionStack.size()); - - Debug("proof:cnf") << "CnfProof::popCurrentAssertion " - << d_currentAssertionStack.back().first << std::endl; - - d_currentAssertionStack.pop_back(); - - Debug("proof:cnf") << "CnfProof::popCurrentAssertion " - << "new stack size = " << d_currentAssertionStack.size() - << std::endl; -} - -Node CnfProof::getCurrentAssertion() { - Assert(d_currentAssertionStack.size()); - return d_currentAssertionStack.back().first; -} - -bool CnfProof::getCurrentAssertionKind() -{ - return d_currentAssertionStack.back().second; -} - -} // namespace cvc5 diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h deleted file mode 100644 index 8e8f2bc91..000000000 --- a/src/proof/cnf_proof.h +++ /dev/null @@ -1,97 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Liana Hadarean, Haniel Barbosa, Andres Noetzli - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A manager for CnfProofs. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__CNF_PROOF_H -#define CVC5__CNF_PROOF_H - -#include -#include - -#include "context/cdhashmap.h" -#include "proof/clause_id.h" -#include "proof/proof_manager.h" - -namespace cvc5 { -namespace prop { - class CnfStream; - } // namespace prop - -class CnfProof; - -typedef std::unordered_map NodeToNode; -typedef std::unordered_set ClauseIdSet; - -typedef context::CDHashMap ClauseIdToNode; -typedef std::pair NodePair; -typedef std::set NodePairSet; - -typedef std::unordered_set NodeSet; - -class CnfProof { -protected: - cvc5::prop::CnfStream* d_cnfStream; - - /** Map from ClauseId to the assertion that lead to adding this clause **/ - ClauseIdToNode d_clauseToAssertion; - - /** Top of stack is assertion currently being converted to CNF. Also saves - * whether it is input (rather than a lemma). **/ - std::vector> d_currentAssertionStack; - - /** Map from top-level fact to facts/assertion that it follows from **/ - NodeToNode d_cnfDeps; - - ClauseIdSet d_explanations; - - // The clause ID of the unit clause defining the true SAT literal. - ClauseId d_trueUnitClause; - // The clause ID of the unit clause defining the false SAT literal. - ClauseId d_falseUnitClause; - - std::string d_name; -public: - CnfProof(cvc5::prop::CnfStream* cnfStream, - context::Context* ctx, - const std::string& name); - ~CnfProof(); - - /** Methods for logging what the CnfStream does **/ - // map the clause back to the current assertion where it came from - void registerConvertedClause(ClauseId clause); - - /** Clause is one of the clauses defining top-level assertion node*/ - void setClauseAssertion(ClauseId clause, Node node); - - /** Current assertion being converted and whether it is an input (rather than - * a lemma) */ - void pushCurrentAssertion(Node assertion, bool isInput = false); - void popCurrentAssertion(); - Node getCurrentAssertion(); - bool getCurrentAssertionKind(); - - /** - * Checks whether the assertion stack is empty. - */ - bool isAssertionStackEmpty() const { return d_currentAssertionStack.empty(); } - - // accessors for the leaf assertions that are being converted to CNF - Node getAssertionForClause(ClauseId clause); -};/* class CnfProof */ - -} // namespace cvc5 - -#endif /* CVC5__CNF_PROOF_H */ diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp deleted file mode 100644 index f46317953..000000000 --- a/src/proof/proof_manager.cpp +++ /dev/null @@ -1,220 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Liana Hadarean, Morgan Deters, Andres Noetzli - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - */ - -#include "proof/proof_manager.h" - -#include "base/check.h" -#include "context/context.h" -#include "expr/node_visitor.h" -#include "options/bv_options.h" -#include "options/smt_options.h" -#include "proof/clause_id.h" -#include "proof/cnf_proof.h" -#include "proof/sat_proof_implementation.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "smt/smt_statistics_registry.h" -#include "theory/arrays/theory_arrays.h" -#include "theory/output_channel.h" -#include "theory/term_registration_visitor.h" -#include "theory/uf/equality_engine.h" -#include "theory/uf/theory_uf.h" -#include "theory/valuation.h" -#include "util/hash.h" - -namespace cvc5 { - -ProofManager::ProofManager(context::Context* context) - : d_context(context), - d_satProof(nullptr), - d_cnfProof(nullptr), - d_inputCoreFormulas(context), - d_outputCoreFormulas(context), - d_nextId(0), - d_deps(context) -{ -} - -ProofManager::~ProofManager() {} - -ProofManager* ProofManager::currentPM() { - return smt::currentProofManager(); -} - -CoreSatProof* ProofManager::getSatProof() -{ - Assert(currentPM()->d_satProof); - return currentPM()->d_satProof.get(); -} - -CnfProof* ProofManager::getCnfProof() -{ - Assert(currentPM()->d_cnfProof); - return currentPM()->d_cnfProof.get(); -} - -void ProofManager::initSatProof(Minisat::Solver* solver) -{ - // Destroy old instance before initializing new one to avoid issues with - // registering stats - d_satProof.reset(); - d_satProof.reset(new CoreSatProof(solver, d_context, "satproof::")); -} - -void ProofManager::initCnfProof(prop::CnfStream* cnfStream, - context::Context* ctx) -{ - Assert(d_satProof != nullptr); - - d_cnfProof.reset(new CnfProof(cnfStream, ctx, "")); - - // true and false have to be setup in a special way - Node true_node = NodeManager::currentNM()->mkConst(true); - Node false_node = NodeManager::currentNM()->mkConst(false).notNode(); - - d_cnfProof->pushCurrentAssertion(true_node); - d_cnfProof->registerConvertedClause(d_satProof->getTrueUnit()); - d_cnfProof->popCurrentAssertion(); - - d_cnfProof->pushCurrentAssertion(false_node); - d_cnfProof->registerConvertedClause(d_satProof->getFalseUnit()); - d_cnfProof->popCurrentAssertion(); -} - -void ProofManager::traceDeps(TNode n, CDNodeSet* coreAssertions) -{ - Debug("cores") << "trace deps " << n << std::endl; - if ((n.isConst() && n == NodeManager::currentNM()->mkConst(true)) || - (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst(false))) { - return; - } - if (d_inputCoreFormulas.find(n) != d_inputCoreFormulas.end()) - { - // originating formula was in core set - Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl; - coreAssertions->insert(n); - } else { - Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl; - if(d_deps.find(n) == d_deps.end()) { - InternalError() - << "Cannot trace dependence information back to input assertion:\n`" - << n << "'"; - } - Assert(d_deps.find(n) != d_deps.end()); - std::vector deps = (*d_deps.find(n)).second; - - for(std::vector::const_iterator i = deps.begin(); i != deps.end(); ++i) { - Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl; - if( !(*i).isNull() ){ - traceDeps(*i, coreAssertions); - } - } - } -} - -void ProofManager::traceUnsatCore() { - Assert(options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF); - d_satProof->refreshProof(); - IdToSatClause used_lemmas; - IdToSatClause used_inputs; - d_satProof->collectClausesUsed(used_inputs, - used_lemmas); - - // At this point, there should be no assertions without a clause id - Assert(d_cnfProof->isAssertionStackEmpty()); - - IdToSatClause::const_iterator it = used_inputs.begin(); - for(; it != used_inputs.end(); ++it) { - Node node = d_cnfProof->getAssertionForClause(it->first); - - Debug("cores") << "core input assertion " << node << "\n"; - // trace dependences back to actual assertions - // (this adds them to the unsat core) - traceDeps(node, &d_outputCoreFormulas); - } -} - -bool ProofManager::unsatCoreAvailable() const { - return d_satProof->derivedEmptyClause(); -} - -std::vector ProofManager::extractUnsatCore() -{ - std::vector result; - output_core_iterator it = begin_unsat_core(); - output_core_iterator end = end_unsat_core(); - while ( it != end ) { - result.push_back(*it); - ++it; - } - return result; -} - -void ProofManager::constructSatProof() -{ - if (!d_satProof->proofConstructed()) - { - d_satProof->constructProof(); - } -} - -void ProofManager::getLemmasInUnsatCore(std::vector& lemmas) -{ - Assert(options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - << "Cannot compute unsat core when proofs are off"; - Assert(unsatCoreAvailable()) - << "Cannot get unsat core at this time. Mabye the input is SAT?"; - constructSatProof(); - IdToSatClause used_lemmas; - IdToSatClause used_inputs; - d_satProof->collectClausesUsed(used_inputs, used_lemmas); - Debug("pf::lemmasUnsatCore") << "Retrieving all lemmas in unsat core\n"; - IdToSatClause::const_iterator it; - for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) - { - Node lemma = d_cnfProof->getAssertionForClause(it->first); - Debug("pf::lemmasUnsatCore") << "Retrieved lemma " << lemma << "\n"; - lemmas.push_back(lemma); - } -} - -void ProofManager::addCoreAssertion(Node formula) -{ - Debug("cores") << "assert: " << formula << std::endl; - d_deps[formula]; // empty vector of deps - d_inputCoreFormulas.insert(formula); -} - -void ProofManager::addDependence(TNode n, TNode dep) { - if(dep != n) { - Debug("cores") << "dep: " << n << " : " << dep << std::endl; - if( !dep.isNull() && d_deps.find(dep) == d_deps.end()) { - Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl; - } - std::vector deps = d_deps[n].get(); - deps.push_back(dep); - d_deps[n].set(deps); - } -} - -void ProofManager::addUnsatCore(Node formula) -{ - Assert(d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end()); - d_outputCoreFormulas.insert(formula); -} - -} // namespace cvc5 diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h deleted file mode 100644 index 8d1bbc70c..000000000 --- a/src/proof/proof_manager.h +++ /dev/null @@ -1,124 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Liana Hadarean, Haniel Barbosa, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A manager for Proofs. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__PROOF_MANAGER_H -#define CVC5__PROOF_MANAGER_H - -#include -#include -#include - -#include "context/cdhashmap.h" -#include "context/cdhashset.h" -#include "expr/node.h" -#include "proof/clause_id.h" - -namespace cvc5 { - -// forward declarations -namespace Minisat { - class Solver; -}/* Minisat namespace */ - -namespace prop { - class CnfStream; - } // namespace prop - -class SmtEngine; - -template class TSatProof; -typedef TSatProof CoreSatProof; - -class CnfProof; - -typedef TSatProof CoreSatProof; - -namespace prop { - typedef uint64_t SatVariable; - class SatLiteral; - typedef std::vector SatClause; - } // namespace prop - -typedef std::unordered_map IdToSatClause; -typedef context::CDHashSet CDNodeSet; -typedef context::CDHashMap> CDNodeToNodes; -typedef std::unordered_set IdHashSet; - -class ProofManager { - context::Context* d_context; - - std::unique_ptr d_satProof; - std::unique_ptr d_cnfProof; - - // information that will need to be shared across proofs - CDNodeSet d_inputCoreFormulas; - CDNodeSet d_outputCoreFormulas; - - int d_nextId; - - CDNodeToNodes d_deps; - -public: - ProofManager(context::Context* context); - ~ProofManager(); - - static ProofManager* currentPM(); - - // initialization - void initSatProof(Minisat::Solver* solver); - void initCnfProof(cvc5::prop::CnfStream* cnfStream, context::Context* ctx); - - // getting various proofs - static CoreSatProof* getSatProof(); - static CnfProof* getCnfProof(); - - /** Public unsat core methods **/ - void addCoreAssertion(Node formula); - - void addDependence(TNode n, TNode dep); - void addUnsatCore(Node formula); - - // trace dependences back to unsat core - void traceDeps(TNode n, CDNodeSet* coreAssertions); - void traceUnsatCore(); - - typedef CDNodeSet::const_iterator output_core_iterator; - - output_core_iterator begin_unsat_core() const - { - return d_outputCoreFormulas.begin(); - } - output_core_iterator end_unsat_core() const - { - return d_outputCoreFormulas.end(); - } - size_t size_unsat_core() const { return d_outputCoreFormulas.size(); } - std::vector extractUnsatCore(); - - bool unsatCoreAvailable() const; - void getLemmasInUnsatCore(std::vector& lemmas); - - int nextId() { return d_nextId++; } - -private: - void constructSatProof(); - -};/* class ProofManager */ - -} // namespace cvc5 - -#endif /* CVC5__PROOF_MANAGER_H */ diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h deleted file mode 100644 index b85d0bc08..000000000 --- a/src/proof/sat_proof.h +++ /dev/null @@ -1,368 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Liana Hadarean, Tim King, Andres Noetzli - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Resolution proof. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__SAT__PROOF_H -#define CVC5__SAT__PROOF_H - -#include -#include -#include -#include -#include - -#include "context/cdhashmap.h" -#include "context/cdmaybe.h" -#include "expr/node.h" -#include "proof/clause_id.h" -#include "proof/proof_manager.h" -#include "util/statistics_stats.h" - -// Forward declarations. -namespace cvc5 { -class CnfProof; -} // namespace cvc5 - -namespace cvc5 { -/** - * Helper debugging functions - */ -template -void printDebug(typename Solver::TLit l); -template -void printDebug(typename Solver::TClause& c); - -enum ClauseKind { - INPUT, - THEORY_LEMMA, // we need to distinguish because we must reprove deleted - // theory lemmas - LEARNT -}; /* enum ClauseKind */ - -template -struct ResStep { - typename Solver::TLit lit; - ClauseId id; - bool sign; - ResStep(typename Solver::TLit l, ClauseId i, bool s) - : lit(l), id(i), sign(s) {} -}; /* struct ResStep */ - -template -class ResChain { - public: - typedef std::vector > ResSteps; - typedef std::set LitSet; - - ResChain(ClauseId start); - ~ResChain(); - - void addStep(typename Solver::TLit, ClauseId, bool); - bool redundantRemoved() { - return (d_redundantLits == NULL || d_redundantLits->empty()); - } - void addRedundantLit(typename Solver::TLit lit); - - // accessor methods - ClauseId getStart() const { return d_start; } - const ResSteps& getSteps() const { return d_steps; } - LitSet* getRedundant() const { return d_redundantLits; } - - private: - ClauseId d_start; - ResSteps d_steps; - LitSet* d_redundantLits; -}; /* class ResChain */ - -template -class TSatProof { - protected: - typedef ResChain ResolutionChain; - - typedef std::set LitSet; - typedef std::set VarSet; - typedef std::unordered_map IdCRefMap; - typedef std::unordered_map ClauseIdMap; - typedef context::CDHashMap IdUnitMap; - typedef context::CDHashMap UnitIdMap; - typedef context::CDHashMap IdResMap; - typedef std::unordered_map IdProofRuleMap; - typedef std::vector ResStack; - typedef std::set IdSet; - typedef std::vector LitVector; - typedef std::unordered_map - IdToMinisatClause; - typedef std::unordered_map IdToConflicts; - - public: - TSatProof(Solver* solver, context::Context* context, - const std::string& name, bool checkRes = false); - ~TSatProof(); - - void startResChain(typename Solver::TLit start); - void startResChain(typename Solver::TCRef start); - void addResolutionStep(typename Solver::TLit lit, - typename Solver::TCRef clause, bool sign); - /** - * Pops the current resolution of the stack and stores it - * in the resolution map. Also registers the 'clause' parameter - * @param clause the clause the resolution is proving - */ - // void endResChain(typename Solver::TCRef clause); - void endResChain(typename Solver::TLit lit); - void endResChain(ClauseId id); - - /** - * Pops the current resolution of the stack *without* storing it. - */ - void cancelResChain(); - - /** - * Stores in the current derivation the redundant literals that were - * eliminated from the conflict clause during conflict clause minimization. - * @param lit the eliminated literal - */ - void storeLitRedundant(typename Solver::TLit lit); - - /// update the CRef Id maps when Minisat does memory reallocation x - void updateCRef(typename Solver::TCRef old_ref, - typename Solver::TCRef new_ref); - void finishUpdateCRef(); - - /** - * Constructs the empty clause resolution from the final conflict - * - * @param conflict - */ - void finalizeProof(typename Solver::TCRef conflict); - - /// clause registration methods - - ClauseId registerClause(const typename Solver::TCRef clause, ClauseKind kind); - ClauseId registerUnitClause(const typename Solver::TLit lit, ClauseKind kind); - void registerTrueLit(const typename Solver::TLit lit); - void registerFalseLit(const typename Solver::TLit lit); - - ClauseId getTrueUnit() const; - ClauseId getFalseUnit() const; - - void registerAssumption(const typename Solver::TVar var); - ClauseId registerAssumptionConflict(const typename Solver::TLitVec& confl); - - ClauseId storeUnitConflict(typename Solver::TLit lit, ClauseKind kind); - - /** - * Marks the deleted clauses as deleted. Note we may still use them in the - * final - * resolution. - * @param clause - */ - void markDeleted(typename Solver::TCRef clause); - bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); } - /** - * Constructs the resolution of ~q and resolves it with the current - * resolution thus eliminating q from the current clause - * @param q the literal to be resolved out - */ - void resolveOutUnit(typename Solver::TLit q); - /** - * Constructs the resolution of the literal lit. Called when a clause - * containing lit becomes satisfied and is removed. - * @param lit - */ - void storeUnitResolution(typename Solver::TLit lit); - - /** - * Constructs the SAT proof for the given clause, - * by collecting the needed clauses in the d_seen - * data-structures, also notifying the proofmanager. - */ - void constructProof(ClauseId id); - void constructProof() { constructProof(d_emptyClauseId); } - void refreshProof(ClauseId id); - void refreshProof() { refreshProof(d_emptyClauseId); } - bool proofConstructed() const; - void collectClauses(ClauseId id); - bool derivedEmptyClause() const; - prop::SatClause* buildClause(ClauseId id); - - void collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas); - - void storeClauseGlue(ClauseId clause, int glue); - - bool isInputClause(ClauseId id) const; - bool isLemmaClause(ClauseId id) const; - bool isAssumptionConflict(ClauseId id) const; - - bool hasResolutionChain(ClauseId id) const; - - /** Returns the resolution chain associated with id. Assert fails if - * hasResolution(id) does not hold. */ - const ResolutionChain& getResolutionChain(ClauseId id) const; - - const ClauseId& getEmptyClauseId() const { return d_emptyClauseId; } - const IdSet& getSeenLearnt() const { return d_seenLearnt; } - const IdToConflicts& getAssumptionConflicts() const - { - return d_assumptionConflictsDebug; - } - - private: - bool isUnit(ClauseId id) const; - typename Solver::TLit getUnit(ClauseId id) const; - - bool isUnit(typename Solver::TLit lit) const; - ClauseId getUnitId(typename Solver::TLit lit) const; - - void createLitSet(ClauseId id, LitSet& set); - - /** - * Registers a ClauseId with a resolution chain res. - * Takes ownership of the memory associated with res. - */ - void registerResolution(ClauseId id, ResolutionChain* res); - - - bool hasClauseIdForCRef(typename Solver::TCRef clause) const; - ClauseId getClauseIdForCRef(typename Solver::TCRef clause) const; - - bool hasClauseIdForLiteral(typename Solver::TLit lit) const; - ClauseId getClauseIdForLiteral(typename Solver::TLit lit) const; - - bool hasClauseRef(ClauseId id) const; - typename Solver::TCRef getClauseRef(ClauseId id) const; - - - const typename Solver::TClause& getClause(typename Solver::TCRef ref) const; - - void getLitVec(ClauseId id, LitVector& vec); - - bool checkResolution(ClauseId id); - - /** - * Constructs a resolution tree that proves lit - * and returns the ClauseId for the unit clause lit - * @param lit the literal we are proving - * - * @return - */ - ClauseId resolveUnit(typename Solver::TLit lit); - - /** - * Does a depth first search on removed literals and adds the literals - * to be removed in the proper order to the stack. - * - * @param lit the literal we are recursing on - * @param removedSet the previously computed set of redundant literals - * @param removeStack the stack of literals in reverse order of resolution - */ - void removedDfs(typename Solver::TLit lit, LitSet* removedSet, - LitVector& removeStack, LitSet& inClause, LitSet& seen); - void removeRedundantFromRes(ResChain* res, ClauseId id); - - void print(ClauseId id) const; - void printRes(ClauseId id) const; - void printRes(const ResolutionChain& res) const; - - std::unordered_map d_glueMap; - struct Statistics { - IntStat d_numLearnedClauses; - IntStat d_numLearnedInProof; - IntStat d_numLemmasInProof; - AverageStat d_avgChainLength; - HistogramStat d_resChainLengths; - HistogramStat d_usedResChainLengths; - HistogramStat d_clauseGlue; - HistogramStat d_usedClauseGlue; - Statistics(const std::string& name); - }; - - const ClauseId d_emptyClauseId; - IdSet d_seenLearnt; - IdToConflicts d_assumptionConflictsDebug; - - // Internal data. - Solver* d_solver; - context::Context* d_context; - - // clauses - IdCRefMap d_idClause; - ClauseIdMap d_clauseId; - IdUnitMap d_idUnit; - UnitIdMap d_unitId; - IdHashSet d_deleted; - IdToSatClause d_deletedTheoryLemmas; - - IdHashSet d_inputClauses; - IdHashSet d_lemmaClauses; - VarSet d_assumptions; // assumption literals for bv solver - IdHashSet d_assumptionConflicts; // assumption conflicts not actually added - // to SAT solver - - // Resolutions. - - /** - * Map from ClauseId to resolution chain corresponding proving the - * clause corresponding to the ClauseId. d_resolutionChains owns the - * memory of the ResChain* it contains. - */ - IdResMap d_resolutionChains; - - /* - * Stack containting current ResChain* we are working on. d_resStack - * owns the memory for the ResChain* it contains. Invariant: no - * ResChain* pointer can be both in d_resStack and - * d_resolutionChains. Memory ownership is transfered from - * d_resStack to d_resolutionChains via registerResolution. - */ - ResStack d_resStack; - bool d_checkRes; - - const ClauseId d_nullId; - - // temporary map for updating CRefs - ClauseIdMap d_temp_clauseId; - IdCRefMap d_temp_idClause; - - // unit conflict - context::CDMaybe d_unitConflictId; - - ClauseId d_trueLit; - ClauseId d_falseLit; - - IdToSatClause d_seenInputs; - IdToSatClause d_seenLemmas; - - bool d_satProofConstructed; - Statistics d_statistics; -}; /* class TSatProof */ - -template -prop::SatLiteral toSatLiteral(typename Solver::TLit lit); - -/** - * Convert from minisat clause to SatClause - * - * @param minisat_cl - * @param sat_cl - */ -template -void toSatClause(const typename Solver::TClause& minisat_cl, - prop::SatClause& sat_cl); - -} // namespace cvc5 - -#endif /* CVC5__SAT__PROOF_H */ diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h deleted file mode 100644 index c411ae741..000000000 --- a/src/proof/sat_proof_implementation.h +++ /dev/null @@ -1,1047 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Liana Hadarean, Tim King, Guy Katz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Resolution proof. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__SAT__PROOF_IMPLEMENTATION_H -#define CVC5__SAT__PROOF_IMPLEMENTATION_H - -#include "proof/clause_id.h" -#include "proof/sat_proof.h" -#include "prop/minisat/core/Solver.h" -#include "prop/minisat/minisat.h" -#include "prop/sat_solver_types.h" -#include "smt/smt_statistics_registry.h" - -namespace cvc5 { - -template -void printLit(typename Solver::TLit l) { - Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1; -} - -template -void printClause(const typename Solver::TClause& c) { - for (int i = 0; i < c.size(); i++) { - Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; - } -} - -template -void printClause(const std::vector& c) { - for (unsigned i = 0; i < c.size(); i++) { - Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; - } -} - -template -void printLitSet(const std::set& s) { - typename std::set::const_iterator it = s.begin(); - for (; it != s.end(); ++it) { - printLit(*it); - Debug("proof:sat") << " "; - } - Debug("proof:sat") << std::endl; -} - -// purely debugging functions -template -void printDebug(typename Solver::TLit l) { - Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << std::endl; -} -template -void printDebug(typename Solver::TClause& c) { - for (int i = 0; i < c.size(); i++) { - Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; - } - Debug("proof:sat") << std::endl; -} - -/** - * Converts the clause associated to id to a set of literals - * - * @param id the clause id - * @param set the clause converted to a set of literals - */ -template -void TSatProof::createLitSet(ClauseId id, LitSet& set) { - Assert(set.empty()); - if (isUnit(id)) { - set.insert(getUnit(id)); - return; - } - if (id == d_emptyClauseId) { - return; - } - // if it's an assumption - if (d_assumptionConflictsDebug.find(id) != d_assumptionConflictsDebug.end()) { - LitVector* clause = d_assumptionConflictsDebug[id]; - for (unsigned i = 0; i < clause->size(); ++i) { - set.insert(clause->operator[](i)); - } - return; - } - - typename Solver::TCRef ref = getClauseRef(id); - const typename Solver::TClause& c = getClause(ref); - for (int i = 0; i < c.size(); i++) { - set.insert(c[i]); - } -} - -/** - * Resolves clause1 and clause2 on variable var and stores the - * result in clause1 - * @param v - * @param clause1 - * @param clause2 - */ -template -bool resolve(const typename Solver::TLit v, - std::set& clause1, - std::set& clause2, bool s) { - Assert(!clause1.empty()); - Assert(!clause2.empty()); - typename Solver::TLit var = sign(v) ? ~v : v; - if (s) { - // literal appears positive in the first clause - if (!clause2.count(~var)) { - if (Debug.isOn("proof:sat")) { - Debug("proof:sat") << "proof:resolve: Missing literal "; - printLit(var); - Debug("proof:sat") << std::endl; - } - return false; - } - clause1.erase(var); - clause2.erase(~var); - typename std::set::iterator it = clause2.begin(); - for (; it != clause2.end(); ++it) { - clause1.insert(*it); - } - } else { - // literal appears negative in the first clause - if (!clause1.count(~var) || !clause2.count(var)) { - if (Debug.isOn("proof:sat")) { - Debug("proof:sat") << "proof:resolve: Missing literal "; - printLit(var); - Debug("proof:sat") << std::endl; - } - return false; - } - clause1.erase(~var); - clause2.erase(var); - typename std::set::iterator it = clause2.begin(); - for (; it != clause2.end(); ++it) { - clause1.insert(*it); - } - } - return true; -} - -/// ResChain -template -ResChain::ResChain(ClauseId start) - : d_start(start), d_steps(), d_redundantLits(NULL) {} - -template -ResChain::~ResChain() { - if (d_redundantLits != NULL) { - delete d_redundantLits; - } -} - -template -void ResChain::addStep(typename Solver::TLit lit, ClauseId id, - bool sign) { - ResStep step(lit, id, sign); - d_steps.push_back(step); -} - -template -void ResChain::addRedundantLit(typename Solver::TLit lit) { - if (d_redundantLits) { - d_redundantLits->insert(lit); - } else { - d_redundantLits = new LitSet(); - d_redundantLits->insert(lit); - } -} - -/// SatProof -template -TSatProof::TSatProof(Solver* solver, - context::Context* context, - const std::string& name, - bool checkRes) - : d_emptyClauseId(ClauseIdEmpty), - d_seenLearnt(), - d_assumptionConflictsDebug(), - d_solver(solver), - d_context(context), - d_idClause(), - d_clauseId(), - d_idUnit(context), - d_unitId(context), - d_deleted(), - d_inputClauses(), - d_lemmaClauses(), - d_assumptions(), - d_assumptionConflicts(), - d_resolutionChains(d_context), - d_resStack(), - d_checkRes(checkRes), - d_nullId(-2), - d_temp_clauseId(), - d_temp_idClause(), - d_unitConflictId(context), - d_trueLit(ClauseIdUndef), - d_falseLit(ClauseIdUndef), - d_seenInputs(), - d_seenLemmas(), - d_satProofConstructed(false), - d_statistics(name) -{ -} - -template -TSatProof::~TSatProof() { - // FIXME: double free if deleted clause also appears in d_seenLemmas? - IdToSatClause::const_iterator it = d_deletedTheoryLemmas.begin(); - IdToSatClause::const_iterator end = d_deletedTheoryLemmas.end(); - - for (; it != end; ++it) { - ClauseId id = it->first; - // otherwise deleted in next loop - if (d_seenLemmas.find(id) == d_seenLemmas.end()) { - delete it->second; - } - } - - IdToSatClause::const_iterator seen_lemma_it = d_seenLemmas.begin(); - IdToSatClause::const_iterator seen_lemma_end = d_seenLemmas.end(); - - for (; seen_lemma_it != seen_lemma_end; ++seen_lemma_it) { - delete seen_lemma_it->second; - } - - IdToSatClause::const_iterator seen_input_it = d_seenInputs.begin(); - IdToSatClause::const_iterator seen_input_end = d_seenInputs.end(); - - for (; seen_input_it != seen_input_end; ++seen_input_it) { - delete seen_input_it->second; - } - - typedef typename IdResMap::const_iterator ResolutionChainIterator; - ResolutionChainIterator resolution_it = d_resolutionChains.begin(); - ResolutionChainIterator resolution_it_end = d_resolutionChains.end(); - for (; resolution_it != resolution_it_end; ++resolution_it) { - ResChain* current = (*resolution_it).second; - delete current; - } - - // It could be the case that d_resStack is not empty at destruction time - // (for example in the SAT case). - typename ResStack::const_iterator resolution_stack_it = d_resStack.begin(); - typename ResStack::const_iterator resolution_stack_it_end = d_resStack.end(); - for (; resolution_stack_it != resolution_stack_it_end; - ++resolution_stack_it) { - ResChain* current = *resolution_stack_it; - delete current; - } -} - -/** - * Returns true if the resolution chain corresponding to id - * does resolve to the clause associated to id - * @param id - * - * @return - */ -template -bool TSatProof::checkResolution(ClauseId id) { - if (d_checkRes) { - bool validRes = true; - Assert(hasResolutionChain(id)); - const ResolutionChain& res = getResolutionChain(id); - LitSet clause1; - createLitSet(res.getStart(), clause1); - const typename ResolutionChain::ResSteps& steps = res.getSteps(); - for (unsigned i = 0; i < steps.size(); i++) { - typename Solver::TLit var = steps[i].lit; - LitSet clause2; - createLitSet(steps[i].id, clause2); - if (!resolve(var, clause1, clause2, steps[i].sign)) - { - validRes = false; - break; - } - } - // compare clause we claimed to prove with the resolution result - if (isUnit(id)) { - // special case if it was a unit clause - typename Solver::TLit unit = getUnit(id); - validRes = clause1.size() == clause1.count(unit) && !clause1.empty(); - return validRes; - } - if (id == d_emptyClauseId) { - return clause1.empty(); - } - - LitVector c; - getLitVec(id, c); - - for (unsigned i = 0; i < c.size(); ++i) { - int count = clause1.erase(c[i]); - if (count == 0) { - if (Debug.isOn("proof:sat")) { - Debug("proof:sat") - << "proof:checkResolution::literal not in computed result "; - printLit(c[i]); - Debug("proof:sat") << "\n"; - } - validRes = false; - } - } - validRes = clause1.empty(); - if (!validRes) { - if (Debug.isOn("proof:sat")) { - Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, " - "unremoved literals: \n"; - printLitSet(clause1); - Debug("proof:sat") << "proof:checkResolution:: result should be: \n"; - printClause(c); - } - } - return validRes; - - } else { - return true; - } -} - -/// helper methods -template -bool TSatProof::hasClauseIdForCRef(typename Solver::TCRef ref) const { - return d_clauseId.find(ref) != d_clauseId.end(); -} - -template -ClauseId TSatProof::getClauseIdForCRef( - typename Solver::TCRef ref) const { - if (d_clauseId.find(ref) == d_clauseId.end()) { - Debug("proof:sat") << "Missing clause \n"; - } - Assert(hasClauseIdForCRef(ref)); - return d_clauseId.find(ref)->second; -} - -template -bool TSatProof::hasClauseIdForLiteral(typename Solver::TLit lit) const { - return d_unitId.find(toInt(lit)) != d_unitId.end(); -} - -template -ClauseId TSatProof::getClauseIdForLiteral( - typename Solver::TLit lit) const { - Assert(hasClauseIdForLiteral(lit)); - return (*d_unitId.find(toInt(lit))).second; -} - -template -bool TSatProof::hasClauseRef(ClauseId id) const { - return d_idClause.find(id) != d_idClause.end(); -} - -template -typename Solver::TCRef TSatProof::getClauseRef(ClauseId id) const { - if (!hasClauseRef(id)) { - Debug("proof:sat") << "proof:getClauseRef cannot find clause " << id << " " - << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" - : "") - << (isUnit(id) ? "Unit" : "") << std::endl; - } - Assert(hasClauseRef(id)); - return d_idClause.find(id)->second; -} - -template -const typename Solver::TClause& TSatProof::getClause( - typename Solver::TCRef ref) const { - Assert(ref != Solver::TCRef_Undef); - Assert(ref >= 0 && ref < d_solver->ca.size()); - return d_solver->ca[ref]; -} - -template -void TSatProof::getLitVec(ClauseId id, LitVector& vec) { - if (isUnit(id)) { - typename Solver::TLit lit = getUnit(id); - vec.push_back(lit); - return; - } - if (isAssumptionConflict(id)) { - vec = *(d_assumptionConflictsDebug[id]); - return; - } - typename Solver::TCRef cref = getClauseRef(id); - const typename Solver::TClause& cl = getClause(cref); - for (int i = 0; i < cl.size(); ++i) { - vec.push_back(cl[i]); - } -} - -template -bool TSatProof::isUnit(ClauseId id) const { - return d_idUnit.find(id) != d_idUnit.end(); -} - -template -typename Solver::TLit TSatProof::getUnit(ClauseId id) const { - Assert(isUnit(id)); - return (*d_idUnit.find(id)).second; -} - -template -bool TSatProof::isUnit(typename Solver::TLit lit) const { - return d_unitId.find(toInt(lit)) != d_unitId.end(); -} - -template -ClauseId TSatProof::getUnitId(typename Solver::TLit lit) const { - Assert(isUnit(lit)); - return (*d_unitId.find(toInt(lit))).second; -} - -template -bool TSatProof::hasResolutionChain(ClauseId id) const { - return d_resolutionChains.find(id) != d_resolutionChains.end(); -} - -template -const typename TSatProof::ResolutionChain& -TSatProof::getResolutionChain(ClauseId id) const { - Assert(hasResolutionChain(id)); - const ResolutionChain* chain = (*d_resolutionChains.find(id)).second; - return *chain; -} - -template -bool TSatProof::isInputClause(ClauseId id) const { - return d_inputClauses.find(id) != d_inputClauses.end(); -} - -template -bool TSatProof::isLemmaClause(ClauseId id) const { - return d_lemmaClauses.find(id) != d_lemmaClauses.end(); -} - -template -bool TSatProof::isAssumptionConflict(ClauseId id) const { - return d_assumptionConflicts.find(id) != d_assumptionConflicts.end(); -} - -template -void TSatProof::print(ClauseId id) const { - if (d_deleted.find(id) != d_deleted.end()) { - Debug("proof:sat") << "del" << id; - } else if (isUnit(id)) { - printLit(getUnit(id)); - } else if (id == d_emptyClauseId) { - Debug("proof:sat") << "empty " << std::endl; - } else { - typename Solver::TCRef ref = getClauseRef(id); - printClause(getClause(ref)); - } -} - -template -void TSatProof::printRes(ClauseId id) const { - Assert(hasResolutionChain(id)); - Debug("proof:sat") << "id " << id << ": "; - printRes(getResolutionChain(id)); -} - -template -void TSatProof::printRes(const ResolutionChain& res) const { - ClauseId start_id = res.getStart(); - - if (Debug.isOn("proof:sat")) { - Debug("proof:sat") << "("; - print(start_id); - } - - const typename ResolutionChain::ResSteps& steps = res.getSteps(); - for (unsigned i = 0; i < steps.size(); i++) { - typename Solver::TLit v = steps[i].lit; - ClauseId id = steps[i].id; - - if (Debug.isOn("proof:sat")) { - Debug("proof:sat") << "["; - printLit(v); - Debug("proof:sat") << "] "; - print(id); - } - } - Debug("proof:sat") << ") \n"; -} - -/// registration methods -template -ClauseId TSatProof::registerClause(typename Solver::TCRef clause, - ClauseKind kind) { - Assert(clause != Solver::TCRef_Undef); - typename ClauseIdMap::iterator it = d_clauseId.find(clause); - if (it == d_clauseId.end()) { - ClauseId newId = ProofManager::currentPM()->nextId(); - - d_clauseId.insert(std::make_pair(clause, newId)); - d_idClause.insert(std::make_pair(newId, clause)); - if (kind == INPUT) { - Assert(d_inputClauses.find(newId) == d_inputClauses.end()); - d_inputClauses.insert(newId); - } - if (kind == THEORY_LEMMA) { - Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - d_lemmaClauses.insert(newId); - Debug("pf::sat") << "TSatProof::registerClause registering a new lemma clause: " - << newId << " = " << *buildClause(newId) - << std::endl; - } - } - - ClauseId id = d_clauseId[clause]; - Assert(kind != INPUT || d_inputClauses.count(id)); - Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id)); - - Debug("proof:sat:detailed") << "registerClause CRef: " << clause - << " id: " << d_clauseId[clause] - << " kind: " << kind << "\n"; - // ProofManager::currentPM()->setRegisteredClauseId( d_clauseId[clause] ); - return id; -} - -template -ClauseId TSatProof::registerUnitClause(typename Solver::TLit lit, - ClauseKind kind) { - Debug("cores") << "registerUnitClause " << kind << std::endl; - typename UnitIdMap::iterator it = d_unitId.find(toInt(lit)); - if (it == d_unitId.end()) { - ClauseId newId = ProofManager::currentPM()->nextId(); - - if (d_unitId.find(toInt(lit)) == d_unitId.end()) - d_unitId[toInt(lit)] = newId; - if (d_idUnit.find(newId) == d_idUnit.end()) - d_idUnit[newId] = lit; - - if (kind == INPUT) { - Assert(d_inputClauses.find(newId) == d_inputClauses.end()); - Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new " - "input (UNIT CLAUSE): " - << lit << std::endl; - d_inputClauses.insert(newId); - } - if (kind == THEORY_LEMMA) { - Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new lemma (UNIT CLAUSE): " - << lit - << std::endl; - d_lemmaClauses.insert(newId); - } - } - ClauseId id = d_unitId[toInt(lit)]; - Assert(kind != INPUT || d_inputClauses.count(id)); - Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id)); - Debug("proof:sat:detailed") << "registerUnitClause id: " << id - << " kind: " << kind << "\n"; - // ProofManager::currentPM()->setRegisteredClauseId( d_unitId[toInt(lit)] ); - return id; -} -template -void TSatProof::registerTrueLit(const typename Solver::TLit lit) { - Assert(d_trueLit == ClauseIdUndef); - d_trueLit = registerUnitClause(lit, INPUT); -} - -template -void TSatProof::registerFalseLit(const typename Solver::TLit lit) { - Assert(d_falseLit == ClauseIdUndef); - d_falseLit = registerUnitClause(lit, INPUT); -} - -template -ClauseId TSatProof::getTrueUnit() const { - Assert(d_trueLit != ClauseIdUndef); - return d_trueLit; -} - -template -ClauseId TSatProof::getFalseUnit() const { - Assert(d_falseLit != ClauseIdUndef); - return d_falseLit; -} - -template -void TSatProof::registerAssumption(const typename Solver::TVar var) { - Assert(d_assumptions.find(var) == d_assumptions.end()); - d_assumptions.insert(var); -} - -template -ClauseId TSatProof::registerAssumptionConflict( - const typename Solver::TLitVec& confl) { - Debug("proof:sat:detailed") << "registerAssumptionConflict " << std::endl; - // Uniqueness is checked in the bit-vector proof - // should be vars - for (int i = 0; i < confl.size(); ++i) { - Assert(d_assumptions.find(var(confl[i])) != d_assumptions.end()); - } - ClauseId new_id = ProofManager::currentPM()->nextId(); - d_assumptionConflicts.insert(new_id); - LitVector* vec_confl = new LitVector(confl.size()); - for (int i = 0; i < confl.size(); ++i) { - vec_confl->operator[](i) = confl[i]; - } - if (Debug.isOn("proof:sat:detailed")) { - printClause(*vec_confl); - Debug("proof:sat:detailed") << "\n"; - } - - d_assumptionConflictsDebug[new_id] = vec_confl; - return new_id; -} - -template -void TSatProof::removedDfs(typename Solver::TLit lit, - LitSet* removedSet, LitVector& removeStack, - LitSet& inClause, LitSet& seen) { - // if we already added the literal return - if (seen.count(lit)) { - return; - } - - typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); - if (reason_ref == Solver::TCRef_Undef) { - seen.insert(lit); - removeStack.push_back(lit); - return; - } - - int size = getClause(reason_ref).size(); - for (int i = 1; i < size; i++) { - typename Solver::TLit v = getClause(reason_ref)[i]; - if (inClause.count(v) == 0 && seen.count(v) == 0) { - removedDfs(v, removedSet, removeStack, inClause, seen); - } - } - if (seen.count(lit) == 0) { - seen.insert(lit); - removeStack.push_back(lit); - } -} - -template -void TSatProof::removeRedundantFromRes(ResChain* res, - ClauseId id) { - LitSet* removed = res->getRedundant(); - if (removed == NULL) { - return; - } - - LitSet inClause; - createLitSet(id, inClause); - - LitVector removeStack; - LitSet seen; - for (typename LitSet::iterator it = removed->begin(); it != removed->end(); - ++it) { - removedDfs(*it, removed, removeStack, inClause, seen); - } - - for (int i = removeStack.size() - 1; i >= 0; --i) { - typename Solver::TLit lit = removeStack[i]; - typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); - ClauseId reason_id; - - if (reason_ref == Solver::TCRef_Undef) { - Assert(isUnit(~lit)); - reason_id = getUnitId(~lit); - } else { - reason_id = registerClause(reason_ref, LEARNT); - } - res->addStep(lit, reason_id, !sign(lit)); - } - removed->clear(); -} - -template -void TSatProof::registerResolution(ClauseId id, ResChain* res) { - Assert(res != NULL); - - removeRedundantFromRes(res, id); - Assert(res->redundantRemoved()); - - // Because the SAT solver can add the same clause multiple times, it - // could be the case that a resolution chain for this clause already - // exists (e.g. when removing units in addClause). - if (hasResolutionChain(id)) { - ResChain* current = (*d_resolutionChains.find(id)).second; - delete current; - } - - d_resolutionChains.insert(id, res); - - if (Debug.isOn("proof:sat")) { - printRes(id); - } - if (d_checkRes) { - Assert(checkResolution(id)); - } - -} - -/// recording resolutions -template -void TSatProof::startResChain(typename Solver::TCRef start) { - ClauseId id = getClauseIdForCRef(start); - ResolutionChain* res = new ResolutionChain(id); - d_resStack.push_back(res); -} - -template -void TSatProof::startResChain(typename Solver::TLit start) { - ClauseId id = getUnitId(start); - ResolutionChain* res = new ResolutionChain(id); - d_resStack.push_back(res); -} - -template -void TSatProof::addResolutionStep(typename Solver::TLit lit, - typename Solver::TCRef clause, - bool sign) { - ClauseId id = registerClause(clause, LEARNT); - ResChain* res = d_resStack.back(); - res->addStep(lit, id, sign); -} - -template -void TSatProof::endResChain(ClauseId id) { - Debug("proof:sat:detailed") << "endResChain " << id << "\n"; - Assert(d_resStack.size() > 0); - ResChain* res = d_resStack.back(); - registerResolution(id, res); - d_resStack.pop_back(); -} - -template -void TSatProof::endResChain(typename Solver::TLit lit) { - Assert(d_resStack.size() > 0); - ClauseId id = registerUnitClause(lit, LEARNT); - Debug("proof:sat:detailed") << "endResChain unit " << id << "\n"; - ResolutionChain* res = d_resStack.back(); - d_glueMap[id] = 1; - registerResolution(id, res); - d_resStack.pop_back(); -} - -template -void TSatProof::cancelResChain() { - Assert(d_resStack.size() > 0); - ResolutionChain* back = d_resStack.back(); - delete back; - d_resStack.pop_back(); -} - -template -void TSatProof::storeLitRedundant(typename Solver::TLit lit) { - Assert(d_resStack.size() > 0); - ResolutionChain* res = d_resStack.back(); - res->addRedundantLit(lit); -} - -/// constructing resolutions -template -void TSatProof::resolveOutUnit(typename Solver::TLit lit) { - ClauseId id = resolveUnit(~lit); - ResChain* res = d_resStack.back(); - res->addStep(lit, id, !sign(lit)); -} -template -void TSatProof::storeUnitResolution(typename Solver::TLit lit) { - Debug("cores") << "STORE UNIT RESOLUTION" << std::endl; - resolveUnit(lit); -} -template -ClauseId TSatProof::resolveUnit(typename Solver::TLit lit) { - // first check if we already have a resolution for lit - - if (isUnit(lit)) { - ClauseId id = getClauseIdForLiteral(lit); - Assert(hasResolutionChain(id) || isInputClause(id) || isLemmaClause(id)); - return id; - } - typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); - Assert(reason_ref != Solver::TCRef_Undef); - - ClauseId reason_id = registerClause(reason_ref, LEARNT); - - ResChain* res = new ResChain(reason_id); - // Here, the call to resolveUnit() can reallocate memory in the - // clause allocator. So reload reason ptr each time. - const typename Solver::TClause& initial_reason = getClause(reason_ref); - size_t current_reason_size = initial_reason.size(); - for (size_t i = 0; i < current_reason_size; i++) { - const typename Solver::TClause& current_reason = getClause(reason_ref); - current_reason_size = current_reason.size(); - typename Solver::TLit l = current_reason[i]; - if (lit != l) { - ClauseId res_id = resolveUnit(~l); - res->addStep(l, res_id, !sign(l)); - } - } - ClauseId unit_id = registerUnitClause(lit, LEARNT); - registerResolution(unit_id, res); - return unit_id; -} - -template -ClauseId TSatProof::storeUnitConflict( - typename Solver::TLit conflict_lit, ClauseKind kind) { - Debug("cores") << "STORE UNIT CONFLICT" << std::endl; - Assert(!d_unitConflictId.isSet()); - d_unitConflictId.set(registerUnitClause(conflict_lit, kind)); - Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId.get() - << "\n"; - return d_unitConflictId.get(); -} - -template -void TSatProof::finalizeProof(typename Solver::TCRef conflict_ref) { - Assert(d_resStack.size() == 0); - Assert(conflict_ref != Solver::TCRef_Undef); - ClauseId conflict_id; - if (conflict_ref == Solver::TCRef_Lazy) { - Assert(d_unitConflictId.isSet()); - conflict_id = d_unitConflictId.get(); - - ResChain* res = new ResChain(conflict_id); - typename Solver::TLit lit = d_idUnit[conflict_id]; - ClauseId res_id = resolveUnit(~lit); - res->addStep(lit, res_id, !sign(lit)); - registerResolution(d_emptyClauseId, res); - return; - - } else { - Assert(!d_unitConflictId.isSet()); - conflict_id = registerClause(conflict_ref, LEARNT); // FIXME - } - - if (Debug.isOn("proof:sat")) { - Debug("proof:sat") << "proof::finalizeProof Final Conflict "; - print(conflict_id); - Debug("proof:sat") << std::endl; - } - - ResChain* res = new ResChain(conflict_id); - // Here, the call to resolveUnit() can reallocate memory in the - // clause allocator. So reload conflict ptr each time. - for (int i = 0; i < getClause(conflict_ref).size(); ++i) { - const typename Solver::TClause& conflict = getClause(conflict_ref); - typename Solver::TLit lit = conflict[i]; - ClauseId res_id = resolveUnit(~lit); - res->addStep(lit, res_id, !sign(lit)); - } - - registerResolution(d_emptyClauseId, res); -} - -/// CRef manager -template -void TSatProof::updateCRef(typename Solver::TCRef oldref, - typename Solver::TCRef newref) { - if (d_clauseId.find(oldref) == d_clauseId.end()) { - return; - } - ClauseId id = getClauseIdForCRef(oldref); - Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end()); - Assert(d_temp_idClause.find(id) == d_temp_idClause.end()); - d_temp_clauseId[newref] = id; - d_temp_idClause[id] = newref; -} - -template -void TSatProof::finishUpdateCRef() { - d_clauseId.swap(d_temp_clauseId); - d_temp_clauseId.clear(); - - d_idClause.swap(d_temp_idClause); - d_temp_idClause.clear(); -} - -template -void TSatProof::markDeleted(typename Solver::TCRef clause) { - if (hasClauseIdForCRef(clause)) { - ClauseId id = getClauseIdForCRef(clause); - Assert(d_deleted.find(id) == d_deleted.end()); - d_deleted.insert(id); - if (isLemmaClause(id)) { - const typename Solver::TClause& minisat_cl = getClause(clause); - prop::SatClause* sat_cl = new prop::SatClause(); - toSatClause(minisat_cl, *sat_cl); - d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); - } - } -} - -template -void TSatProof::constructProof(ClauseId conflict) { - d_satProofConstructed = true; - collectClauses(conflict); -} - -template -void TSatProof::refreshProof(ClauseId conflict) { - IdToSatClause::const_iterator seen_lemma_it = d_seenLemmas.begin(); - IdToSatClause::const_iterator seen_lemma_end = d_seenLemmas.end(); - - for (; seen_lemma_it != seen_lemma_end; ++seen_lemma_it) { - if (d_deletedTheoryLemmas.find(seen_lemma_it->first) == d_deletedTheoryLemmas.end()) - delete seen_lemma_it->second; - } - - IdToSatClause::const_iterator seen_input_it = d_seenInputs.begin(); - IdToSatClause::const_iterator seen_input_end = d_seenInputs.end(); - - for (; seen_input_it != seen_input_end; ++seen_input_it) { - delete seen_input_it->second; - } - - d_seenInputs.clear(); - d_seenLemmas.clear(); - d_seenLearnt.clear(); - - collectClauses(conflict); -} - -template -bool TSatProof::proofConstructed() const { - return d_satProofConstructed; -} - -template -prop::SatClause* TSatProof::buildClause(ClauseId id) { - if (isUnit(id)) { - typename Solver::TLit lit = getUnit(id); - prop::SatLiteral sat_lit = toSatLiteral(lit); - prop::SatClause* clause = new prop::SatClause(); - clause->push_back(sat_lit); - return clause; - } - - if (isDeleted(id)) { - prop::SatClause* clause = d_deletedTheoryLemmas.find(id)->second; - return clause; - } - - typename Solver::TCRef ref = getClauseRef(id); - const typename Solver::TClause& minisat_cl = getClause(ref); - prop::SatClause* clause = new prop::SatClause(); - toSatClause(minisat_cl, *clause); - return clause; -} - -template -bool TSatProof::derivedEmptyClause() const { - return hasResolutionChain(d_emptyClauseId); -} - -template -void TSatProof::collectClauses(ClauseId id) { - if (d_seenInputs.find(id) != d_seenInputs.end() || - d_seenLemmas.find(id) != d_seenLemmas.end() || - d_seenLearnt.find(id) != d_seenLearnt.end()) { - return; - } - - if (isInputClause(id)) { - d_seenInputs.insert(std::make_pair(id, buildClause(id))); - return; - } else if (isLemmaClause(id)) { - d_seenLemmas.insert(std::make_pair(id, buildClause(id))); - return; - } else if (!isAssumptionConflict(id)) { - d_seenLearnt.insert(id); - } - - const ResolutionChain& res = getResolutionChain(id); - const typename ResolutionChain::ResSteps& steps = res.getSteps(); - ClauseId start = res.getStart(); - collectClauses(start); - - for (size_t i = 0; i < steps.size(); i++) { - collectClauses(steps[i].id); - } -} - -template -void TSatProof::collectClausesUsed(IdToSatClause& inputs, - IdToSatClause& lemmas) { - inputs = d_seenInputs; - lemmas = d_seenLemmas; -} - -template -void TSatProof::storeClauseGlue(ClauseId clause, int glue) { - Assert(d_glueMap.find(clause) == d_glueMap.end()); - d_glueMap.insert(std::make_pair(clause, glue)); -} - -template -TSatProof::Statistics::Statistics(const std::string& prefix) - : d_numLearnedClauses( - smtStatisticsRegistry().registerInt(prefix + "NumLearnedClauses")), - d_numLearnedInProof( - smtStatisticsRegistry().registerInt(prefix + "NumLearnedInProof")), - d_numLemmasInProof( - smtStatisticsRegistry().registerInt(prefix + "NumLemmasInProof")), - d_avgChainLength(smtStatisticsRegistry().registerAverage( - prefix + "AvgResChainLength")), - d_resChainLengths(smtStatisticsRegistry().registerHistogram( - prefix + "ResChainLengthsHist")), - d_usedResChainLengths(smtStatisticsRegistry().registerHistogram( - prefix + "UsedResChainLengthsHist")), - d_clauseGlue(smtStatisticsRegistry().registerHistogram( - prefix + "ClauseGlueHist")), - d_usedClauseGlue(smtStatisticsRegistry().registerHistogram( - prefix + "UsedClauseGlueHist")) -{ -} - -inline std::ostream& operator<<(std::ostream& out, cvc5::ClauseKind k) -{ - switch (k) { - case cvc5::INPUT: out << "INPUT"; break; - case cvc5::THEORY_LEMMA: out << "THEORY_LEMMA"; break; - case cvc5::LEARNT: out << "LEARNT"; break; - default: - out << "ClauseKind Unknown! [" << unsigned(k) << "]"; - } - - return out; -} - -} // namespace cvc5 - -#endif /* CVC5__SAT__PROOF_IMPLEMENTATION_H */ 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& 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& 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& 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& 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& 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& 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& 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& 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& 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& 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& 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& 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(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(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* 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 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; public: static CRef TCRef_Undef; @@ -103,9 +101,6 @@ class Solver { /** Is the lemma removable */ vec lemmas_removable; - /** Nodes being converted to CNF */ - std::vector 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 TSatProof; -} // namespace cvc5 -namespace cvc5 { -namespace Minisat { +class Solver; //================================================================================================= // Variables, literals, lifted booleans, clauses: @@ -320,9 +314,7 @@ class ClauseAllocator : public RegionAllocator RegionAllocator::free(clauseWord32Size(c.size(), c.has_extra())); } - void reloc(CRef& cr, - ClauseAllocator& to, - cvc5::TSatProof* 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 +prop::SatLiteral toSatLiteral(typename Solver::TLit lit); + +template +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); diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 7dc2e915d..504dce71e 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -23,7 +23,6 @@ #include "options/expr_options.h" #include "options/language.h" #include "options/smt_options.h" -#include "proof/proof_manager.h" #include "smt/abstract_values.h" #include "smt/env.h" #include "smt/smt_engine.h" @@ -193,25 +192,6 @@ void Assertions::addFormula(TNode n, } } - // Give it to the old proof manager - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - if (inInput) - { // n is an input assertion - if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() - || options::checkUnsatCores()) - { - ProofManager::currentPM()->addCoreAssertion(n); - } - } - else - { - // n is the result of an unknown preprocessing step, add it to dependency - // map to null - ProofManager::currentPM()->addDependence(n, Node::null()); - } - } - // Add the normalized formula to the queue d_assertions.push_back(n, isAssumption, true); } diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index be19923af..e7870e4d7 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -104,8 +104,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // set proofs on if not yet set - if (options::unsatCores() && !options::produceProofs() - && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF) + if (options::unsatCores() && !options::produceProofs()) { if (opts.wasSetByUser(options::produceProofs)) { @@ -318,7 +317,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // new unsat core specific restrictions for proofs if (options::unsatCores() - && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF) { // no fine-graininess @@ -413,12 +411,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.set(options::produceAssertions, true); } - // whether we want to force safe unsat cores, i.e., if we are in the OLD_PROOF - // unsat core mode or ASSUMPTIONS, the new default, since other ones are - // experimental + // whether we want to force safe unsat cores, i.e., if we are in the default + // ASSUMPTIONS mode, since other ones are experimental bool safeUnsatCores = - options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF - || options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS; + options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS; // Disable options incompatible with incremental solving, unsat cores or // output an error if enabled explicitly. It is also currently incompatible diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0e1ff8878..bd38f630d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -33,7 +33,6 @@ #include "options/smt_options.h" #include "options/theory_options.h" #include "printer/printer.h" -#include "proof/proof_manager.h" #include "proof/unsat_core.h" #include "prop/prop_engine.h" #include "smt/abduction_solver.h" @@ -91,7 +90,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) d_routListener(new ResourceOutListener(*this)), d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)), d_smtSolver(nullptr), - d_proofManager(nullptr), d_model(nullptr), d_checkModels(nullptr), d_pfManager(nullptr), @@ -140,15 +138,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) // make the quantifier elimination solver d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver)); - // The ProofManager is constructed before any other proof objects such as - // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are - // initialized in TheoryEngine and PropEngine respectively. - Assert(d_proofManager == nullptr); - - // d_proofManager must be created before Options has been finished - // being parsed from the input file. Because of this, we cannot trust - // that d_env->getOption(options::unsatCores) is set correctly yet. - d_proofManager.reset(new ProofManager(getUserContext())); } bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); } @@ -317,15 +306,6 @@ SmtEngine::~SmtEngine() //destroy all passes before destroying things that they refer to d_pp->cleanup(); - // d_proofManager is always created when proofs are enabled at configure - // time. Because of this, this code should not be wrapped in PROOF() which - // additionally checks flags such as - // d_env->getOption(options::produceProofs). - // - // Note: the proof manager must be destroyed before the theory engine. - // Because the destruction of the proofs depends on contexts owned be the - // theory solvers. - d_proofManager.reset(nullptr); d_pfManager.reset(nullptr); d_ucManager.reset(nullptr); @@ -1403,12 +1383,6 @@ UnsatCore SmtEngine::getUnsatCoreInternal() "Cannot get an unsat core unless immediately preceded by " "UNSAT/ENTAILED response."); } - // use old proof infrastructure - if (!d_pfManager) - { - d_proofManager->traceUnsatCore(); // just to trigger core creation - return UnsatCore(d_proofManager->extractUnsatCore()); - } // generate with new proofs PropEngine* pe = getPropEngine(); Assert(pe != nullptr); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 924e3c974..b8cd1c3d7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -41,7 +41,6 @@ class TypeNode; class Env; class NodeManager; class TheoryEngine; -class ProofManager; class UnsatCore; class LogicRequest; class StatisticsRegistry; @@ -99,7 +98,6 @@ class SmtScope; class PfManager; class UnsatCoreManager; -ProofManager* currentProofManager(); } // namespace smt /* -------------------------------------------------------------------------- */ @@ -858,12 +856,6 @@ class CVC5_EXPORT SmtEngine /** Get a pointer to the PropEngine owned by this SmtEngine. */ prop::PropEngine* getPropEngine(); - /** - * Get a pointer to the ProofManager owned by this SmtEngine. - * TODO (project #37): this is the old proof manager and will be deleted - */ - ProofManager* getProofManager() { return d_proofManager.get(); }; - /** Get the resource manager of this SMT engine */ ResourceManager* getResourceManager() const; @@ -1076,8 +1068,6 @@ class CVC5_EXPORT SmtEngine /** The SMT solver */ std::unique_ptr d_smtSolver; - /** The (old) proof manager TODO (project #37): delete this */ - std::unique_ptr d_proofManager; /** * The SMT-level model object, which contains information about how to * print the model, as well as a pointer to the underlying TheoryModel diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 962529924..98f4c8d70 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -35,11 +35,6 @@ SmtEngine* currentSmtEngine() { bool smtEngineInScope() { return s_smtEngine_current != NULL; } -ProofManager* currentProofManager() { - Assert(s_smtEngine_current != NULL); - return s_smtEngine_current->getProofManager(); -} - ResourceManager* currentResourceManager() { return s_smtEngine_current->getResourceManager(); diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index 76bc5c641..cc231fa3c 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -27,7 +27,6 @@ namespace cvc5 { -class ProofManager; class SmtEngine; class StatisticsRegistry; @@ -36,9 +35,6 @@ namespace smt { SmtEngine* currentSmtEngine(); bool smtEngineInScope(); -// FIXME: Maybe move into SmtScope? -ProofManager* currentProofManager(); - /** get the current resource manager */ ResourceManager* currentResourceManager(); diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 34ef53194..eaf5cf82f 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -23,7 +23,6 @@ #include "expr/term_context_stack.h" #include "expr/term_conversion_proof_generator.h" #include "options/smt_options.h" -#include "proof/proof_manager.h" using namespace std; diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 0415d4271..9effdbec7 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -21,7 +21,6 @@ #include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" -#include "proof/proof_manager.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp index e53b1ed13..a3bdf10ad 100644 --- a/src/theory/quantifiers/quantifiers_macros.cpp +++ b/src/theory/quantifiers/quantifiers_macros.cpp @@ -18,7 +18,6 @@ #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" -#include "proof/proof_manager.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" #include "theory/quantifiers/quantifiers_registry.h" diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index d83c326c7..c0f1805ff 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -19,7 +19,6 @@ #include "expr/skolem_manager.h" #include "options/smt_options.h" #include "options/strings_options.h" -#include "proof/proof_manager.h" #include "smt/logic_exception.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/strings/arith_entail.h" diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 7124a8890..8885abe6b 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -20,7 +20,6 @@ #include "base/output.h" #include "options/smt_options.h" -#include "proof/proof_manager.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/uf/eq_proof.h"