This commit removes the remaining old proof code and the code to produce unsat cores based on it.
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
[[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."
#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"
{
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;
}
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);
}
#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"
#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"
{
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)
bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
{
- Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF);
bool result = true;
bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
if (simpDidALotOfWork)
Assert(assertionsToPreprocess->getRealAssertionsEnd()
== assertionsToPreprocess->size());
Assert(!options::incrementalSolving());
- Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF);
context::Context fakeContext;
TheoryEngine* te = d_preprocContext->getTheoryEngine();
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 =
#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"
{
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);
- }
}
}
+++ /dev/null
-/******************************************************************************
- * 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<Node, bool>(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
+++ /dev/null
-/******************************************************************************
- * 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 <unordered_map>
-#include <unordered_set>
-
-#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<Node, Node> NodeToNode;
-typedef std::unordered_set<ClauseId> ClauseIdSet;
-
-typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
-typedef std::pair<Node, Node> NodePair;
-typedef std::set<NodePair> NodePairSet;
-
-typedef std::unordered_set<Node> 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<std::pair<Node, bool>> 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 */
+++ /dev/null
-/******************************************************************************
- * 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<bool>(true);
- Node false_node = NodeManager::currentNM()->mkConst<bool>(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<bool>(true)) ||
- (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(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<Node> deps = (*d_deps.find(n)).second;
-
- for(std::vector<Node>::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<Node> ProofManager::extractUnsatCore()
-{
- std::vector<Node> 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<Node>& 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<Node> 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
+++ /dev/null
-/******************************************************************************
- * 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 <memory>
-#include <unordered_map>
-#include <unordered_set>
-
-#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 Solver> class TSatProof;
-typedef TSatProof<cvc5::Minisat::Solver> CoreSatProof;
-
-class CnfProof;
-
-typedef TSatProof<cvc5::Minisat::Solver> CoreSatProof;
-
-namespace prop {
- typedef uint64_t SatVariable;
- class SatLiteral;
- typedef std::vector<SatLiteral> SatClause;
- } // namespace prop
-
-typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause;
-typedef context::CDHashSet<Node> CDNodeSet;
-typedef context::CDHashMap<Node, std::vector<Node>> CDNodeToNodes;
-typedef std::unordered_set<ClauseId> IdHashSet;
-
-class ProofManager {
- context::Context* d_context;
-
- std::unique_ptr<CoreSatProof> d_satProof;
- std::unique_ptr<CnfProof> 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<Node> extractUnsatCore();
-
- bool unsatCoreAvailable() const;
- void getLemmasInUnsatCore(std::vector<Node>& lemmas);
-
- int nextId() { return d_nextId++; }
-
-private:
- void constructSatProof();
-
-};/* class ProofManager */
-
-} // namespace cvc5
-
-#endif /* CVC5__PROOF_MANAGER_H */
+++ /dev/null
-/******************************************************************************
- * 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 <iosfwd>
-#include <set>
-#include <sstream>
-#include <unordered_map>
-#include <vector>
-
-#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 <class Solver>
-void printDebug(typename Solver::TLit l);
-template <class Solver>
-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 <class Solver>
-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 Solver>
-class ResChain {
- public:
- typedef std::vector<ResStep<Solver> > ResSteps;
- typedef std::set<typename Solver::TLit> 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 Solver>
-class TSatProof {
- protected:
- typedef ResChain<Solver> ResolutionChain;
-
- typedef std::set<typename Solver::TLit> LitSet;
- typedef std::set<typename Solver::TVar> VarSet;
- typedef std::unordered_map<ClauseId, typename Solver::TCRef> IdCRefMap;
- typedef std::unordered_map<typename Solver::TCRef, ClauseId> ClauseIdMap;
- typedef context::CDHashMap<ClauseId, typename Solver::TLit> IdUnitMap;
- typedef context::CDHashMap<int, ClauseId> UnitIdMap;
- typedef context::CDHashMap<ClauseId, ResolutionChain*> IdResMap;
- typedef std::unordered_map<ClauseId, uint64_t> IdProofRuleMap;
- typedef std::vector<ResolutionChain*> ResStack;
- typedef std::set<ClauseId> IdSet;
- typedef std::vector<typename Solver::TLit> LitVector;
- typedef std::unordered_map<ClauseId, typename Solver::TClause&>
- IdToMinisatClause;
- typedef std::unordered_map<ClauseId, LitVector*> 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<Solver>* res, ClauseId id);
-
- void print(ClauseId id) const;
- void printRes(ClauseId id) const;
- void printRes(const ResolutionChain& res) const;
-
- std::unordered_map<ClauseId, int> d_glueMap;
- struct Statistics {
- IntStat d_numLearnedClauses;
- IntStat d_numLearnedInProof;
- IntStat d_numLemmasInProof;
- AverageStat d_avgChainLength;
- HistogramStat<uint64_t> d_resChainLengths;
- HistogramStat<uint64_t> d_usedResChainLengths;
- HistogramStat<uint64_t> d_clauseGlue;
- HistogramStat<uint64_t> 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<ClauseId> d_unitConflictId;
-
- ClauseId d_trueLit;
- ClauseId d_falseLit;
-
- IdToSatClause d_seenInputs;
- IdToSatClause d_seenLemmas;
-
- bool d_satProofConstructed;
- Statistics d_statistics;
-}; /* class TSatProof */
-
-template <class Solver>
-prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
-
-/**
- * Convert from minisat clause to SatClause
- *
- * @param minisat_cl
- * @param sat_cl
- */
-template <class Solver>
-void toSatClause(const typename Solver::TClause& minisat_cl,
- prop::SatClause& sat_cl);
-
-} // namespace cvc5
-
-#endif /* CVC5__SAT__PROOF_H */
+++ /dev/null
-/******************************************************************************
- * 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 <class Solver>
-void printLit(typename Solver::TLit l) {
- Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1;
-}
-
-template <class Solver>
-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 <class Solver>
-void printClause(const std::vector<typename Solver::TLit>& c) {
- for (unsigned i = 0; i < c.size(); i++) {
- Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
- }
-}
-
-template <class Solver>
-void printLitSet(const std::set<typename Solver::TLit>& s) {
- typename std::set<typename Solver::TLit>::const_iterator it = s.begin();
- for (; it != s.end(); ++it) {
- printLit<Solver>(*it);
- Debug("proof:sat") << " ";
- }
- Debug("proof:sat") << std::endl;
-}
-
-// purely debugging functions
-template <class Solver>
-void printDebug(typename Solver::TLit l) {
- Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << std::endl;
-}
-template <class Solver>
-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 <class Solver>
-void TSatProof<Solver>::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 <class Solver>
-bool resolve(const typename Solver::TLit v,
- std::set<typename Solver::TLit>& clause1,
- std::set<typename Solver::TLit>& 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<Solver>(var);
- Debug("proof:sat") << std::endl;
- }
- return false;
- }
- clause1.erase(var);
- clause2.erase(~var);
- typename std::set<typename Solver::TLit>::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<Solver>(var);
- Debug("proof:sat") << std::endl;
- }
- return false;
- }
- clause1.erase(~var);
- clause2.erase(var);
- typename std::set<typename Solver::TLit>::iterator it = clause2.begin();
- for (; it != clause2.end(); ++it) {
- clause1.insert(*it);
- }
- }
- return true;
-}
-
-/// ResChain
-template <class Solver>
-ResChain<Solver>::ResChain(ClauseId start)
- : d_start(start), d_steps(), d_redundantLits(NULL) {}
-
-template <class Solver>
-ResChain<Solver>::~ResChain() {
- if (d_redundantLits != NULL) {
- delete d_redundantLits;
- }
-}
-
-template <class Solver>
-void ResChain<Solver>::addStep(typename Solver::TLit lit, ClauseId id,
- bool sign) {
- ResStep<Solver> step(lit, id, sign);
- d_steps.push_back(step);
-}
-
-template <class Solver>
-void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) {
- if (d_redundantLits) {
- d_redundantLits->insert(lit);
- } else {
- d_redundantLits = new LitSet();
- d_redundantLits->insert(lit);
- }
-}
-
-/// SatProof
-template <class Solver>
-TSatProof<Solver>::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 <class Solver>
-TSatProof<Solver>::~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<Solver>* 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<Solver>* 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 <class Solver>
-bool TSatProof<Solver>::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<Solver>(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<Solver>(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<Solver>(clause1);
- Debug("proof:sat") << "proof:checkResolution:: result should be: \n";
- printClause<Solver>(c);
- }
- }
- return validRes;
-
- } else {
- return true;
- }
-}
-
-/// helper methods
-template <class Solver>
-bool TSatProof<Solver>::hasClauseIdForCRef(typename Solver::TCRef ref) const {
- return d_clauseId.find(ref) != d_clauseId.end();
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::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 <class Solver>
-bool TSatProof<Solver>::hasClauseIdForLiteral(typename Solver::TLit lit) const {
- return d_unitId.find(toInt(lit)) != d_unitId.end();
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::getClauseIdForLiteral(
- typename Solver::TLit lit) const {
- Assert(hasClauseIdForLiteral(lit));
- return (*d_unitId.find(toInt(lit))).second;
-}
-
-template <class Solver>
-bool TSatProof<Solver>::hasClauseRef(ClauseId id) const {
- return d_idClause.find(id) != d_idClause.end();
-}
-
-template <class Solver>
-typename Solver::TCRef TSatProof<Solver>::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 <class Solver>
-const typename Solver::TClause& TSatProof<Solver>::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 <class Solver>
-void TSatProof<Solver>::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 <class Solver>
-bool TSatProof<Solver>::isUnit(ClauseId id) const {
- return d_idUnit.find(id) != d_idUnit.end();
-}
-
-template <class Solver>
-typename Solver::TLit TSatProof<Solver>::getUnit(ClauseId id) const {
- Assert(isUnit(id));
- return (*d_idUnit.find(id)).second;
-}
-
-template <class Solver>
-bool TSatProof<Solver>::isUnit(typename Solver::TLit lit) const {
- return d_unitId.find(toInt(lit)) != d_unitId.end();
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::getUnitId(typename Solver::TLit lit) const {
- Assert(isUnit(lit));
- return (*d_unitId.find(toInt(lit))).second;
-}
-
-template <class Solver>
-bool TSatProof<Solver>::hasResolutionChain(ClauseId id) const {
- return d_resolutionChains.find(id) != d_resolutionChains.end();
-}
-
-template <class Solver>
-const typename TSatProof<Solver>::ResolutionChain&
-TSatProof<Solver>::getResolutionChain(ClauseId id) const {
- Assert(hasResolutionChain(id));
- const ResolutionChain* chain = (*d_resolutionChains.find(id)).second;
- return *chain;
-}
-
-template <class Solver>
-bool TSatProof<Solver>::isInputClause(ClauseId id) const {
- return d_inputClauses.find(id) != d_inputClauses.end();
-}
-
-template <class Solver>
-bool TSatProof<Solver>::isLemmaClause(ClauseId id) const {
- return d_lemmaClauses.find(id) != d_lemmaClauses.end();
-}
-
-template <class Solver>
-bool TSatProof<Solver>::isAssumptionConflict(ClauseId id) const {
- return d_assumptionConflicts.find(id) != d_assumptionConflicts.end();
-}
-
-template <class Solver>
-void TSatProof<Solver>::print(ClauseId id) const {
- if (d_deleted.find(id) != d_deleted.end()) {
- Debug("proof:sat") << "del" << id;
- } else if (isUnit(id)) {
- printLit<Solver>(getUnit(id));
- } else if (id == d_emptyClauseId) {
- Debug("proof:sat") << "empty " << std::endl;
- } else {
- typename Solver::TCRef ref = getClauseRef(id);
- printClause<Solver>(getClause(ref));
- }
-}
-
-template <class Solver>
-void TSatProof<Solver>::printRes(ClauseId id) const {
- Assert(hasResolutionChain(id));
- Debug("proof:sat") << "id " << id << ": ";
- printRes(getResolutionChain(id));
-}
-
-template <class Solver>
-void TSatProof<Solver>::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<Solver>(v);
- Debug("proof:sat") << "] ";
- print(id);
- }
- }
- Debug("proof:sat") << ") \n";
-}
-
-/// registration methods
-template <class Solver>
-ClauseId TSatProof<Solver>::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 <class Solver>
-ClauseId TSatProof<Solver>::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 <class Solver>
-void TSatProof<Solver>::registerTrueLit(const typename Solver::TLit lit) {
- Assert(d_trueLit == ClauseIdUndef);
- d_trueLit = registerUnitClause(lit, INPUT);
-}
-
-template <class Solver>
-void TSatProof<Solver>::registerFalseLit(const typename Solver::TLit lit) {
- Assert(d_falseLit == ClauseIdUndef);
- d_falseLit = registerUnitClause(lit, INPUT);
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::getTrueUnit() const {
- Assert(d_trueLit != ClauseIdUndef);
- return d_trueLit;
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::getFalseUnit() const {
- Assert(d_falseLit != ClauseIdUndef);
- return d_falseLit;
-}
-
-template <class Solver>
-void TSatProof<Solver>::registerAssumption(const typename Solver::TVar var) {
- Assert(d_assumptions.find(var) == d_assumptions.end());
- d_assumptions.insert(var);
-}
-
-template <class Solver>
-ClauseId TSatProof<Solver>::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<Solver>(*vec_confl);
- Debug("proof:sat:detailed") << "\n";
- }
-
- d_assumptionConflictsDebug[new_id] = vec_confl;
- return new_id;
-}
-
-template <class Solver>
-void TSatProof<Solver>::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 <class Solver>
-void TSatProof<Solver>::removeRedundantFromRes(ResChain<Solver>* 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 <class Solver>
-void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* 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<Solver>* 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 <class Solver>
-void TSatProof<Solver>::startResChain(typename Solver::TCRef start) {
- ClauseId id = getClauseIdForCRef(start);
- ResolutionChain* res = new ResolutionChain(id);
- d_resStack.push_back(res);
-}
-
-template <class Solver>
-void TSatProof<Solver>::startResChain(typename Solver::TLit start) {
- ClauseId id = getUnitId(start);
- ResolutionChain* res = new ResolutionChain(id);
- d_resStack.push_back(res);
-}
-
-template <class Solver>
-void TSatProof<Solver>::addResolutionStep(typename Solver::TLit lit,
- typename Solver::TCRef clause,
- bool sign) {
- ClauseId id = registerClause(clause, LEARNT);
- ResChain<Solver>* res = d_resStack.back();
- res->addStep(lit, id, sign);
-}
-
-template <class Solver>
-void TSatProof<Solver>::endResChain(ClauseId id) {
- Debug("proof:sat:detailed") << "endResChain " << id << "\n";
- Assert(d_resStack.size() > 0);
- ResChain<Solver>* res = d_resStack.back();
- registerResolution(id, res);
- d_resStack.pop_back();
-}
-
-template <class Solver>
-void TSatProof<Solver>::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 <class Solver>
-void TSatProof<Solver>::cancelResChain() {
- Assert(d_resStack.size() > 0);
- ResolutionChain* back = d_resStack.back();
- delete back;
- d_resStack.pop_back();
-}
-
-template <class Solver>
-void TSatProof<Solver>::storeLitRedundant(typename Solver::TLit lit) {
- Assert(d_resStack.size() > 0);
- ResolutionChain* res = d_resStack.back();
- res->addRedundantLit(lit);
-}
-
-/// constructing resolutions
-template <class Solver>
-void TSatProof<Solver>::resolveOutUnit(typename Solver::TLit lit) {
- ClauseId id = resolveUnit(~lit);
- ResChain<Solver>* res = d_resStack.back();
- res->addStep(lit, id, !sign(lit));
-}
-template <class Solver>
-void TSatProof<Solver>::storeUnitResolution(typename Solver::TLit lit) {
- Debug("cores") << "STORE UNIT RESOLUTION" << std::endl;
- resolveUnit(lit);
-}
-template <class Solver>
-ClauseId TSatProof<Solver>::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<Solver>* res = new ResChain<Solver>(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 <class Solver>
-ClauseId TSatProof<Solver>::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 <class Solver>
-void TSatProof<Solver>::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<Solver>* res = new ResChain<Solver>(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<Solver>* res = new ResChain<Solver>(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 <class Solver>
-void TSatProof<Solver>::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 <class Solver>
-void TSatProof<Solver>::finishUpdateCRef() {
- d_clauseId.swap(d_temp_clauseId);
- d_temp_clauseId.clear();
-
- d_idClause.swap(d_temp_idClause);
- d_temp_idClause.clear();
-}
-
-template <class Solver>
-void TSatProof<Solver>::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<Solver>(minisat_cl, *sat_cl);
- d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl));
- }
- }
-}
-
-template <class Solver>
-void TSatProof<Solver>::constructProof(ClauseId conflict) {
- d_satProofConstructed = true;
- collectClauses(conflict);
-}
-
-template <class Solver>
-void TSatProof<Solver>::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 <class Solver>
-bool TSatProof<Solver>::proofConstructed() const {
- return d_satProofConstructed;
-}
-
-template <class Solver>
-prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) {
- if (isUnit(id)) {
- typename Solver::TLit lit = getUnit(id);
- prop::SatLiteral sat_lit = toSatLiteral<Solver>(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<Solver>(minisat_cl, *clause);
- return clause;
-}
-
-template <class Solver>
-bool TSatProof<Solver>::derivedEmptyClause() const {
- return hasResolutionChain(d_emptyClauseId);
-}
-
-template <class Solver>
-void TSatProof<Solver>::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 <class Solver>
-void TSatProof<Solver>::collectClausesUsed(IdToSatClause& inputs,
- IdToSatClause& lemmas) {
- inputs = d_seenInputs;
- lemmas = d_seenLemmas;
-}
-
-template <class Solver>
-void TSatProof<Solver>::storeClauseGlue(ClauseId clause, int glue) {
- Assert(d_glueMap.find(clause) == d_glueMap.end());
- d_glueMap.insert(std::make_pair(clause, glue));
-}
-
-template <class Solver>
-TSatProof<Solver>::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<uint64_t>(
- prefix + "ResChainLengthsHist")),
- d_usedResChainLengths(smtStatisticsRegistry().registerHistogram<uint64_t>(
- prefix + "UsedResChainLengthsHist")),
- d_clauseGlue(smtStatisticsRegistry().registerHistogram<uint64_t>(
- prefix + "ClauseGlueHist")),
- d_usedClauseGlue(smtStatisticsRegistry().registerHistogram<uint64_t>(
- 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 */
#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"
d_flitPolicy(flpol),
d_registrar(registrar),
d_name(name),
- d_cnfProof(nullptr),
d_removable(false),
d_resourceManager(rm)
{
ClauseId clauseId = d_satSolver->addClause(c, d_removable);
- if (d_cnfProof && clauseId != ClauseIdUndef)
- {
- d_cnfProof->registerConvertedClause(clauseId);
- }
return clauseId != ClauseIdUndef;
}
// 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);
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;
}
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";
<< ", 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)
#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"
/** 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
/** 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
#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"
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);
// 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));
- }
}
// 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);
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);
// 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);
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);
<< 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
}
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)
}
return ok;
} else {
- if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
- {
- id = ClauseIdUndef;
- }
return ok;
}
}
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]));
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]);
}
// 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);
}
}
}
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"))
{
// 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")
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();
- }
}
}
}
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
if (decisionLevel() == 0)
{
- if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
- {
- ProofManager::getSatProof()->finalizeProof(confl);
- }
if (needProof())
{
if (confl == CRef_Lazy)
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]);
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]);
vec<Watcher>& ws = watches[p];
for (int j = 0; j < ws.size(); j++)
{
- ca.reloc(ws[j].cref,
- to,
- options::unsatCoresMode()
- == options::UnsatCoresMode::OLD_PROOF
- ? ProofManager::getSatProof()
- : nullptr);
+ ca.reloc(ws[j].cref, to);
}
}
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);
}
}
// Last index in the trail
int backtrack_index = trail.size();
- Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
- || lemmas.size() == static_cast<int>(lemmas_cnf_assertion.size()));
-
// Attach all the clauses and enqueue all the propagations
for (int j = 0; j < lemmas.size(); ++j)
{
}
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 {
// 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) {
} 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]);
}
}
- Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
- || lemmas.size() == static_cast<int>(lemmas_cnf_assertion.size()));
// Clear the lemmas
lemmas.clear();
- lemmas_cnf_assertion.clear();
lemmas_removable.clear();
if (conflict != CRef_Undef) {
return conflict;
}
-void ClauseAllocator::reloc(CRef& cr,
- ClauseAllocator& to,
- cvc5::TSatProof<Solver>* proof)
+void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to)
{
Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl;
// FIXME what is this CRef_lazy
if (cr == CRef_Lazy) return;
- CRef old = cr; // save the old reference
Clause& c = operator[](cr);
if (c.reloced()) { cr = c.relocation(); return; }
cr = to.alloc(c.level(), c, c.removable());
c.relocate(cr);
- if (proof)
- {
- proof->updateCRef(old, cr);
- }
// Copy extra data-fields:
// (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
to[cr].mark(c.mark());
#include "util/resource_manager.h"
namespace cvc5 {
-template <class Solver> class TSatProof;
namespace prop {
class PropEngine;
friend class cvc5::prop::PropEngine;
friend class cvc5::prop::TheoryProxy;
friend class cvc5::prop::SatProofManager;
- friend class cvc5::TSatProof<Minisat::Solver>;
public:
static CRef TCRef_Undef;
/** Is the lemma removable */
vec<bool> lemmas_removable;
- /** Nodes being converted to CNF */
- std::vector<cvc5::Node> lemmas_cnf_assertion;
-
/** Do a another check if FULL_EFFORT was the last one */
bool recheck;
namespace cvc5 {
namespace Minisat {
-class Solver;
-}
-template <class Solver>
-class TSatProof;
-} // namespace cvc5
-namespace cvc5 {
-namespace Minisat {
+class Solver;
//=================================================================================================
// Variables, literals, lifted booleans, clauses:
RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
}
- void reloc(CRef& cr,
- ClauseAllocator& to,
- cvc5::TSatProof<Solver>* proof = NULL);
+ void reloc(CRef& cr, ClauseAllocator& to);
// Implementation moved to Solver.cc.
};
#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"
#include "util/statistics_registry.h"
namespace cvc5 {
+
+template <class Solver>
+prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
+
+template <class Solver>
+void toSatClause(const typename Solver::TClause& minisat_cl,
+ prop::SatClause& sat_cl);
+
namespace prop {
class MinisatSatSolver : public CDCLTSatSolverInterface
#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"
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()
#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"
|| 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);
#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"
}
}
- // 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);
}
}
// 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))
{
// 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
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
#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"
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),
// 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(); }
//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);
"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);
class Env;
class NodeManager;
class TheoryEngine;
-class ProofManager;
class UnsatCore;
class LogicRequest;
class StatisticsRegistry;
class PfManager;
class UnsatCoreManager;
-ProofManager* currentProofManager();
} // namespace smt
/* -------------------------------------------------------------------------- */
/** 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;
/** The SMT solver */
std::unique_ptr<smt::SmtSolver> d_smtSolver;
- /** The (old) proof manager TODO (project #37): delete this */
- std::unique_ptr<ProofManager> 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
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();
namespace cvc5 {
-class ProofManager;
class SmtEngine;
class StatisticsRegistry;
SmtEngine* currentSmtEngine();
bool smtEngineInScope();
-// FIXME: Maybe move into SmtScope?
-ProofManager* currentProofManager();
-
/** get the current resource manager */
ResourceManager* currentResourceManager();
#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;
#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"
#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"
#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"
#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"
projects / cvc5.git / commitdiff