diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/proof_manager.cpp | 22 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 16 | ||||
-rw-r--r-- | src/proof/unsat_core.h | 25 |
3 files changed, 34 insertions, 29 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 93b07b762..20b0e8a92 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -95,17 +95,18 @@ void ProofManager::initCnfProof(prop::CnfStream* cnfStream, d_cnfProof->popCurrentAssertion(); } - -void ProofManager::traceDeps(TNode n, CDExprSet* coreAssertions) { +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.toExpr()) != d_inputCoreFormulas.end()) { + 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.toExpr()); + coreAssertions->insert(n); } else { Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl; if(d_deps.find(n) == d_deps.end()) { @@ -151,8 +152,9 @@ bool ProofManager::unsatCoreAvailable() const { return d_satProof->derivedEmptyClause(); } -std::vector<Expr> ProofManager::extractUnsatCore() { - std::vector<Expr> result; +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 ) { @@ -190,9 +192,10 @@ void ProofManager::getLemmasInUnsatCore(std::vector<Node>& lemmas) } } -void ProofManager::addCoreAssertion(Expr formula) { +void ProofManager::addCoreAssertion(Node formula) +{ Debug("cores") << "assert: " << formula << std::endl; - d_deps[Node::fromExpr(formula)]; // empty vector of deps + d_deps[formula]; // empty vector of deps d_inputCoreFormulas.insert(formula); } @@ -208,7 +211,8 @@ void ProofManager::addDependence(TNode n, TNode dep) { } } -void ProofManager::addUnsatCore(Expr formula) { +void ProofManager::addUnsatCore(Node formula) +{ Assert(d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end()); d_outputCoreFormulas.insert(formula); } diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 1c2a1ce9a..7276f6402 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -57,7 +57,7 @@ namespace prop { }/* CVC4::prop namespace */ typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause; -typedef context::CDHashSet<Expr, ExprHashFunction> CDExprSet; +typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet; typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction> CDNodeToNodes; typedef std::unordered_set<ClauseId> IdHashSet; @@ -68,8 +68,8 @@ class ProofManager { std::unique_ptr<CnfProof> d_cnfProof; // information that will need to be shared across proofs - CDExprSet d_inputCoreFormulas; - CDExprSet d_outputCoreFormulas; + CDNodeSet d_inputCoreFormulas; + CDNodeSet d_outputCoreFormulas; int d_nextId; @@ -90,16 +90,16 @@ public: static CnfProof* getCnfProof(); /** Public unsat core methods **/ - void addCoreAssertion(Expr formula); + void addCoreAssertion(Node formula); void addDependence(TNode n, TNode dep); - void addUnsatCore(Expr formula); + void addUnsatCore(Node formula); // trace dependences back to unsat core - void traceDeps(TNode n, CDExprSet* coreAssertions); + void traceDeps(TNode n, CDNodeSet* coreAssertions); void traceUnsatCore(); - typedef CDExprSet::const_iterator output_core_iterator; + typedef CDNodeSet::const_iterator output_core_iterator; output_core_iterator begin_unsat_core() const { @@ -110,7 +110,7 @@ public: return d_outputCoreFormulas.end(); } size_t size_unsat_core() const { return d_outputCoreFormulas.size(); } - std::vector<Expr> extractUnsatCore(); + std::vector<Node> extractUnsatCore(); bool unsatCoreAvailable() const; void getLemmasInUnsatCore(std::vector<Node>& lemmas); diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h index f50cabbe6..b0e3de24e 100644 --- a/src/proof/unsat_core.h +++ b/src/proof/unsat_core.h @@ -15,7 +15,7 @@ ** \todo document this file **/ -#include "cvc4_public.h" +#include "cvc4_private.h" #ifndef CVC4__UNSAT_CORE_H #define CVC4__UNSAT_CORE_H @@ -23,29 +23,27 @@ #include <iosfwd> #include <vector> -#include "expr/expr.h" +#include "expr/node.h" namespace CVC4 { class SmtEngine; -class UnsatCore; - -std::ostream& operator<<(std::ostream& out, const UnsatCore& core) CVC4_PUBLIC; - -class CVC4_PUBLIC UnsatCore { - friend std::ostream& operator<<(std::ostream&, const UnsatCore&); +class UnsatCore +{ /** The SmtEngine we're associated with */ SmtEngine* d_smt; - std::vector<Expr> d_core; + std::vector<Node> d_core; void initMessage() const; public: UnsatCore() : d_smt(NULL) {} - UnsatCore(SmtEngine* smt, std::vector<Expr> core) : d_smt(smt), d_core(core) { + UnsatCore(SmtEngine* smt, const std::vector<Node>& core) + : d_smt(smt), d_core(core) + { initMessage(); } @@ -56,8 +54,8 @@ public: size_t size() const { return d_core.size(); } - typedef std::vector<Expr>::const_iterator iterator; - typedef std::vector<Expr>::const_iterator const_iterator; + typedef std::vector<Node>::const_iterator iterator; + typedef std::vector<Node>::const_iterator const_iterator; const_iterator begin() const; const_iterator end() const; @@ -69,6 +67,9 @@ public: };/* class UnsatCore */ +/** Print the unsat core to stream out */ +std::ostream& operator<<(std::ostream& out, const UnsatCore& core); + }/* CVC4 namespace */ #endif /* CVC4__UNSAT_CORE_H */ |