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.

diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake
index 6da71dc6495ad4fa009411e58acb3cc7628d0300..9c160e4fc49145579069973608625aab0268ee92 100644 (file)
--- a/cmake/ConfigureCVC4.cmake
+++ b/cmake/ConfigureCVC4.cmake
@@ -95,5 +95,7 @@ check_c_source_compiles(
 set(CVC4_CLN_IMP ${CVC4_USE_CLN_IMP})
 # Defined if using the GMP multi-precision arithmetic library.
 set(CVC4_GMP_IMP ${CVC4_USE_GMP_IMP})
+# Defined if using the libpoly polynomial library.
+set(CVC4_POLY_IMP ${CVC4_USE_POLY_IMP})
 # Define the full name of this package.
 set(CVC4_PACKAGE_NAME "${PROJECT_NAME}")

diff --git a/cvc4autoconfig.h.in b/cvc4autoconfig.h.in
index 48d826697b01935a5738c6023e71bbb9291d5c80..3d3412d662afb9199bf4ee69295a6039b1a3eb86 100644 (file)
--- a/cvc4autoconfig.h.in
+++ b/cvc4autoconfig.h.in
@@ -28,6 +28,9 @@
 /* Define to use the GMP multi-precision arithmetic library. */
 #cmakedefine CVC4_GMP_IMP
 
+/* Define to use the libpoly polynomial library. */
+#cmakedefine CVC4_POLY_IMP
+
 /* Define to 1 if Boost threading library has support for thread attributes. */
 #cmakedefine01 BOOST_HAS_THREAD_ATTR
 

diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 8736b7a086078fee4fd39701348c06dc6458bfa6..ada6286f79f7685fc1c92ddaf32ce88de30ed14c 100644 (file)
--- 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 3357355740230baa0f6b613c5c575e7190473ed5..153341c7ec37ab1036fd5663496b50bf1a03ceb2 100644 (file)
--- 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 1df61e706ea4a8f4f0c1e528a15907d888ffae9d..10079e9bbd861e89adef257de9e876cc77498f0c 100644 (file)
--- 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 dd485b372216ea80094fbe4d57311d6355493953..3820716c208effac204a72e6539c096bd489d112 100644 (file)
--- 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 fd2458271b6dc8df37e78d40f4e7fdf368f144ca..055de98fe0eafbe9ce32347991f927f60c39b5c9 100644 (file)
--- 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 2e56a64b4538e7d073b7d90f233aa4c0fefd464c..4954e0e46b39ccdad570ee0f5bb468c6f67df18a 100644 (file)
--- 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 b67d78f0d0c863ab5bee3bed9378e3ab283db4a0..7d0346eabcc99a89d5c11dae8fcd27a30a8d1c87 100644 (file)
--- 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 a2160472d738a8142121dcc9956af271110a2215..4a52456ff5bf111aea04bba44488cb05523c01ad 100644 (file)
--- 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 b9ecfc437cbf201654185f77672c2c21aace4f4e..9b41ed6e0ad9815fa48b6149e28477624e941a34 100644 (file)
--- 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 cdc166139c3c20bb19a748eeb8ded7d8f7893cc1..db14184b0017c8d88fcc5cc0cca458a657f374a1 100644 (file)
--- 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 d2b0fd4f5808479f557203cb41950595ef6ce383..01968e70feaf80cdbf941bce74b5746076badcdd 100644 (file)
--- 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 102d2d6aed4e9453eb74bfb1ac51dac52dcc183a..94ed5e318b5cdbea587cfecadb9fb041c2dabfaa 100644 (file)
--- 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 {