diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-04 17:52:11 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-04 17:52:11 -0500 |
| commit | 3f150596fe2186aea1c40b3210e8a0d59dc1ba94 (patch) | |
| tree | d0e3fbe5e3e55ef59783b8b4eb3e15e1f7020a4c /src/theory/arith | |
| parent | 721ce847f4d44fb7ee2509df3b34aad49fc7f484 (diff) | |
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.
Diffstat (limited to 'src/theory/arith')
| -rw-r--r-- | src/theory/arith/nl/nl_lemma_utils.cpp | 4 | ||||
| -rw-r--r-- | src/theory/arith/nl/nl_lemma_utils.h | 2 |
2 files changed, 3 insertions, 3 deletions
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 * |