diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-11-20 14:08:45 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-20 07:08:45 -0600 |
| commit | de0d36b8972954c281f1e97b15d37c07a861cbc1 (patch) | |
| tree | 23063fd32dd8c7d2509684014fca07fe92887b48 /src/theory/arith/nl/iand_solver.cpp | |
| parent | f2ed7b1aebc175b971e3cebf4c0b2fff6e4e895f (diff) | |
Allow to pass ProofGenerator to arithmetic inference manager. (#5488)
This PR prepares the addition of proofs for the arithmetic theory by making addPendingArithLemma() accept a ProofGenerator*.
Diffstat (limited to 'src/theory/arith/nl/iand_solver.cpp')
| -rw-r--r-- | src/theory/arith/nl/iand_solver.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 30441a8f4..e33cfa6cd 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -151,7 +151,8 @@ void IAndSolver::checkFullRefine() Node lem = sumBasedLemma(i); // add lemmas based on sum mode Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl; - d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_SUM_REFINE, true); + d_im.addPendingArithLemma( + lem, InferenceId::NL_IAND_SUM_REFINE, nullptr, true); } else if (options::iandMode() == options::IandMode::BITWISE) { @@ -163,7 +164,8 @@ void IAndSolver::checkFullRefine() Node lem = valueBasedLemma(i); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; - d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_VALUE_REFINE, true); + d_im.addPendingArithLemma( + lem, InferenceId::NL_IAND_VALUE_REFINE, nullptr, true); } } } |