From 3e057f9d0454738429ade62dbad8f5ac0b3274db Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 28 Aug 2020 02:38:36 +0200 Subject: [PATCH] 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. --- src/theory/arith/nl/iand_solver.cpp | 4 ++-- src/theory/arith/nl/inference.cpp | 4 ++++ 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 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 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, -- 2.30.2