diff options
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 33 |
1 files changed, 26 insertions, 7 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 30b5d9fbb..550a4f496 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -53,6 +53,7 @@ namespace CVC4 { class ResourceManager; +class TheoryEngineProofGenerator; /** * A pair of a theory and a node. This is used to mark the flow of @@ -141,6 +142,13 @@ class TheoryEngine { //--------------------------------- new proofs /** Proof node manager used by this theory engine, if proofs are enabled */ ProofNodeManager* d_pnm; + /** The lazy proof object + * + * This stores instructions for how to construct proofs for all theory lemmas. + */ + std::shared_ptr<LazyCDProof> d_lazyProof; + /** The proof generator */ + std::shared_ptr<TheoryEngineProofGenerator> d_tepg; //--------------------------------- end new proofs /** @@ -205,8 +213,12 @@ class TheoryEngine { /** * Called by the theories to notify of a conflict. + * + * @param conflict The trust node containing the conflict and its proof + * generator (if it exists), + * @param theoryId The theory that sent the conflict */ - void conflict(TNode conflict, theory::TheoryId theoryId); + void conflict(theory::TrustNode conflict, theory::TheoryId theoryId); /** * Debugging flag to ensure that shutdown() is called before the @@ -282,13 +294,16 @@ class TheoryEngine { /** * Adds a new lemma, returning its status. * @param node the lemma - * @param negated should the lemma be asserted negated * @param p the properties of the lemma. + * @param atomsTo the theory that atoms of the lemma should be sent to + * @param from the theory that sent the lemma + * @return a lemma status, containing the lemma and context information + * about when it was sent. */ - theory::LemmaStatus lemma(TNode node, - bool negated, + theory::LemmaStatus lemma(theory::TrustNode node, theory::LemmaProperty p, - theory::TheoryId atomsTo); + theory::TheoryId atomsTo = theory::THEORY_LAST, + theory::TheoryId from = theory::THEORY_LAST); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory); @@ -437,7 +452,11 @@ class TheoryEngine { * where the node is the one to be explained, and the theory is the * theory that sent the literal. */ - void getExplanation(std::vector<NodeTheoryPair>& explanationVector); + theory::TrustNode getExplanation( + std::vector<NodeTheoryPair>& explanationVector); + + /** Are proofs enabled? */ + bool isProofEnabled() const; public: /** @@ -555,7 +574,7 @@ class TheoryEngine { /** * Returns an explanation of the node propagated to the SAT solver. */ - Node getExplanation(TNode node); + theory::TrustNode getExplanation(TNode node); /** * Get the pointer to the model object used by this theory engine. |