summaryrefslogtreecommitdiff
path: root/src/theory/fp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp')
-rw-r--r--src/theory/fp/fp_converter.cpp56
-rw-r--r--src/theory/fp/fp_converter.h6
-rw-r--r--src/theory/fp/kinds180
-rw-r--r--src/theory/fp/theory_fp.cpp8
-rw-r--r--src/theory/fp/theory_fp.h4
-rw-r--r--src/theory/fp/theory_fp_rewriter.cpp4
-rw-r--r--src/theory/fp/theory_fp_rewriter.h4
-rw-r--r--src/theory/fp/theory_fp_type_rules.cpp4
-rw-r--r--src/theory/fp/theory_fp_type_rules.h4
-rw-r--r--src/theory/fp/type_enumerator.h4
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback