From 1c494313662b664a606f6f745f67cbd964c61927 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 6 Oct 2014 21:22:57 -0400 Subject: [PATCH] Some minor cleanup. --- src/theory/booleans/theory_bool_type_rules.h | 20 +++++++++++++------- 1 file 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 */ -- 2.30.2