From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Fri, 28 Aug 2020 00:38:36 +0000 (+0200)
Subject: Make iand lemmas use proper Inference types. (#4956)
X-Git-Tag: cvc5-1.0.0~2949
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3e057f9d0454738429ade62dbad8f5ac0b3274db;p=cvc5.git

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 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,