Rename namespace CVC5 to cvc5. (#6258)

11 files changed, 49 insertions, 49 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 48ceaf103..e2f69f19d 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -196,7 +196,7 @@
 #     is with your type checker:
 #
 #       cardinality MY_TYPE \
-#           ::CVC5::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \
+#           ::cvc5::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \
 #           "theory/foo/theory_foo_type_rules.h"
 #
 #   well-founded K wellfoundedness-computer ground-term-computer [header]
@@ -240,13 +240,13 @@
 # commands.
 #
 
-theory THEORY_BUILTIN ::CVC5::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h"
+theory THEORY_BUILTIN ::cvc5::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h"
 typechecker "theory/builtin/theory_builtin_type_rules.h"
 
 properties stable-infinite
 
 # Rewriter responsible for all the terms of the theory
-rewriter ::CVC5::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h"
+rewriter ::cvc5::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h"
 
 sort BUILTIN_OPERATOR_TYPE \
     Cardinality::INTEGERS \
@@ -259,33 +259,33 @@ parameterized SORT_TYPE SORT_TAG 0: "specifies types of user-declared 'uninterpr
 # enough (for now) ?
 cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
 well-founded SORT_TYPE \
-    "::CVC5::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
-    "::CVC5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)"
+    "::cvc5::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
+    "::cvc5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)"
 
 constant UNINTERPRETED_CONSTANT \
-    ::CVC5::UninterpretedConstant \
-    ::CVC5::UninterpretedConstantHashFunction \
+    ::cvc5::UninterpretedConstant \
+    ::cvc5::UninterpretedConstantHashFunction \
     "expr/uninterpreted_constant.h" \
-    "the kind of expressions representing uninterpreted constants; payload is an instance of the CVC5::UninterpretedConstant class (used in models)"
-typerule UNINTERPRETED_CONSTANT ::CVC5::theory::builtin::UninterpretedConstantTypeRule
+    "the kind of expressions representing uninterpreted constants; payload is an instance of the cvc5::UninterpretedConstant class (used in models)"
+typerule UNINTERPRETED_CONSTANT ::cvc5::theory::builtin::UninterpretedConstantTypeRule
 enumerator SORT_TYPE \
-    ::CVC5::theory::builtin::UninterpretedSortEnumerator \
+    ::cvc5::theory::builtin::UninterpretedSortEnumerator \
     "theory/builtin/type_enumerator.h"
 
 constant ABSTRACT_VALUE \
-    ::CVC5::AbstractValue \
-    ::CVC5::AbstractValueHashFunction \
+    ::cvc5::AbstractValue \
+    ::cvc5::AbstractValueHashFunction \
     "util/abstract_value.h" \
-    "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the CVC5::AbstractValue class (used in models)"
-typerule ABSTRACT_VALUE ::CVC5::theory::builtin::AbstractValueTypeRule
+    "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the cvc5::AbstractValue class (used in models)"
+typerule ABSTRACT_VALUE ::cvc5::theory::builtin::AbstractValueTypeRule
 
 # A kind representing "inlined" operators defined with OPERATOR
 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
 # not stored that way.  If you ask for the operator of (EQUAL a b),
 # you'll get a special, singleton (BUILTIN EQUAL) Node.
 constant BUILTIN \
-    ::CVC5::Kind \
-    ::CVC5::kind::KindHashFunction \
+    ::cvc5::Kind \
+    ::cvc5::kind::KindHashFunction \
     "expr/kind.h" \
     "the kind of expressions representing built-in operators"
 
@@ -301,33 +301,33 @@ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, sec
 operator WITNESS 2 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body"
 
 constant TYPE_CONSTANT \
-    ::CVC5::TypeConstant \
-    ::CVC5::TypeConstantHashFunction \
+    ::cvc5::TypeConstant \
+    ::cvc5::TypeConstantHashFunction \
     "expr/kind.h" \
     "a representation for basic types"
 operator FUNCTION_TYPE 2: "a function type"
 cardinality FUNCTION_TYPE \
-    "::CVC5::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
+    "::cvc5::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 well-founded FUNCTION_TYPE \
-    "::CVC5::theory::builtin::FunctionProperties::isWellFounded(%TYPE%)" \
-    "::CVC5::theory::builtin::FunctionProperties::mkGroundTerm(%TYPE%)" \
+    "::cvc5::theory::builtin::FunctionProperties::isWellFounded(%TYPE%)" \
+    "::cvc5::theory::builtin::FunctionProperties::mkGroundTerm(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 enumerator FUNCTION_TYPE \
-    ::CVC5::theory::builtin::FunctionEnumerator \
+    ::cvc5::theory::builtin::FunctionEnumerator \
     "theory/builtin/type_enumerator.h"
 sort SEXPR_TYPE \
     Cardinality::INTEGERS \
     not-well-founded \
     "the type of a symbolic expression"
 
-typerule EQUAL ::CVC5::theory::builtin::EqualityTypeRule
-typerule DISTINCT ::CVC5::theory::builtin::DistinctTypeRule
-typerule SEXPR ::CVC5::theory::builtin::SExprTypeRule
-typerule LAMBDA ::CVC5::theory::builtin::LambdaTypeRule
-typerule WITNESS ::CVC5::theory::builtin::WitnessTypeRule
+typerule EQUAL ::cvc5::theory::builtin::EqualityTypeRule
+typerule DISTINCT ::cvc5::theory::builtin::DistinctTypeRule
+typerule SEXPR ::cvc5::theory::builtin::SExprTypeRule
+typerule LAMBDA ::cvc5::theory::builtin::LambdaTypeRule
+typerule WITNESS ::cvc5::theory::builtin::WitnessTypeRule
 
 # lambda expressions that are isomorphic to array constants can be considered constants
-construle LAMBDA ::CVC5::theory::builtin::LambdaTypeRule
+construle LAMBDA ::cvc5::theory::builtin::LambdaTypeRule
 
 endtheory
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 62f0f1b9a..36a29f88a 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -20,9 +20,9 @@
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 const char* toString(MethodId id)
@@ -497,4 +497,4 @@ Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid)
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index ed68f1215..f80434068 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -22,7 +22,7 @@
 #include "expr/proof_node.h"
 #include "theory/quantifiers/extended_rewrite.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 /**
@@ -179,6 +179,6 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BUILTIN__PROOF_CHECKER_H */
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 83e9d3fed..bd0374675 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -24,7 +24,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace builtin {
 
@@ -62,4 +62,4 @@ void TheoryBuiltin::finishInit()
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 449282ae6..b4de83c02 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -23,7 +23,7 @@
 #include "theory/builtin/theory_builtin_rewriter.h"
 #include "theory/theory.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace builtin {
 
@@ -53,6 +53,6 @@ class TheoryBuiltin : public Theory
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 16fc59a5a..d76bd51dd 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -23,7 +23,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace builtin {
 
@@ -504,4 +504,4 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda(TNode n)
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index c419abdb3..7625aa846 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -22,7 +22,7 @@
 
 #include "theory/theory_rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace builtin {
 
@@ -119,6 +119,6 @@ class TheoryBuiltinRewriter : public TheoryRewriter
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */
diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp
index d5a5c9ab7..c5ea17847 100644
--- a/src/theory/builtin/theory_builtin_type_rules.cpp
+++ b/src/theory/builtin/theory_builtin_type_rules.cpp
@@ -18,7 +18,7 @@
 
 #include "expr/attribute.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace builtin {
 
@@ -47,4 +47,4 @@ Node SortProperties::mkGroundTerm(TypeNode type)
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 815483507..2c474aaee 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -25,7 +25,7 @@
 
 #include <sstream>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace builtin {
 
@@ -248,6 +248,6 @@ class FunctionProperties {
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */
diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp
index 4dda11070..2434bc521 100644
--- a/src/theory/builtin/type_enumerator.cpp
+++ b/src/theory/builtin/type_enumerator.cpp
@@ -18,7 +18,7 @@
 
 #include "theory/builtin/theory_builtin_rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace builtin {
 
@@ -49,4 +49,4 @@ FunctionEnumerator& FunctionEnumerator::operator++()
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index 50cd50dda..7c14bb14c 100644
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -25,7 +25,7 @@
 #include "theory/type_enumerator.h"
 #include "util/integer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace builtin {
 
@@ -106,6 +106,6 @@ class FunctionEnumerator : public TypeEnumeratorBase<FunctionEnumerator>
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */