Rename CVC4_ macros to CVC5_. (#6327)

13 files changed, 25 insertions, 24 deletions

diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 96ab5b526..e399fac4c 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -166,7 +166,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 
 bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id)
 {
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i])));
 #endif
 
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index cac015904..5abdada71 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -16,7 +16,7 @@
 
 #include "prop/cadical.h"
 
-#ifdef CVC4_USE_CADICAL
+#ifdef CVC5_USE_CADICAL
 
 #include "base/check.h"
 
@@ -202,4 +202,4 @@ CadicalSolver::Statistics::~Statistics() {
 }  // namespace prop
 }  // namespace cvc5
 
-#endif  // CVC4_USE_CADICAL
+#endif  // CVC5_USE_CADICAL
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index ed4c166d4..e8a36d0a0 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -19,7 +19,7 @@
 #ifndef CVC5__PROP__CADICAL_H
 #define CVC5__PROP__CADICAL_H
 
-#ifdef CVC4_USE_CADICAL
+#ifdef CVC5_USE_CADICAL
 
 #include "prop/sat_solver.h"
 #include "util/stats_timer.h"
@@ -105,5 +105,5 @@ class CadicalSolver : public SatSolver
 }  // namespace prop
 }  // namespace cvc5
 
-#endif  // CVC4_USE_CADICAL
+#endif  // CVC5_USE_CADICAL
 #endif  // CVC5__PROP__CADICAL_H
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 10c84f582..111c6c2df 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -772,7 +772,7 @@ void CnfStream::convertAndAssert(TNode node, bool negated)
         convertAndAssertIff(node, negated);
         break;
       }
-      CVC4_FALLTHROUGH;
+      CVC5_FALLTHROUGH;
     default:
     {
       Node nnode = node;
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index ce5e4e2b0..5e0b056dc 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -14,7 +14,7 @@
  ** Implementation of the cryptominisat for cvc4 (bitvectors).
  **/
 
-#ifdef CVC4_USE_CRYPTOMINISAT
+#ifdef CVC5_USE_CRYPTOMINISAT
 
 #include "prop/cryptominisat.h"
 
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index ceed47d79..b217cee9c 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -19,7 +19,7 @@
 #ifndef CVC5__PROP__CRYPTOMINISAT_H
 #define CVC5__PROP__CRYPTOMINISAT_H
 
-#ifdef CVC4_USE_CRYPTOMINISAT
+#ifdef CVC5_USE_CRYPTOMINISAT
 
 #include "prop/sat_solver.h"
 #include "util/stats_timer.h"
@@ -108,5 +108,5 @@ class CryptoMinisatSolver : public SatSolver
 }  // namespace prop
 }  // namespace cvc5
 
-#endif  // CVC4_USE_CRYPTOMINISAT
+#endif  // CVC5_USE_CRYPTOMINISAT
 #endif  // CVC5__PROP__CRYPTOMINISAT_H
diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp
index 10b7b07de..949af2901 100644
--- a/src/prop/kissat.cpp
+++ b/src/prop/kissat.cpp
@@ -16,7 +16,7 @@
 
 #include "prop/kissat.h"
 
-#ifdef CVC4_USE_KISSAT
+#ifdef CVC5_USE_KISSAT
 
 #include "base/check.h"
 
@@ -175,4 +175,4 @@ KissatSolver::Statistics::~Statistics()
 }  // namespace prop
 }  // namespace cvc5
 
-#endif  // CVC4_USE_KISSAT
+#endif  // CVC5_USE_KISSAT
diff --git a/src/prop/kissat.h b/src/prop/kissat.h
index 2ab38dbab..b2bc8e074 100644
--- a/src/prop/kissat.h
+++ b/src/prop/kissat.h
@@ -19,7 +19,7 @@
 #ifndef CVC5__PROP__KISSAT_H
 #define CVC5__PROP__KISSAT_H
 
-#ifdef CVC4_USE_KISSAT
+#ifdef CVC5_USE_KISSAT
 
 #include "prop/sat_solver.h"
 #include "util/stats_timer.h"
@@ -99,5 +99,5 @@ class KissatSolver : public SatSolver
 }  // namespace prop
 }  // namespace cvc5
 
-#endif  // CVC4_USE_KISSAT
+#endif  // CVC5_USE_KISSAT
 #endif  // CVC5__PROP__KISSAT_H
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index e29c1032a..e8179c5fe 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -172,10 +172,11 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 
 bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 {
-#ifdef CVC4_ASSERTIONS
-    if (use_simplification) {
-      for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i])));
-    }
+#ifdef CVC5_ASSERTIONS
+  if (use_simplification)
+  {
+    for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i])));
+  }
 #endif
 
     int nclauses = clauses_persistent.size();
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index 76421db9b..8527950ce 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -127,7 +127,7 @@ void ProofCnfStream::convertAndAssert(TNode node, bool negated)
         convertAndAssertIff(node, negated);
         break;
       }
-      CVC4_FALLTHROUGH;
+      CVC5_FALLTHROUGH;
     default:
     {
       // negate
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 0d075de45..ec29d6bd5 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -352,7 +352,7 @@ void SatProofManager::explainLit(
     printClause(reason);
     Trace("sat-proof") << "\n";
   }
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   // pedantically check that the negation of the literal to explain *does not*
   // occur in the reason, otherwise we will loop forever
   for (unsigned i = 0; i < size; ++i)
@@ -372,7 +372,7 @@ void SatProofManager::explainLit(
   Trace("sat-proof") << push;
   for (unsigned i = 0; i < size; ++i)
   {
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
     // pedantically make sure that the reason stays the same
     const Minisat::Clause& reloadedReason = d_solver->ca[reasonRef];
     AlwaysAssert(size == static_cast<unsigned>(reloadedReason.size()));
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 117210431..90eec9153 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -42,7 +42,7 @@ MinisatSatSolver* SatSolverFactory::createCDCLTMinisat(
 SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
                                                  const std::string& name)
 {
-#ifdef CVC4_USE_CRYPTOMINISAT
+#ifdef CVC5_USE_CRYPTOMINISAT
   CryptoMinisatSolver* res = new CryptoMinisatSolver(registry, name);
   res->init();
   return res;
@@ -54,7 +54,7 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
 SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry,
                                            const std::string& name)
 {
-#ifdef CVC4_USE_CADICAL
+#ifdef CVC5_USE_CADICAL
   CadicalSolver* res = new CadicalSolver(registry, name);
   res->init();
   return res;
@@ -66,7 +66,7 @@ SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry,
 SatSolver* SatSolverFactory::createKissat(StatisticsRegistry* registry,
                                           const std::string& name)
 {
-#ifdef CVC4_USE_KISSAT
+#ifdef CVC5_USE_KISSAT
   KissatSolver* res = new KissatSolver(registry, name);
   res->init();
   return res;
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 503b37ed7..e4924ded4 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -21,7 +21,7 @@
 
 // Just defining this for now, since there's no other SAT solver bindings.
 // Optional blocks below will be unconditionally included
-#define CVC4_USE_MINISAT
+#define CVC5_USE_MINISAT
 
 #include <unordered_set>