Merge InferenceIds into one enum (#5892)

This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories.
It merges all InferencedIds into one global enum and makes all theories use them.

3 files changed, 15 insertions, 81 deletions

diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp
index 9bf546af1..9b5187689 100644
--- a/src/theory/bags/infer_info.cpp
+++ b/src/theory/bags/infer_info.cpp
@@ -20,34 +20,7 @@ namespace CVC4 {
 namespace theory {
 namespace bags {
 
-const char* toString(Inference i)
-{
-  switch (i)
-  {
-    case Inference::NONE: return "NONE";
-    case Inference::BAG_NON_NEGATIVE_COUNT: return "BAG_NON_NEGATIVE_COUNT";
-    case Inference::BAG_MK_BAG_SAME_ELEMENT: return "BAG_MK_BAG_SAME_ELEMENT";
-    case Inference::BAG_MK_BAG: return "BAG_MK_BAG";
-    case Inference::BAG_EQUALITY: return "BAG_EQUALITY";
-    case Inference::BAG_DISEQUALITY: return "BAG_DISEQUALITY";
-    case Inference::BAG_EMPTY: return "BAG_EMPTY";
-    case Inference::BAG_UNION_DISJOINT: return "BAG_UNION_DISJOINT";
-    case Inference::BAG_UNION_MAX: return "BAG_UNION_MAX";
-    case Inference::BAG_INTERSECTION_MIN: return "BAG_INTERSECTION_MIN";
-    case Inference::BAG_DIFFERENCE_SUBTRACT: return "BAG_DIFFERENCE_SUBTRACT";
-    case Inference::BAG_DIFFERENCE_REMOVE: return "BAG_DIFFERENCE_REMOVE";
-    case Inference::BAG_DUPLICATE_REMOVAL: return "BAG_DUPLICATE_REMOVAL";
-    default: return "?";
-  }
-}
-
-std::ostream& operator<<(std::ostream& out, Inference i)
-{
-  out << toString(i);
-  return out;
-}
-
-InferInfo::InferInfo() : d_id(Inference::NONE) {}
+InferInfo::InferInfo() : d_id(InferenceId::UNKNOWN) {}
 
 bool InferInfo::process(TheoryInferenceManager* im, bool asLemma)
 {
diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h
index ecfc354d1..8628d19f6 100644
--- a/src/theory/bags/infer_info.h
+++ b/src/theory/bags/infer_info.h
@@ -21,52 +21,13 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "theory/inference_id.h"
 #include "theory/theory_inference.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
-/**
- * Types of inferences used in the procedure
- */
-enum class Inference : uint32_t
-{
-  NONE,
-  BAG_NON_NEGATIVE_COUNT,
-  BAG_MK_BAG_SAME_ELEMENT,
-  BAG_MK_BAG,
-  BAG_EQUALITY,
-  BAG_DISEQUALITY,
-  BAG_EMPTY,
-  BAG_UNION_DISJOINT,
-  BAG_UNION_MAX,
-  BAG_INTERSECTION_MIN,
-  BAG_DIFFERENCE_SUBTRACT,
-  BAG_DIFFERENCE_REMOVE,
-  BAG_DUPLICATE_REMOVAL
-};
-
-/**
- * Converts an inference to a string. Note: This function is also used in
- * `safe_print()`. Changing this functions name or signature will result in
- * `safe_print()` printing "<unsupported>" instead of the proper strings for
- * the enum values.
- *
- * @param i The inference
- * @return The name of the inference
- */
-const char* toString(Inference i);
-
-/**
- * Writes an inference name to a stream.
- *
- * @param out The stream to write to
- * @param i The inference to write to the stream
- * @return The stream
- */
-std::ostream& operator<<(std::ostream& out, Inference i);
-
 class InferenceManager;
 
 /**
@@ -82,8 +43,8 @@ class InferInfo : public TheoryInference
   /** Process this inference */
   bool process(TheoryInferenceManager* im, bool asLemma) override;
   /** The inference identifier */
-  Inference d_id;
-  /** The conclusions */
+  InferenceId d_id;
+  /** The conclusion */
   Node d_conclusion;
   /**
    * The premise(s) of the inference, interpreted conjunctively. These are
diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index 708c25f34..6d8b6a33b 100644
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -38,7 +38,7 @@ InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
   Assert(e.getType() == n.getType().getBagElementType());
 
   InferInfo inferInfo;
-  inferInfo.d_id = Inference::BAG_NON_NEGATIVE_COUNT;
+  inferInfo.d_id = InferenceId::BAG_NON_NEGATIVE_COUNT;
   Node count = d_nm->mkNode(kind::BAG_COUNT, e, n);
 
   Node gte = d_nm->mkNode(kind::GEQ, count, d_zero);
@@ -58,7 +58,7 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e)
   {
     // TODO issue #78: refactor this with BagRewriter
     // (=> true (= (bag.count e (bag e c)) c))
-    inferInfo.d_id = Inference::BAG_MK_BAG_SAME_ELEMENT;
+    inferInfo.d_id = InferenceId::BAG_MK_BAG_SAME_ELEMENT;
     inferInfo.d_conclusion = count.eqNode(n[1]);
   }
   else
@@ -66,7 +66,7 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e)
     // (=>
     //   true
     //   (= (bag.count e (bag x c)) (ite (= e x) c 0)))
-    inferInfo.d_id = Inference::BAG_MK_BAG;
+    inferInfo.d_id = InferenceId::BAG_MK_BAG;
     Node same = d_nm->mkNode(kind::EQUAL, n[0], e);
     Node ite = d_nm->mkNode(kind::ITE, same, n[1], d_zero);
     Node equal = count.eqNode(ite);
@@ -88,7 +88,7 @@ InferInfo InferenceGenerator::bagDisequality(Node n)
   Node B = n[1];
 
   InferInfo inferInfo;
-  inferInfo.d_id = Inference::BAG_DISEQUALITY;
+  inferInfo.d_id = InferenceId::BAG_DISEQUALITY;
 
   TypeNode elementType = A.getType().getBagElementType();
   BoundVarManager* bvm = d_nm->getBoundVarManager();
@@ -123,7 +123,7 @@ InferInfo InferenceGenerator::empty(Node n, Node e)
 
   InferInfo inferInfo;
   Node skolem = getSkolem(n, inferInfo);
-  inferInfo.d_id = Inference::BAG_EMPTY;
+  inferInfo.d_id = InferenceId::BAG_EMPTY;
   Node count = getMultiplicityTerm(e, skolem);
 
   Node equal = count.eqNode(d_zero);
@@ -139,7 +139,7 @@ InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
   Node A = n[0];
   Node B = n[1];
   InferInfo inferInfo;
-  inferInfo.d_id = Inference::BAG_UNION_DISJOINT;
+  inferInfo.d_id = InferenceId::BAG_UNION_DISJOINT;
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -162,7 +162,7 @@ InferInfo InferenceGenerator::unionMax(Node n, Node e)
   Node A = n[0];
   Node B = n[1];
   InferInfo inferInfo;
-  inferInfo.d_id = Inference::BAG_UNION_MAX;
+  inferInfo.d_id = InferenceId::BAG_UNION_MAX;
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -186,7 +186,7 @@ InferInfo InferenceGenerator::intersection(Node n, Node e)
   Node A = n[0];
   Node B = n[1];
   InferInfo inferInfo;
-  inferInfo.d_id = Inference::BAG_INTERSECTION_MIN;
+  inferInfo.d_id = InferenceId::BAG_INTERSECTION_MIN;
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -208,7 +208,7 @@ InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
   Node A = n[0];
   Node B = n[1];
   InferInfo inferInfo;
-  inferInfo.d_id = Inference::BAG_DIFFERENCE_SUBTRACT;
+  inferInfo.d_id = InferenceId::BAG_DIFFERENCE_SUBTRACT;
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -231,7 +231,7 @@ InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
   Node A = n[0];
   Node B = n[1];
   InferInfo inferInfo;
-  inferInfo.d_id = Inference::BAG_DIFFERENCE_REMOVE;
+  inferInfo.d_id = InferenceId::BAG_DIFFERENCE_REMOVE;
 
   Node countA = getMultiplicityTerm(e, A);
   Node countB = getMultiplicityTerm(e, B);
@@ -253,7 +253,7 @@ InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e)
 
   Node A = n[0];
   InferInfo inferInfo;
-  inferInfo.d_id = Inference::BAG_DUPLICATE_REMOVAL;
+  inferInfo.d_id = InferenceId::BAG_DUPLICATE_REMOVAL;
 
   Node countA = getMultiplicityTerm(e, A);
   Node skolem = getSkolem(n, inferInfo);