summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/api/ouroborous.cpp4
-rw-r--r--test/api/smt2_compliance.cpp6
-rw-r--r--test/unit/main/interactive_shell_black.h16
-rw-r--r--test/unit/parser/parser_black.h23
-rw-r--r--test/unit/parser/parser_builder_black.h26
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback