ICP-based solver for nonlinear arithmetic (#5017)

This PR adds a new icp-based solver to be integrated into the nonlinear extension.
It is not meant to be used as a stand-alone ICP solver. It does not implement splits (only propagations) and implements a rather aggressive budget mechanism that aims to quickly stop propagation to allow other solvers to take over. Additionally, it enforces a maximum bit size to avoid divergence.

1 files changed, 8 insertions, 1 deletions

diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index d83bc1b2e..a60b7ac41 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -61,10 +61,17 @@ poly::UPolynomial as_poly_upolynomial(const CVC4::Node& n,
  * While a Node may contain rationals, a Polynomial does not.
  * We therefore also store the denominator of the returned polynomial and
  * use it to construct the integer polynomial recursively.
- * Once the polynomial has been fully constructed, we can ignore the
+ * Once the polynomial has been fully constructed, we can oftentimes ignore the
  * denominator (except for its sign, which is always positive, though).
+ * This is the case if we are solely interested in the roots of the polynomials
+ * (like in the context of CAD). If we need the actual polynomial (for example
+ * in the context of ICP) the second overload provides the denominator in the
+ * third argument.
  */
 poly::Polynomial as_poly_polynomial(const CVC4::Node& n, VariableMapper& vm);
+poly::Polynomial as_poly_polynomial(const CVC4::Node& n,
+                                    VariableMapper& vm,
+                                    poly::Rational& denominator);
 
 /**
  * Constructs a constraints (a polynomial and a sign condition) from the given