+ test infrastructure fixes

+ regenerate configure script
+ add CVC4::Message output class
+ add some IllegalArgument() assertion things
+ rename NodeManager::mkExpr() to mkNode()

4 files changed, 29 insertions, 29 deletions

diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 877ba9d3c..ea1649e12 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -23,27 +23,27 @@ ExprManager::~ExprManager() {
 }
 
 Expr ExprManager::mkExpr(Kind kind) {
-  return Expr(this, new Node(d_nm->mkExpr(kind)));
+  return Expr(this, new Node(d_nm->mkNode(kind)));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
-  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode())));
+  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
-  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3) {
-  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3, const Expr& child4) {
-  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
                                           child4.getNode())));
 }
@@ -51,7 +51,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3, const Expr& child4,
                          const Expr& child5) {
-  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
                                           child5.getNode())));
 }
@@ -64,7 +64,7 @@ Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
     nodes.push_back(it->getNode());
     ++it;
   }
-  return Expr(this, new Node(d_nm->mkExpr(kind, nodes)));
+  return Expr(this, new Node(d_nm->mkNode(kind, nodes)));
 }
 
 Expr ExprManager::mkVar() {
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 40dd70457..334cf1b0e 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -87,35 +87,35 @@ uint64_t Node::hash() const {
 }
 
 Node Node::eqExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(EQUAL, *this, right);
+  return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
 }
 
 Node Node::notExpr() const {
-  return NodeManager::currentNM()->mkExpr(NOT, *this);
+  return NodeManager::currentNM()->mkNode(NOT, *this);
 }
 
 Node Node::andExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(AND, *this, right);
+  return NodeManager::currentNM()->mkNode(AND, *this, right);
 }
 
 Node Node::orExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(OR, *this, right);
+  return NodeManager::currentNM()->mkNode(OR, *this, right);
 }
 
 Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
-  return NodeManager::currentNM()->mkExpr(ITE, *this, thenpart, elsepart);
+  return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
 }
 
 Node Node::iffExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(IFF, *this, right);
+  return NodeManager::currentNM()->mkNode(IFF, *this, right);
 }
 
 Node Node::impExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(IMPLIES, *this, right);
+  return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
 }
 
 Node Node::xorExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(XOR, *this, right);
+  return NodeManager::currentNM()->mkNode(XOR, *this, right);
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 4b550ee3d..7e871d9c3 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -101,32 +101,32 @@ NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
 
 // general expression-builders
 
-Node NodeManager::mkExpr(Kind kind) {
+Node NodeManager::mkNode(Kind kind) {
   return NodeBuilder<>(this, kind);
 }
 
-Node NodeManager::mkExpr(Kind kind, const Node& child1) {
+Node NodeManager::mkNode(Kind kind, const Node& child1) {
   return NodeBuilder<>(this, kind) << child1;
 }
 
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2) {
   return NodeBuilder<>(this, kind) << child1 << child2;
 }
 
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
   return NodeBuilder<>(this, kind) << child1 << child2 << child3;
 }
 
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
   return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
 }
 
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
   return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
 }
 
 // N-ary version
-Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) {
+Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) {
   return NodeBuilder<>(this, kind).append(children);
 }
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 8caa797fa..643f09f11 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -36,14 +36,14 @@ public:
   static NodeManager* currentNM() { return s_current; }
 
   // general expression-builders
-  Node mkExpr(Kind kind);
-  Node mkExpr(Kind kind, const Node& child1);
-  Node mkExpr(Kind kind, const Node& child1, const Node& child2);
-  Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3);
-  Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
-  Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
+  Node mkNode(Kind kind);
+  Node mkNode(Kind kind, const Node& child1);
+  Node mkNode(Kind kind, const Node& child1, const Node& child2);
+  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3);
+  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
+  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
   // N-ary version
-  Node mkExpr(Kind kind, const std::vector<Node>& children);
+  Node mkNode(Kind kind, const std::vector<Node>& children);
 
   // variables are special, because duplicates are permitted
   Node mkVar();