diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-17 18:48:39 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-17 18:48:39 +0000 |
commit | 7eb18a6c4b0ec6fcf4b6474d22307baa04f8f515 (patch) | |
tree | 8621e2e60756ec6770bc949877eef808e7e99d55 /src | |
parent | 3b06265b82d48074b3b733d655efd6dab6481150 (diff) |
+ test infrastructure fixes
+ regenerate configure script
+ add CVC4::Message output class
+ add some IllegalArgument() assertion things
+ rename NodeManager::mkExpr() to mkNode()
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr_manager.cpp | 14 | ||||
-rw-r--r-- | src/expr/node.cpp | 16 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 14 | ||||
-rw-r--r-- | src/expr/node_manager.h | 14 | ||||
-rw-r--r-- | src/main/main.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
-rw-r--r-- | src/util/Assert.h | 39 | ||||
-rw-r--r-- | src/util/output.cpp | 1 | ||||
-rw-r--r-- | src/util/output.h | 18 |
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; |