diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-31 15:23:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-31 22:23:17 +0000 |
commit | a1466978fbc328507406d4a121dab4d1a1047e1d (patch) | |
tree | 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/theory/bv/kinds | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'src/theory/bv/kinds')
-rw-r--r-- | src/theory/bv/kinds | 164 |
1 files changed, 82 insertions, 82 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 32e0e9e85..884ee49e6 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -4,36 +4,36 @@ # src/theory/builtin/kinds. # -theory THEORY_BV ::CVC4::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 ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" +rewriter ::CVC5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" constant BITVECTOR_TYPE \ - ::CVC4::BitVectorSize \ - "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSize >" \ + ::CVC5::BitVectorSize \ + "::CVC5::UnsignedHashFunction< ::CVC5::BitVectorSize >" \ "util/bitvector.h" \ "bit-vector type" cardinality BITVECTOR_TYPE \ - "::CVC4::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \ + "::CVC5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \ "theory/bv/theory_bv_type_rules.h" constant CONST_BITVECTOR \ - ::CVC4::BitVector \ - ::CVC4::BitVectorHashFunction \ + ::CVC5::BitVector \ + ::CVC5::BitVectorHashFunction \ "util/bitvector.h" \ - "a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class" + "a fixed-width bit-vector constant; payload is an instance of the CVC5::BitVector class" enumerator BITVECTOR_TYPE \ - "::CVC4::theory::bv::BitVectorEnumerator" \ + "::CVC5::theory::bv::BitVectorEnumerator" \ "theory/bv/type_enumerator.h" well-founded BITVECTOR_TYPE \ true \ - "(*CVC4::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 \ - ::CVC4::BitVectorBitOf \ - ::CVC4::BitVectorBitOfHashFunction \ + ::CVC5::BitVectorBitOf \ + ::CVC5::BitVectorBitOfHashFunction \ "util/bitvector.h" \ - "operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::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 \ - ::CVC4::BitVectorExtract \ - ::CVC4::BitVectorExtractHashFunction \ + ::CVC5::BitVectorExtract \ + ::CVC5::BitVectorExtractHashFunction \ "util/bitvector.h" \ - "operator for the bit-vector extract; payload is an instance of the CVC4::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 \ - ::CVC4::BitVectorRepeat \ - "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >" \ + ::CVC5::BitVectorRepeat \ + "::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRepeat >" \ "util/bitvector.h" \ - "operator for the bit-vector repeat; payload is an instance of the CVC4::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 \ - ::CVC4::BitVectorRotateLeft \ - "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >" \ + ::CVC5::BitVectorRotateLeft \ + "::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRotateLeft >" \ "util/bitvector.h" \ - "operator for the bit-vector rotate left; payload is an instance of the CVC4::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 \ - ::CVC4::BitVectorRotateRight \ - "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >" \ + ::CVC5::BitVectorRotateRight \ + "::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRotateRight >" \ "util/bitvector.h" \ - "operator for the bit-vector rotate right; payload is an instance of the CVC4::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 \ - ::CVC4::BitVectorSignExtend \ - "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >" \ + ::CVC5::BitVectorSignExtend \ + "::CVC5::UnsignedHashFunction< ::CVC5::BitVectorSignExtend >" \ "util/bitvector.h" \ - "operator for the bit-vector sign-extend; payload is an instance of the CVC4::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 \ - ::CVC4::BitVectorZeroExtend \ - "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >" \ + ::CVC5::BitVectorZeroExtend \ + "::CVC5::UnsignedHashFunction< ::CVC5::BitVectorZeroExtend >" \ "util/bitvector.h" \ - "operator for the bit-vector zero-extend; payload is an instance of the CVC4::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 \ - ::CVC4::IntToBitVector \ - "::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >" \ + ::CVC5::IntToBitVector \ + "::CVC5::UnsignedHashFunction< ::CVC5::IntToBitVector >" \ "util/bitvector.h" \ - "operator for the integer conversion to bit-vector; payload is an instance of the CVC4::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 ::CVC4::theory::bv::BitVectorConstantTypeRule +typerule CONST_BITVECTOR ::CVC5::theory::bv::BitVectorConstantTypeRule ## concatentation kind -typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatTypeRule +typerule BITVECTOR_CONCAT ::CVC5::theory::bv::BitVectorConcatTypeRule ## bit-wise kinds -typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorBVPredTypeRule -typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_NOT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_OR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_XOR ::CVC4::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 ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_SUB ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_SREM ::CVC4::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 ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_LSHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_SHL ::CVC4::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 ::CVC4::theory::bv::BitVectorPredicateTypeRule -typerule BITVECTOR_ULT ::CVC4::theory::bv::BitVectorPredicateTypeRule -typerule BITVECTOR_UGE ::CVC4::theory::bv::BitVectorPredicateTypeRule -typerule BITVECTOR_UGT ::CVC4::theory::bv::BitVectorPredicateTypeRule -typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule -typerule BITVECTOR_SLT ::CVC4::theory::bv::BitVectorPredicateTypeRule -typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule -typerule BITVECTOR_SGT ::CVC4::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 ::CVC4::theory::bv::BitVectorBVPredTypeRule -typerule BITVECTOR_SLTBV ::CVC4::theory::bv::BitVectorBVPredTypeRule +typerule BITVECTOR_ULTBV ::CVC5::theory::bv::BitVectorBVPredTypeRule +typerule BITVECTOR_SLTBV ::CVC5::theory::bv::BitVectorBVPredTypeRule ## if-then-else kind -typerule BITVECTOR_ITE ::CVC4::theory::bv::BitVectorITETypeRule +typerule BITVECTOR_ITE ::CVC5::theory::bv::BitVectorITETypeRule ## reduction kinds -typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule -typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule +typerule BITVECTOR_REDAND ::CVC5::theory::bv::BitVectorUnaryPredicateTypeRule +typerule BITVECTOR_REDOR ::CVC5::theory::bv::BitVectorUnaryPredicateTypeRule ## conversion kinds -typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule +typerule BITVECTOR_TO_NAT ::CVC5::theory::bv::BitVectorConversionTypeRule ## internal kinds -typerule BITVECTOR_ACKERMANNIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule -typerule BITVECTOR_ACKERMANNIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule -typerule BITVECTOR_EAGER_ATOM ::CVC4::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 ::CVC4::theory::bv::BitVectorBitOfTypeRule +typerule BITVECTOR_BITOF ::CVC5::theory::bv::BitVectorBitOfTypeRule typerule BITVECTOR_EXTRACT_OP "SimpleTypeRule<RBuiltinOperator>" -typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule +typerule BITVECTOR_EXTRACT ::CVC5::theory::bv::BitVectorExtractTypeRule typerule BITVECTOR_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>" -typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule +typerule BITVECTOR_REPEAT ::CVC5::theory::bv::BitVectorRepeatTypeRule typerule BITVECTOR_ROTATE_LEFT_OP "SimpleTypeRule<RBuiltinOperator>" -typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_ROTATE_LEFT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_ROTATE_RIGHT_OP "SimpleTypeRule<RBuiltinOperator>" -typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_ROTATE_RIGHT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SIGN_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>" -typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule +typerule BITVECTOR_SIGN_EXTEND ::CVC5::theory::bv::BitVectorExtendTypeRule typerule BITVECTOR_ZERO_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>" -typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule -typerule INT_TO_BITVECTOR_OP ::CVC4::theory::bv::IntToBitVectorOpTypeRule -typerule INT_TO_BITVECTOR ::CVC4::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 |