From a1466978fbc328507406d4a121dab4d1a1047e1d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 31 Mar 2021 15:23:17 -0700 Subject: Rename namespace CVC4 to CVC5. (#6249) --- src/theory/fp/fp_converter.cpp | 62 ++++++------ src/theory/fp/fp_converter.h | 6 +- src/theory/fp/kinds | 180 ++++++++++++++++----------------- src/theory/fp/theory_fp.cpp | 15 +-- src/theory/fp/theory_fp.h | 4 +- src/theory/fp/theory_fp_rewriter.cpp | 16 ++- src/theory/fp/theory_fp_rewriter.h | 8 +- src/theory/fp/theory_fp_type_rules.cpp | 4 +- src/theory/fp/theory_fp_type_rules.h | 4 +- src/theory/fp/type_enumerator.h | 4 +- 10 files changed, 150 insertions(+), 153 deletions(-) (limited to 'src/theory/fp') diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 359079948..879cd2988 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -41,75 +41,75 @@ #ifdef CVC4_USE_SYMFPU namespace symfpu { -using namespace ::CVC4::theory::fp::symfpuSymbolic; +using namespace ::CVC5::theory::fp::symfpuSymbolic; #define CVC4_SYM_ITE_DFN(T) \ template <> \ struct ite \ { \ - static const T iteOp(const symbolicProposition &_cond, \ - const T &_l, \ - const T &_r) \ + static const T iteOp(const symbolicProposition& _cond, \ + const T& _l, \ + const T& _r) \ { \ - ::CVC4::NodeManager *nm = ::CVC4::NodeManager::currentNM(); \ + ::CVC5::NodeManager* nm = ::CVC5::NodeManager::currentNM(); \ \ - ::CVC4::Node cond = _cond; \ - ::CVC4::Node l = _l; \ - ::CVC4::Node r = _r; \ + ::CVC5::Node cond = _cond; \ + ::CVC5::Node l = _l; \ + ::CVC5::Node r = _r; \ \ /* Handle some common symfpu idioms */ \ if (cond.isConst()) \ { \ - return (cond == nm->mkConst(::CVC4::BitVector(1U, 1U))) ? l : r; \ + return (cond == nm->mkConst(::CVC5::BitVector(1U, 1U))) ? l : r; \ } \ else \ { \ - if (l.getKind() == ::CVC4::kind::BITVECTOR_ITE) \ + if (l.getKind() == ::CVC5::kind::BITVECTOR_ITE) \ { \ if (l[1] == r) \ { \ return nm->mkNode( \ - ::CVC4::kind::BITVECTOR_ITE, \ - nm->mkNode(::CVC4::kind::BITVECTOR_AND, \ + ::CVC5::kind::BITVECTOR_ITE, \ + nm->mkNode(::CVC5::kind::BITVECTOR_AND, \ cond, \ - nm->mkNode(::CVC4::kind::BITVECTOR_NOT, l[0])), \ + nm->mkNode(::CVC5::kind::BITVECTOR_NOT, l[0])), \ l[2], \ r); \ } \ else if (l[2] == r) \ { \ return nm->mkNode( \ - ::CVC4::kind::BITVECTOR_ITE, \ - nm->mkNode(::CVC4::kind::BITVECTOR_AND, cond, l[0]), \ + ::CVC5::kind::BITVECTOR_ITE, \ + nm->mkNode(::CVC5::kind::BITVECTOR_AND, cond, l[0]), \ l[1], \ r); \ } \ } \ - else if (r.getKind() == ::CVC4::kind::BITVECTOR_ITE) \ + else if (r.getKind() == ::CVC5::kind::BITVECTOR_ITE) \ { \ if (r[1] == l) \ { \ return nm->mkNode( \ - ::CVC4::kind::BITVECTOR_ITE, \ - nm->mkNode(::CVC4::kind::BITVECTOR_AND, \ - nm->mkNode(::CVC4::kind::BITVECTOR_NOT, cond), \ - nm->mkNode(::CVC4::kind::BITVECTOR_NOT, r[0])), \ + ::CVC5::kind::BITVECTOR_ITE, \ + nm->mkNode(::CVC5::kind::BITVECTOR_AND, \ + nm->mkNode(::CVC5::kind::BITVECTOR_NOT, cond), \ + nm->mkNode(::CVC5::kind::BITVECTOR_NOT, r[0])), \ r[2], \ l); \ } \ else if (r[2] == l) \ { \ return nm->mkNode( \ - ::CVC4::kind::BITVECTOR_ITE, \ - nm->mkNode(::CVC4::kind::BITVECTOR_AND, \ - nm->mkNode(::CVC4::kind::BITVECTOR_NOT, cond), \ + ::CVC5::kind::BITVECTOR_ITE, \ + nm->mkNode(::CVC5::kind::BITVECTOR_AND, \ + nm->mkNode(::CVC5::kind::BITVECTOR_NOT, cond), \ r[0]), \ r[1], \ l); \ } \ } \ } \ - return T(nm->mkNode(::CVC4::kind::BITVECTOR_ITE, cond, l, r)); \ + return T(nm->mkNode(::CVC5::kind::BITVECTOR_ITE, cond, l, r)); \ } \ } @@ -148,7 +148,7 @@ void probabilityAnnotation(const traits::prop &p, #define SYMFPU_NUMBER_OF_ROUNDING_MODES 5 #endif -namespace CVC4 { +namespace CVC5 { namespace theory { namespace fp { namespace symfpuSymbolic { @@ -412,8 +412,8 @@ symbolicBitVector symbolicBitVector::maxValue(const bwt &w) symbolicBitVector leadingZero(symbolicBitVector::zero(1)); symbolicBitVector base(symbolicBitVector::allOnes(w - 1)); - return symbolicBitVector(::CVC4::NodeManager::currentNM()->mkNode( - ::CVC4::kind::BITVECTOR_CONCAT, leadingZero, base)); + return symbolicBitVector(::CVC5::NodeManager::currentNM()->mkNode( + ::CVC5::kind::BITVECTOR_CONCAT, leadingZero, base)); } template <> @@ -428,8 +428,8 @@ symbolicBitVector symbolicBitVector::minValue(const bwt &w) symbolicBitVector leadingOne(symbolicBitVector::one(1)); symbolicBitVector base(symbolicBitVector::zero(w - 1)); - return symbolicBitVector(::CVC4::NodeManager::currentNM()->mkNode( - ::CVC4::kind::BITVECTOR_CONCAT, leadingOne, base)); + return symbolicBitVector(::CVC5::NodeManager::currentNM()->mkNode( + ::CVC5::kind::BITVECTOR_CONCAT, leadingOne, base)); } template <> @@ -817,7 +817,7 @@ Node FpConverter::propToNode(const prop &p) const { NodeManager *nm = NodeManager::currentNM(); Node value = - nm->mkNode(kind::EQUAL, p, nm->mkConst(::CVC4::BitVector(1U, 1U))); + nm->mkNode(kind::EQUAL, p, nm->mkConst(::CVC5::BitVector(1U, 1U))); return value; } Node FpConverter::ubvToNode(const ubv &u) const { return u; } @@ -1739,4 +1739,4 @@ Node FpConverter::getValue(Valuation &val, TNode var) } // namespace fp } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 6623f308c..e952699a7 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -45,7 +45,7 @@ #include "theory/rewriter.h" #endif -namespace CVC4 { +namespace CVC5 { namespace theory { namespace fp { @@ -97,7 +97,7 @@ class traits typedef traits::bwt bwt; /** - * Wrap the CVC4::Node types so that we can debug issues with this back-end + * Wrap the CVC5::Node types so that we can debug issues with this back-end */ class nodeWrapper : public Node { @@ -352,6 +352,6 @@ class FpConverter } // namespace fp } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__FP__THEORY_FP_H */ diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index 49ed92dee..4a4d16b55 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -4,9 +4,9 @@ # src/theory/builtin/kinds. # -theory THEORY_FP ::CVC4::theory::fp::TheoryFp "theory/fp/theory_fp.h" +theory THEORY_FP ::CVC5::theory::fp::TheoryFp "theory/fp/theory_fp.h" typechecker "theory/fp/theory_fp_type_rules.h" -rewriter ::CVC4::theory::fp::TheoryFpRewriter "theory/fp/theory_fp_rewriter.h" +rewriter ::CVC5::theory::fp::TheoryFpRewriter "theory/fp/theory_fp_rewriter.h" properties check @@ -14,19 +14,19 @@ properties check # constants... constant CONST_FLOATINGPOINT \ - ::CVC4::FloatingPoint \ - ::CVC4::FloatingPointHashFunction \ + ::CVC5::FloatingPoint \ + ::CVC5::FloatingPointHashFunction \ "util/floatingpoint.h" \ "a floating-point literal" -typerule CONST_FLOATINGPOINT ::CVC4::theory::fp::FloatingPointConstantTypeRule +typerule CONST_FLOATINGPOINT ::CVC5::theory::fp::FloatingPointConstantTypeRule constant CONST_ROUNDINGMODE \ - ::CVC4::RoundingMode \ - ::CVC4::RoundingModeHashFunction \ + ::CVC5::RoundingMode \ + ::CVC5::RoundingModeHashFunction \ "util/floatingpoint.h" \ "a floating-point rounding mode" -typerule CONST_ROUNDINGMODE ::CVC4::theory::fp::RoundingModeConstantTypeRule +typerule CONST_ROUNDINGMODE ::CVC5::theory::fp::RoundingModeConstantTypeRule @@ -39,272 +39,272 @@ sort ROUNDINGMODE_TYPE \ "floating-point rounding mode" enumerator ROUNDINGMODE_TYPE \ - "::CVC4::theory::fp::RoundingModeEnumerator" \ + "::CVC5::theory::fp::RoundingModeEnumerator" \ "theory/fp/type_enumerator.h" constant FLOATINGPOINT_TYPE \ - ::CVC4::FloatingPointSize \ - ::CVC4::FloatingPointSizeHashFunction \ + ::CVC5::FloatingPointSize \ + ::CVC5::FloatingPointSizeHashFunction \ "util/floatingpoint.h" \ "floating-point type" cardinality FLOATINGPOINT_TYPE \ - "::CVC4::theory::fp::CardinalityComputer::computeCardinality(%TYPE%)" \ + "::CVC5::theory::fp::CardinalityComputer::computeCardinality(%TYPE%)" \ "theory/fp/theory_fp_type_rules.h" enumerator FLOATINGPOINT_TYPE \ - "::CVC4::theory::fp::FloatingPointEnumerator" \ + "::CVC5::theory::fp::FloatingPointEnumerator" \ "theory/fp/type_enumerator.h" well-founded FLOATINGPOINT_TYPE \ true \ - "(*CVC4::theory::TypeEnumerator(%TYPE%))" \ + "(*CVC5::theory::TypeEnumerator(%TYPE%))" \ "theory/type_enumerator.h" # operators... operator FLOATINGPOINT_FP 3 "construct a floating-point literal from bit vectors" -typerule FLOATINGPOINT_FP ::CVC4::theory::fp::FloatingPointFPTypeRule +typerule FLOATINGPOINT_FP ::CVC5::theory::fp::FloatingPointFPTypeRule operator FLOATINGPOINT_EQ 2: "floating-point equality" -typerule FLOATINGPOINT_EQ ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_EQ ::CVC5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ABS 1 "floating-point absolute value" -typerule FLOATINGPOINT_ABS ::CVC4::theory::fp::FloatingPointOperationTypeRule +typerule FLOATINGPOINT_ABS ::CVC5::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_NEG 1 "floating-point negation" -typerule FLOATINGPOINT_NEG ::CVC4::theory::fp::FloatingPointOperationTypeRule +typerule FLOATINGPOINT_NEG ::CVC5::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_PLUS 3 "floating-point addition" -typerule FLOATINGPOINT_PLUS ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_PLUS ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_SUB 3 "floating-point sutraction" -typerule FLOATINGPOINT_SUB ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_SUB ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_MULT 3 "floating-point multiply" -typerule FLOATINGPOINT_MULT ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_MULT ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_DIV 3 "floating-point division" -typerule FLOATINGPOINT_DIV ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_DIV ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_FMA 4 "floating-point fused multiply and add" -typerule FLOATINGPOINT_FMA ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_FMA ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_SQRT 2 "floating-point square root" -typerule FLOATINGPOINT_SQRT ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_SQRT ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_REM 2 "floating-point remainder" -typerule FLOATINGPOINT_REM ::CVC4::theory::fp::FloatingPointOperationTypeRule +typerule FLOATINGPOINT_REM ::CVC5::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_RTI 2 "floating-point round to integral" -typerule FLOATINGPOINT_RTI ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_RTI ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_MIN 2 "floating-point minimum" -typerule FLOATINGPOINT_MIN ::CVC4::theory::fp::FloatingPointOperationTypeRule +typerule FLOATINGPOINT_MIN ::CVC5::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_MAX 2 "floating-point maximum" -typerule FLOATINGPOINT_MAX ::CVC4::theory::fp::FloatingPointOperationTypeRule +typerule FLOATINGPOINT_MAX ::CVC5::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_MIN_TOTAL 3 "floating-point minimum (defined for all inputs)" -typerule FLOATINGPOINT_MIN_TOTAL ::CVC4::theory::fp::FloatingPointPartialOperationTypeRule +typerule FLOATINGPOINT_MIN_TOTAL ::CVC5::theory::fp::FloatingPointPartialOperationTypeRule operator FLOATINGPOINT_MAX_TOTAL 3 "floating-point maximum (defined for all inputs)" -typerule FLOATINGPOINT_MAX_TOTAL ::CVC4::theory::fp::FloatingPointPartialOperationTypeRule +typerule FLOATINGPOINT_MAX_TOTAL ::CVC5::theory::fp::FloatingPointPartialOperationTypeRule operator FLOATINGPOINT_LEQ 2: "floating-point less than or equal" -typerule FLOATINGPOINT_LEQ ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_LEQ ::CVC5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_LT 2: "floating-point less than" -typerule FLOATINGPOINT_LT ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_LT ::CVC5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_GEQ 2: "floating-point greater than or equal" -typerule FLOATINGPOINT_GEQ ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_GEQ ::CVC5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_GT 2: "floating-point greater than" -typerule FLOATINGPOINT_GT ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_GT ::CVC5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISN 1 "floating-point is normal" -typerule FLOATINGPOINT_ISN ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISN ::CVC5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISSN 1 "floating-point is sub-normal" -typerule FLOATINGPOINT_ISSN ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISSN ::CVC5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISZ 1 "floating-point is zero" -typerule FLOATINGPOINT_ISZ ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISZ ::CVC5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISINF 1 "floating-point is infinite" -typerule FLOATINGPOINT_ISINF ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISINF ::CVC5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISNAN 1 "floating-point is NaN" -typerule FLOATINGPOINT_ISNAN ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISNAN ::CVC5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISNEG 1 "floating-point is negative" -typerule FLOATINGPOINT_ISNEG ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISNEG ::CVC5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISPOS 1 "floating-point is positive" -typerule FLOATINGPOINT_ISPOS ::CVC4::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISPOS ::CVC5::theory::fp::FloatingPointTestTypeRule constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \ - ::CVC4::FloatingPointToFPIEEEBitVector \ - "::CVC4::FloatingPointConvertSortHashFunction<0x1>" \ + ::CVC5::FloatingPointToFPIEEEBitVector \ + "::CVC5::FloatingPointConvertSortHashFunction<0x1>" \ "util/floatingpoint.h" \ "operator for to_fp from bit vector" -typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP ::CVC5::theory::fp::FloatingPointParametricOpTypeRule parameterized FLOATINGPOINT_TO_FP_IEEE_BITVECTOR FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP 1 "convert an IEEE-754 bit vector to floating-point" -typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR ::CVC4::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule +typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR ::CVC5::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \ - ::CVC4::FloatingPointToFPFloatingPoint \ - "::CVC4::FloatingPointConvertSortHashFunction<0x2>" \ + ::CVC5::FloatingPointToFPFloatingPoint \ + "::CVC5::FloatingPointConvertSortHashFunction<0x2>" \ "util/floatingpoint.h" \ "operator for to_fp from floating point" -typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP ::CVC5::theory::fp::FloatingPointParametricOpTypeRule parameterized FLOATINGPOINT_TO_FP_FLOATINGPOINT FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP 2 "convert between floating-point sorts" -typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT ::CVC4::theory::fp::FloatingPointToFPFloatingPointTypeRule +typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT ::CVC5::theory::fp::FloatingPointToFPFloatingPointTypeRule constant FLOATINGPOINT_TO_FP_REAL_OP \ - ::CVC4::FloatingPointToFPReal \ - "::CVC4::FloatingPointConvertSortHashFunction<0x4>" \ + ::CVC5::FloatingPointToFPReal \ + "::CVC5::FloatingPointConvertSortHashFunction<0x4>" \ "util/floatingpoint.h" \ "operator for to_fp from real" -typerule FLOATINGPOINT_TO_FP_REAL_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_FP_REAL_OP ::CVC5::theory::fp::FloatingPointParametricOpTypeRule parameterized FLOATINGPOINT_TO_FP_REAL FLOATINGPOINT_TO_FP_REAL_OP 2 "convert a real to floating-point" -typerule FLOATINGPOINT_TO_FP_REAL ::CVC4::theory::fp::FloatingPointToFPRealTypeRule +typerule FLOATINGPOINT_TO_FP_REAL ::CVC5::theory::fp::FloatingPointToFPRealTypeRule constant FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP \ - ::CVC4::FloatingPointToFPSignedBitVector \ - "::CVC4::FloatingPointConvertSortHashFunction<0x8>" \ + ::CVC5::FloatingPointToFPSignedBitVector \ + "::CVC5::FloatingPointConvertSortHashFunction<0x8>" \ "util/floatingpoint.h" \ "operator for to_fp from signed bit vector" -typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP ::CVC5::theory::fp::FloatingPointParametricOpTypeRule parameterized FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP 2 "convert a signed bit vector to floating-point" -typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR ::CVC4::theory::fp::FloatingPointToFPSignedBitVectorTypeRule +typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR ::CVC5::theory::fp::FloatingPointToFPSignedBitVectorTypeRule constant FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP \ - ::CVC4::FloatingPointToFPUnsignedBitVector \ - "::CVC4::FloatingPointConvertSortHashFunction<0x10>" \ + ::CVC5::FloatingPointToFPUnsignedBitVector \ + "::CVC5::FloatingPointConvertSortHashFunction<0x10>" \ "util/floatingpoint.h" \ "operator for to_fp from unsigned bit vector" -typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP ::CVC5::theory::fp::FloatingPointParametricOpTypeRule parameterized FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP 2 "convert an unsigned bit vector to floating-point" -typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR ::CVC4::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule +typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR ::CVC5::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule constant FLOATINGPOINT_TO_FP_GENERIC_OP \ - ::CVC4::FloatingPointToFPGeneric \ - "::CVC4::FloatingPointConvertSortHashFunction<0x11>" \ + ::CVC5::FloatingPointToFPGeneric \ + "::CVC5::FloatingPointConvertSortHashFunction<0x11>" \ "util/floatingpoint.h" \ "operator for a generic to_fp" -typerule FLOATINGPOINT_TO_FP_GENERIC_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_FP_GENERIC_OP ::CVC5::theory::fp::FloatingPointParametricOpTypeRule parameterized FLOATINGPOINT_TO_FP_GENERIC FLOATINGPOINT_TO_FP_GENERIC_OP 1:2 "a generic conversion to floating-point, used in parsing only" -typerule FLOATINGPOINT_TO_FP_GENERIC ::CVC4::theory::fp::FloatingPointToFPGenericTypeRule +typerule FLOATINGPOINT_TO_FP_GENERIC ::CVC5::theory::fp::FloatingPointToFPGenericTypeRule constant FLOATINGPOINT_TO_UBV_OP \ - ::CVC4::FloatingPointToUBV \ - "::CVC4::FloatingPointToBVHashFunction<0x1>" \ + ::CVC5::FloatingPointToUBV \ + "::CVC5::FloatingPointToBVHashFunction<0x1>" \ "util/floatingpoint.h" \ "operator for to_ubv" -typerule FLOATINGPOINT_TO_UBV_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_UBV_OP ::CVC5::theory::fp::FloatingPointParametricOpTypeRule parameterized FLOATINGPOINT_TO_UBV FLOATINGPOINT_TO_UBV_OP 2 "convert a floating-point value to an unsigned bit vector" -typerule FLOATINGPOINT_TO_UBV ::CVC4::theory::fp::FloatingPointToUBVTypeRule +typerule FLOATINGPOINT_TO_UBV ::CVC5::theory::fp::FloatingPointToUBVTypeRule constant FLOATINGPOINT_TO_UBV_TOTAL_OP \ - ::CVC4::FloatingPointToUBVTotal \ - "::CVC4::FloatingPointToBVHashFunction<0x4>" \ + ::CVC5::FloatingPointToUBVTotal \ + "::CVC5::FloatingPointToBVHashFunction<0x4>" \ "util/floatingpoint.h" \ "operator for to_ubv_total" -typerule FLOATINGPOINT_TO_UBV_TOTAL_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_UBV_TOTAL_OP ::CVC5::theory::fp::FloatingPointParametricOpTypeRule parameterized FLOATINGPOINT_TO_UBV_TOTAL FLOATINGPOINT_TO_UBV_TOTAL_OP 3 "convert a floating-point value to an unsigned bit vector (defined for all inputs)" -typerule FLOATINGPOINT_TO_UBV_TOTAL ::CVC4::theory::fp::FloatingPointToUBVTotalTypeRule +typerule FLOATINGPOINT_TO_UBV_TOTAL ::CVC5::theory::fp::FloatingPointToUBVTotalTypeRule constant FLOATINGPOINT_TO_SBV_OP \ - ::CVC4::FloatingPointToSBV \ - "::CVC4::FloatingPointToBVHashFunction<0x2>" \ + ::CVC5::FloatingPointToSBV \ + "::CVC5::FloatingPointToBVHashFunction<0x2>" \ "util/floatingpoint.h" \ "operator for to_sbv" -typerule FLOATINGPOINT_TO_SBV_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_SBV_OP ::CVC5::theory::fp::FloatingPointParametricOpTypeRule parameterized FLOATINGPOINT_TO_SBV FLOATINGPOINT_TO_SBV_OP 2 "convert a floating-point value to a signed bit vector" -typerule FLOATINGPOINT_TO_SBV ::CVC4::theory::fp::FloatingPointToSBVTypeRule +typerule FLOATINGPOINT_TO_SBV ::CVC5::theory::fp::FloatingPointToSBVTypeRule constant FLOATINGPOINT_TO_SBV_TOTAL_OP \ - ::CVC4::FloatingPointToSBVTotal \ - "::CVC4::FloatingPointToBVHashFunction<0x8>" \ + ::CVC5::FloatingPointToSBVTotal \ + "::CVC5::FloatingPointToBVHashFunction<0x8>" \ "util/floatingpoint.h" \ "operator for to_sbv_total" -typerule FLOATINGPOINT_TO_SBV_TOTAL_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_SBV_TOTAL_OP ::CVC5::theory::fp::FloatingPointParametricOpTypeRule parameterized FLOATINGPOINT_TO_SBV_TOTAL FLOATINGPOINT_TO_SBV_TOTAL_OP 3 "convert a floating-point value to a signed bit vector (defined for all inputs)" -typerule FLOATINGPOINT_TO_SBV_TOTAL ::CVC4::theory::fp::FloatingPointToSBVTotalTypeRule +typerule FLOATINGPOINT_TO_SBV_TOTAL ::CVC5::theory::fp::FloatingPointToSBVTotalTypeRule operator FLOATINGPOINT_TO_REAL 1 "floating-point to real" -typerule FLOATINGPOINT_TO_REAL ::CVC4::theory::fp::FloatingPointToRealTypeRule +typerule FLOATINGPOINT_TO_REAL ::CVC5::theory::fp::FloatingPointToRealTypeRule operator FLOATINGPOINT_TO_REAL_TOTAL 2 "floating-point to real (defined for all inputs)" -typerule FLOATINGPOINT_TO_REAL_TOTAL ::CVC4::theory::fp::FloatingPointToRealTotalTypeRule +typerule FLOATINGPOINT_TO_REAL_TOTAL ::CVC5::theory::fp::FloatingPointToRealTotalTypeRule operator FLOATINGPOINT_COMPONENT_NAN 1 "NaN component of a word-blasted floating-point number" -typerule FLOATINGPOINT_COMPONENT_NAN ::CVC4::theory::fp::FloatingPointComponentBit +typerule FLOATINGPOINT_COMPONENT_NAN ::CVC5::theory::fp::FloatingPointComponentBit operator FLOATINGPOINT_COMPONENT_INF 1 "Inf component of a word-blasted floating-point number" -typerule FLOATINGPOINT_COMPONENT_INF ::CVC4::theory::fp::FloatingPointComponentBit +typerule FLOATINGPOINT_COMPONENT_INF ::CVC5::theory::fp::FloatingPointComponentBit operator FLOATINGPOINT_COMPONENT_ZERO 1 "Zero component of a word-blasted floating-point number" -typerule FLOATINGPOINT_COMPONENT_ZERO ::CVC4::theory::fp::FloatingPointComponentBit +typerule FLOATINGPOINT_COMPONENT_ZERO ::CVC5::theory::fp::FloatingPointComponentBit operator FLOATINGPOINT_COMPONENT_SIGN 1 "Sign component of a word-blasted floating-point number" -typerule FLOATINGPOINT_COMPONENT_SIGN ::CVC4::theory::fp::FloatingPointComponentBit +typerule FLOATINGPOINT_COMPONENT_SIGN ::CVC5::theory::fp::FloatingPointComponentBit operator FLOATINGPOINT_COMPONENT_EXPONENT 1 "Exponent component of a word-blasted floating-point number" -typerule FLOATINGPOINT_COMPONENT_EXPONENT ::CVC4::theory::fp::FloatingPointComponentExponent +typerule FLOATINGPOINT_COMPONENT_EXPONENT ::CVC5::theory::fp::FloatingPointComponentExponent operator FLOATINGPOINT_COMPONENT_SIGNIFICAND 1 "Significand component of a word-blasted floating-point number" -typerule FLOATINGPOINT_COMPONENT_SIGNIFICAND ::CVC4::theory::fp::FloatingPointComponentSignificand +typerule FLOATINGPOINT_COMPONENT_SIGNIFICAND ::CVC5::theory::fp::FloatingPointComponentSignificand operator ROUNDINGMODE_BITBLAST 1 "The bit-vector for a non-deterministic rounding mode" -typerule ROUNDINGMODE_BITBLAST ::CVC4::theory::fp::RoundingModeBitBlast +typerule ROUNDINGMODE_BITBLAST ::CVC5::theory::fp::RoundingModeBitBlast endtheory diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 3099d9aab..ea9ea902c 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -33,7 +33,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace fp { @@ -774,7 +774,7 @@ void TheoryFp::convertAndEquateTerm(TNode node) { NodeManager *nm = NodeManager::currentNM(); handleLemma( - nm->mkNode(kind::EQUAL, addA, nm->mkConst(::CVC4::BitVector(1U, 1U)))); + nm->mkNode(kind::EQUAL, addA, nm->mkConst(::CVC5::BitVector(1U, 1U)))); #endif ++oldAdditionalAssertions; @@ -791,10 +791,11 @@ void TheoryFp::convertAndEquateTerm(TNode node) { #ifdef SYMFPUPROPISBOOL handleLemma(nm->mkNode(kind::EQUAL, node, converted)); #else - handleLemma( - nm->mkNode(kind::EQUAL, node, - nm->mkNode(kind::EQUAL, converted, - nm->mkConst(::CVC4::BitVector(1U, 1U))))); + handleLemma(nm->mkNode( + kind::EQUAL, + node, + nm->mkNode( + kind::EQUAL, converted, nm->mkConst(::CVC5::BitVector(1U, 1U))))); #endif } else { @@ -1156,4 +1157,4 @@ void TheoryFp::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { } // namespace fp } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index b15b5c2dd..2607a33c6 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -31,7 +31,7 @@ #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace fp { @@ -189,6 +189,6 @@ class TheoryFp : public Theory } // namespace fp } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__FP__THEORY_FP_H */ diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 3e03bbdbe..65e27fc48 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -37,7 +37,7 @@ #include "theory/fp/fp_converter.h" #include "theory/fp/theory_fp_rewriter.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace fp { @@ -324,8 +324,7 @@ namespace rewrite { return RewriteResponse(REWRITE_DONE, node); } -}; /* CVC4::theory::fp::rewrite */ - + }; // namespace rewrite namespace constantFold { @@ -978,8 +977,7 @@ namespace constantFold { NodeManager::currentNM()->mkConst(value)); } -}; /* CVC4::theory::fp::constantFold */ - + }; // namespace constantFold /** * Initialize the rewriter. @@ -1421,8 +1419,6 @@ TheoryFpRewriter::TheoryFpRewriter() return res; } - -}/* CVC4::theory::fp namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - + } // namespace fp + } // namespace theory + } // namespace CVC5 diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h index 5591246b4..bfdf90d44 100644 --- a/src/theory/fp/theory_fp_rewriter.h +++ b/src/theory/fp/theory_fp_rewriter.h @@ -22,7 +22,7 @@ #include "theory/theory_rewriter.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace fp { @@ -51,8 +51,8 @@ class TheoryFpRewriter : public TheoryRewriter RewriteFunction d_constantFoldTable[kind::LAST_KIND]; }; /* class TheoryFpRewriter */ -}/* CVC4::theory::fp namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace fp +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__FP__THEORY_FP_REWRITER_H */ diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp index 165c9b924..6b87f8af3 100644 --- a/src/theory/fp/theory_fp_type_rules.cpp +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -18,7 +18,7 @@ #include "theory/theory.h" #include "util/roundingmode.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace fp { @@ -812,4 +812,4 @@ Cardinality CardinalityComputer::computeCardinality(TypeNode type) } // namespace fp } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index aef2d0a50..632ae660d 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC4 { +namespace CVC5 { class NodeManager; @@ -229,6 +229,6 @@ class CardinalityComputer } // namespace fp } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h index 01145472d..535ed7c69 100644 --- a/src/theory/fp/type_enumerator.h +++ b/src/theory/fp/type_enumerator.h @@ -26,7 +26,7 @@ #include "util/bitvector.h" #include "util/floatingpoint.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace fp { @@ -120,6 +120,6 @@ class RoundingModeEnumerator } // namespace fp } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__FP__TYPE_ENUMERATOR_H */ -- cgit v1.2.3