diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-19 09:34:36 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-19 09:34:36 +0100 |
commit | ce58453982ddd53a5fc08d9db4c6c3f49b852838 (patch) | |
tree | e77cb66ff4d5bca985524d3c2befd33d580916af /src/theory/arith/arith_preprocess.cpp | |
parent | 6ae21de6f85d9629018c1b6bf912ef39f3e169fb (diff) |
Cleanup of inferences in arithmetic theory (#5927)
This PR cleans up several issues in the arithmetic theory mostly related to its usage of InferenceId and the TheoryInferenceManager:
remove the ArithLemma class and uses SimpleTheoryLemma instead
only use NlLemma if we actually need it
use proper InferenceIds everywhere
remove unused code in the nonlinear extension
Diffstat (limited to 'src/theory/arith/arith_preprocess.cpp')
-rw-r--r-- | src/theory/arith/arith_preprocess.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index 80217195f..3e0937e8b 100644 --- a/src/theory/arith/arith_preprocess.cpp +++ b/src/theory/arith/arith_preprocess.cpp @@ -49,7 +49,7 @@ bool ArithPreprocess::reduceAssertion(TNode atom) // tn is of kind REWRITE, turn this into a LEMMA here TrustNode tlem = TrustNode::mkTrustLemma(tn.getProven(), tn.getGenerator()); // must preprocess - d_im.trustedLemma(tlem, InferenceId::UNKNOWN); + d_im.trustedLemma(tlem, InferenceId::ARITH_PP_ELIM_OPERATORS); // mark the atom as reduced d_reduced[atom] = true; return true; |