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/arith/kinds | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'src/theory/arith/kinds')
-rw-r--r-- | src/theory/arith/kinds | 64 |
1 files changed, 32 insertions, 32 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 04bdc277e..b839ccc22 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -4,13 +4,13 @@ # src/theory/builtin/kinds. # -theory THEORY_ARITH ::CVC4::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 ::CVC4::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 \ - ::CVC4::Divisible \ - ::CVC4::DivisibleHashFunction \ + ::CVC5::Divisible \ + ::CVC5::DivisibleHashFunction \ "util/divisible.h" \ - "operator for the divisibility-by-k predicate; payload is an instance of the CVC4::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 \ - ::CVC4::Rational \ - ::CVC4::RationalHashFunction \ + ::CVC5::Rational \ + ::CVC5::RationalHashFunction \ "util/rational.h" \ - "a multiple-precision rational constant; payload is an instance of the CVC4::Rational class" + "a multiple-precision rational constant; payload is an instance of the CVC5::Rational class" enumerator REAL_TYPE \ - "::CVC4::theory::arith::RationalEnumerator" \ + "::CVC5::theory::arith::RationalEnumerator" \ "theory/arith/type_enumerator.h" enumerator INTEGER_TYPE \ - "::CVC4::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 \ - ::CVC4::IndexedRootPredicate \ - ::CVC4::IndexedRootPredicateHashFunction \ + ::CVC5::IndexedRootPredicate \ + ::CVC5::IndexedRootPredicateHashFunction \ "util/indexed_root_predicate.h" \ - "operator for the indexed root predicate; payload is an instance of the CVC4::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 ::CVC4::theory::arith::ArithOperatorTypeRule -typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule -typerule NONLINEAR_MULT ::CVC4::theory::arith::ArithOperatorTypeRule -typerule MINUS ::CVC4::theory::arith::ArithOperatorTypeRule -typerule UMINUS ::CVC4::theory::arith::ArithOperatorTypeRule -typerule DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule -typerule POW ::CVC4::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 ::CVC4::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 ::CVC4::theory::arith::IndexedRootPredicateTypeRule +typerule INDEXED_ROOT_PREDICATE ::CVC5::theory::arith::IndexedRootPredicateTypeRule -typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule -typerule CAST_TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule -typerule TO_INTEGER ::CVC4::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 ::CVC4::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 ::CVC4::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 \ - ::CVC4::IntAnd \ - "::CVC4::UnsignedHashFunction< ::CVC4::IntAnd >" \ + ::CVC5::IntAnd \ + "::CVC5::UnsignedHashFunction< ::CVC5::IntAnd >" \ "util/iand.h" \ - "operator for integer AND; payload is an instance of the CVC4::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 ::CVC4::theory::arith::IAndOpTypeRule -typerule IAND ::CVC4::theory::arith::IAndTypeRule +typerule IAND_OP ::CVC5::theory::arith::IAndOpTypeRule +typerule IAND ::CVC5::theory::arith::IAndTypeRule endtheory |