diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/api/ouroborous.cpp | 4 | ||||
-rw-r--r-- | test/api/smt2_compliance.cpp | 6 | ||||
-rw-r--r-- | test/unit/main/interactive_shell_black.h | 16 | ||||
-rw-r--r-- | test/unit/parser/parser_black.h | 23 | ||||
-rw-r--r-- | test/unit/parser/parser_builder_black.h | 26 |
5 files changed, 51 insertions, 24 deletions
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index 5ddc3ec26..5ed240233 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -111,7 +111,9 @@ void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTL int runTest() { std::unique_ptr<api::Solver> solver = std::unique_ptr<api::Solver>(new api::Solver()); - psr = ParserBuilder(solver.get(), "internal-buffer") + std::unique_ptr<parser::SymbolManager> symman( + new parser::SymbolManager(solver.get())); + psr = ParserBuilder(solver.get(), symman.get(), "internal-buffer") .withStringInput(declarations) .withInputLanguage(input::LANG_SMTLIB_V2) .build(); diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index e5781cfaa..7f9035636 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -43,7 +43,6 @@ int main() std::unique_ptr<api::Solver> solver = std::unique_ptr<api::Solver>(new api::Solver(&opts)); - testGetInfo(solver.get(), ":error-behavior"); testGetInfo(solver.get(), ":name"); testGetInfo(solver.get(), ":authors"); @@ -61,7 +60,10 @@ int main() void testGetInfo(api::Solver* solver, const char* s) { - ParserBuilder pb(solver, "<internal>", solver->getOptions()); + std::unique_ptr<parser::SymbolManager> symman( + new parser::SymbolManager(solver)); + + ParserBuilder pb(solver, symman.get(), "<internal>", solver->getOptions()); Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build(); assert(p != NULL); Command* c = p->nextCommand(); diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index 417cfa94d..af6960ff7 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -27,6 +27,7 @@ #include "options/language.h" #include "options/options.h" #include "parser/parser_builder.h" +#include "parser/symbol_manager.h" #include "smt/command.h" using namespace CVC4; @@ -42,7 +43,9 @@ class InteractiveShellBlack : public CxxTest::TestSuite d_options.set(options::in, d_sin); d_options.set(options::out, d_sout); d_options.set(options::inputLanguage, language::input::LANG_CVC4); + d_symman.reset(nullptr); d_solver.reset(new api::Solver(&d_options)); + d_symman.reset(new parser::SymbolManager(d_solver.get())); } void tearDown() override @@ -53,18 +56,18 @@ class InteractiveShellBlack : public CxxTest::TestSuite void testAssertTrue() { *d_sin << "ASSERT TRUE;\n" << flush; - InteractiveShell shell(d_solver.get()); + InteractiveShell shell(d_solver.get(), d_symman.get()); countCommands( shell, 1, 1 ); } void testQueryFalse() { *d_sin << "QUERY FALSE;\n" << flush; - InteractiveShell shell(d_solver.get()); + InteractiveShell shell(d_solver.get(), d_symman.get()); countCommands( shell, 1, 1 ); } void testDefUse() { - InteractiveShell shell(d_solver.get()); + InteractiveShell shell(d_solver.get(), d_symman.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... */ @@ -72,7 +75,7 @@ class InteractiveShellBlack : public CxxTest::TestSuite } void testDefUse2() { - InteractiveShell shell(d_solver.get()); + InteractiveShell shell(d_solver.get(), d_symman.get()); /* readCommand may return a sequence, see above. */ *d_sin << "x : REAL;\n" << flush; Command* tmp = shell.readCommand(); @@ -82,20 +85,21 @@ class InteractiveShellBlack : public CxxTest::TestSuite } void testEmptyLine() { - InteractiveShell shell(d_solver.get()); + InteractiveShell shell(d_solver.get(), d_symman.get()); *d_sin << flush; countCommands(shell,0,0); } void testRepeatedEmptyLines() { *d_sin << "\n\n\n"; - InteractiveShell shell(d_solver.get()); + InteractiveShell shell(d_solver.get(), d_symman.get()); /* Might return up to four empties, might return nothing */ countCommands( shell, 0, 3 ); } private: std::unique_ptr<api::Solver> d_solver; + std::unique_ptr<parser::SymbolManager> d_symman; Options d_options; stringstream* d_sin; stringstream* d_sout; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index dfe2ee138..2bdd5c950 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -29,9 +29,9 @@ #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/smt2/smt2.h" +#include "parser/symbol_manager.h" #include "smt/command.h" - using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::language::input; @@ -70,7 +70,8 @@ class ParserBlack // Debug.on("parser-extra"); // cerr << "Testing good input: <<" << goodInput << ">>" << endl; // istringstream stream(goodInputs[i]); - Parser* parser = ParserBuilder(d_solver.get(), "test") + d_symman.reset(new parser::SymbolManager(d_solver.get())); + Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(goodInput) .withOptions(d_options) .withInputLanguage(d_lang) @@ -101,7 +102,8 @@ class ParserBlack // cerr << "Testing bad input: '" << badInput << "'\n"; // Debug.on("parser"); - Parser* parser = ParserBuilder(d_solver.get(), "test") + d_symman.reset(new parser::SymbolManager(d_solver.get())); + Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(badInput) .withOptions(d_options) .withInputLanguage(d_lang) @@ -132,7 +134,8 @@ class ParserBlack // Debug.on("parser"); // istringstream stream(context + goodBooleanExprs[i]); - Parser* parser = ParserBuilder(d_solver.get(), "test") + d_symman.reset(new parser::SymbolManager(d_solver.get())); + Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(goodExpr) .withOptions(d_options) .withInputLanguage(d_lang) @@ -179,7 +182,8 @@ class ParserBlack // Debug.on("parser-extra"); // cout << "Testing bad expr: '" << badExpr << "'\n"; - Parser* parser = ParserBuilder(d_solver.get(), "test") + d_symman.reset(new parser::SymbolManager(d_solver.get())); + Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(badExpr) .withOptions(d_options) .withInputLanguage(d_lang) @@ -206,14 +210,21 @@ class ParserBlack void setUp() { d_options.set(options::parseOnly, true); + // ensure the old symbol manager is deleted + d_symman.reset(nullptr); d_solver.reset(new api::Solver(&d_options)); } - void tearDown() { d_solver.reset(nullptr); } + void tearDown() + { + d_symman.reset(nullptr); + d_solver.reset(nullptr); + } private: InputLanguage d_lang; std::unique_ptr<api::Solver> d_solver; + std::unique_ptr<parser::SymbolManager> d_symman; }; /* class ParserBlack */ diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index 003424397..b8ec96836 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -28,6 +28,7 @@ #include "options/language.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "parser/symbol_manager.h" using namespace CVC4; using namespace CVC4::parser; @@ -37,7 +38,13 @@ using namespace std; class ParserBuilderBlack : public CxxTest::TestSuite { public: - void setUp() override { d_solver.reset(new api::Solver()); } + void setUp() override + { + // ensure the old symbol manager is deleted + d_symman.reset(nullptr); + d_solver.reset(new api::Solver()); + d_symman.reset(new parser::SymbolManager(d_solver.get())); + } void tearDown() override {} @@ -45,8 +52,8 @@ class ParserBuilderBlack : public CxxTest::TestSuite { char *filename = mkTemp(); - checkEmptyInput( - ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4)); + checkEmptyInput(ParserBuilder(d_solver.get(), d_symman.get(), filename) + .withInputLanguage(LANG_CVC4)); remove(filename); free(filename); @@ -59,35 +66,35 @@ class ParserBuilderBlack : public CxxTest::TestSuite fs << "TRUE" << std::endl; fs.close(); - checkTrueInput( - ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4)); + checkTrueInput(ParserBuilder(d_solver.get(), d_symman.get(), filename) + .withInputLanguage(LANG_CVC4)); remove(filename); free(filename); } void testEmptyStringInput() { - checkEmptyInput(ParserBuilder(d_solver.get(), "foo") + checkEmptyInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo") .withInputLanguage(LANG_CVC4) .withStringInput("")); } void testTrueStringInput() { - checkTrueInput(ParserBuilder(d_solver.get(), "foo") + checkTrueInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo") .withInputLanguage(LANG_CVC4) .withStringInput("TRUE")); } void testEmptyStreamInput() { stringstream ss( "", ios_base::in ); - checkEmptyInput(ParserBuilder(d_solver.get(), "foo") + checkEmptyInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo") .withInputLanguage(LANG_CVC4) .withStreamInput(ss)); } void testTrueStreamInput() { stringstream ss( "TRUE", ios_base::in ); - checkTrueInput(ParserBuilder(d_solver.get(), "foo") + checkTrueInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo") .withInputLanguage(LANG_CVC4) .withStreamInput(ss)); } @@ -127,5 +134,6 @@ class ParserBuilderBlack : public CxxTest::TestSuite } std::unique_ptr<api::Solver> d_solver; + std::unique_ptr<parser::SymbolManager> d_symman; }; // class ParserBuilderBlack |