diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-08-28 02:38:36 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-27 17:38:36 -0700 |
| commit | 3e057f9d0454738429ade62dbad8f5ac0b3274db (patch) | |
| tree | f028abd6c8775a15dfadbadbc52be0d144daf1ca | |
| parent | 4adff162770a841d136ec44146928c2296eaf1b2 (diff) | |
Make iand lemmas use proper Inference types. (#4956)
For some reason, the nl subsolver for IAND did not annotate its lemmas with `Inference` types yet. This commit adds appropriate `Inference` values and makes the IAND solver use them.
| -rw-r--r-- | src/theory/arith/nl/iand_solver.cpp | 4 | ||||
| -rw-r--r-- | src/theory/arith/nl/inference.cpp | 4 | ||||
| -rw-r--r-- | src/theory/arith/nl/inference.h | 5 |
3 files changed, 11 insertions, 2 deletions
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index fd6eedc5a..3b6c3cbe4 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -101,7 +101,7 @@ std::vector<NlLemma> IAndSolver::checkInitialRefine() Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE" << std::endl; - lems.push_back(lem); + lems.emplace_back(lem, Inference::IAND_INIT_REFINE); } } return lems; @@ -163,7 +163,7 @@ std::vector<NlLemma> IAndSolver::checkFullRefine() Node lem = valueBasedLemma(i); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; - lems.push_back(lem); + lems.emplace_back(lem, Inference::IAND_VALUE_REFINE); } } } diff --git a/src/theory/arith/nl/inference.cpp b/src/theory/arith/nl/inference.cpp index 34242e746..0d8413777 100644 --- a/src/theory/arith/nl/inference.cpp +++ b/src/theory/arith/nl/inference.cpp @@ -39,6 +39,10 @@ const char* toString(Inference i) case Inference::T_MONOTONICITY: return "T_MONOTONICITY"; case Inference::T_SECANT: return "T_SECANT"; case Inference::T_TANGENT: return "T_TANGENT"; + case Inference::IAND_INIT_REFINE: return "IAND_INIT_REFINE"; + case Inference::IAND_VALUE_REFINE: return "IAND_VALUE_REFINE"; + case Inference::CAD_CONFLICT: return "CAD_CONFLICT"; + case Inference::CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL"; default: return "?"; } } diff --git a/src/theory/arith/nl/inference.h b/src/theory/arith/nl/inference.h index 20c1a06a2..0cf6ad3bd 100644 --- a/src/theory/arith/nl/inference.h +++ b/src/theory/arith/nl/inference.h @@ -67,6 +67,11 @@ enum class Inference : uint32_t T_TANGENT, // secant refinement, the dual of the above inference T_SECANT, + //-------------------- iand solver + // initial refinements (IAndSolver::checkInitialRefine) + IAND_INIT_REFINE, + // value refinements (IAndSolver::checkFullRefine) + IAND_VALUE_REFINE, //-------------------- cad solver // conflict / infeasible subset obtained from cad CAD_CONFLICT, |