diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-11 15:55:31 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-11 15:55:31 +0100 |
commit | 1d0492104a200f6fa5cc7a1cee539436ee26ea99 (patch) | |
tree | a66ff6b0bc869f1e84dceb03ddbcc7910e23c77c /src/theory/arith/nl/iand_solver.cpp | |
parent | b3f05d5c25facaf0c34ee79faed060bda3f61a8d (diff) |
Merge InferenceIds into one enum (#5892)
This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories.
It merges all InferencedIds into one global enum and makes all theories use them.
Diffstat (limited to 'src/theory/arith/nl/iand_solver.cpp')
-rw-r--r-- | src/theory/arith/nl/iand_solver.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 5415e6a86..ff51f7bb5 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -99,7 +99,7 @@ void IAndSolver::checkInitialRefine() Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE" << std::endl; - d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_INIT_REFINE); + d_im.addPendingArithLemma(lem, InferenceId::ARITH_NL_IAND_INIT_REFINE); } } } @@ -153,7 +153,7 @@ void IAndSolver::checkFullRefine() // note that lemma can contain div/mod, and will be preprocessed in the // prop engine d_im.addPendingArithLemma( - lem, InferenceId::NL_IAND_SUM_REFINE, nullptr, true); + lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true); } else if (options::iandMode() == options::IandMode::BITWISE) { @@ -163,7 +163,7 @@ void IAndSolver::checkFullRefine() // note that lemma can contain div/mod, and will be preprocessed in the // prop engine d_im.addPendingArithLemma( - lem, InferenceId::NL_IAND_BITWISE_REFINE, nullptr, true); + lem, InferenceId::ARITH_NL_IAND_BITWISE_REFINE, nullptr, true); } else { @@ -173,7 +173,7 @@ void IAndSolver::checkFullRefine() << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; // value lemmas should not contain div/mod so we don't need to tag it with PREPROCESS d_im.addPendingArithLemma(lem, - InferenceId::NL_IAND_VALUE_REFINE, + InferenceId::ARITH_NL_IAND_VALUE_REFINE, nullptr, true, LemmaProperty::NONE); |