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.

diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index fd6eedc5a510c6e4028b712c7f83bcd774628f62..3b6c3cbe440fd55ad83c86780ef248fb996e4ec6 100644 (file)
--- 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 34242e746da58d63a4c16da4d72faaa901e3de52..0d84137777860af0dcdd808035c37bf0131d22c7 100644 (file)
--- 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 20c1a06a29d145ae941a8b86d0352935a8bf015d..0cf6ad3bde37d30399f78c1dedf71140018317e5 100644 (file)
--- 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,