+ test infrastructure fixes

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

9 files changed, 88 insertions, 32 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();
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 4e408823f..187a0f316 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -81,6 +81,7 @@ int main(int argc, char *argv[]) {
       Trace.setStream(CVC4::null_os);
       Notice.setStream(CVC4::null_os);
       Chat.setStream(CVC4::null_os);
+      Message.setStream(CVC4::null_os);
       Warning.setStream(CVC4::null_os);
     } else {
       if(options.verbosity < 2) {
@@ -90,6 +91,7 @@ int main(int argc, char *argv[]) {
         Notice.setStream(CVC4::null_os);
       }
       if(options.verbosity < 0) {
+        Message.setStream(CVC4::null_os);
         Warning.setStream(CVC4::null_os);
       }
     }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 723263177..f07ad577e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -41,7 +41,7 @@ Node SmtEngine::processAssertionList() {
   for(std::vector<Node>::iterator i = d_assertions.begin();
       i != d_assertions.end();
       ++i)
-    asserts = asserts.isNull() ? *i : d_em->mkExpr(AND, asserts, *i);
+    asserts = asserts.isNull() ? *i : d_em->mkNode(AND, asserts, *i);
   return asserts;
 }
 
diff --git a/src/util/Assert.h b/src/util/Assert.h
index c3b81727c..26a1ee7d4 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -122,7 +122,8 @@ public:
     va_list args;
     va_start(args, fmt);
     construct("Illegal argument detected",
-              argDesc, function, file, line, fmt, args);
+              ( std::string(argDesc) + " invalid" ).c_str(),
+              function, file, line, fmt, args);
     va_end(args);
   }
 
@@ -130,7 +131,31 @@ public:
                            const char* file, unsigned line) :
     AssertionException() {
     construct("Illegal argument detected",
-              argDesc, function, file, line);
+              ( std::string(argDesc) + " invalid" ).c_str(),
+              function, file, line);
+  }
+
+  IllegalArgumentException(const char* condStr, const char* argDesc,
+                           const char* function, const char* file,
+                           unsigned line, const char* fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Illegal argument detected",
+              ( std::string(argDesc) + " invalid; expected " +
+                condStr + " to hold" ).c_str(),
+              function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  IllegalArgumentException(const char* condStr, const char* argDesc,
+                           const char* function, const char* file,
+                           unsigned line) :
+    AssertionException() {
+    construct("Illegal argument detected",
+              ( std::string(argDesc) + " invalid; expected " +
+                condStr + " to hold" ).c_str(),
+              function, file, line);
   }
 };/* class IllegalArgumentException */
 
@@ -146,11 +171,21 @@ public:
   throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define IllegalArgument(arg, msg...) \
   throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+#define CheckArgument(cond, arg, msg...)         \
+  AlwaysAssertArgument(cond, arg, ## msg)
+#define AlwaysAssertArgument(cond, arg, msg...)  \
+  do { \
+    if(EXPECT_FALSE( ! (cond) )) { \
+      throw IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+    } \
+  } while(0)
 
 #ifdef CVC4_ASSERTIONS
 #  define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
+#  define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
 #else /* ! CVC4_ASSERTIONS */
 #  define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
+#  define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
 #endif /* CVC4_ASSERTIONS */
 
 }/* CVC4 namespace */
diff --git a/src/util/output.cpp b/src/util/output.cpp
index e07f32a66..103a3d61a 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -22,6 +22,7 @@ std::ostream null_os(&null_sb);
 
 DebugC   Debug  (&std::cout);
 WarningC Warning(&std::cerr);
+MessageC Message(&std::cout);
 NoticeC  Notice (&std::cout);
 ChatC    Chat   (&std::cout);
 TraceC   Trace  (&std::cout);
diff --git a/src/util/output.h b/src/util/output.h
index b6532b93a..43dfe8a40 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -91,6 +91,24 @@ public:
 
 extern WarningC Warning CVC4_PUBLIC;
 
+class CVC4_PUBLIC MessageC {
+  std::ostream *d_os;
+
+public:
+  MessageC(std::ostream* os) : d_os(os) {}
+
+  void operator()(const char* s) { *d_os << s; }
+  void operator()(std::string s) { *d_os << s; }
+
+  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  std::ostream& operator()() { return *d_os; }
+
+  void setStream(std::ostream& os) { d_os = &os; }
+};/* class Message */
+
+extern MessageC Message CVC4_PUBLIC;
+
 class CVC4_PUBLIC NoticeC {
   std::ostream *d_os;