From 91d85704313de6be9fd382833f5cedd39e24a6fa Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 8 Aug 2018 19:21:47 -0700 Subject: Plug solver API object into parser. (#2240) --- test/system/ouroborous.cpp | 15 ++- test/system/smt2_compliance.cpp | 43 +++--- test/unit/main/interactive_shell_black.h | 77 +++++------ test/unit/parser/parser_black.h | 217 ++++++++++++++++--------------- test/unit/parser/parser_builder_black.h | 127 ++++++++---------- 5 files changed, 241 insertions(+), 238 deletions(-) (limited to 'test') diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index 1df405a17..a135e6c6c 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -2,7 +2,7 @@ /*! \file ouroborous.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Tim King, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -28,6 +28,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr.h" #include "expr/expr_iomanip.h" #include "options/set_language.h" @@ -108,12 +109,12 @@ void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTL int runTest() { - ExprManager em; - psr = - ParserBuilder(&em, "internal-buffer") - .withStringInput(declarations) - .withInputLanguage(input::LANG_SMTLIB_V2) - .build(); + std::unique_ptr solver = + std::unique_ptr(new api::Solver()); + psr = ParserBuilder(solver.get(), "internal-buffer") + .withStringInput(declarations) + .withInputLanguage(input::LANG_SMTLIB_V2) + .build(); // we don't need to execute them, but we DO need to parse them to // get the declarations diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp index 134185dc4..8a14094d3 100644 --- a/test/system/smt2_compliance.cpp +++ b/test/system/smt2_compliance.cpp @@ -2,7 +2,7 @@ /*! \file smt2_compliance.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Aina Niemetz, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -18,6 +18,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr_manager.h" #include "options/options.h" #include "options/set_language.h" @@ -30,43 +31,45 @@ using namespace CVC4; using namespace CVC4::parser; using namespace std; -void testGetInfo(SmtEngine& smt, const char* s); +void testGetInfo(api::Solver* solver, const char* s); -int main() { +int main() +{ Options opts; opts.setInputLanguage(language::input::LANG_SMTLIB_V2); opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); - ExprManager em(opts); - SmtEngine smt(&em); + std::unique_ptr solver = + std::unique_ptr(new api::Solver(&opts)); - testGetInfo(smt, ":error-behavior"); - testGetInfo(smt, ":name"); - testGetInfo(smt, ":authors"); - testGetInfo(smt, ":version"); - testGetInfo(smt, ":status"); - testGetInfo(smt, ":reason-unknown"); - testGetInfo(smt, ":arbitrary-undefined-keyword"); - testGetInfo(smt, ":56");// legal - testGetInfo(smt, ":<=");// legal - testGetInfo(smt, ":->");// legal - testGetInfo(smt, ":all-statistics"); + testGetInfo(solver.get(), ":error-behavior"); + testGetInfo(solver.get(), ":name"); + testGetInfo(solver.get(), ":authors"); + testGetInfo(solver.get(), ":version"); + testGetInfo(solver.get(), ":status"); + testGetInfo(solver.get(), ":reason-unknown"); + testGetInfo(solver.get(), ":arbitrary-undefined-keyword"); + testGetInfo(solver.get(), ":56"); // legal + testGetInfo(solver.get(), ":<="); // legal + testGetInfo(solver.get(), ":->"); // legal + testGetInfo(solver.get(), ":all-statistics"); return 0; } -void testGetInfo(SmtEngine& smt, const char* s) { - ParserBuilder pb(smt.getExprManager(), "", - smt.getExprManager()->getOptions()); +void testGetInfo(api::Solver* solver, const char* s) +{ + ParserBuilder pb( + solver, "", solver->getExprManager()->getOptions()); Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build(); assert(p != NULL); Command* c = p->nextCommand(); assert(c != NULL); cout << c << endl; stringstream ss; - c->invoke(&smt, ss); + c->invoke(solver->getSmtEngine(), ss); assert(p->nextCommand() == NULL); delete p; delete c; diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index cf68b5465..44b3660c9 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -2,7 +2,7 @@ /*! \file interactive_shell_black.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King + ** Christopher L. Conway, Aina Niemetz, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -20,6 +20,7 @@ #include #include +#include "api/cvc4cpp.h" #include "expr/expr_manager.h" #include "main/interactive_shell.h" #include "options/base_options.h" @@ -31,64 +32,38 @@ using namespace CVC4; using namespace std; -class InteractiveShellBlack : public CxxTest::TestSuite { -private: - ExprManager* d_exprManager; - Options d_options; - stringstream* d_sin; - stringstream* d_sout; - - /** - * Read up to maxCommands+1 from the shell and throw an assertion error if - * it's fewer than minCommands and more than maxCommands. - * Note that an empty string followed by EOF may be returned as an empty - * command, and not NULL (subsequent calls to readCommand() should return - * NULL). E.g., "CHECKSAT;\n" may return two commands: the CHECKSAT, - * followed by an empty command, followed by NULL. - */ - void countCommands(InteractiveShell& shell, - int minCommands, - int maxCommands) { - Command* cmd; - int n = 0; - while( n <= maxCommands && (cmd = shell.readCommand()) != NULL ) { - ++n; - delete cmd; - } - TS_ASSERT( n <= maxCommands ); - TS_ASSERT( n >= minCommands ); - } - +class InteractiveShellBlack : public CxxTest::TestSuite +{ public: - void setUp() { + void setUp() + { d_sin = new stringstream; d_sout = new stringstream; d_options.set(options::in, d_sin); d_options.set(options::out, d_sout); d_options.set(options::inputLanguage, language::input::LANG_CVC4); - d_exprManager = new ExprManager(d_options); + d_solver.reset(new api::Solver(&d_options)); } void tearDown() { - delete d_exprManager; delete d_sin; delete d_sout; } void testAssertTrue() { *d_sin << "ASSERT TRUE;\n" << flush; - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.get()); countCommands( shell, 1, 1 ); } void testQueryFalse() { *d_sin << "QUERY FALSE;\n" << flush; - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.get()); countCommands( shell, 1, 1 ); } void testDefUse() { - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.get()); *d_sin << "x : REAL; ASSERT x > 0;\n" << flush; /* readCommand may return a sequence, so we can't say for sure whether it will return 1 or 2... */ @@ -96,7 +71,7 @@ private: } void testDefUse2() { - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.get()); /* readCommand may return a sequence, see above. */ *d_sin << "x : REAL;\n" << flush; Command* tmp = shell.readCommand(); @@ -106,16 +81,42 @@ private: } void testEmptyLine() { - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.get()); *d_sin << flush; countCommands(shell,0,0); } void testRepeatedEmptyLines() { *d_sin << "\n\n\n"; - InteractiveShell shell(*d_exprManager); + InteractiveShell shell(d_solver.get()); /* Might return up to four empties, might return nothing */ countCommands( shell, 0, 3 ); } + private: + std::unique_ptr d_solver; + Options d_options; + stringstream* d_sin; + stringstream* d_sout; + + /** + * Read up to maxCommands+1 from the shell and throw an assertion error if + * it's fewer than minCommands and more than maxCommands. Note that an empty + * string followed by EOF may be returned as an empty command, and not NULL + * (subsequent calls to readCommand() should return NULL). E.g., "CHECKSAT;\n" + * may return two commands: the CHECKSAT, followed by an empty command, + * followed by NULL. + */ + void countCommands(InteractiveShell& shell, int minCommands, int maxCommands) + { + Command* cmd; + int n = 0; + while (n <= maxCommands && (cmd = shell.readCommand()) != NULL) + { + ++n; + delete cmd; + } + TS_ASSERT(n <= maxCommands); + TS_ASSERT(n >= minCommands); + } }; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index b3c36e2c4..7b52e0662 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -2,7 +2,7 @@ /*! \file parser_black.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Morgan Deters, Tim King + ** Christopher L. Conway, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -19,6 +19,7 @@ #include #include +#include "api/cvc4cpp.h" #include "base/output.h" #include "expr/expr.h" #include "expr/expr_manager.h" @@ -36,69 +37,71 @@ using namespace CVC4::parser; using namespace CVC4::language::input; using namespace std; -class ParserBlack { - InputLanguage d_lang; - ExprManager *d_exprManager; - -protected: +class ParserBlack +{ + protected: Options d_options; /* Set up declaration context for expr inputs */ virtual void setupContext(Parser& parser) { /* a, b, c: BOOLEAN */ - parser.mkVar("a",d_exprManager->booleanType()); - parser.mkVar("b",d_exprManager->booleanType()); - parser.mkVar("c",d_exprManager->booleanType()); + parser.mkVar("a", d_solver->getExprManager()->booleanType()); + parser.mkVar("b", d_solver->getExprManager()->booleanType()); + parser.mkVar("c", d_solver->getExprManager()->booleanType()); /* t, u, v: TYPE */ Type t = parser.mkSort("t"); Type u = parser.mkSort("u"); Type v = parser.mkSort("v"); /* f : t->u; g: u->v; h: v->t; */ - parser.mkVar("f", d_exprManager->mkFunctionType(t,u)); - parser.mkVar("g", d_exprManager->mkFunctionType(u,v)); - parser.mkVar("h", d_exprManager->mkFunctionType(v,t)); + parser.mkVar("f", d_solver->getExprManager()->mkFunctionType(t, u)); + parser.mkVar("g", d_solver->getExprManager()->mkFunctionType(u, v)); + parser.mkVar("h", d_solver->getExprManager()->mkFunctionType(v, t)); /* x:t; y:u; z:v; */ parser.mkVar("x",t); parser.mkVar("y",u); parser.mkVar("z",v); } - void tryGoodInput(const string goodInput) { - try { -// Debug.on("parser"); -// Debug.on("parser-extra"); -// cerr << "Testing good input: <<" << goodInput << ">>" << endl; -// istringstream stream(goodInputs[i]); - Parser *parser = - ParserBuilder(d_exprManager,"test") - .withStringInput(goodInput) - .withOptions(d_options) - .withInputLanguage(d_lang) - .build(); - TS_ASSERT( !parser->done() ); - Command* cmd; - while((cmd = parser->nextCommand()) != NULL) { - Debug("parser") << "Parsed command: " << (*cmd) << endl; - delete cmd; - } - - TS_ASSERT( parser->done() ); - delete parser; -// Debug.off("parser"); -// Debug.off("parser-extra"); - } catch (Exception& e) { - cout << "\nGood input failed:\n" << goodInput << endl - << e << endl; -// Debug.off("parser"); - throw; + void tryGoodInput(const string goodInput) + { + try + { + // Debug.on("parser"); + // Debug.on("parser-extra"); + // cerr << "Testing good input: <<" << goodInput << ">>" << endl; + // istringstream stream(goodInputs[i]); + Parser* parser = ParserBuilder(d_solver.get(), "test") + .withStringInput(goodInput) + .withOptions(d_options) + .withInputLanguage(d_lang) + .build(); + TS_ASSERT(!parser->done()); + Command* cmd; + while ((cmd = parser->nextCommand()) != NULL) + { + Debug("parser") << "Parsed command: " << (*cmd) << endl; + delete cmd; } + + TS_ASSERT(parser->done()); + delete parser; + // Debug.off("parser"); + // Debug.off("parser-extra"); + } + catch (Exception& e) + { + cout << "\nGood input failed:\n" << goodInput << endl << e << endl; + // Debug.off("parser"); + throw; + } } - void tryBadInput(const string badInput, bool strictMode = false) { -// cerr << "Testing bad input: '" << badInput << "'\n"; -// Debug.on("parser"); + void tryBadInput(const string badInput, bool strictMode = false) + { + // cerr << "Testing bad input: '" << badInput << "'\n"; + // Debug.on("parser"); - Parser* parser = ParserBuilder(d_exprManager, "test") + Parser* parser = ParserBuilder(d_solver.get(), "test") .withStringInput(badInput) .withOptions(d_options) .withInputLanguage(d_lang) @@ -107,7 +110,8 @@ protected: TS_ASSERT_THROWS( { Command* cmd; - while ((cmd = parser->nextCommand()) != NULL) { + while ((cmd = parser->nextCommand()) != NULL) + { Debug("parser") << "Parsed command: " << (*cmd) << endl; delete cmd; } @@ -118,37 +122,40 @@ protected: delete parser; } - void tryGoodExpr(const string goodExpr) { -// Debug.on("parser"); -// Debug.on("parser-extra"); - try { -// cerr << "Testing good expr: '" << goodExpr << "'\n"; - // Debug.on("parser"); -// istringstream stream(context + goodBooleanExprs[i]); - - Parser *parser = - ParserBuilder(d_exprManager,"test") - .withStringInput(goodExpr) - .withOptions(d_options) - .withInputLanguage(d_lang) - .build(); - - TS_ASSERT( !parser->done() ); - setupContext(*parser); - TS_ASSERT( !parser->done() ); - Expr e = parser->nextExpression(); - TS_ASSERT( !e.isNull() ); - e = parser->nextExpression(); - TS_ASSERT( parser->done() ); - TS_ASSERT( e.isNull() ); - delete parser; - } catch (Exception& e) { - cout << endl - << "Good expr failed." << endl - << "Input: <<" << goodExpr << ">>" << endl - << "Output: <<" << e << ">>" << endl; - throw; - } + void tryGoodExpr(const string goodExpr) + { + // Debug.on("parser"); + // Debug.on("parser-extra"); + try + { + // cerr << "Testing good expr: '" << goodExpr << "'\n"; + // Debug.on("parser"); + // istringstream stream(context + goodBooleanExprs[i]); + + Parser* parser = ParserBuilder(d_solver.get(), "test") + .withStringInput(goodExpr) + .withOptions(d_options) + .withInputLanguage(d_lang) + .build(); + + TS_ASSERT(!parser->done()); + setupContext(*parser); + TS_ASSERT(!parser->done()); + Expr e = parser->nextExpression(); + TS_ASSERT(!e.isNull()); + e = parser->nextExpression(); + TS_ASSERT(parser->done()); + TS_ASSERT(e.isNull()); + delete parser; + } + catch (Exception& e) + { + cout << endl + << "Good expr failed." << endl + << "Input: <<" << goodExpr << ">>" << endl + << "Output: <<" << e << ">>" << endl; + throw; + } } /* NOTE: The check implemented here may fail if a bad expression @@ -159,44 +166,48 @@ protected: * input was consumed here, so just be careful to avoid valid * prefixes in tests. */ - void tryBadExpr(const string badExpr, bool strictMode = false) { -// Debug.on("parser"); -// Debug.on("parser-extra"); -// cout << "Testing bad expr: '" << badExpr << "'\n"; - - Parser *parser = - ParserBuilder(d_exprManager,"test") - .withStringInput(badExpr) - .withOptions(d_options) - .withInputLanguage(d_lang) - .withStrictMode(strictMode) - .build(); - setupContext(*parser); - TS_ASSERT( !parser->done() ); - TS_ASSERT_THROWS - ( Expr e = parser->nextExpression(); - cout << endl - << "Bad expr succeeded." << endl - << "Input: <<" << badExpr << ">>" << endl - << "Output: <<" << e << ">>" << endl;, - const ParserException& ); - delete parser; -// Debug.off("parser"); + void tryBadExpr(const string badExpr, bool strictMode = false) + { + // Debug.on("parser"); + // Debug.on("parser-extra"); + // cout << "Testing bad expr: '" << badExpr << "'\n"; + + Parser* parser = ParserBuilder(d_solver.get(), "test") + .withStringInput(badExpr) + .withOptions(d_options) + .withInputLanguage(d_lang) + .withStrictMode(strictMode) + .build(); + setupContext(*parser); + TS_ASSERT(!parser->done()); + TS_ASSERT_THROWS(Expr e = parser->nextExpression(); + cout << endl + << "Bad expr succeeded." << endl + << "Input: <<" << badExpr << ">>" << endl + << "Output: <<" << e << ">>" << endl; + , const ParserException&); + delete parser; + // Debug.off("parser"); } ParserBlack(InputLanguage lang) : d_lang(lang) { } - void setUp() { - d_exprManager = new ExprManager; + void setUp() + { d_options.set(options::parseOnly, true); + d_solver.reset(new api::Solver(&d_options)); } void tearDown() { - delete d_exprManager; } -};/* class ParserBlack */ + + private: + InputLanguage d_lang; + std::unique_ptr d_solver; + +}; /* class ParserBlack */ class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack { typedef ParserBlack super; diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index 066c45fe1..45baf177f 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -2,7 +2,7 @@ /*! \file parser_builder_black.h ** \verbatim ** Top contributors (to current version): - ** Christopher L. Conway, Tim King, Morgan Deters + ** Christopher L. Conway, Aina Niemetz, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -24,6 +24,7 @@ #include #include +#include "api/cvc4cpp.h" #include "options/language.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -34,57 +35,19 @@ using namespace CVC4::parser; using namespace CVC4::language::input; using namespace std; -class ParserBuilderBlack : public CxxTest::TestSuite { +class ParserBuilderBlack : public CxxTest::TestSuite +{ + public: + void setUp() { d_solver.reset(new api::Solver()); } - ExprManager *d_exprManager; + void tearDown() {} - void checkEmptyInput(ParserBuilder& builder) { - Parser *parser = builder.build(); - TS_ASSERT( parser != NULL ); - - Expr e = parser->nextExpression(); - TS_ASSERT( e.isNull() ); - - delete parser; - } - - void checkTrueInput(ParserBuilder& builder) { - Parser *parser = builder.build(); - TS_ASSERT( parser != NULL ); - - Expr e = parser->nextExpression(); - TS_ASSERT_EQUALS( e, d_exprManager->mkConst(true) ); - - e = parser->nextExpression(); - TS_ASSERT( e.isNull() ); - delete parser; - } - - char* mkTemp() { - char *filename = strdup("/tmp/testinput.XXXXXX"); - int fd = mkstemp(filename); - TS_ASSERT( fd != -1 ); - close(fd); - return filename; - } - -public: - - void setUp() { - d_exprManager = new ExprManager; - } - - void tearDown() { - delete d_exprManager; - } - - void testEmptyFileInput() { + void testEmptyFileInput() + { char *filename = mkTemp(); checkEmptyInput( - ParserBuilder(d_exprManager,filename) - .withInputLanguage(LANG_CVC4) - ); + ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4)); remove(filename); free(filename); @@ -98,48 +61,72 @@ public: fs.close(); checkTrueInput( - ParserBuilder(d_exprManager,filename) - .withInputLanguage(LANG_CVC4) - ); + ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4)); remove(filename); free(filename); } void testEmptyStringInput() { - checkEmptyInput( - ParserBuilder(d_exprManager,"foo") - .withInputLanguage(LANG_CVC4) - .withStringInput("") - ); + checkEmptyInput(ParserBuilder(d_solver.get(), "foo") + .withInputLanguage(LANG_CVC4) + .withStringInput("")); } void testTrueStringInput() { - checkTrueInput( - ParserBuilder(d_exprManager,"foo") - .withInputLanguage(LANG_CVC4) - .withStringInput("TRUE") - ); + checkTrueInput(ParserBuilder(d_solver.get(), "foo") + .withInputLanguage(LANG_CVC4) + .withStringInput("TRUE")); } void testEmptyStreamInput() { stringstream ss( "", ios_base::in ); - checkEmptyInput( - ParserBuilder(d_exprManager,"foo") - .withInputLanguage(LANG_CVC4) - .withStreamInput(ss) - ); + checkEmptyInput(ParserBuilder(d_solver.get(), "foo") + .withInputLanguage(LANG_CVC4) + .withStreamInput(ss)); } void testTrueStreamInput() { stringstream ss( "TRUE", ios_base::in ); - checkTrueInput( - ParserBuilder(d_exprManager,"foo") - .withInputLanguage(LANG_CVC4) - .withStreamInput(ss) - ); + checkTrueInput(ParserBuilder(d_solver.get(), "foo") + .withInputLanguage(LANG_CVC4) + .withStreamInput(ss)); } + private: + void checkEmptyInput(ParserBuilder &builder) + { + Parser *parser = builder.build(); + TS_ASSERT(parser != NULL); + + Expr e = parser->nextExpression(); + TS_ASSERT(e.isNull()); + + delete parser; + } + + void checkTrueInput(ParserBuilder &builder) + { + Parser *parser = builder.build(); + TS_ASSERT(parser != NULL); + + Expr e = parser->nextExpression(); + TS_ASSERT_EQUALS(e, d_solver->getExprManager()->mkConst(true)); + + e = parser->nextExpression(); + TS_ASSERT(e.isNull()); + delete parser; + } + + char *mkTemp() + { + char *filename = strdup("/tmp/testinput.XXXXXX"); + int fd = mkstemp(filename); + TS_ASSERT(fd != -1); + close(fd); + return filename; + } + std::unique_ptr d_solver; }; // class ParserBuilderBlack -- cgit v1.2.3