Fix compilation without LibPoly (#5118)

Commit e969318 introduced the ICP-based
solver for nonlinear arithmetic. That code, however, depends on LibPoly.
When configuring CVC4 without LibPoly, the code doesn't compile because
the class ICPSolver is missing. This commit adds a dummy version if
ICPSolver to remedy the issue.

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index d7909b96130a4fd896df5cc2405c06409a792abe..e9c217501331b190dad158c913d7a9d35cc2e1fa 100644 (file)
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -23,7 +23,7 @@ jobs:
 
         include:
           - name: production
-            config: production --all-bindings --lfsc --editline
+            config: production --all-bindings --lfsc --editline --poly
             cache-key: production
             python-bindings: true
             check-examples: true
@@ -44,7 +44,7 @@ jobs:
             exclude_regress: 1-4
 
           - name: debug-cln
-            config: debug --symfpu --cln --gpl --no-debug-symbols --no-proofs
+            config: debug --symfpu --cln --gpl --no-debug-symbols --no-proofs --poly
             cache-key: debug-cln
             os: ubuntu-latest
             exclude_regress: 1-4
@@ -158,7 +158,6 @@ jobs:
       run: |
         ${{ matrix.env }} ./configure.sh ${{ matrix.config }} \
           --python3 \
-          --poly \
           --prefix=$(pwd)/build/install \
           --unit-testing
 

diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index 12884152731c3c6988cfd82c348c1bc358c0b1da..ea9fc8f418a5a3c2a45a51e9edd3315aec9f7cea 100644 (file)
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -14,8 +14,6 @@
 
 #include "theory/arith/nl/icp/icp_solver.h"
 
-#ifdef CVC4_POLY_IMP
-
 #include <iostream>
 
 #include "base/check.h"
@@ -33,6 +31,8 @@ namespace arith {
 namespace nl {
 namespace icp {
 
+#ifdef CVC4_POLY_IMP
+
 namespace {
 /** A simple wrapper to nicely print an interval assignment. */
 struct IAWrapper
@@ -355,10 +355,22 @@ void ICPSolver::check()
   }
 }
 
+#else /* CVC4_POLY_IMP */
+
+void ICPSolver::reset(const std::vector<Node>& assertions)
+{
+  Unimplemented() << "ICPSolver requires CVC4 to be configured with LibPoly";
+}
+
+void ICPSolver::check()
+{
+  Unimplemented() << "ICPSolver requires CVC4 to be configured with LibPoly";
+}
+
+#endif /* CVC4_POLY_IMP */
+
 }  // namespace icp
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
 }  // namespace CVC4
-
-#endif

diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index 5fcd45fc6ba72d643cc37ceaf49316debb12dae2..61429b5a2671a62f6b0f1c3910010e452937c296 100644 (file)
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -19,6 +19,7 @@
 
 #ifdef CVC4_POLY_IMP
 #include <poly/polyxx.h>
+#endif /* CVC4_POLY_IMP */
 
 #include "expr/node.h"
 #include "theory/arith/inference_manager.h"
@@ -34,6 +35,8 @@ namespace arith {
 namespace nl {
 namespace icp {
 
+#ifdef CVC4_POLY_IMP
+
 /**
  * This class implements an ICP-based solver. As it is intended to be used in
  * conjunction with other solvers, it only performs contractions, but does not
@@ -132,6 +135,18 @@ class ICPSolver
   void check();
 };
 
+#else /* CVC4_POLY_IMP */
+
+class ICPSolver
+{
+ public:
+  ICPSolver(InferenceManager& im) {}
+  void reset(const std::vector<Node>& assertions);
+  void check();
+};
+
+#endif /* CVC4_POLY_IMP */
+
 }  // namespace icp
 }  // namespace nl
 }  // namespace arith
@@ -139,4 +154,3 @@ class ICPSolver
 }  // namespace CVC4
 
 #endif
-#endif
\ No newline at end of file