Rename namespace CVC4 to CVC5. (#6249)

25 files changed, 84 insertions, 82 deletions

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index b36c6eb96..eebe14226 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -28,10 +28,10 @@
 #include "theory/uf/theory_uf.h"
 
 using namespace std;
-using namespace CVC4::kind;
-using namespace CVC4::context;
+using namespace CVC5::kind;
+using namespace CVC5::context;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -1764,6 +1764,6 @@ CardinalityExtension::Statistics::~Statistics()
   smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
 }
 
-}/* CVC4::theory namespace::uf */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace uf
+}  // namespace theory
+}  // namespace CVC5
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index d701adfc4..85129a89b 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -23,7 +23,7 @@
 #include "theory/theory.h"
 #include "util/statistics_registry.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -461,8 +461,8 @@ class CardinalityExtension
   NodeBoolMap d_rel_eqc;
 }; /* class CardinalityExtension */
 
-}/* CVC4::theory namespace::uf */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace uf
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY_UF_STRONG_SOLVER_H */
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 3cbac95a2..fec9179f3 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -20,7 +20,7 @@
 #include "expr/proof_checker.h"
 #include "options/uf_options.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace eq {
 
@@ -1438,4 +1438,4 @@ Node EqProof::addToProof(
 
 }  // namespace eq
 }  // Namespace theory
-}  // Namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h
index 2effb88a9..665731d2b 100644
--- a/src/theory/uf/eq_proof.h
+++ b/src/theory/uf/eq_proof.h
@@ -17,7 +17,7 @@
 #include "expr/node.h"
 #include "theory/uf/equality_engine_types.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class CDProof;
 
@@ -355,4 +355,4 @@ class EqProof
 
 }  // Namespace eq
 }  // Namespace theory
-}  // Namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 2d34bd547..a4bb76245 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -24,7 +24,7 @@
 #include "theory/rewriter.h"
 #include "theory/uf/eq_proof.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace eq {
 
@@ -2635,4 +2635,4 @@ EqualityNodeId EqualityEngine::TriggerTermSet::getTrigger(TheoryId tag) const
 
 } // Namespace uf
 } // Namespace theory
-} // Namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index d1c0ece95..74af68227 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -35,7 +35,7 @@
 #include "theory/uf/equality_engine_types.h"
 #include "util/statistics_registry.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace eq {
 
@@ -845,6 +845,6 @@ private:
 
 } // Namespace eq
 } // Namespace theory
-} // Namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/uf/equality_engine_iterator.cpp b/src/theory/uf/equality_engine_iterator.cpp
index 48b2552cd..c9a35f6e3 100644
--- a/src/theory/uf/equality_engine_iterator.cpp
+++ b/src/theory/uf/equality_engine_iterator.cpp
@@ -16,7 +16,7 @@
 
 #include "theory/uf/equality_engine.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace eq {
 
@@ -132,4 +132,4 @@ bool EqClassIterator::isFinished() const { return d_current == null_id; }
 
 }  // namespace eq
 }  // Namespace theory
-}  // Namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/uf/equality_engine_iterator.h b/src/theory/uf/equality_engine_iterator.h
index 1d1089090..33562a99e 100644
--- a/src/theory/uf/equality_engine_iterator.h
+++ b/src/theory/uf/equality_engine_iterator.h
@@ -20,7 +20,7 @@
 #include "expr/node.h"
 #include "theory/uf/equality_engine_types.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace eq {
 
@@ -79,6 +79,6 @@ class EqClassIterator
 
 }  // Namespace eq
 }  // Namespace theory
-}  // Namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/uf/equality_engine_notify.h b/src/theory/uf/equality_engine_notify.h
index 7904d7cf6..bd353375f 100644
--- a/src/theory/uf/equality_engine_notify.h
+++ b/src/theory/uf/equality_engine_notify.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace eq {
 
@@ -115,6 +115,6 @@ class EqualityEngineNotifyNone : public EqualityEngineNotify
 
 }  // Namespace eq
 }  // Namespace theory
-}  // Namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 5714099f9..092b4bd89 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -26,7 +26,7 @@
 
 #include "util/hash.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace eq {
 
