diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-08 19:07:52 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-08 19:07:52 -0500 |
commit | bc5056c8927e8fbffbe9e9d103f0a81f8ab49480 (patch) | |
tree | b600bdc0b38cd59bc08e248c265ad0e77af2c82c /src/theory/theory_engine.h | |
parent | 2edc04bdfdac32ce899c98c4a8887c037b1f6a3f (diff) |
(proof-new) Theory engine proof producing (#5195)
This completes proof support in TheoryEngine.
The main addition in this PR is to make its getExplanation method proof producing.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e410bddd5..fd6d1af27 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -42,6 +42,7 @@ #include "theory/term_registration_visitor.h" #include "theory/theory.h" #include "theory/theory_preprocessor.h" +#include "theory/trust_node.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" #include "util/hash.h" @@ -111,7 +112,6 @@ class TheoryEngine { /** Shared terms database can use the internals notify the theories */ friend class SharedTermsDatabase; - friend class theory::CombinationEngine; friend class theory::EngineOutputChannel; friend class theory::CombinationEngine; friend class theory::SharedSolver; @@ -175,9 +175,6 @@ class TheoryEngine { /** are we in eager model building mode? (see setEagerModelBuilding). */ bool d_eager_model_building; - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; - typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap; - /** * Output channels for individual theories. */ @@ -315,7 +312,8 @@ class TheoryEngine { ResourceManager* rm, RemoveTermFormulas& iteRemover, const LogicInfo& logic, - OutputManager& outMgr); + OutputManager& outMgr, + ProofNodeManager* pnm); /** Destroys a theory engine */ ~TheoryEngine(); @@ -339,7 +337,7 @@ class TheoryEngine { *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo, - nullptr); + d_pnm); theory::Rewriter::registerTheoryRewriter( theoryId, d_theoryTable[theoryId]->getTheoryRewriter()); } @@ -365,6 +363,9 @@ class TheoryEngine { return d_propEngine; } + /** Get the proof node manager */ + ProofNodeManager* getProofNodeManager() const; + /** * Get a pointer to the underlying sat context. */ @@ -740,7 +741,6 @@ private: private: IntStat d_arithSubstitutionsAdded; - };/* class TheoryEngine */ }/* CVC4 namespace */ |