diff options
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/fp_converter.cpp | 56 | ||||
-rw-r--r-- | src/theory/fp/fp_converter.h | 6 | ||||
-rw-r--r-- | src/theory/fp/kinds | 180 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 8 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.h | 4 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 4 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.h | 4 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.cpp | 4 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.h | 4 | ||||
-rw-r--r-- | src/theory/fp/type_enumerator.h | 4 |
10 files changed, 137 insertions, 137 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 879cd2988..3b5a115c8 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -41,7 +41,7 @@ #ifdef CVC4_USE_SYMFPU namespace symfpu { -using namespace ::CVC5::theory::fp::symfpuSymbolic; +using namespace ::cvc5::theory::fp::symfpuSymbolic; #define CVC4_SYM_ITE_DFN(T) \ template <> \ @@ -51,65 +51,65 @@ using namespace ::CVC5::theory::fp::symfpuSymbolic; const T& _l, \ const T& _r) \ { \ - ::CVC5::NodeManager* nm = ::CVC5::NodeManager::currentNM(); \ + ::cvc5::NodeManager* nm = ::cvc5::NodeManager::currentNM(); \ \ - ::CVC5::Node cond = _cond; \ - ::CVC5::Node l = _l; \ - ::CVC5::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(::CVC5::BitVector(1U, 1U))) ? l : r; \ + return (cond == nm->mkConst(::cvc5::BitVector(1U, 1U))) ? l : r; \ } \ else \ { \ - if (l.getKind() == ::CVC5::kind::BITVECTOR_ITE) \ + if (l.getKind() == ::cvc5::kind::BITVECTOR_ITE) \ { \ if (l[1] == r) \ { \ return nm->mkNode( \ - ::CVC5::kind::BITVECTOR_ITE, \ - nm->mkNode(::CVC5::kind::BITVECTOR_AND, \ + ::cvc5::kind::BITVECTOR_ITE, \ + nm->mkNode(::cvc5::kind::BITVECTOR_AND, \ cond, \ - nm->mkNode(::CVC5::kind::BITVECTOR_NOT, l[0])), \ + nm->mkNode(::cvc5::kind::BITVECTOR_NOT, l[0])), \ l[2], \ r); \ } \ else if (l[2] == r) \ { \ return nm->mkNode( \ - ::CVC5::kind::BITVECTOR_ITE, \ - nm->mkNode(::CVC5::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() == ::CVC5::kind::BITVECTOR_ITE) \ + else if (r.getKind() == ::cvc5::kind::BITVECTOR_ITE) \ { \ if (r[1] == l) \ { \ return nm->mkNode( \ - ::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])), \ + ::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( \ - ::CVC5::kind::BITVECTOR_ITE, \ - nm->mkNode(::CVC5::kind::BITVECTOR_AND, \ - nm->mkNode(::CVC5::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(::CVC5::kind::BITVECTOR_ITE, cond, l, r)); \ + return T(nm->mkNode(::cvc5::kind::BITVECTOR_ITE, cond, l, r)); \ } \ } @@ -148,7 +148,7 @@ void probabilityAnnotation<traits, traits::prop>(const traits::prop &p, #define SYMFPU_NUMBER_OF_ROUNDING_MODES 5 #endif -namespace CVC5 { +namespace cvc5 { namespace theory { namespace fp { namespace symfpuSymbolic { @@ -412,8 +412,8 @@ symbolicBitVector<true> symbolicBitVector<true>::maxValue(const bwt &w) symbolicBitVector<true> leadingZero(symbolicBitVector<true>::zero(1)); symbolicBitVector<true> base(symbolicBitVector<true>::allOnes(w - 1)); - return symbolicBitVector<true>(::CVC5::NodeManager::currentNM()->mkNode( - ::CVC5::kind::BITVECTOR_CONCAT, leadingZero, base)); + return symbolicBitVector<true>(::cvc5::NodeManager::currentNM()->mkNode( + ::cvc5::kind::BITVECTOR_CONCAT, leadingZero, base)); } template <> @@ -428,8 +428,8 @@ symbolicBitVector<true> symbolicBitVector<true>::minValue(const bwt &w) symbolicBitVector<true> leadingOne(symbolicBitVector<true>::one(1)); symbolicBitVector<true> base(symbolicBitVector<true>::zero(w - 1)); - return symbolicBitVector<true>(::CVC5::NodeManager::currentNM()->mkNode( - ::CVC5::kind::BITVECTOR_CONCAT, leadingOne, base)); + return symbolicBitVector<true>(::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(::CVC5::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 CVC5 +} // namespace cvc5 diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index e952699a7..f25ce0822 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 CVC5 { +namespace cvc5 { namespace theory { namespace fp { @@ -97,7 +97,7 @@ class traits typedef traits::bwt bwt; /** - * Wrap the CVC5::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 CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__FP__THEORY_FP_H */ diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index 4a4d16b55..d67738a63 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -4,9 +4,9 @@ # src/theory/builtin/kinds. # -theory THEORY_FP ::CVC5::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 ::CVC5::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 \ - ::CVC5::FloatingPoint \ - ::CVC5::FloatingPointHashFunction \ + ::cvc5::FloatingPoint \ + ::cvc5::FloatingPointHashFunction \ "util/floatingpoint.h" \ "a floating-point literal" -typerule CONST_FLOATINGPOINT ::CVC5::theory::fp::FloatingPointConstantTypeRule +typerule CONST_FLOATINGPOINT ::cvc5::theory::fp::FloatingPointConstantTypeRule constant CONST_ROUNDINGMODE \ - ::CVC5::RoundingMode \ - ::CVC5::RoundingModeHashFunction \ + ::cvc5::RoundingMode \ + ::cvc5::RoundingModeHashFunction \ "util/floatingpoint.h" \ "a floating-point rounding mode" -typerule CONST_ROUNDINGMODE ::CVC5::theory::fp::RoundingModeConstantTypeRule +typerule CONST_ROUNDINGMODE ::cvc5::theory::fp::RoundingModeConstantTypeRule @@ -39,272 +39,272 @@ sort ROUNDINGMODE_TYPE \ "floating-point rounding mode" enumerator ROUNDINGMODE_TYPE \ - "::CVC5::theory::fp::RoundingModeEnumerator" \ + "::cvc5::theory::fp::RoundingModeEnumerator" \ "theory/fp/type_enumerator.h" constant FLOATINGPOINT_TYPE \ - ::CVC5::FloatingPointSize \ - ::CVC5::FloatingPointSizeHashFunction \ + ::cvc5::FloatingPointSize \ + ::cvc5::FloatingPointSizeHashFunction \ "util/floatingpoint.h" \ "floating-point type" cardinality FLOATINGPOINT_TYPE \ - "::CVC5::theory::fp::CardinalityComputer::computeCardinality(%TYPE%)" \ + "::cvc5::theory::fp::CardinalityComputer::computeCardinality(%TYPE%)" \ "theory/fp/theory_fp_type_rules.h" enumerator FLOATINGPOINT_TYPE \ - "::CVC5::theory::fp::FloatingPointEnumerator" \ + "::cvc5::theory::fp::FloatingPointEnumerator" \ "theory/fp/type_enumerator.h" well-founded FLOATINGPOINT_TYPE \ true \ - "(*CVC5::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 ::CVC5::theory::fp::FloatingPointFPTypeRule +typerule FLOATINGPOINT_FP ::cvc5::theory::fp::FloatingPointFPTypeRule operator FLOATINGPOINT_EQ 2: "floating-point equality" -typerule FLOATINGPOINT_EQ ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_EQ ::cvc5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ABS 1 "floating-point absolute value" -typerule FLOATINGPOINT_ABS ::CVC5::theory::fp::FloatingPointOperationTypeRule +typerule FLOATINGPOINT_ABS ::cvc5::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_NEG 1 "floating-point negation" -typerule FLOATINGPOINT_NEG ::CVC5::theory::fp::FloatingPointOperationTypeRule +typerule FLOATINGPOINT_NEG ::cvc5::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_PLUS 3 "floating-point addition" -typerule FLOATINGPOINT_PLUS ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_PLUS ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_SUB 3 "floating-point sutraction" -typerule FLOATINGPOINT_SUB ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_SUB ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_MULT 3 "floating-point multiply" -typerule FLOATINGPOINT_MULT ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_MULT ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_DIV 3 "floating-point division" -typerule FLOATINGPOINT_DIV ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_DIV ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_FMA 4 "floating-point fused multiply and add" -typerule FLOATINGPOINT_FMA ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_FMA ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_SQRT 2 "floating-point square root" -typerule FLOATINGPOINT_SQRT ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_SQRT ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_REM 2 "floating-point remainder" -typerule FLOATINGPOINT_REM ::CVC5::theory::fp::FloatingPointOperationTypeRule +typerule FLOATINGPOINT_REM ::cvc5::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_RTI 2 "floating-point round to integral" -typerule FLOATINGPOINT_RTI ::CVC5::theory::fp::FloatingPointRoundingOperationTypeRule +typerule FLOATINGPOINT_RTI ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_MIN 2 "floating-point minimum" -typerule FLOATINGPOINT_MIN ::CVC5::theory::fp::FloatingPointOperationTypeRule +typerule FLOATINGPOINT_MIN ::cvc5::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_MAX 2 "floating-point maximum" -typerule FLOATINGPOINT_MAX ::CVC5::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 ::CVC5::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 ::CVC5::theory::fp::FloatingPointPartialOperationTypeRule +typerule FLOATINGPOINT_MAX_TOTAL ::cvc5::theory::fp::FloatingPointPartialOperationTypeRule operator FLOATINGPOINT_LEQ 2: "floating-point less than or equal" -typerule FLOATINGPOINT_LEQ ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_LEQ ::cvc5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_LT 2: "floating-point less than" -typerule FLOATINGPOINT_LT ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_LT ::cvc5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_GEQ 2: "floating-point greater than or equal" -typerule FLOATINGPOINT_GEQ ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_GEQ ::cvc5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_GT 2: "floating-point greater than" -typerule FLOATINGPOINT_GT ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_GT ::cvc5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISN 1 "floating-point is normal" -typerule FLOATINGPOINT_ISN ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISN ::cvc5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISSN 1 "floating-point is sub-normal" -typerule FLOATINGPOINT_ISSN ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISSN ::cvc5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISZ 1 "floating-point is zero" -typerule FLOATINGPOINT_ISZ ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISZ ::cvc5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISINF 1 "floating-point is infinite" -typerule FLOATINGPOINT_ISINF ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISINF ::cvc5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISNAN 1 "floating-point is NaN" -typerule FLOATINGPOINT_ISNAN ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISNAN ::cvc5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISNEG 1 "floating-point is negative" -typerule FLOATINGPOINT_ISNEG ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISNEG ::cvc5::theory::fp::FloatingPointTestTypeRule operator FLOATINGPOINT_ISPOS 1 "floating-point is positive" -typerule FLOATINGPOINT_ISPOS ::CVC5::theory::fp::FloatingPointTestTypeRule +typerule FLOATINGPOINT_ISPOS ::cvc5::theory::fp::FloatingPointTestTypeRule constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \ - ::CVC5::FloatingPointToFPIEEEBitVector \ - "::CVC5::FloatingPointConvertSortHashFunction<0x1>" \ + ::cvc5::FloatingPointToFPIEEEBitVector \ + "::cvc5::FloatingPointConvertSortHashFunction<0x1>" \ "util/floatingpoint.h" \ "operator for to_fp from bit vector" -typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP ::CVC5::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 ::CVC5::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule +typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR ::cvc5::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \ - ::CVC5::FloatingPointToFPFloatingPoint \ - "::CVC5::FloatingPointConvertSortHashFunction<0x2>" \ + ::cvc5::FloatingPointToFPFloatingPoint \ + "::cvc5::FloatingPointConvertSortHashFunction<0x2>" \ "util/floatingpoint.h" \ "operator for to_fp from floating point" -typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP ::CVC5::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 ::CVC5::theory::fp::FloatingPointToFPFloatingPointTypeRule +typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT ::cvc5::theory::fp::FloatingPointToFPFloatingPointTypeRule constant FLOATINGPOINT_TO_FP_REAL_OP \ - ::CVC5::FloatingPointToFPReal \ - "::CVC5::FloatingPointConvertSortHashFunction<0x4>" \ + ::cvc5::FloatingPointToFPReal \ + "::cvc5::FloatingPointConvertSortHashFunction<0x4>" \ "util/floatingpoint.h" \ "operator for to_fp from real" -typerule FLOATINGPOINT_TO_FP_REAL_OP ::CVC5::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 ::CVC5::theory::fp::FloatingPointToFPRealTypeRule +typerule FLOATINGPOINT_TO_FP_REAL ::cvc5::theory::fp::FloatingPointToFPRealTypeRule constant FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP \ - ::CVC5::FloatingPointToFPSignedBitVector \ - "::CVC5::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 ::CVC5::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 ::CVC5::theory::fp::FloatingPointToFPSignedBitVectorTypeRule +typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR ::cvc5::theory::fp::FloatingPointToFPSignedBitVectorTypeRule constant FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP \ - ::CVC5::FloatingPointToFPUnsignedBitVector \ - "::CVC5::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 ::CVC5::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 ::CVC5::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule +typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR ::cvc5::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule constant FLOATINGPOINT_TO_FP_GENERIC_OP \ - ::CVC5::FloatingPointToFPGeneric \ - "::CVC5::FloatingPointConvertSortHashFunction<0x11>" \ + ::cvc5::FloatingPointToFPGeneric \ + "::cvc5::FloatingPointConvertSortHashFunction<0x11>" \ "util/floatingpoint.h" \ "operator for a generic to_fp" -typerule FLOATINGPOINT_TO_FP_GENERIC_OP ::CVC5::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 ::CVC5::theory::fp::FloatingPointToFPGenericTypeRule +typerule FLOATINGPOINT_TO_FP_GENERIC ::cvc5::theory::fp::FloatingPointToFPGenericTypeRule constant FLOATINGPOINT_TO_UBV_OP \ - ::CVC5::FloatingPointToUBV \ - "::CVC5::FloatingPointToBVHashFunction<0x1>" \ + ::cvc5::FloatingPointToUBV \ + "::cvc5::FloatingPointToBVHashFunction<0x1>" \ "util/floatingpoint.h" \ "operator for to_ubv" -typerule FLOATINGPOINT_TO_UBV_OP ::CVC5::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 ::CVC5::theory::fp::FloatingPointToUBVTypeRule +typerule FLOATINGPOINT_TO_UBV ::cvc5::theory::fp::FloatingPointToUBVTypeRule constant FLOATINGPOINT_TO_UBV_TOTAL_OP \ - ::CVC5::FloatingPointToUBVTotal \ - "::CVC5::FloatingPointToBVHashFunction<0x4>" \ + ::cvc5::FloatingPointToUBVTotal \ + "::cvc5::FloatingPointToBVHashFunction<0x4>" \ "util/floatingpoint.h" \ "operator for to_ubv_total" -typerule FLOATINGPOINT_TO_UBV_TOTAL_OP ::CVC5::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 ::CVC5::theory::fp::FloatingPointToUBVTotalTypeRule +typerule FLOATINGPOINT_TO_UBV_TOTAL ::cvc5::theory::fp::FloatingPointToUBVTotalTypeRule constant FLOATINGPOINT_TO_SBV_OP \ - ::CVC5::FloatingPointToSBV \ - "::CVC5::FloatingPointToBVHashFunction<0x2>" \ + ::cvc5::FloatingPointToSBV \ + "::cvc5::FloatingPointToBVHashFunction<0x2>" \ "util/floatingpoint.h" \ "operator for to_sbv" -typerule FLOATINGPOINT_TO_SBV_OP ::CVC5::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 ::CVC5::theory::fp::FloatingPointToSBVTypeRule +typerule FLOATINGPOINT_TO_SBV ::cvc5::theory::fp::FloatingPointToSBVTypeRule constant FLOATINGPOINT_TO_SBV_TOTAL_OP \ - ::CVC5::FloatingPointToSBVTotal \ - "::CVC5::FloatingPointToBVHashFunction<0x8>" \ + ::cvc5::FloatingPointToSBVTotal \ + "::cvc5::FloatingPointToBVHashFunction<0x8>" \ "util/floatingpoint.h" \ "operator for to_sbv_total" -typerule FLOATINGPOINT_TO_SBV_TOTAL_OP ::CVC5::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 ::CVC5::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 ::CVC5::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 ::CVC5::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 ::CVC5::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 ::CVC5::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 ::CVC5::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 ::CVC5::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 ::CVC5::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 ::CVC5::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 ::CVC5::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 ea9ea902c..38444c7af 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -33,7 +33,7 @@ using namespace std; -namespace CVC5 { +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(::CVC5::BitVector(1U, 1U)))); + nm->mkNode(kind::EQUAL, addA, nm->mkConst(::cvc5::BitVector(1U, 1U)))); #endif ++oldAdditionalAssertions; @@ -795,7 +795,7 @@ void TheoryFp::convertAndEquateTerm(TNode node) { kind::EQUAL, node, nm->mkNode( - kind::EQUAL, converted, nm->mkConst(::CVC5::BitVector(1U, 1U))))); + kind::EQUAL, converted, nm->mkConst(::cvc5::BitVector(1U, 1U))))); #endif } else { @@ -1157,4 +1157,4 @@ void TheoryFp::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { } // namespace fp } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 2607a33c6..87c63a231 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 CVC5 { +namespace cvc5 { namespace theory { namespace fp { @@ -189,6 +189,6 @@ class TheoryFp : public Theory } // namespace fp } // namespace theory -} // namespace CVC5 +} // 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 65e27fc48..d84c553de 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 CVC5 { +namespace cvc5 { namespace theory { namespace fp { @@ -1421,4 +1421,4 @@ TheoryFpRewriter::TheoryFpRewriter() } // namespace fp } // namespace theory - } // namespace CVC5 + } // namespace cvc5 diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h index bfdf90d44..52d22f3d3 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 CVC5 { +namespace cvc5 { namespace theory { namespace fp { @@ -53,6 +53,6 @@ class TheoryFpRewriter : public TheoryRewriter } // namespace fp } // namespace theory -} // namespace CVC5 +} // 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 6b87f8af3..d7060ad98 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 CVC5 { +namespace cvc5 { namespace theory { namespace fp { @@ -812,4 +812,4 @@ Cardinality CardinalityComputer::computeCardinality(TypeNode type) } // namespace fp } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index 632ae660d..0002b2abf 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 CVC5 { +namespace cvc5 { class NodeManager; @@ -229,6 +229,6 @@ class CardinalityComputer } // namespace fp } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h index 535ed7c69..73946ce5a 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 CVC5 { +namespace cvc5 { namespace theory { namespace fp { @@ -120,6 +120,6 @@ class RoundingModeEnumerator } // namespace fp } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__FP__TYPE_ENUMERATOR_H */ |