diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/.gitignore | 2 | ||||
-rw-r--r-- | test/regress/.gitignore | 2 | ||||
-rw-r--r-- | test/regress/regress0/.gitignore | 2 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 13 | ||||
-rw-r--r-- | test/regress/regress0/precedence/.gitignore | 1 | ||||
-rw-r--r-- | test/regress/regress0/precedence/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/uf/.gitignore | 1 | ||||
-rw-r--r-- | test/regress/regress0/uf/Makefile.am | 11 | ||||
-rw-r--r-- | test/regress/regress1/.gitignore | 2 | ||||
-rw-r--r-- | test/regress/regress2/.gitignore | 2 | ||||
-rw-r--r-- | test/regress/regress3/.gitignore | 2 | ||||
-rw-r--r-- | test/system/.gitignore | 1 | ||||
-rw-r--r-- | test/unit/.gitignore | 2 | ||||
-rw-r--r-- | test/unit/expr/.gitignore | 4 | ||||
-rw-r--r-- | test/unit/parser/parser_black.h | 132 |
15 files changed, 112 insertions, 68 deletions
diff --git a/test/.gitignore b/test/.gitignore new file mode 100644 index 000000000..f39e98071 --- /dev/null +++ b/test/.gitignore @@ -0,0 +1,2 @@ +/.deps +/Makefile.in diff --git a/test/regress/.gitignore b/test/regress/.gitignore new file mode 100644 index 000000000..f39e98071 --- /dev/null +++ b/test/regress/.gitignore @@ -0,0 +1,2 @@ +/.deps +/Makefile.in diff --git a/test/regress/regress0/.gitignore b/test/regress/regress0/.gitignore new file mode 100644 index 000000000..f39e98071 --- /dev/null +++ b/test/regress/regress0/.gitignore @@ -0,0 +1,2 @@ +/.deps +/Makefile.in diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 29141d633..eb07b22fb 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,22 +1,23 @@ SUBDIRS = precedence uf TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 -TESTS = bug32.cvc \ +TESTS = \ distinct.smt \ flet.smt \ flet2.smt \ - hole6.cvc \ let.smt \ let2.smt \ + simple2.smt \ + simple.smt \ + simple-uf.smt \ + bug32.cvc \ + hole6.cvc \ logops.01.cvc \ logops.02.cvc \ logops.03.cvc \ logops.04.cvc \ logops.05.cvc \ - simple2.smt \ simple.cvc \ - simple.smt \ - simple-uf.smt \ smallcnf.cvc \ test11.cvc \ test9.cvc \ @@ -42,7 +43,7 @@ TESTS = bug32.cvc \ wiki.19.cvc \ wiki.20.cvc \ wiki.21.cvc - + # synonyms for "check" .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/precedence/.gitignore b/test/regress/regress0/precedence/.gitignore new file mode 100644 index 000000000..10a7e8d6c --- /dev/null +++ b/test/regress/regress0/precedence/.gitignore @@ -0,0 +1 @@ +/Makefile.in diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 36722b81b..0b4fcd4a6 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -1,5 +1,6 @@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4 -TESTS = iff-implies.cvc \ +TESTS = \ + iff-implies.cvc \ implies-iff.cvc \ implies-or.cvc \ or-implies.cvc \ diff --git a/test/regress/regress0/uf/.gitignore b/test/regress/regress0/uf/.gitignore new file mode 100644 index 000000000..10a7e8d6c --- /dev/null +++ b/test/regress/regress0/uf/.gitignore @@ -0,0 +1 @@ +/Makefile.in diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index b456f2809..ec99fd45c 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -1,8 +1,5 @@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4 -TESTS = simple.01.cvc \ - simple.02.cvc \ - simple.03.cvc \ - simple.04.cvc \ +TESTS = \ euf_simp01.smt \ euf_simp02.smt \ euf_simp03.smt \ @@ -17,7 +14,11 @@ TESTS = simple.01.cvc \ euf_simp13.smt \ dead_dnd002.smt \ iso_brn001.smt \ - SEQ032_size2.smt + SEQ032_size2.smt \ + simple.01.cvc \ + simple.02.cvc \ + simple.03.cvc \ + simple.04.cvc # synonyms for "check" .PHONY: regress regress0 test diff --git a/test/regress/regress1/.gitignore b/test/regress/regress1/.gitignore new file mode 100644 index 000000000..f39e98071 --- /dev/null +++ b/test/regress/regress1/.gitignore @@ -0,0 +1,2 @@ +/.deps +/Makefile.in diff --git a/test/regress/regress2/.gitignore b/test/regress/regress2/.gitignore new file mode 100644 index 000000000..f39e98071 --- /dev/null +++ b/test/regress/regress2/.gitignore @@ -0,0 +1,2 @@ +/.deps +/Makefile.in diff --git a/test/regress/regress3/.gitignore b/test/regress/regress3/.gitignore new file mode 100644 index 000000000..f39e98071 --- /dev/null +++ b/test/regress/regress3/.gitignore @@ -0,0 +1,2 @@ +/.deps +/Makefile.in diff --git a/test/system/.gitignore b/test/system/.gitignore new file mode 100644 index 000000000..10a7e8d6c --- /dev/null +++ b/test/system/.gitignore @@ -0,0 +1 @@ +/Makefile.in diff --git a/test/unit/.gitignore b/test/unit/.gitignore new file mode 100644 index 000000000..f39e98071 --- /dev/null +++ b/test/unit/.gitignore @@ -0,0 +1,2 @@ +/.deps +/Makefile.in diff --git a/test/unit/expr/.gitignore b/test/unit/expr/.gitignore new file mode 100644 index 000000000..71ef9896d --- /dev/null +++ b/test/unit/expr/.gitignore @@ -0,0 +1,4 @@ +/expr_black +/expr_black.cpp +/expr_white +/expr_white.cpp diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index f7d4eff24..b7c58ba99 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -19,7 +19,7 @@ #include "expr/expr.h" #include "expr/expr_manager.h" -#include "parser/parser.h" +#include "parser/input.h" #include "expr/command.h" #include "util/output.h" @@ -27,6 +27,28 @@ using namespace CVC4; using namespace CVC4::parser; using namespace std; +/* Set up declaration context for expr inputs */ + +void setupContext(Input* input) { + /* a, b, c: BOOLEAN */ + input->mkVar("a",(Type*)input->booleanType()); + input->mkVar("b",(Type*)input->booleanType()); + input->mkVar("c",(Type*)input->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", input->functionType(t,u)); + input->mkVar("g", input->functionType(u,v)); + input->mkVar("h", input->functionType(v,t)); + /* x:t; y:u; z:v; */ + input->mkVar("x",t); + input->mkVar("y",u); + input->mkVar("z",v); +} + + /************************** CVC test inputs ********************************/ const string goodCvc4Inputs[] = { @@ -44,9 +66,8 @@ const string goodCvc4Inputs[] = { const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string); -const string cvc4ExprContext = "a,b,c:BOOLEAN;"; -/* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */ +/* The following expressions are valid after setupContext. */ const string goodCvc4Exprs[] = { "a AND b", "a AND b OR c", @@ -71,7 +92,7 @@ const string badCvc4Inputs[] = { const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string); -/* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */ +/* The following expressions are invalid even after setupContext. */ const string badCvc4Exprs[] = { "a AND", // wrong arity "AND(a,b)", // not infix @@ -100,18 +121,7 @@ const string goodSmtInputs[] = { const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string); -/* The parser is just going to read this benchmark and leave its decls - in the context. The SMT exprs below will then be able to refer to them, - even though they're "out of scope." */ -const string smtExprContext = - "(benchmark foo\n" - " :extrasorts (t u v)\n" - " :extrapreds ((a) (b) (c))\n" - " :extrafuns ((f t u) (g u v) (h v t) (x t) (y u) (z v)))\n"; - -/* The following expressions are good in a context where a, b, and c - have been declared as BOOLEAN, t, u, v, are sorts, f, g, h are - functions, and x, y, z are variables. */ +/* The following expressions are valid after setupContext. */ const string goodSmtExprs[] = { "(and a b)", "(or (and a b) c)", @@ -134,7 +144,7 @@ const string badSmtInputs[] = { const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string); -/* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */ +/* The following expressions are invalid even after setupContext. */ const string badSmtExprs[] = { "(and)", // wrong arity "(and a b", // no closing paren @@ -152,61 +162,66 @@ const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); class ParserBlack : public CxxTest::TestSuite { ExprManager *d_exprManager; - void tryGoodInputs(Parser::InputLanguage d_lang, const string goodInputs[], int numInputs) { + void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) { for(int i = 0; i < numInputs; ++i) { try { - // cout << "Testing good input: '" << goodInputs[i] << "'\n"; - // Debug.on("parser"); - istringstream stream(goodInputs[i]); - Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream, "test"); - TS_ASSERT( !smtParser->done() ); +// 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 = smtParser->parseNextCommand())) { + while((cmd = parser->parseNextCommand())) { // cout << "Parsed command: " << (*cmd) << endl; } - TS_ASSERT( smtParser->parseNextCommand() == NULL ); - TS_ASSERT( smtParser->done() ); - delete smtParser; + 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(Parser::InputLanguage d_lang, const string badInputs[], int numInputs) { + void tryBadInputs(InputLanguage d_lang, const string badInputs[], int numInputs) { for(int i = 0; i < numInputs; ++i) { - // cout << "Testing bad input: '" << badInputs[i] << "'\n"; - istringstream stream(badInputs[i]); - Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream, "test"); +// 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(smtParser->parseNextCommand()); + ( while(parser->parseNextCommand()); cout << "\nBad input succeeded:\n" << badInputs[i] << endl;, ParserException ); - delete smtParser; +// Debug.off("parser"); + delete parser; } } - void tryGoodExprs(Parser::InputLanguage d_lang,const string& context, const string goodBooleanExprs[], int numExprs) { + 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]); - Parser* parser = Parser::getNewParser(d_exprManager, d_lang, stream, "test"); +// istringstream stream(context + goodBooleanExprs[i]); + Input* parser = Input::newStringParser(d_exprManager, d_lang, + goodBooleanExprs[i], "test"); TS_ASSERT( !parser->done() ); - Command* cmd = parser->parseNextCommand(); + setupContext(parser); TS_ASSERT( !parser->done() ); - Expr e; - while(e = parser->parseNextExpression()) { - // cout << "Parsed expr: " << e << endl; - } + Expr e = parser->parseNextExpression(); + TS_ASSERT( !e.isNull() ); + e = parser->parseNextExpression(); TS_ASSERT( parser->done() ); TS_ASSERT( e.isNull() ); - delete cmd; delete parser; } catch (Exception& e) { cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl; @@ -216,17 +231,22 @@ class ParserBlack : public CxxTest::TestSuite { } } - void tryBadExprs(Parser::InputLanguage d_lang,const string& context, const string badBooleanExprs[], int numExprs) { + 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]); - Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream, "test"); +// 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 - ( smtParser->parseNextExpression(); + ( parser->parseNextExpression(); cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, ParserException ); - delete smtParser; + delete parser; } //Debug.off("parser"); } @@ -241,34 +261,34 @@ public: } void testGoodCvc4Inputs() { - tryGoodInputs(Parser::LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); + tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); } void testBadCvc4Inputs() { - tryBadInputs(Parser::LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs); + tryBadInputs(LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs); } void testGoodCvc4Exprs() { - tryGoodExprs(Parser::LANG_CVC4,cvc4ExprContext,goodCvc4Exprs,numGoodCvc4Exprs); + tryGoodExprs(LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs); } void testBadCvc4Exprs() { - tryBadExprs(Parser::LANG_CVC4,cvc4ExprContext,badCvc4Exprs,numBadCvc4Exprs); + tryBadExprs(LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs); } void testGoodSmtInputs() { - tryGoodInputs(Parser::LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs); + tryGoodInputs(LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs); } void testBadSmtInputs() { - tryBadInputs(Parser::LANG_SMTLIB,badSmtInputs,numBadSmtInputs); + tryBadInputs(LANG_SMTLIB,badSmtInputs,numBadSmtInputs); } void testGoodSmtExprs() { - tryGoodExprs(Parser::LANG_SMTLIB,smtExprContext,goodSmtExprs,numGoodSmtExprs); + tryGoodExprs(LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs); } void testBadSmtExprs() { - tryBadExprs(Parser::LANG_SMTLIB,smtExprContext,badSmtExprs,numBadSmtExprs); + tryBadExprs(LANG_SMTLIB,badSmtExprs,numBadSmtExprs); } }; |