@@ -359,6 +359,6 @@ struct TriggerInfo {
 
 } // namespace eq
 } // namespace theory
-} // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H */
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 7984813ac..c159ff3b4 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -21,9 +21,9 @@
 #include "theory/uf/theory_uf_rewriter.h"
 
 using namespace std;
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -455,4 +455,4 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
 
 }  // namespace uf
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h
index 90b0b67c5..3ca647f28 100644
--- a/src/theory/uf/ho_extension.h
+++ b/src/theory/uf/ho_extension.h
@@ -25,7 +25,7 @@
 #include "theory/theory_model.h"
 #include "theory/theory_state.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -198,6 +198,6 @@ class HoExtension
 
 }  // namespace uf
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* __CVC4__THEORY__UF__HO_EXTENSION_H */
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 9564899fe..ab2e422ee 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -4,32 +4,32 @@
 # src/theory/builtin/kinds.
 #
 
-theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h"
+theory THEORY_UF ::CVC5::theory::uf::TheoryUF "theory/uf/theory_uf.h"
 typechecker "theory/uf/theory_uf_type_rules.h"
 
 properties stable-infinite parametric
 properties check ppStaticLearn presolve
 
-rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
+rewriter ::CVC5::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
 parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function"
 
-typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule
+typerule APPLY_UF ::CVC5::theory::uf::UfTypeRule
 
 variable BOOLEAN_TERM_VARIABLE "Boolean term variable"
 
 operator CARDINALITY_CONSTRAINT 2 "cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S"
-typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule
+typerule CARDINALITY_CONSTRAINT ::CVC5::theory::uf::CardinalityConstraintTypeRule
 
 operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature"
-typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule
+typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC5::theory::uf::CombinedCardinalityConstraintTypeRule
 
 parameterized PARTIAL_APPLY_UF APPLY_UF 1: "partial uninterpreted function application"
-typerule PARTIAL_APPLY_UF ::CVC4::theory::uf::PartialTypeRule
+typerule PARTIAL_APPLY_UF ::CVC5::theory::uf::PartialTypeRule
 
 operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S"
-typerule CARDINALITY_VALUE ::CVC4::theory::uf::CardinalityValueTypeRule
+typerule CARDINALITY_VALUE ::CVC5::theory::uf::CardinalityValueTypeRule
 
 operator HO_APPLY 2 "higher-order (partial) function application"
-typerule HO_APPLY ::CVC4::theory::uf::HoApplyTypeRule
+typerule HO_APPLY ::CVC5::theory::uf::HoApplyTypeRule
 
 endtheory
diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp
index 2c102c4ca..2688c0574 100644
--- a/src/theory/uf/proof_checker.cpp
+++ b/src/theory/uf/proof_checker.cpp
@@ -16,9 +16,9 @@
 
 #include "theory/uf/theory_uf_rewriter.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -207,4 +207,4 @@ Node UfProofRuleChecker::checkInternal(PfRule id,
 
 }  // namespace uf
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/uf/proof_checker.h b/src/theory/uf/proof_checker.h
index bb999dc15..502aeaa59 100644
--- a/src/theory/uf/proof_checker.h
+++ b/src/theory/uf/proof_checker.h
@@ -21,7 +21,7 @@
 #include "expr/proof_checker.h"
 #include "expr/proof_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -44,6 +44,6 @@ class UfProofRuleChecker : public ProofRuleChecker
 
 }  // namespace uf
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__UF__PROOF_CHECKER_H */
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 7db887b56..2837a02aa 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -22,9 +22,9 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_checker.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace eq {
 
@@ -549,4 +549,4 @@ void ProofEqEngine::explainWithProof(Node lit,
 
 }  // namespace eq
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index adf8d2c18..5129ad1df 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -26,7 +26,7 @@
 #include "expr/node.h"
 #include "theory/eager_proof_generator.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofNode;
 class ProofNodeManager;
@@ -296,6 +296,6 @@ class ProofEqEngine : public EagerProofGenerator
 
 }  // namespace eq
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__STRINGS__PROOF_MANAGER_H */
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index ca7254fb6..9b25c8906 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -48,11 +48,11 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
-using namespace ::CVC4::context;
+using namespace ::CVC5::context;
 
 SymmetryBreaker::Template::Template() :
   d_template(),
