summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/expr_manager_template.cpp66
-rw-r--r--src/expr/node.h1
-rw-r--r--src/expr/node_manager.h70
-rw-r--r--src/parser/cvc/cvc_input.cpp4
-rw-r--r--src/parser/cvc/cvc_input.h6
-rw-r--r--src/parser/input.h4
-rw-r--r--src/parser/parser.cpp10
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h8
8 files changed, 135 insertions, 34 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5fcbad3a2..343f060e9 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -77,7 +77,11 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
kind::kindToString(kind).c_str(),
minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
- return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
+ try {
+ return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+ }
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
@@ -88,8 +92,14 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
kind::kindToString(kind).c_str(),
minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
- return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(),
- child2.getNode()));
+ try {
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
+ child1.getNode(),
+ child2.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())),
+ e.getMessage());
+ }
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
@@ -101,7 +111,15 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
kind::kindToString(kind).c_str(),
minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
- return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), child2.getNode(), child3.getNode()));
+ try {
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
+ child1.getNode(),
+ child2.getNode(),
+ child3.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())),
+ e.getMessage());
+ }
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
@@ -113,9 +131,16 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
kind::kindToString(kind).c_str(),
minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
- return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(),
- child2.getNode(), child3.getNode(),
- child4.getNode()));
+ try {
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
+ child1.getNode(),
+ child2.getNode(),
+ child3.getNode(),
+ child4.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())),
+ e.getMessage());
+ }
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
@@ -128,9 +153,17 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
kind::kindToString(kind).c_str(),
minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
- return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(),
- child2.getNode(), child3.getNode(),
- child5.getNode()));
+ try {
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
+ child1.getNode(),
+ child2.getNode(),
+ child3.getNode(),
+ child4.getNode(),
+ child5.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())),
+ e.getMessage());
+ }
}
Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
@@ -150,7 +183,12 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
nodes.push_back(it->getNode());
++it;
}
- return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
+ try {
+ return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())),
+ e.getMessage());
+ }
}
Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
@@ -171,7 +209,11 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
nodes.push_back(it->getNode());
++it;
}
- return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
+ try {
+ return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage());
+ }
}
/** Make a function type from domain to range. */
diff --git a/src/expr/node.h b/src/expr/node.h
index 4b1a0e5be..222185e8c 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -34,6 +34,7 @@
#include "expr/metakind.h"
#include "expr/expr.h"
#include "util/Assert.h"
+#include "util/configuration.h"
#include "util/output.h"
namespace CVC4 {
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7a53cabfc..b7c7f871e 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -242,6 +242,12 @@ class NodeManager {
// bool containsDecision(TNode); // is "atomic"
// bool properlyContainsDecision(TNode); // all children are atomic
+ template <unsigned nchild_thresh>
+ Node doMkNode(NodeBuilder<nchild_thresh>&);
+
+ template <unsigned nchild_thresh>
+ Node* doMkNodePtr(NodeBuilder<nchild_thresh>&);
+
public:
NodeManager(context::Context* ctxt);
@@ -779,61 +785,91 @@ inline TypeNode NodeManager::mkSort(const std::string& name) {
return type;
}
+template <unsigned nchild_thresh>
+inline Node NodeManager::doMkNode(NodeBuilder<nchild_thresh>& nb) {
+ Node n = nb.constructNode();
+ if( Configuration::isDebugBuild() ) {
+ // force an immediate type check
+ getType(n,true);
+ }
+ return n;
+}
+
+template <unsigned nchild_thresh>
+inline Node* NodeManager::doMkNodePtr(NodeBuilder<nchild_thresh>& nb) {
+ Node* np = nb.constructNodePtr();
+ if( Configuration::isDebugBuild() ) {
+ // force an immediate type check
+ getType(*np,true);
+ }
+ return np;
+}
+
+
inline Node NodeManager::mkNode(Kind kind, TNode child1) {
- return NodeBuilder<1>(this, kind) << child1;
+ NodeBuilder<1> nb(this, kind);
+ nb << child1;
+ return doMkNode(nb);
}
inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
NodeBuilder<1> nb(this, kind);
nb << child1;
- return nb.constructNodePtr();
+ return doMkNodePtr(nb);
}
inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
- return NodeBuilder<2>(this, kind) << child1 << child2;
+ NodeBuilder<2> nb(this, kind);
+ nb << child1 << child2;
+ return doMkNode(nb);
}
inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
NodeBuilder<2> nb(this, kind);
nb << child1 << child2;
- return nb.constructNodePtr();
+ return doMkNodePtr(nb);
}
inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
TNode child3) {
- return NodeBuilder<3>(this, kind) << child1 << child2 << child3;
+ NodeBuilder<3> nb(this, kind);
+ nb << child1 << child2 << child3;
+ return doMkNode(nb);
}
inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
TNode child3) {
NodeBuilder<3> nb(this, kind);
nb << child1 << child2 << child3;
- return nb.constructNodePtr();
+ return doMkNodePtr(nb);
}
inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
TNode child3, TNode child4) {
- return NodeBuilder<4>(this, kind) << child1 << child2 << child3 << child4;
+ NodeBuilder<4> nb(this, kind);
+ nb << child1 << child2 << child3 << child4;
+ return doMkNode(nb);
}
inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
TNode child3, TNode child4) {
NodeBuilder<4> nb(this, kind);
nb << child1 << child2 << child3 << child4;
- return nb.constructNodePtr();
+ return doMkNodePtr(nb);
}
inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
TNode child3, TNode child4, TNode child5) {
- return NodeBuilder<5>(this, kind) << child1 << child2 << child3 << child4
- << child5;
+ NodeBuilder<5> nb(this, kind);
+ nb << child1 << child2 << child3 << child4 << child5;
+ return doMkNode(nb);
}
inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
TNode child3, TNode child4, TNode child5) {
NodeBuilder<5> nb(this, kind);
nb << child1 << child2 << child3 << child4 << child5;
- return nb.constructNodePtr();
+ return doMkNodePtr(nb);
}
// N-ary version
@@ -841,14 +877,18 @@ template <bool ref_count>
inline Node NodeManager::mkNode(Kind kind,
const std::vector<NodeTemplate<ref_count> >&
children) {
- return NodeBuilder<>(this, kind).append(children);
+ NodeBuilder<> nb(this, kind);
+ nb.append(children);
+ return doMkNode(nb);
}
template <bool ref_count>
inline Node* NodeManager::mkNodePtr(Kind kind,
const std::vector<NodeTemplate<ref_count> >&
children) {
- return NodeBuilder<>(this, kind).append(children).constructNodePtr();
+ NodeBuilder<> nb(this, kind);
+ nb.append(children);
+ return doMkNodePtr(nb);
}
// N-ary version for operators
@@ -860,7 +900,7 @@ inline Node NodeManager::mkNode(TNode opNode,
NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
nb << opNode;
nb.append(children);
- return nb;
+ return doMkNode(nb);
}
template <bool ref_count>
@@ -870,7 +910,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode,
NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
nb << opNode;
nb.append(children);
- return nb.constructNodePtr();
+ return doMkNodePtr(nb);
}
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 6b38abaab..3532b8aa7 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -59,12 +59,12 @@ CvcInput::~CvcInput() {
}
Command* CvcInput::parseCommand()
- throw (ParserException, AssertionException) {
+ throw (ParserException, TypeCheckingException, AssertionException) {
return d_pCvcParser->parseCommand(d_pCvcParser);
}
Expr CvcInput::parseExpr()
- throw (ParserException, AssertionException) {
+ throw (ParserException, TypeCheckingException, AssertionException) {
return d_pCvcParser->parseExpr(d_pCvcParser);
}
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 6a37680e8..cce935c0b 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -71,14 +71,16 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand() throw(ParserException, AssertionException);
+ Command* parseCommand()
+ throw(ParserException, TypeCheckingException, AssertionException);
/** Parse an expression from the input. Returns a null <code>Expr</code>
* if there is no expression there to parse.
*
* @throws ParserException if an error is encountered during parsing.
*/
- Expr parseExpr() throw(ParserException, AssertionException);
+ Expr parseExpr()
+ throw(ParserException, TypeCheckingException, AssertionException);
private:
diff --git a/src/parser/input.h b/src/parser/input.h
index 62015ba51..1a90a4191 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -155,7 +155,7 @@ protected:
* @throws ParserException if an error is encountered during parsing.
*/
virtual Command* parseCommand()
- throw (ParserException, AssertionException) = 0;
+ throw (ParserException, TypeCheckingException, AssertionException) = 0;
/**
* Throws a <code>ParserException</code> with the given message.
@@ -171,7 +171,7 @@ protected:
* @throws ParserException if an error is encountered during parsing.
*/
virtual Expr parseExpr()
- throw (ParserException, AssertionException) = 0;
+ throw (ParserException, TypeCheckingException, AssertionException) = 0;
/** Set the Parser object for this input. */
virtual void setParser(Parser& parser) = 0;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 2bad12e2c..f73e268a3 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -234,6 +234,11 @@ Command* Parser::nextCommand() throw(ParserException) {
} catch(ParserException& e) {
setDone();
throw;
+ } catch(TypeCheckingException& e) {
+ setDone();
+ stringstream ss;
+ ss << e.getMessage() << ": " << e.getExpression();
+ parseError( ss.str() );
}
}
Debug("parser") << "nextCommand() => " << cmd << std::endl;
@@ -252,6 +257,11 @@ Expr Parser::nextExpression() throw(ParserException) {
} catch(ParserException& e) {
setDone();
throw;
+ } catch(TypeCheckingException& e) {
+ setDone();
+ stringstream ss;
+ ss << e.getMessage() << ": " << e.getExpression();
+ parseError( ss.str() );
}
}
Debug("parser") << "nextExpression() => " << result << std::endl;
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 ) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback