diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 21:22:57 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 21:22:57 -0400 |
commit | 1c494313662b664a606f6f745f67cbd964c61927 (patch) | |
tree | 1f080655da2d6e3e9aed2f363bc56179fdcf2206 /src/theory/booleans | |
parent | 87b9af34d7864044aa70720cfd32bf259750772b (diff) |
Some minor cleanup.
Diffstat (limited to 'src/theory/booleans')
-rw-r--r-- | src/theory/booleans/theory_bool_type_rules.h | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index d2836c85e..9d12e1bb1 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -42,10 +42,10 @@ public: } return booleanType; } -}; +};/* class BooleanTypeRule */ class IteTypeRule { - public: +public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode thenType = n[1].getType(check); @@ -57,15 +57,21 @@ class IteTypeRule { throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean"); } if (iteType.isNull()) { - throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be a subtype of a common type."); + std::stringstream ss; + ss << "Both branches of the ITE must be a subtype of a common type." << std::endl + << "then branch: " << n[1] << std::endl + << "its type : " << thenType << std::endl + << "else branch: " << n[2] << std::endl + << "its type : " << elseType << std::endl; + throw TypeCheckingExceptionPrivate(n, ss.str()); } } return iteType; } -}; +};/* class IteTypeRule */ -}/* namespace CVC4::theory::boolean */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ +}/* CVC4::theory::boolean namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__THEORY_BOOL_TYPE_RULES_H */ |