Rename CVC4_ macros to CVC5_. (#6327)

23 files changed, 36 insertions, 36 deletions

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index c9f3ce3da..4cd9077ca 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -17,7 +17,7 @@
 
 #include "theory/arith/nl/cad/cdcac.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include "options/arith_options.h"
 #include "theory/arith/nl/cad/projections.h"
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 0d5d4ce74..58aa41bd1 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -20,7 +20,7 @@
 #ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_H
 #define CVC5__THEORY__ARITH__NL__CAD__CDCAC_H
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include <poly/polyxx.h>
 
diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp
index 999e491f6..3ceb36bd3 100644
--- a/src/theory/arith/nl/cad/cdcac_utils.cpp
+++ b/src/theory/arith/nl/cad/cdcac_utils.cpp
@@ -16,7 +16,7 @@
 
 #include "theory/arith/nl/cad/cdcac_utils.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include "theory/arith/nl/cad/projections.h"
 
diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h
index 3cfbb138c..50f2f8bc9 100644
--- a/src/theory/arith/nl/cad/cdcac_utils.h
+++ b/src/theory/arith/nl/cad/cdcac_utils.h
@@ -19,7 +19,7 @@
 #ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
 #define CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include <poly/polyxx.h>
 
diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/cad/constraints.cpp
index 75d1cb723..b244bd358 100644
--- a/src/theory/arith/nl/cad/constraints.cpp
+++ b/src/theory/arith/nl/cad/constraints.cpp
@@ -16,7 +16,7 @@
 
 #include "theory/arith/nl/cad/constraints.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include <algorithm>
 
diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h
index efc69d468..1ddbfc821 100644
--- a/src/theory/arith/nl/cad/constraints.h
+++ b/src/theory/arith/nl/cad/constraints.h
@@ -19,7 +19,7 @@
 #ifndef CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
 #define CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include <poly/polyxx.h>
 
diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp
index 1bac0c160..8aea538f1 100644
--- a/src/theory/arith/nl/cad/projections.cpp
+++ b/src/theory/arith/nl/cad/projections.cpp
@@ -16,7 +16,7 @@
 
 #include "theory/arith/nl/cad/projections.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include "base/check.h"
 
diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h
index c1ce91303..f3c8aa0f1 100644
--- a/src/theory/arith/nl/cad/projections.h
+++ b/src/theory/arith/nl/cad/projections.h
@@ -19,7 +19,7 @@
 #ifndef CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H
 #define CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H
 
-#ifdef CVC4_USE_POLY
+#ifdef CVC5_USE_POLY
 
 #include <poly/polyxx.h>
 
diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
index 73e19aa28..291447647 100644
--- a/src/theory/arith/nl/cad/proof_generator.cpp
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/arith/nl/cad/proof_generator.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include "theory/lazy_tree_proof_generator.h"
 #include "theory/arith/nl/poly_conversion.h"
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index 9365cc337..993524504 100644
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -17,7 +17,7 @@
 #ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
 #define CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include <poly/polyxx.h>
 
diff --git a/src/theory/arith/nl/cad/variable_ordering.cpp b/src/theory/arith/nl/cad/variable_ordering.cpp
index 7ebbc90dd..e7c8b214a 100644
--- a/src/theory/arith/nl/cad/variable_ordering.cpp
+++ b/src/theory/arith/nl/cad/variable_ordering.cpp
@@ -16,7 +16,7 @@
 
 #include "theory/arith/nl/cad/variable_ordering.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include "util/poly_util.h"
 
diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h
index b4336d395..fb40a7b7d 100644
--- a/src/theory/arith/nl/cad/variable_ordering.h
+++ b/src/theory/arith/nl/cad/variable_ordering.h
@@ -19,7 +19,7 @@
 #ifndef CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
 #define CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include <poly/polyxx.h>
 
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index aa9bce776..202788ba1 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -31,7 +31,7 @@ CadSolver::CadSolver(InferenceManager& im,
                      context::Context* ctx,
                      ProofNodeManager* pnm)
     :
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
       d_CAC(ctx, pnm),
 #endif
       d_foundSatisfiability(false),
@@ -42,7 +42,7 @@ CadSolver::CadSolver(InferenceManager& im,
   SkolemManager* sm = nm->getSkolemManager();
   d_ranVariable = sm->mkDummySkolem(
       "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME);
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
   ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
   if (pc != nullptr)
   {
@@ -56,7 +56,7 @@ CadSolver::~CadSolver() {}
 
 void CadSolver::initLastCall(const std::vector<Node>& assertions)
 {
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
   if (Trace.isOn("nl-cad"))
   {
     Trace("nl-cad") << "CadSolver::initLastCall" << std::endl;
@@ -83,7 +83,7 @@ void CadSolver::initLastCall(const std::vector<Node>& assertions)
 
 void CadSolver::checkFull()
 {
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
   if (d_CAC.getConstraints().getConstraints().empty()) {
     Trace("nl-cad") << "No constraints. Return." << std::endl;
     return;
@@ -115,7 +115,7 @@ void CadSolver::checkFull()
 
 void CadSolver::checkPartial()
 {
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
   if (d_CAC.getConstraints().getConstraints().empty()) {
     Trace("nl-cad") << "No constraints. Return." << std::endl;
     return;
@@ -165,7 +165,7 @@ void CadSolver::checkPartial()
 
 bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions)
 {
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
   if (!d_foundSatisfiability)
   {
     return false;
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 2ea27fce7..1d51cf9c5 100644
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -87,7 +87,7 @@ class CadSolver
    */
   Node d_ranVariable;
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
   /**
    * The object implementing the actual decision procedure.
    */
diff --git a/src/theory/arith/nl/icp/candidate.cpp b/src/theory/arith/nl/icp/candidate.cpp
index 31b7b085b..4a6d0748a 100644
--- a/src/theory/arith/nl/icp/candidate.cpp
+++ b/src/theory/arith/nl/icp/candidate.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/arith/nl/icp/candidate.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include <iostream>
 
diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h
index 524342658..d65db52b5 100644
--- a/src/theory/arith/nl/icp/candidate.h
+++ b/src/theory/arith/nl/icp/candidate.h
@@ -17,7 +17,7 @@
 
 #include "cvc4_private.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 #include <poly/polyxx.h>
 
 #include "expr/node.h"
diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index 2f6cdf220..39504c3aa 100644
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -32,7 +32,7 @@ namespace arith {
 namespace nl {
 namespace icp {
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 namespace {
 /** A simple wrapper to nicely print an interval assignment. */
@@ -366,7 +366,7 @@ void ICPSolver::check()
   }
 }
 
-#else /* CVC4_POLY_IMP */
+#else /* CVC5_POLY_IMP */
 
 void ICPSolver::reset(const std::vector<Node>& assertions)
 {
@@ -378,7 +378,7 @@ void ICPSolver::check()
   Unimplemented() << "ICPSolver requires CVC4 to be configured with LibPoly";
 }
 
-#endif /* CVC4_POLY_IMP */
+#endif /* CVC5_POLY_IMP */
 
 }  // namespace icp
 }  // namespace nl
diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index b392dc430..0efb2021f 100644
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -17,9 +17,9 @@
 
 #include "cvc4_private.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 #include <poly/polyxx.h>
-#endif /* CVC4_POLY_IMP */
+#endif /* CVC5_POLY_IMP */
 
 #include "expr/node.h"
 #include "theory/arith/bound_inference.h"
@@ -37,7 +37,7 @@ class InferenceManager;
 namespace nl {
 namespace icp {
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 /**
  * This class implements an ICP-based solver. As it is intended to be used in
@@ -137,7 +137,7 @@ class ICPSolver
   void check();
 };
 
-#else /* CVC4_POLY_IMP */
+#else /* CVC5_POLY_IMP */
 
 class ICPSolver
 {
@@ -147,7 +147,7 @@ class ICPSolver
   void check();
 };
 
-#endif /* CVC4_POLY_IMP */
+#endif /* CVC5_POLY_IMP */
 
 }  // namespace icp
 }  // namespace nl
diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp
index e0e93e1dd..6a914bc03 100644
--- a/src/theory/arith/nl/icp/intersection.cpp
+++ b/src/theory/arith/nl/icp/intersection.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/arith/nl/icp/intersection.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include <iostream>
 
diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h
index a77a605d0..a82ad6b8e 100644
--- a/src/theory/arith/nl/icp/intersection.h
+++ b/src/theory/arith/nl/icp/intersection.h
@@ -17,7 +17,7 @@
 
 #include "cvc4_private.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include <cstddef>
 
diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h
index 7716d029f..42f2084e0 100644
--- a/src/theory/arith/nl/icp/interval.h
+++ b/src/theory/arith/nl/icp/interval.h
@@ -17,7 +17,7 @@
 
 #include "cvc4_private.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 #include <poly/polyxx.h>
 
 #include "expr/node.h"
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index c7b549655..f708896a6 100644
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -16,7 +16,7 @@
 
 #include "poly_conversion.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include "expr/node.h"
 #include "expr/node_manager_attributes.h"
@@ -451,7 +451,7 @@ Node lower_bound_as_node(const Node& var,
       poly::get_upper(poly::get_isolating_interval(alg)));
   int sl = poly::sign_at(get_defining_polynomial(alg),
                          poly::get_lower(poly::get_isolating_interval(alg)));
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   int su = poly::sign_at(get_defining_polynomial(alg),
                          poly::get_upper(poly::get_isolating_interval(alg)));
   Assert(sl != 0 && su != 0 && sl != su);
@@ -507,7 +507,7 @@ Node upper_bound_as_node(const Node& var,
       poly::get_lower(poly::get_isolating_interval(alg)));
   Rational u = poly_utils::toRational(
       poly::get_upper(poly::get_isolating_interval(alg)));
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   int sl = poly::sign_at(get_defining_polynomial(alg),
                          poly::get_lower(poly::get_isolating_interval(alg)));
 #endif
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index 0a9d0f313..c97923f23 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -19,7 +19,7 @@
 
 #include "cvc4_private.h"
 
-#ifdef CVC4_POLY_IMP
+#ifdef CVC5_POLY_IMP
 
 #include <poly/polyxx.h>