Use BoundInference in nonlinear extension (#5359)

Currently the NonlinearExtensions uses a custom logic to eliminate redundant bounds and perform tightening on bound integer terms. As these replacements are not recorded, incorrect conflicts are being sent to the InferenceManager.
This PR replaces this logic by the BoundInference class and fixes the issues with conflicts by
- allowing BoundInference to collect bounds on arbitrary left hand sides (instead of only variables),
- improving origin tracking in BoundInference by explicitly constructing the new bound constraints,
- adding tightening of integer bounds,
- emitting lemmas instead of conflicts, and finally
- replacing the current logic by using the BoundInference class.

1 files changed, 4 insertions, 4 deletions

diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index a76a781c4..0e4e21b76 100644
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -785,12 +785,12 @@ poly::IntervalAssignment getBounds(VariableMapper& vm, const BoundInference& bi)
   for (const auto& vb : bi.get())
   {
     poly::Variable v = vm(vb.first);
-    poly::Value l = vb.second.lower.isNull()
+    poly::Value l = vb.second.lower_value.isNull()
                         ? poly::Value::minus_infty()
-                        : node_to_value(vb.second.lower, vb.first);
-    poly::Value u = vb.second.upper.isNull()
+                        : node_to_value(vb.second.lower_value, vb.first);
+    poly::Value u = vb.second.upper_value.isNull()
                         ? poly::Value::plus_infty()
-                        : node_to_value(vb.second.upper, vb.first);
+                        : node_to_value(vb.second.upper_value, vb.first);
     poly::Interval i(l, vb.second.lower_strict, u, vb.second.upper_strict);
     res.set(v, i);
   }