diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-28 22:57:36 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-28 22:57:36 +0000 |
commit | 88766918615793536224bf50d0bb70ec9f9efd93 (patch) | |
tree | 5a038bb2c17199f43d7a422063751bc3839b7388 /src/theory | |
parent | d2787f41e72184fbdf2619d3c0466bed9b6211be (diff) |
Forcing a type check on Node construction in debug mode (Fixes: #188)
NOTE: mkNode/mkExpr/parsing functions can now throw type checking exceptions
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 33e4c942f..354bf02bd 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -25,6 +25,8 @@ #include "expr/type_node.h" #include "expr/expr.h" +#include <sstream> + namespace CVC4 { namespace theory { namespace builtin { @@ -39,7 +41,11 @@ class EqualityTypeRule { TypeNode rhsType = n[1].getType(check); if ( lhsType != rhsType ) { - throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type"); + std::stringstream ss; + ss << "Types do not match in equation "; + ss << "[" << lhsType << "<>" << rhsType << "]"; + + throw TypeCheckingExceptionPrivate(n, ss.str()); } if ( lhsType == booleanType ) { |