From: Andrew Reynolds Date: Fri, 4 Sep 2020 22:52:11 +0000 (-0500) Subject: Add asLemma flag to theory inference process (#5030) X-Git-Tag: cvc5-1.0.0~2890 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f150596fe2186aea1c40b3210e8a0d59dc1ba94;p=cvc5.git Add asLemma flag to theory inference process (#5030) This is required for strings, which uses the same data structure, InferInfo, for both lemmas and facts. This ensures the process method of theory inference knows where we are a pending lemma or a pending fact. It also makes a few changes necessary for the proof-new branch, including disabling the proof node manager in the inference manager for datatypes. --- diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index 58a552815..152d4647c 100644 --- a/src/theory/arith/nl/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -22,9 +22,9 @@ namespace theory { namespace arith { namespace nl { -bool NlLemma::process(TheoryInferenceManager* im) +bool NlLemma::process(TheoryInferenceManager* im, bool asLemma) { - bool res = ArithLemma::process(im); + bool res = ArithLemma::process(im, asLemma); if (d_nlext != nullptr) { d_nlext->processSideEffect(*this); diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index 1c0635f1f..0d3a6d547 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -57,7 +57,7 @@ class NlLemma : public ArithLemma } ~NlLemma() {} - bool process(TheoryInferenceManager* im) override; + bool process(TheoryInferenceManager* im, bool asLemma) override; /** secant points to add * diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 1faf71aa9..8daa68a27 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -66,7 +66,7 @@ bool DatatypesInference::mustCommunicateFact(Node n, Node exp) return false; } -bool DatatypesInference::process(TheoryInferenceManager* im) +bool DatatypesInference::process(TheoryInferenceManager* im, bool asLemma) { // check to see if we have to communicate it to the rest of the system if (mustCommunicateFact(d_conc, d_exp)) @@ -89,7 +89,7 @@ bool DatatypesInference::process(TheoryInferenceManager* im) InferenceManager::InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, state, pnm) + : InferenceManagerBuffered(t, state, nullptr) { } diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index 0dfdfb281..794d26430 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -55,7 +55,7 @@ class DatatypesInference : public SimpleTheoryInternalFact * Process this fact, possibly as a fact or as a lemma, depending on the * above method. */ - bool process(TheoryInferenceManager* im) override; + bool process(TheoryInferenceManager* im, bool asLemma) override; }; /** diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index 3ba41a431..b0d092d74 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -86,7 +86,7 @@ void InferenceManagerBuffered::doPendingFacts() { // process this fact, which notice may enqueue more pending facts in this // loop. - d_pendingFact[i]->process(this); + d_pendingFact[i]->process(this, false); i++; } d_pendingFact.clear(); @@ -97,7 +97,7 @@ void InferenceManagerBuffered::doPendingLemmas() for (const std::unique_ptr& plem : d_pendingLem) { // process this lemma - plem->process(this); + plem->process(this, true); } d_pendingLem.clear(); } diff --git a/src/theory/theory_inference.cpp b/src/theory/theory_inference.cpp index 618dc640b..38e01eea5 100644 --- a/src/theory/theory_inference.cpp +++ b/src/theory/theory_inference.cpp @@ -28,9 +28,10 @@ SimpleTheoryLemma::SimpleTheoryLemma(Node n, { } -bool SimpleTheoryLemma::process(TheoryInferenceManager* im) +bool SimpleTheoryLemma::process(TheoryInferenceManager* im, bool asLemma) { Assert(!d_node.isNull()); + Assert(asLemma); // send (trusted) lemma on the output channel with property p return im->trustedLemma(TrustNode::mkTrustLemma(d_node, d_pg), d_property); } @@ -42,8 +43,9 @@ SimpleTheoryInternalFact::SimpleTheoryInternalFact(Node conc, { } -bool SimpleTheoryInternalFact::process(TheoryInferenceManager* im) +bool SimpleTheoryInternalFact::process(TheoryInferenceManager* im, bool asLemma) { + Assert(!asLemma); bool polarity = d_conc.getKind() != NOT; TNode atom = polarity ? d_conc : d_conc[0]; // no double negation or conjunctive conclusions diff --git a/src/theory/theory_inference.h b/src/theory/theory_inference.h index 8d98051bf..6090b5a02 100644 --- a/src/theory/theory_inference.h +++ b/src/theory/theory_inference.h @@ -40,15 +40,26 @@ class TheoryInference * method should make call(s) to inference manager to process this * inference, as well as processing any specific side effects. This method * typically makes a single call to the provided inference manager e.g. - * d_im->trustedLemma or d_im->assertFactInternal. Notice it is the sole + * d_im->trustedLemma or d_im->assertInternalFact. Notice it is the sole * responsibility of this class to make this call; the inference manager * does not call itself otherwise when processing pending inferences. * + * @param im The inference manager to use + * @param asLemma Whether this inference is being processed as a lemma + * during doPendingLemmas (otherwise it is being processed in doPendingFacts). + * Typically, this method calls lemma or conflict when asLemma is + * true, and assertInternalFact when this flag is false, although this + * behavior is (intentionally) not strictly enforced. In particular, the + * choice to send a conflict, lemma or fact may depend on local state of the + * theory, which may change while the inference is pending. Hence the + * implementation of this method may choose to implement any call to the + * inference manager. This flag simply serves to track whether the inference + * initially was added a pending lemma or not. * @return true if the inference was successfully processed by the inference * manager. This method for instance returns false if it corresponds to a * lemma that was already cached by im and hence was discarded. */ - virtual bool process(TheoryInferenceManager* im) = 0; + virtual bool process(TheoryInferenceManager* im, bool asLemma) = 0; }; /** @@ -62,9 +73,10 @@ class SimpleTheoryLemma : public TheoryInference virtual ~SimpleTheoryLemma() {} /** * Send the lemma using inference manager im, return true if the lemma was - * sent. + * sent. It should be the case that asLemma = true or an assertion failure + * is thrown. */ - virtual bool process(TheoryInferenceManager* im) override; + virtual bool process(TheoryInferenceManager* im, bool asLemma) override; /** The lemma to send */ Node d_node; /** The lemma property (see OutputChannel::lemma) */ @@ -80,7 +92,7 @@ class SimpleTheoryLemma : public TheoryInference /** * A simple internal fact with no side effects. Makes a single call to - * assertFactInternal in its process method. + * assertInternalFact in its process method. */ class SimpleTheoryInternalFact : public TheoryInference { @@ -89,9 +101,10 @@ class SimpleTheoryInternalFact : public TheoryInference virtual ~SimpleTheoryInternalFact() {} /** * Send the lemma using inference manager im, return true if the lemma was - * sent. + * sent. It should be the case that asLemma = false or an assertion failure + * is thrown. */ - virtual bool process(TheoryInferenceManager* im) override; + virtual bool process(TheoryInferenceManager* im, bool asLemma) override; /** The lemma to send */ Node d_conc; /** The explanation */ diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 801d6a266..ff6f0ebc7 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -64,6 +64,11 @@ bool TheoryInferenceManager::hasSent() const || d_numCurrentFacts > 0; } +eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine() +{ + return d_pfee.get(); +} + void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b) { if (!d_theoryState.isInConflict()) diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 97baeaa40..496a7f0f1 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -97,6 +97,8 @@ class TheoryInferenceManager * since the last call to reset. */ bool hasSent() const; + /** Get the underlying proof equality engine */ + eq::ProofEqEngine* getProofEqEngine(); //--------------------------------------- propagations /** * T-propagate literal lit, possibly encountered by equality engine,