diff options
Diffstat (limited to 'src/theory/theory_inference.h')
| -rw-r--r-- | src/theory/theory_inference.h | 27 |
1 files changed, 20 insertions, 7 deletions
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 */ |