@@ -800,8 +800,8 @@ void SymmetryBreaker::insertUsedIn(Term term, const Permutation& p, set<Node>& c
   }
 }
 
-}/* CVC4::theory::uf namespace */
-}/* CVC4::theory namespace */
+}  // namespace uf
+}  // namespace theory
 
 std::ostream& operator<<(std::ostream& out, const theory::uf::SymmetryBreaker::Permutation& p) {
   out << "{";
@@ -816,4 +816,4 @@ std::ostream& operator<<(std::ostream& out, const theory::uf::SymmetryBreaker::P
   return out;
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 2a95e5bc7..8ce0c2c44 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -57,7 +57,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_timer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -170,11 +170,13 @@ private:
 
 };/* class SymmetryBreaker */
 
-}/* CVC4::theory::uf namespace */
-}/* CVC4::theory namespace */
+}  // namespace uf
+}  // namespace theory
 
-std::ostream& operator<<(std::ostream& out, const ::CVC4::theory::uf::SymmetryBreaker::Permutation& p);
+std::ostream& operator<<(
+    std::ostream& out,
+    const ::CVC5::theory::uf::SymmetryBreaker::Permutation& p);
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__UF__SYMMETRY_BREAKER_H */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index aaa9d60f0..29bb6ba7d 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -35,7 +35,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -691,6 +691,6 @@ bool TheoryUF::isHigherOrderType(TypeNode tn)
   return ret;
 }
 
-} /* namespace CVC4::theory::uf */
-} /* namespace CVC4::theory */
-} /* namespace CVC4 */
+}  // namespace uf
+}  // namespace theory
+} // namespace CVC5
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 8d2edaffe..97cfc1fa5 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -29,7 +29,7 @@
 #include "theory/uf/symmetry_breaker.h"
 #include "theory/uf/theory_uf_rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -181,8 +181,8 @@ private:
   std::map<TypeNode, bool> d_isHoType;
 };/* class TheoryUF */
 
-}/* CVC4::theory::uf namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace uf
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__UF__THEORY_UF_H */
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index abb0c2e6c..5727d62cd 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -21,9 +21,9 @@
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -243,4 +243,4 @@ Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){
 
 }  // namespace uf
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 62ec8204f..b1e0eea8f 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -21,7 +21,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 
 class TheoryModel;
@@ -114,6 +114,6 @@ public:
 
 }
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index ea4f66d16..ffa0ec22f 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -26,7 +26,7 @@
 #include "theory/substitutions.h"
 #include "theory/theory_rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -208,8 +208,8 @@ public: //conversion between HO_APPLY AND APPLY_UF
   }
 }; /* class TheoryUfRewriter */
 
-}/* CVC4::theory::uf namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace uf
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__UF__THEORY_UF_REWRITER_H */
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index aad1ad63d..c21b36669 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -21,7 +21,7 @@
 
 #include <climits>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace uf {
 
@@ -80,7 +80,7 @@ class CardinalityConstraintTypeRule {
         throw TypeCheckingExceptionPrivate(
             n, "cardinality constraint must be a constant");
       }
-      CVC4::Rational r(INT_MAX);
+      CVC5::Rational r(INT_MAX);
       if (n[1].getConst<Rational>() > r) {
         throw TypeCheckingExceptionPrivate(
             n, "Exceeded INT_MAX in cardinality constraint");
@@ -108,7 +108,7 @@ class CombinedCardinalityConstraintTypeRule {
         throw TypeCheckingExceptionPrivate(
             n, "combined cardinality constraint must be a constant");
       }
-      CVC4::Rational r(INT_MAX);
+      CVC5::Rational r(INT_MAX);
       if (n[0].getConst<Rational>() > r) {
         throw TypeCheckingExceptionPrivate(
             n, "Exceeded INT_MAX in combined cardinality constraint");
@@ -176,8 +176,8 @@ class HoApplyTypeRule {
   }
 }; /* class HoApplyTypeRule */
 
-} /* CVC4::theory::uf namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+}  // namespace uf
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H */