Rename namespace CVC5 to cvc5. (#6258)

1 files changed, 32 insertions, 32 deletions

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index b839ccc22..f9f88cddf 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -4,13 +4,13 @@
 # src/theory/builtin/kinds.
 #
 
-theory THEORY_ARITH ::CVC5::theory::arith::TheoryArith "theory/arith/theory_arith.h"
+theory THEORY_ARITH ::cvc5::theory::arith::TheoryArith "theory/arith/theory_arith.h"
 typechecker "theory/arith/theory_arith_type_rules.h"
 
 properties stable-infinite
 properties check propagate ppStaticLearn presolve notifyRestart
 
-rewriter ::CVC5::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h"
+rewriter ::cvc5::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h"
 
 operator PLUS 2: "arithmetic addition (N-ary)"
 operator MULT 2: "arithmetic multiplication (N-ary)"
@@ -44,10 +44,10 @@ operator ARCCOTANGENT 1 "arc cotangent"
 operator SQRT 1 "square root"
 
 constant DIVISIBLE_OP \
-        ::CVC5::Divisible \
-        ::CVC5::DivisibleHashFunction \
+        ::cvc5::Divisible \
+        ::cvc5::DivisibleHashFunction \
         "util/divisible.h" \
-        "operator for the divisibility-by-k predicate; payload is an instance of the CVC5::Divisible class"
+        "operator for the divisibility-by-k predicate; payload is an instance of the cvc5::Divisible class"
 
 sort REAL_TYPE \
     Cardinality::REALS \
@@ -63,16 +63,16 @@ sort INTEGER_TYPE \
     "integer type"
 
 constant CONST_RATIONAL \
-    ::CVC5::Rational \
-    ::CVC5::RationalHashFunction \
+    ::cvc5::Rational \
+    ::cvc5::RationalHashFunction \
     "util/rational.h" \
-    "a multiple-precision rational constant; payload is an instance of the CVC5::Rational class"
+    "a multiple-precision rational constant; payload is an instance of the cvc5::Rational class"
 
 enumerator REAL_TYPE \
-    "::CVC5::theory::arith::RationalEnumerator" \
+    "::cvc5::theory::arith::RationalEnumerator" \
     "theory/arith/type_enumerator.h"
 enumerator INTEGER_TYPE \
-    "::CVC5::theory::arith::IntegerEnumerator" \
+    "::cvc5::theory::arith::IntegerEnumerator" \
     "theory/arith/type_enumerator.h"
 
 operator LT 2 "less than, x < y"
@@ -82,10 +82,10 @@ operator GEQ 2 "greater than or equal, x >= y"
 
 # represents an indexed root predicate. See util/indexed_root_predicate.h for more documentation.
 constant INDEXED_ROOT_PREDICATE_OP \
-	::CVC5::IndexedRootPredicate \
-	::CVC5::IndexedRootPredicateHashFunction \
+	::cvc5::IndexedRootPredicate \
+	::cvc5::IndexedRootPredicateHashFunction \
 	"util/indexed_root_predicate.h" \
-	"operator for the indexed root predicate; payload is an instance of the CVC5::IndexedRootPredicate class"
+	"operator for the indexed root predicate; payload is an instance of the cvc5::IndexedRootPredicate class"
 parameterized INDEXED_ROOT_PREDICATE INDEXED_ROOT_PREDICATE_OP 2 "indexed root predicate; first parameter is a INDEXED_ROOT_PREDICATE_OP, second is a real variable compared to zero, third is a polynomial"
 
 operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)"
@@ -99,15 +99,15 @@ operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this
 # This way, we avoid having 2 nested TO_REAL nodess as a result of Solver::mkTerm(TO_REAL, Solver::mkReal(int val))
 operator CAST_TO_REAL 1 "cast term to real same as TO_REAL, but it is used internally, whereas TO_REAL is accessible in the API"
 
