Rename namespace CVC5 to cvc5. (#6258)

1 files changed, 82 insertions, 82 deletions

diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 884ee49e6..3a1032bc3 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -4,36 +4,36 @@
 # src/theory/builtin/kinds.
 #
 
-theory THEORY_BV ::CVC5::theory::bv::TheoryBV "theory/bv/theory_bv.h"
+theory THEORY_BV ::cvc5::theory::bv::TheoryBV "theory/bv/theory_bv.h"
 typechecker "theory/bv/theory_bv_type_rules.h"
 
 properties finite
 properties check propagate presolve ppStaticLearn
 
-rewriter ::CVC5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
+rewriter ::cvc5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
 
 constant BITVECTOR_TYPE \
-	::CVC5::BitVectorSize \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorSize >" \
+	::cvc5::BitVectorSize \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \
 	"util/bitvector.h" \
 	"bit-vector type"
 cardinality BITVECTOR_TYPE \
-	"::CVC5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
+	"::cvc5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
 	"theory/bv/theory_bv_type_rules.h"
 
 constant CONST_BITVECTOR \
-    ::CVC5::BitVector \
-    ::CVC5::BitVectorHashFunction \
+    ::cvc5::BitVector \
+    ::cvc5::BitVectorHashFunction \
     "util/bitvector.h" \
-    "a fixed-width bit-vector constant; payload is an instance of the CVC5::BitVector class"
+    "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class"
 
 enumerator BITVECTOR_TYPE \
-    "::CVC5::theory::bv::BitVectorEnumerator" \
+    "::cvc5::theory::bv::BitVectorEnumerator" \
     "theory/bv/type_enumerator.h"
 
 well-founded BITVECTOR_TYPE \
     true \
-    "(*CVC5::theory::TypeEnumerator(%TYPE%))" \
+    "(*cvc5::theory::TypeEnumerator(%TYPE%))" \
     "theory/type_enumerator.h"
 
 ### non-parameterized operator kinds ------------------------------------------
@@ -99,139 +99,139 @@ operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bi
 ### parameterized operator kinds ----------------------------------------------
 
 constant BITVECTOR_BITOF_OP \
-	::CVC5::BitVectorBitOf \
-	::CVC5::BitVectorBitOfHashFunction \
+	::cvc5::BitVectorBitOf \
+	::cvc5::BitVectorBitOfHashFunction \
 	"util/bitvector.h" \
-	"operator for the bit-vector boolean bit extract; payload is an instance of the CVC5::BitVectorBitOf class"
+	"operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class"
 parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term"
 
 constant BITVECTOR_EXTRACT_OP \
-	::CVC5::BitVectorExtract \
-	::CVC5::BitVectorExtractHashFunction \
+	::cvc5::BitVectorExtract \
+	::cvc5::BitVectorExtractHashFunction \
 	"util/bitvector.h" \
-	"operator for the bit-vector extract; payload is an instance of the CVC5::BitVectorExtract class"
+	"operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class"
 parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term"
 
 constant BITVECTOR_REPEAT_OP \
-	::CVC5::BitVectorRepeat \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRepeat >" \
+	::cvc5::BitVectorRepeat \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector repeat; payload is an instance of the CVC5::BitVectorRepeat class"
+	"operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class"
 parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term"
 
 constant BITVECTOR_ROTATE_LEFT_OP \
-	::CVC5::BitVectorRotateLeft \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRotateLeft >" \
+	::cvc5::BitVectorRotateLeft \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector rotate left; payload is an instance of the CVC5::BitVectorRotateLeft class"
+	"operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class"
 parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term"
 
 constant BITVECTOR_ROTATE_RIGHT_OP \
-	::CVC5::BitVectorRotateRight \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRotateRight >" \
+	::cvc5::BitVectorRotateRight \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector rotate right; payload is an instance of the CVC5::BitVectorRotateRight class"
+	"operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class"
 parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term"
 
 constant BITVECTOR_SIGN_EXTEND_OP \
-	::CVC5::BitVectorSignExtend \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorSignExtend >" \
+	::cvc5::BitVectorSignExtend \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector sign-extend; payload is an instance of the CVC5::BitVectorSignExtend class"
+	"operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class"
 parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term"
 
 constant BITVECTOR_ZERO_EXTEND_OP \
-	::CVC5::BitVectorZeroExtend \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorZeroExtend >" \
+	::cvc5::BitVectorZeroExtend \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector zero-extend; payload is an instance of the CVC5::BitVectorZeroExtend class"
+	"operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class"
 parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term"
 
 constant INT_TO_BITVECTOR_OP \
-	::CVC5::IntToBitVector \
-	"::CVC5::UnsignedHashFunction< ::CVC5::IntToBitVector >" \
+	::cvc5::IntToBitVector \
+	"::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \
 	"util/bitvector.h" \
-	"operator for the integer conversion to bit-vector; payload is an instance of the CVC5::IntToBitVector class"
+	"operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class"
 parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term"
 
 ### type rules for non-parameterized operator kinds ---------------------------
 
-typerule CONST_BITVECTOR ::CVC5::theory::bv::BitVectorConstantTypeRule
+typerule CONST_BITVECTOR ::cvc5::theory::bv::BitVectorConstantTypeRule
 
 ## concatentation kind
-typerule BITVECTOR_CONCAT ::CVC5::theory::bv::BitVectorConcatTypeRule
+typerule BITVECTOR_CONCAT ::cvc5::theory::bv::BitVectorConcatTypeRule
 
 ## bit-wise kinds
-typerule BITVECTOR_AND ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_COMP ::CVC5::theory::bv::BitVectorBVPredTypeRule
-typerule BITVECTOR_NAND ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_NOR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_NOT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_OR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_XNOR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_XOR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_AND ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_COMP ::cvc5::theory::bv::BitVectorBVPredTypeRule
+typerule BITVECTOR_NAND ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NOR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NOT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_OR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_XNOR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_XOR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 
 ## arithmetic kinds
-typerule BITVECTOR_MULT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_NEG ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_PLUS ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SUB ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_UDIV ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_UREM ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SDIV ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SMOD ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SREM ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_MULT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NEG ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_PLUS ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SUB ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_UDIV ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_UREM ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SDIV ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SMOD ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SREM ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 
 ## shift kinds
-typerule BITVECTOR_ASHR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_LSHR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SHL ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ASHR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_LSHR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SHL ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 
 ## inequality kinds
-typerule BITVECTOR_ULE ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_ULT ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_UGE ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_UGT ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SLE ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SLT ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SGE ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SGT ::CVC5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_ULE ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_ULT ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_UGE ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_UGT ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SLE ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SLT ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SGE ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SGT ::cvc5::theory::bv::BitVectorPredicateTypeRule
 # inequalities with return type bit-vector of size 1
-typerule BITVECTOR_ULTBV ::CVC5::theory::bv::BitVectorBVPredTypeRule
-typerule BITVECTOR_SLTBV ::CVC5::theory::bv::BitVectorBVPredTypeRule
+typerule BITVECTOR_ULTBV ::cvc5::theory::bv::BitVectorBVPredTypeRule
+typerule BITVECTOR_SLTBV ::cvc5::theory::bv::BitVectorBVPredTypeRule
 
 ## if-then-else kind
-typerule BITVECTOR_ITE ::CVC5::theory::bv::BitVectorITETypeRule
+typerule BITVECTOR_ITE ::cvc5::theory::bv::BitVectorITETypeRule
 
 ## reduction kinds
-typerule BITVECTOR_REDAND ::CVC5::theory::bv::BitVectorUnaryPredicateTypeRule
-typerule BITVECTOR_REDOR ::CVC5::theory::bv::BitVectorUnaryPredicateTypeRule
+typerule BITVECTOR_REDAND ::cvc5::theory::bv::BitVectorUnaryPredicateTypeRule
+typerule BITVECTOR_REDOR ::cvc5::theory::bv::BitVectorUnaryPredicateTypeRule
 
 ## conversion kinds
-typerule BITVECTOR_TO_NAT ::CVC5::theory::bv::BitVectorConversionTypeRule
+typerule BITVECTOR_TO_NAT ::cvc5::theory::bv::BitVectorConversionTypeRule
 
 ## internal kinds
-typerule BITVECTOR_ACKERMANNIZE_UDIV ::CVC5::theory::bv::BitVectorAckermanizationUdivTypeRule
-typerule BITVECTOR_ACKERMANNIZE_UREM ::CVC5::theory::bv::BitVectorAckermanizationUremTypeRule
-typerule BITVECTOR_EAGER_ATOM ::CVC5::theory::bv::BitVectorEagerAtomTypeRule
+typerule BITVECTOR_ACKERMANNIZE_UDIV ::cvc5::theory::bv::BitVectorAckermanizationUdivTypeRule
+typerule BITVECTOR_ACKERMANNIZE_UREM ::cvc5::theory::bv::BitVectorAckermanizationUremTypeRule
+typerule BITVECTOR_EAGER_ATOM ::cvc5::theory::bv::BitVectorEagerAtomTypeRule
 
 ### type rules for parameterized operator kinds -------------------------------
 
 typerule BITVECTOR_BITOF_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_BITOF ::CVC5::theory::bv::BitVectorBitOfTypeRule
+typerule BITVECTOR_BITOF ::cvc5::theory::bv::BitVectorBitOfTypeRule
 typerule BITVECTOR_EXTRACT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_EXTRACT ::CVC5::theory::bv::BitVectorExtractTypeRule
+typerule BITVECTOR_EXTRACT ::cvc5::theory::bv::BitVectorExtractTypeRule
 typerule BITVECTOR_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_REPEAT ::CVC5::theory::bv::BitVectorRepeatTypeRule
+typerule BITVECTOR_REPEAT ::cvc5::theory::bv::BitVectorRepeatTypeRule
 typerule BITVECTOR_ROTATE_LEFT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_ROTATE_LEFT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ROTATE_LEFT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_ROTATE_RIGHT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_ROTATE_RIGHT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ROTATE_RIGHT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_SIGN_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_SIGN_EXTEND ::CVC5::theory::bv::BitVectorExtendTypeRule
+typerule BITVECTOR_SIGN_EXTEND ::cvc5::theory::bv::BitVectorExtendTypeRule
 typerule BITVECTOR_ZERO_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_ZERO_EXTEND ::CVC5::theory::bv::BitVectorExtendTypeRule
-typerule INT_TO_BITVECTOR_OP ::CVC5::theory::bv::IntToBitVectorOpTypeRule
-typerule INT_TO_BITVECTOR ::CVC5::theory::bv::BitVectorConversionTypeRule
+typerule BITVECTOR_ZERO_EXTEND ::cvc5::theory::bv::BitVectorExtendTypeRule
+typerule INT_TO_BITVECTOR_OP ::cvc5::theory::bv::IntToBitVectorOpTypeRule
+typerule INT_TO_BITVECTOR ::cvc5::theory::bv::BitVectorConversionTypeRule
 
 endtheory