diff options
author | Tim King <taking@cs.nyu.edu> | 2010-05-21 19:27:18 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-05-21 19:27:18 +0000 |
commit | 4ba56dc24c972afae6137e4dd6a05f3957e48bf5 (patch) | |
tree | 45bde947434108368092d09a355108469b58d524 /src/expr | |
parent | 5321d62fce6c747fa9d11e9df5b2ef8c4e25de21 (diff) |
Small fixes to TheoryArith. Added a hack to make Integers a subtype of Real. See Bug 127 for a discussion of the hack. I am also adding a regression test that does not work (bug 128). It is not enabled so make check should still be fine.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/builtin_type_rules.h | 2 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 3 | ||||
-rw-r--r-- | src/expr/type_node.h | 4 |
3 files changed, 5 insertions, 4 deletions
diff --git a/src/expr/builtin_type_rules.h b/src/expr/builtin_type_rules.h index 2a6b43b22..e0ad0b038 100644 --- a/src/expr/builtin_type_rules.h +++ b/src/expr/builtin_type_rules.h @@ -23,7 +23,7 @@ namespace CVC4 { class EqualityTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingException) { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingExceptionPrivate) { if (n[0].getType() != n[1].getType()) { throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type"); } diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index da16000ce..821349b45 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -28,7 +28,8 @@ bool TypeNode::isInteger() const { } bool TypeNode::isReal() const { - return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE; + return getKind() == kind::TYPE_CONSTANT + && (getConst<TypeConstant>() == REAL_TYPE || getConst<TypeConstant>() == INTEGER_TYPE); } /** Is this a function type? */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 1d32fffda..f7b1a6b9e 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -110,7 +110,7 @@ public: * @return true if expressions are equal, false otherwise */ bool operator==(const TypeNode& typeNode) const { - return d_nv == typeNode.d_nv; + return d_nv == typeNode.d_nv || (typeNode.isReal() && this->isReal()); } /** @@ -119,7 +119,7 @@ public: * @return true if expressions are equal, false otherwise */ bool operator!=(const TypeNode& typeNode) const { - return d_nv != typeNode.d_nv; + return !(*this == typeNode); } /** |