diff options
| -rw-r--r-- | src/theory/engine_output_channel.cpp | 47 | ||||
| -rw-r--r-- | src/theory/engine_output_channel.h | 18 | ||||
| -rw-r--r-- | src/theory/output_channel.h | 29 |
3 files changed, 90 insertions, 4 deletions
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index 2a86c43a4..d83d2ba62 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -85,8 +85,9 @@ theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); }); + TrustNode tlem = TrustNode::mkTrustLemma(lemma); theory::LemmaStatus result = - d_engine->lemma(lemma, + d_engine->lemma(tlem.getNode(), rule, false, removable, @@ -234,8 +235,9 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl; - theory::LemmaStatus result = - d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory); + TrustNode tlem = TrustNode::mkTrustLemma(lemma); + theory::LemmaStatus result = d_engine->lemma( + tlem.getNode(), RULE_SPLIT, false, removable, false, d_theory); return result; } @@ -257,7 +259,8 @@ void EngineOutputChannel::conflict(TNode conflictNode, Assert(!proof); // Theory shouldn't be producing proofs yet ++d_statistics.conflicts; d_engine->d_outputChannelUsed = true; - d_engine->conflict(conflictNode, d_theory); + TrustNode tConf = TrustNode::mkTrustConflict(conflictNode); + d_engine->conflict(tConf.getNode(), d_theory); } void EngineOutputChannel::demandRestart() @@ -298,5 +301,41 @@ void EngineOutputChannel::handleUserAttribute(const char* attr, d_engine->handleUserAttribute(attr, t); } +void EngineOutputChannel::trustedConflict(TrustNode pconf) +{ + Assert(pconf.getKind() == TrustNodeKind::CONFLICT); + Trace("theory::conflict") + << "EngineOutputChannel<" << d_theory << ">::conflict(" << pconf.getNode() + << ")" << std::endl; + if (pconf.getGenerator() != nullptr) + { + ++d_statistics.trustedConflicts; + } + ++d_statistics.conflicts; + d_engine->d_outputChannelUsed = true; + d_engine->conflict(pconf.getNode(), d_theory); +} + +LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, + bool removable, + bool preprocess, + bool sendAtoms) +{ + Assert(plem.getKind() == TrustNodeKind::LEMMA); + if (plem.getGenerator() != nullptr) + { + ++d_statistics.trustedLemmas; + } + ++d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + // now, call the normal interface for lemma + return d_engine->lemma(plem.getNode(), + RULE_INVALID, + false, + removable, + preprocess, + sendAtoms ? d_theory : theory::THEORY_LAST); +} + } // namespace theory } // namespace CVC4 diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h index 992ef064b..d7b26928d 100644 --- a/src/theory/engine_output_channel.h +++ b/src/theory/engine_output_channel.h @@ -67,6 +67,24 @@ class EngineOutputChannel : public theory::OutputChannel void handleUserAttribute(const char* attr, theory::Theory* t) override; + /** + * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method + * sends conf on the output channel of this class whose proof can be generated + * by the generator pfg. Apart from pfg, the interface for this method is + * the same as calling OutputChannel::lemma on conf. + */ + void trustedConflict(TrustNode pconf) override; + /** + * Let plem be the pair (Node lem, ProofGenerator * pfg). + * Send lem on the output channel of this class whose proof can be generated + * by the generator pfg. Apart from pfg, the interface for this method is + * the same as calling OutputChannel::lemma on lem. + */ + LemmaStatus trustedLemma(TrustNode plem, + bool removable = false, + bool preprocess = false, + bool sendAtoms = false) override; + protected: /** * Statistics for a particular theory. diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 215ec8e0a..ff13d1b6b 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -21,9 +21,11 @@ #include <memory> +#include "expr/proof_node.h" #include "proof/proof_manager.h" #include "smt/logic_exception.h" #include "theory/interrupted.h" +#include "theory/trust_node.h" #include "util/proof.h" #include "util/resource_manager.h" @@ -188,6 +190,33 @@ class OutputChannel { */ virtual void demandRestart() {} + //---------------------------- new proof + /** + * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method + * sends conf on the output channel of this class whose proof can be generated + * by the generator pfg. Apart from pfg, the interface for this method is + * the same as OutputChannel. + */ + virtual void trustedConflict(TrustNode pconf) + { + Unreachable() << "OutputChannel::trustedConflict: no implementation" + << std::endl; + } + /** + * Let plem be the pair (Node lem, ProofGenerator * pfg). + * Send lem on the output channel of this class whose proof can be generated + * by the generator pfg. Apart from pfg, the interface for this method is + * the same as OutputChannel. + */ + virtual LemmaStatus trustedLemma(TrustNode lem, + bool removable = false, + bool preprocess = false, + bool sendAtoms = false) + { + Unreachable() << "OutputChannel::trustedLemma: no implementation" + << std::endl; + } + //---------------------------- end new proof }; /* class OutputChannel */ } // namespace theory |