diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/expr/expr_black.h | 4 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 20 | ||||
-rw-r--r-- | test/unit/parser/parser_black.h | 294 | ||||
-rw-r--r-- | test/unit/parser/parser_white.h | 6 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 4 |
5 files changed, 17 insertions, 311 deletions
diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h index 03d4ba31c..936381cd6 100644 --- a/test/unit/expr/expr_black.h +++ b/test/unit/expr/expr_black.h @@ -51,8 +51,8 @@ public: try { d_em = new ExprManager; - a = new Expr(d_em->mkVar(d_em->booleanType(), "a")); - b = new Expr(d_em->mkVar(d_em->booleanType(), "b")); + a = new Expr(d_em->mkVar("a",d_em->booleanType())); + b = new Expr(d_em->mkVar("b", d_em->booleanType())); c = new Expr(d_em->mkExpr(MULT, *a, *b)); mult = new Expr(d_em->mkConst(MULT)); plus = new Expr(d_em->mkConst(PLUS)); diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 9e199aa9a..17657683d 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -215,8 +215,8 @@ public: /* We don't have access to the ids so we can't test the implementation * in the black box tests. */ - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType(), "a"); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType(), "b"); + Node a = d_nodeManager->mkVar("a", d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar("b", d_nodeManager->booleanType()); TS_ASSERT(a<b || b<a); TS_ASSERT(!(a<b && b<a)); @@ -492,10 +492,10 @@ public: void testToString() { Type* booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkVar(booleanType, "w"); - Node x = d_nodeManager->mkVar(booleanType, "x"); - Node y = d_nodeManager->mkVar(booleanType, "y"); - Node z = d_nodeManager->mkVar(booleanType, "z"); + Node w = d_nodeManager->mkVar("w",booleanType); + Node x = d_nodeManager->mkVar("x",booleanType); + Node y = d_nodeManager->mkVar("y",booleanType); + Node z = d_nodeManager->mkVar("z",booleanType); Node m = NodeBuilder<>() << w << x << kind::OR; Node n = NodeBuilder<>() << m << y << z << kind::AND; @@ -505,10 +505,10 @@ public: void testToStream() { Type* booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkVar(booleanType, "w"); - Node x = d_nodeManager->mkVar(booleanType, "x"); - Node y = d_nodeManager->mkVar(booleanType, "y"); - Node z = d_nodeManager->mkVar(booleanType, "z"); + Node w = d_nodeManager->mkVar("w",booleanType); + Node x = d_nodeManager->mkVar("x",booleanType); + Node y = d_nodeManager->mkVar("y",booleanType); + Node z = d_nodeManager->mkVar("z",booleanType); Node m = NodeBuilder<>() << x << y << kind::OR; Node n = NodeBuilder<>() << w << m << z << kind::AND; Node o = NodeBuilder<>() << n << n << kind::XOR; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h deleted file mode 100644 index 5a341830b..000000000 --- a/test/unit/parser/parser_black.h +++ /dev/null @@ -1,294 +0,0 @@ -/********************* */ -/** parser_black.h - ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Black box testing of CVC4::parser::SmtParser. - **/ - -#include <cxxtest/TestSuite.h> -//#include <string> -#include <sstream> - -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "parser/input.h" -#include "expr/command.h" -#include "util/output.h" - -using namespace CVC4; -using namespace CVC4::parser; -using namespace std; - - -/************************** CVC test inputs ********************************/ - -const string goodCvc4Inputs[] = { - "", // empty string is OK - "ASSERT TRUE;", - "QUERY TRUE;", - "CHECKSAT FALSE;", - "a, b : BOOLEAN;", - "a, b : BOOLEAN; QUERY (a => b) AND a => b;", - "T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;", - "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;", - "%% nothing but a comment", - "% a comment\nASSERT TRUE; %a command\n% another comment", - }; - -const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string); - - -/* The following expressions are valid after setupContext. */ -const string goodCvc4Exprs[] = { - "a AND b", - "a AND b OR c", - "(a => b) AND a => b", - "(a <=> b) AND (NOT a)", - "(a XOR b) <=> (a OR b) AND (NOT (a AND b))" -}; - -const int numGoodCvc4Exprs = sizeof(goodCvc4Exprs) / sizeof(string); - -const string badCvc4Inputs[] = { - ";", // no command - "ASSERT;", // no args - "QUERY", - "CHECKSAT", - "a, b : boolean;", // lowercase boolean isn't a type - "0x : INT;", // 0x isn't an identifier - "a, b : BOOLEAN\nQUERY (a => b) AND a => b;", // no semicolon after decl - "a : BOOLEAN; a: BOOLEAN;" // double decl - "a, b: BOOLEAN; QUERY a(b);" // non-function used as function - }; - -const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string); - -/* The following expressions are invalid even after setupContext. */ -const string badCvc4Exprs[] = { - "a AND", // wrong arity - "AND(a,b)", // not infix - "(OR (AND a b) c)", // not infix - "a IMPLIES b", // should be => - "a NOT b", // wrong arity, not infix - "a and b" // wrong case -}; - -const int numBadCvc4Exprs = sizeof(badCvc4Exprs) / sizeof(string); - -/************************** SMT test inputs ********************************/ - -const string goodSmtInputs[] = { - "", // empty string is OK - "(benchmark foo :assumption true)", - "(benchmark bar :formula true)", - "(benchmark qux :formula false)", - "(benchmark baz :extrapreds ( (a) (b) ) )", - "(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))", - "(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) ) :formula (= (f x) x))", - "(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))", - ";; nothing but a comment", - "; a comment\n(benchmark foo ; hello\n :formula true; goodbye\n)" - }; - -const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string); - -/* The following expressions are valid after setupContext. */ -const string goodSmtExprs[] = { - "(and a b)", - "(or (and a b) c)", - "(implies (and (implies a b) a) b)", - "(and (iff a b) (not a))", - "(iff (xor a b) (and (or a b) (not (and a b))))", - "(ite a (f x) y)", - "(if_then_else a (f x) y)" -}; - -const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string); - -const string badSmtInputs[] = { - "(benchmark foo)", // empty benchmark is not OK - "(benchmark bar :assumption)", // no args - "(benchmark bar :formula)", - "(benchmark baz :extrapreds ( (a) (a) ) )", // double decl - "(benchmark zub :extrasorts (a) :extrapreds (p a))" // (p a) needs parens - }; - -const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string); - -/* The following expressions are invalid even after setupContext. */ -const string badSmtExprs[] = { - "(and)", // wrong arity - "(and a b", // no closing paren - "(a and b)", // infix - "(OR (AND a b) c)", // wrong case - "(a IMPLIES b)", // infix AND wrong case - "(not a b)", // wrong arity - "not a", // needs parens - "(ite a x)", // wrong arity - "(a b)" // using non-function as function -}; - -const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); - -class ParserBlack : public CxxTest::TestSuite { - ExprManager *d_exprManager; - - /* Set up declaration context for expr inputs */ - - void setupContext(Input* input) { - /* a, b, c: BOOLEAN */ - input->mkVar("a",(Type*)d_exprManager->booleanType()); - input->mkVar("b",(Type*)d_exprManager->booleanType()); - input->mkVar("c",(Type*)d_exprManager->booleanType()); - /* t, u, v: TYPE */ - Type *t = input->newSort("t"); - Type *u = input->newSort("u"); - Type *v = input->newSort("v"); - /* f : t->u; g: u->v; h: v->t; */ - input->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u)); - input->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v)); - input->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t)); - /* x:t; y:u; z:v; */ - input->mkVar("x",t); - input->mkVar("y",u); - input->mkVar("z",v); - } - - void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) { - for(int i = 0; i < numInputs; ++i) { - try { -// Debug.on("parser"); -// Debug.on("parser-extra"); - Debug("test") << "Testing good input: '" << goodInputs[i] << "'\n"; -// istringstream stream(goodInputs[i]); - Input* parser = Input::newStringParser(d_exprManager, d_lang, goodInputs[i], "test"); - TS_ASSERT( !parser->done() ); - Command* cmd; - while((cmd = parser->parseNextCommand())) { - // cout << "Parsed command: " << (*cmd) << endl; - } - TS_ASSERT( parser->parseNextCommand() == NULL ); - TS_ASSERT( parser->done() ); - delete parser; -// Debug.off("parser"); -// Debug.off("parser-extra"); - } catch (Exception& e) { - cout << "\nGood input failed:\n" << goodInputs[i] << endl - << e << endl; -// Debug.off("parser-extra"); - throw; - } - } - } - - void tryBadInputs(InputLanguage d_lang, const string badInputs[], int numInputs) { - for(int i = 0; i < numInputs; ++i) { -// cout << "Testing bad input: '" << badInputs[i] << "'\n"; -// Debug.on("parser"); - Input* parser = Input::newStringParser(d_exprManager, d_lang, badInputs[i], "test"); - TS_ASSERT_THROWS - ( while(parser->parseNextCommand()); - cout << "\nBad input succeeded:\n" << badInputs[i] << endl;, - ParserException ); -// Debug.off("parser"); - delete parser; - } - } - - void tryGoodExprs(InputLanguage d_lang, const string goodBooleanExprs[], int numExprs) { - // cout << "Using context: " << context << endl; -// Debug.on("parser"); -// Debug.on("parser-extra"); - for(int i = 0; i < numExprs; ++i) { - try { - // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n"; - // Debug.on("parser"); -// istringstream stream(context + goodBooleanExprs[i]); - Input* parser = Input::newStringParser(d_exprManager, d_lang, - goodBooleanExprs[i], "test"); - TS_ASSERT( !parser->done() ); - setupContext(parser); - TS_ASSERT( !parser->done() ); - Expr e = parser->parseNextExpression(); - TS_ASSERT( !e.isNull() ); - e = parser->parseNextExpression(); - TS_ASSERT( parser->done() ); - TS_ASSERT( e.isNull() ); - delete parser; - } catch (Exception& e) { - cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl; - cout << e; - throw e; - } - } - } - - void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs) { - //Debug.on("parser"); - for(int i = 0; i < numExprs; ++i) { - // cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n"; -// istringstream stream(context + badBooleanExprs[i]); - Input* parser = Input::newStringParser(d_exprManager, d_lang, - badBooleanExprs[i], "test"); - - TS_ASSERT( !parser->done() ); - setupContext(parser); - TS_ASSERT( !parser->done() ); - TS_ASSERT_THROWS - ( parser->parseNextExpression(); - cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, - ParserException ); - delete parser; - } - //Debug.off("parser"); - } - -public: - void setUp() { - d_exprManager = new ExprManager(); - } - - void tearDown() { - delete d_exprManager; - } - - void testGoodCvc4Inputs() { - tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); - } - - void testBadCvc4Inputs() { - tryBadInputs(LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs); - } - - void testGoodCvc4Exprs() { - tryGoodExprs(LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs); - } - - void testBadCvc4Exprs() { - tryBadExprs(LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs); - } - - void testGoodSmtInputs() { - tryGoodInputs(LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs); - } - - void testBadSmtInputs() { - tryBadInputs(LANG_SMTLIB,badSmtInputs,numBadSmtInputs); - } - - void testGoodSmtExprs() { - tryGoodExprs(LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs); - } - - void testBadSmtExprs() { - tryBadExprs(LANG_SMTLIB,badSmtExprs,numBadSmtExprs); - } -}; diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h index 270061c29..d0959cf6f 100644 --- a/test/unit/parser/parser_white.h +++ b/test/unit/parser/parser_white.h @@ -150,9 +150,9 @@ class ParserWhite : public CxxTest::TestSuite { parserState->mkVar("b",(Type*)d_exprManager->booleanType()); parserState->mkVar("c",(Type*)d_exprManager->booleanType()); /* t, u, v: TYPE */ - Type *t = parserState->newSort("t"); - Type *u = parserState->newSort("u"); - Type *v = parserState->newSort("v"); + Type *t = parserState->mkSort("t"); + Type *u = parserState->mkSort("u"); + Type *v = parserState->mkSort("v"); /* f : t->u; g: u->v; h: v->t; */ parserState->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u)); parserState->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v)); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index c6da48291..905294c27 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -214,8 +214,8 @@ public: Type* typeX = d_nm->booleanType(); Type* typeF = d_nm->mkFunctionType(typeX, typeX); - Node x = d_nm->mkVar(typeX, "x"); - Node f = d_nm->mkVar(typeF, "f"); + Node x = d_nm->mkVar("x",typeX); + Node f = d_nm->mkVar("f",typeF); Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); Node f_x_eq_x = f_x.eqNode(x); |