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/nl/icp | |
| 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/nl/icp')
| -rw-r--r-- | src/theory/arith/nl/icp/icp_solver.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index af6093be1..af86d69fd 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -348,8 +348,8 @@ void ICPSolver::check() { mis.emplace_back(n.negate()); } - d_im.addPendingArithLemma(NodeManager::currentNM()->mkOr(mis), - InferenceId::ARITH_NL_ICP_CONFLICT); + d_im.addPendingLemma(NodeManager::currentNM()->mkOr(mis), + InferenceId::ARITH_NL_ICP_CONFLICT); did_progress = true; progress = false; break; @@ -360,7 +360,7 @@ void ICPSolver::check() std::vector<Node> lemmas = generateLemmas(); for (const auto& l : lemmas) { - d_im.addPendingArithLemma(l, InferenceId::ARITH_NL_ICP_PROPAGATION); + d_im.addPendingLemma(l, InferenceId::ARITH_NL_ICP_PROPAGATION); } } } |