diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-09-10 10:19:32 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-10 17:19:32 +0000 |
| commit | fd4b373b9a66a590e0d9618c744312e1050472a0 (patch) | |
| tree | 70d869506a0b80b51961da8e0a5bbe82d440b6a2 /src/theory | |
| parent | 80d5885363f12df98bfa46f76cc9594e56a25197 (diff) | |
FP: Do not send trivial lemmas. (#7167)
Fixes #7002.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/fp/theory_fp.cpp | 9 | ||||
| -rw-r--r-- | src/theory/fp/theory_fp.h | 3 |
2 files changed, 10 insertions, 2 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index ad7c1a656..075a6633f 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -72,7 +72,8 @@ TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation) d_rewriter(userContext()), d_state(env, valuation), d_im(env, *this, d_state, d_pnm, "theory::fp::", false), - d_wbFactsCache(userContext()) + d_wbFactsCache(userContext()), + d_true(d_env.getNodeManager()->mkConst(true)) { // indicate we are using the default theory state and inference manager d_theoryState = &d_state; @@ -701,7 +702,11 @@ void TheoryFp::handleLemma(Node node, InferenceId id) Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl; // will be preprocessed when sent, which is important because it contains // embedded ITEs - d_im.lemma(node, id); + if (rewrite(node) != d_true) + { + /* We only send non-trivial lemmas. */ + d_im.lemma(node, id); + } } bool TheoryFp::propagateLit(TNode node) diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 1e1041980..663be2f81 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -157,6 +157,9 @@ class TheoryFp : public Theory TheoryInferenceManager d_im; /** Cache of word-blasted facts. */ context::CDHashSet<Node> d_wbFactsCache; + + /** True constant. */ + Node d_true; }; } // namespace fp |