Cleanup of inferences in arithmetic theory (#5927)

This PR cleans up several issues in the arithmetic theory mostly related to its usage of InferenceId and the TheoryInferenceManager:

    remove the ArithLemma class and uses SimpleTheoryLemma instead
    only use NlLemma if we actually need it
    use proper InferenceIds everywhere
    remove unused code in the nonlinear extension

1 files changed, 36 insertions, 24 deletions

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index cb15b4326..0268fa31a 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -21,30 +21,42 @@ const char* toString(InferenceId i)
 {
   switch (i)
   {
-    case InferenceId::ARITH_NL_CONGRUENCE: return "CONGRUENCE";
-    case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT: return "SHARED_TERM_VALUE_SPLIT";
-    case InferenceId::ARITH_NL_SPLIT_ZERO: return "SPLIT_ZERO";
-    case InferenceId::ARITH_NL_SIGN: return "SIGN";
-    case InferenceId::ARITH_NL_COMPARISON: return "COMPARISON";
-    case InferenceId::ARITH_NL_INFER_BOUNDS: return "INFER_BOUNDS";
-    case InferenceId::ARITH_NL_INFER_BOUNDS_NT: return "INFER_BOUNDS_NT";
-    case InferenceId::ARITH_NL_FACTOR: return "FACTOR";
-    case InferenceId::ARITH_NL_RES_INFER_BOUNDS: return "RES_INFER_BOUNDS";
-    case InferenceId::ARITH_NL_TANGENT_PLANE: return "TANGENT_PLANE";
-    case InferenceId::ARITH_NL_T_PURIFY_ARG: return "T_PURIFY_ARG";
-    case InferenceId::ARITH_NL_T_INIT_REFINE: return "T_INIT_REFINE";
-    case InferenceId::ARITH_NL_T_PI_BOUND: return "T_PI_BOUND";
-    case InferenceId::ARITH_NL_T_MONOTONICITY: return "T_MONOTONICITY";
-    case InferenceId::ARITH_NL_T_SECANT: return "T_SECANT";
-    case InferenceId::ARITH_NL_T_TANGENT: return "T_TANGENT";
-    case InferenceId::ARITH_NL_IAND_INIT_REFINE: return "IAND_INIT_REFINE";
-    case InferenceId::ARITH_NL_IAND_VALUE_REFINE: return "IAND_VALUE_REFINE";
-    case InferenceId::ARITH_NL_IAND_SUM_REFINE: return "IAND_SUM_REFINE";
-    case InferenceId::ARITH_NL_IAND_BITWISE_REFINE: return "IAND_BITWISE_REFINE";
-    case InferenceId::ARITH_NL_CAD_CONFLICT: return "CAD_CONFLICT";
-    case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL";
-    case InferenceId::ARITH_NL_ICP_CONFLICT: return "ICP_CONFLICT";
-    case InferenceId::ARITH_NL_ICP_PROPAGATION: return "ICP_PROPAGATION";
+    case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS";
+    case InferenceId::ARITH_NL_CONGRUENCE: return "ARITH_NL_CONGRUENCE";
+    case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT:
+      return "ARITH_NL_SHARED_TERM_VALUE_SPLIT";
+    case InferenceId::ARITH_NL_CM_QUADRATIC_EQ:
+      return "ARITH_NL_CM_QUADRATIC_EQ";
+    case InferenceId::ARITH_NL_SPLIT_ZERO: return "ARITH_NL_SPLIT_ZERO";
+    case InferenceId::ARITH_NL_SIGN: return "ARITH_NL_SIGN";
+    case InferenceId::ARITH_NL_COMPARISON: return "ARITH_NL_COMPARISON";
+    case InferenceId::ARITH_NL_INFER_BOUNDS: return "ARITH_NL_INFER_BOUNDS";
+    case InferenceId::ARITH_NL_INFER_BOUNDS_NT:
+      return "ARITH_NL_INFER_BOUNDS_NT";
+    case InferenceId::ARITH_NL_FACTOR: return "ARITH_NL_FACTOR";
+    case InferenceId::ARITH_NL_RES_INFER_BOUNDS:
+      return "ARITH_NL_RES_INFER_BOUNDS";
+    case InferenceId::ARITH_NL_TANGENT_PLANE: return "ARITH_NL_TANGENT_PLANE";
+    case InferenceId::ARITH_NL_T_PURIFY_ARG: return "ARITH_NL_T_PURIFY_ARG";
+    case InferenceId::ARITH_NL_T_INIT_REFINE: return "ARITH_NL_T_INIT_REFINE";
+    case InferenceId::ARITH_NL_T_PI_BOUND: return "ARITH_NL_T_PI_BOUND";
+    case InferenceId::ARITH_NL_T_MONOTONICITY: return "ARITH_NL_T_MONOTONICITY";
+    case InferenceId::ARITH_NL_T_SECANT: return "ARITH_NL_T_SECANT";
+    case InferenceId::ARITH_NL_T_TANGENT: return "ARITH_NL_T_TANGENT";
+    case InferenceId::ARITH_NL_IAND_INIT_REFINE:
+      return "ARITH_NL_IAND_INIT_REFINE";
+    case InferenceId::ARITH_NL_IAND_VALUE_REFINE:
+      return "ARITH_NL_IAND_VALUE_REFINE";
+    case InferenceId::ARITH_NL_IAND_SUM_REFINE:
+      return "ARITH_NL_IAND_SUM_REFINE";
+    case InferenceId::ARITH_NL_IAND_BITWISE_REFINE:
+      return "ARITH_NL_IAND_BITWISE_REFINE";
+    case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT";
+    case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL:
+      return "ARITH_NL_CAD_EXCLUDED_INTERVAL";
+    case InferenceId::ARITH_NL_ICP_CONFLICT: return "ARITH_NL_ICP_CONFLICT";
+    case InferenceId::ARITH_NL_ICP_PROPAGATION:
+      return "ARITH_NL_ICP_PROPAGATION";
 
     case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT";
     case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";