Add proper define for libpoly usage (#6050)

When adding libpoly, we forgot to add a proper define to cvc4autoconfig and included real_algebraic_number.h everywhere to get this define. This PR introduces the CVC4_POLY_IMP define and removes all obsolete includes to real_algebraic_number.h.

12 files changed, 9 insertions, 18 deletions

diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 8736b7a08..ada6286f7 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -20,8 +20,6 @@
 #ifndef CVC4__THEORY__ARITH__NL__CAD__CDCAC_H
 #define CVC4__THEORY__ARITH__NL__CAD__CDCAC_H
 
-#include "util/real_algebraic_number.h"
-
 #ifdef CVC4_POLY_IMP
 
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h
index 335735574..153341c7e 100644
--- a/src/theory/arith/nl/cad/cdcac_utils.h
+++ b/src/theory/arith/nl/cad/cdcac_utils.h
@@ -19,8 +19,6 @@
 #ifndef CVC4__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
 #define CVC4__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
 
-#include "util/real_algebraic_number.h"
-
 #ifdef CVC4_POLY_IMP
 
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h
index 1df61e706..10079e9bb 100644
--- a/src/theory/arith/nl/cad/constraints.h
+++ b/src/theory/arith/nl/cad/constraints.h
@@ -19,8 +19,6 @@
 #ifndef CVC4__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
 #define CVC4__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
 
-#include "util/real_algebraic_number.h"
-
 #ifdef CVC4_POLY_IMP
 
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h
index dd485b372..3820716c2 100644
--- a/src/theory/arith/nl/cad/projections.h
+++ b/src/theory/arith/nl/cad/projections.h
@@ -19,8 +19,6 @@
 #ifndef CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H
 #define CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H
 
-#include "util/real_algebraic_number.h"
-
 #ifdef CVC4_USE_POLY
 
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index fd2458271..055de98fe 100644
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -17,8 +17,6 @@
 #ifndef CVC4__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
 #define CVC4__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
 
-#include "util/real_algebraic_number.h"
-
 #ifdef CVC4_POLY_IMP
 
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h
index 2e56a64b4..4954e0e46 100644
--- a/src/theory/arith/nl/cad/variable_ordering.h
+++ b/src/theory/arith/nl/cad/variable_ordering.h
@@ -19,8 +19,6 @@
 #ifndef CVC4__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
 #define CVC4__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
 
-#include "util/real_algebraic_number.h"
-
 #ifdef CVC4_POLY_IMP
 
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index b67d78f0d..7d0346eab 100644
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -21,7 +21,6 @@
 #include "expr/node.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/cad/proof_checker.h"
-#include "util/real_algebraic_number.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h
index a2160472d..4a52456ff 100644
--- a/src/theory/arith/nl/icp/candidate.h
+++ b/src/theory/arith/nl/icp/candidate.h
@@ -15,7 +15,7 @@
 #ifndef CVC4__THEORY__ARITH__ICP__CANDIDATE_H
 #define CVC4__THEORY__ARITH__ICP__CANDIDATE_H
 
-#include "util/real_algebraic_number.h"
+#include "cvc4_private.h"
 
 #ifdef CVC4_POLY_IMP
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index b9ecfc437..9b41ed6e0 100644
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -15,7 +15,7 @@
 #ifndef CVC4__THEORY__ARITH__ICP__ICP_SOLVER_H
 #define CVC4__THEORY__ARITH__ICP__ICP_SOLVER_H
 
-#include "util/real_algebraic_number.h"
+#include "cvc4_private.h"
 
 #ifdef CVC4_POLY_IMP
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h
index cdc166139..db14184b0 100644
--- a/src/theory/arith/nl/icp/intersection.h
+++ b/src/theory/arith/nl/icp/intersection.h
@@ -15,9 +15,12 @@
 #ifndef CVC4__THEORY__ARITH__ICP__INTERSECTION_H
 #define CVC4__THEORY__ARITH__ICP__INTERSECTION_H
 
-#include "util/real_algebraic_number.h"
+#include "cvc4_private.h"
 
 #ifdef CVC4_POLY_IMP
+
+#include <cstddef>
+
 namespace poly {
   class Interval;
 }
diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h
index d2b0fd4f5..01968e70f 100644
--- a/src/theory/arith/nl/icp/interval.h
+++ b/src/theory/arith/nl/icp/interval.h
@@ -15,7 +15,7 @@
 #ifndef CVC4__THEORY__ARITH__ICP__INTERVAL_H
 #define CVC4__THEORY__ARITH__ICP__INTERVAL_H
 
-#include "util/real_algebraic_number.h"
+#include "cvc4_private.h"
 
 #ifdef CVC4_POLY_IMP
 #include <poly/polyxx.h>
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index 102d2d6ae..94ed5e318 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -17,7 +17,7 @@
 #ifndef CVC4__THEORY__ARITH__NL__POLY_CONVERSION_H
 #define CVC4__THEORY__ARITH__NL__POLY_CONVERSION_H
 
-#include "util/real_algebraic_number.h"
+#include "cvc4_private.h"
 
 #ifdef CVC4_POLY_IMP
 
@@ -28,6 +28,7 @@
 #include <utility>
 
 #include "expr/node.h"
+#include "util/real_algebraic_number.h"
 
 namespace CVC4 {
 namespace theory {