-typerule PLUS ::CVC5::theory::arith::ArithOperatorTypeRule
-typerule MULT ::CVC5::theory::arith::ArithOperatorTypeRule
-typerule NONLINEAR_MULT ::CVC5::theory::arith::ArithOperatorTypeRule
-typerule MINUS ::CVC5::theory::arith::ArithOperatorTypeRule
-typerule UMINUS ::CVC5::theory::arith::ArithOperatorTypeRule
-typerule DIVISION ::CVC5::theory::arith::ArithOperatorTypeRule
-typerule POW ::CVC5::theory::arith::ArithOperatorTypeRule
+typerule PLUS ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule MULT ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule NONLINEAR_MULT ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule MINUS ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule UMINUS ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule DIVISION ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule POW ::cvc5::theory::arith::ArithOperatorTypeRule
 
-typerule CONST_RATIONAL ::CVC5::theory::arith::ArithConstantTypeRule
+typerule CONST_RATIONAL ::cvc5::theory::arith::ArithConstantTypeRule
 
 typerule LT "SimpleTypeRule<RBool, AReal, AReal>"
 typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>"
@@ -115,11 +115,11 @@ typerule GT "SimpleTypeRule<RBool, AReal, AReal>"
 typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>"
 
 typerule INDEXED_ROOT_PREDICATE_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule INDEXED_ROOT_PREDICATE ::CVC5::theory::arith::IndexedRootPredicateTypeRule
+typerule INDEXED_ROOT_PREDICATE ::cvc5::theory::arith::IndexedRootPredicateTypeRule
 
-typerule TO_REAL ::CVC5::theory::arith::ArithOperatorTypeRule
-typerule CAST_TO_REAL ::CVC5::theory::arith::ArithOperatorTypeRule
-typerule TO_INTEGER ::CVC5::theory::arith::ArithOperatorTypeRule
+typerule TO_REAL ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule CAST_TO_REAL ::cvc5::theory::arith::ArithOperatorTypeRule
+typerule TO_INTEGER ::cvc5::theory::arith::ArithOperatorTypeRule
 typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>"
 
 typerule ABS "SimpleTypeRule<RInteger, AInteger>"
@@ -128,7 +128,7 @@ typerule INTS_MODULUS "SimpleTypeRule<RInteger, AInteger, AInteger>"
 typerule DIVISIBLE "SimpleTypeRule<RBool, AInteger>"
 typerule DIVISIBLE_OP "SimpleTypeRule<RBuiltinOperator>"
 
-typerule DIVISION_TOTAL ::CVC5::theory::arith::ArithOperatorTypeRule
+typerule DIVISION_TOTAL ::cvc5::theory::arith::ArithOperatorTypeRule
 typerule INTS_DIVISION_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
 typerule INTS_MODULUS_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
 
@@ -150,20 +150,20 @@ typerule SQRT "SimpleTypeRule<RReal, AReal>"
 
 nullaryoperator PI "pi"
 
-typerule PI ::CVC5::theory::arith::RealNullaryOperatorTypeRule
+typerule PI ::cvc5::theory::arith::RealNullaryOperatorTypeRule
 
 # Integer AND, which is parameterized by a (positive) bitwidth k.
 # ((_ iand k) i1 i2) is equivalent to:
 # (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2)))
 # for all integers i1, i2.
 constant IAND_OP \
-	::CVC5::IntAnd \
-	"::CVC5::UnsignedHashFunction< ::CVC5::IntAnd >" \
+	::cvc5::IntAnd \
+	"::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >" \
 	"util/iand.h" \
-	"operator for integer AND; payload is an instance of the CVC5::IntAnd class"
+	"operator for integer AND; payload is an instance of the cvc5::IntAnd class"
 parameterized IAND IAND_OP 2 "integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms"
 
-typerule IAND_OP ::CVC5::theory::arith::IAndOpTypeRule
-typerule IAND ::CVC5::theory::arith::IAndTypeRule
+typerule IAND_OP ::cvc5::theory::arith::IAndOpTypeRule
+typerule IAND ::cvc5::theory::arith::IAndTypeRule
 
 endtheory