diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-08 23:12:28 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-08 23:12:28 +0000 |
commit | e63abd23b45a078a42cafb277a4817abb4d044a1 (patch) | |
tree | 43b8aaccc9b49887280e0c77471c5346eb1cf9c4 /src/expr/expr_manager_template.cpp | |
parent | fccdb4cbe2cde7c34e82f33e9de850a046fef888 (diff) |
* (define-fun...) now has proper type checking in non-debug builds
(resolves bug #212)
* also closed some other type checking loopholes in SmtEngine
* small fixes to define-sort (resolves bug #214)
* infrastructural support for printing expressions in languages
other than the internal representation language using an IO
manipulator, e.g.:
cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr;
main() sets the output language for all streams to correspond to
the input language
* support delaying type checking in debug builds, so that one can debug
the type checker itself (before it was difficult, because debug builds did
all the type checking on Node creation!): new command-line flag
--no-early-type-checking (only makes sense for debug builds)
* disallowed copy-construction of ExprManager and NodeManager, and made other
constructors explicit; previously it was easy to unintentionally create
duplicate managers, with really weird results (i.e., disappearing
attributes!)
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 32 |
1 files changed, 15 insertions, 17 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 55b59d13c..5cf3373c2 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -34,9 +34,9 @@ using namespace CVC4::kind; namespace CVC4 { -ExprManager::ExprManager() : +ExprManager::ExprManager(bool earlyTypeChecking) : d_ctxt(new Context), - d_nodeManager(new NodeManager(d_ctxt)) { + d_nodeManager(new NodeManager(d_ctxt, earlyTypeChecking)) { } ExprManager::~ExprManager() { @@ -75,7 +75,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { try { return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); + throw TypeCheckingException(this, &e); } } @@ -92,8 +92,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { child1.getNode(), child2.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), - e.getMessage()); + throw TypeCheckingException(this, &e); } } @@ -112,8 +111,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, child2.getNode(), child3.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), - e.getMessage()); + throw TypeCheckingException(this, &e); } } @@ -133,8 +131,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, child3.getNode(), child4.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), - e.getMessage()); + throw TypeCheckingException(this, &e); } } @@ -156,8 +153,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, child4.getNode(), child5.getNode())); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), - e.getMessage()); + throw TypeCheckingException(this, &e); } } @@ -181,8 +177,7 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { try { return Expr(this, d_nodeManager->mkNodePtr(kind, nodes)); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), - e.getMessage()); + throw TypeCheckingException(this, &e); } } @@ -207,7 +202,7 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) { try { return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes)); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); + throw TypeCheckingException(this, &e); } } @@ -309,16 +304,19 @@ Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingExceptio NodeManagerScope nms(d_nodeManager); Type t; try { - t = Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode(), check))); + t = Type(d_nodeManager, + new TypeNode(d_nodeManager->getType(e.getNode(), check))); } catch (const TypeCheckingExceptionPrivate& e) { - throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); + throw TypeCheckingException(this, &e); } return t; } Expr ExprManager::mkVar(const std::string& name, const Type& type) { NodeManagerScope nms(d_nodeManager); - return Expr(this, d_nodeManager->mkVarPtr(name, *type.d_typeNode)); + Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode); + Debug("nm") << "set " << name << " on " << *n << std::endl; + return Expr(this, n); } Expr ExprManager::mkVar(const Type& type) { |