summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/api/ouroborous.cpp13
-rw-r--r--test/api/smt2_compliance.cpp10
-rw-r--r--test/unit/parser/parser_black.cpp23
-rw-r--r--test/unit/parser/parser_builder_black.cpp35
4 files changed, 44 insertions, 37 deletions
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index c226da13b..721f25db8 100644
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -31,6 +31,7 @@
#include "api/cpp/cvc5.h"
#include "options/set_language.h"
+#include "parser/input_parser.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt/command.h"
@@ -104,19 +105,19 @@ std::string parse(std::string instr,
SymbolManager symman(&solver);
std::unique_ptr<Parser> parser(
ParserBuilder(&solver, &symman).withInputLanguage(ilang).build());
- parser->setInput(
- Input::newStringInput(ilang, declarations, "internal-buffer"));
+ std::unique_ptr<InputParser> inputParser =
+ parser->parseString("internal-buffer", declarations);
// we don't need to execute the commands, but we DO need to parse them to
// get the declarations
- while (Command* c = parser->nextCommand())
+ while (Command* c = inputParser->nextCommand())
{
delete c;
}
assert(parser->done()); // parser should be done
- parser->setInput(Input::newStringInput(ilang, instr, "internal-buffer"));
- api::Term e = parser->nextExpression();
+ inputParser = parser->parseString("internal-buffer", instr);
+ api::Term e = inputParser->nextExpression();
std::string s = e.toString();
- assert(parser->nextExpression().isNull()); // next expr should be null
+ assert(inputParser->nextExpression().isNull()); // next expr should be null
return s;
}
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index 04b366cf0..90e13ef2d 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -20,6 +20,7 @@
#include "api/cpp/cvc5.h"
#include "options/options.h"
#include "options/set_language.h"
+#include "parser/input_parser.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt/command.h"
@@ -62,16 +63,15 @@ void testGetInfo(api::Solver* solver, const char* s)
std::unique_ptr<Parser> p(
ParserBuilder(solver, symman.get(), solver->getOptions()).build());
- p->setInput(Input::newStringInput(language::input::LANG_SMTLIB_V2,
- string("(get-info ") + s + ")",
- "<internal>"));
+ std::unique_ptr<InputParser> inputParser =
+ p->parseString("<internal>", string("(get-info ") + s + ")");
assert(p != NULL);
- Command* c = p->nextCommand();
+ Command* c = inputParser->nextCommand();
assert(c != NULL);
cout << c << endl;
stringstream ss;
c->invoke(solver, symman.get(), ss);
- assert(p->nextCommand() == NULL);
+ assert(inputParser->nextCommand() == NULL);
delete c;
cout << ss.str() << endl << endl;
}
diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
index 78a67f6d0..a0cd0499e 100644
--- a/test/unit/parser/parser_black.cpp
+++ b/test/unit/parser/parser_black.cpp
@@ -21,6 +21,7 @@
#include "options/base_options.h"
#include "options/language.h"
#include "options/options.h"
+#include "parser/input_parser.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "parser/smt2/smt2.h"
@@ -90,10 +91,11 @@ class TestParserBlackParser : public TestInternal
.withOptions(d_options)
.withInputLanguage(d_lang)
.build());
- parser->setInput(Input::newStringInput(d_lang, goodInput, "test"));
+ std::unique_ptr<InputParser> inputParser =
+ parser->parseString("test", goodInput);
ASSERT_FALSE(parser->done());
Command* cmd;
- while ((cmd = parser->nextCommand()) != NULL)
+ while ((cmd = inputParser->nextCommand()) != NULL)
{
Debug("parser") << "Parsed command: " << (*cmd) << std::endl;
delete cmd;
@@ -110,11 +112,12 @@ class TestParserBlackParser : public TestInternal
.withInputLanguage(d_lang)
.withStrictMode(strictMode)
.build());
- parser->setInput(Input::newStringInput(d_lang, badInput, "test"));
+ std::unique_ptr<InputParser> inputParser =
+ parser->parseString("test", badInput);
ASSERT_THROW(
{
Command* cmd;
- while ((cmd = parser->nextCommand()) != NULL)
+ while ((cmd = inputParser->nextCommand()) != NULL)
{
Debug("parser") << "Parsed command: " << (*cmd) << std::endl;
delete cmd;
@@ -131,7 +134,8 @@ class TestParserBlackParser : public TestInternal
.withOptions(d_options)
.withInputLanguage(d_lang)
.build());
- parser->setInput(Input::newStringInput(d_lang, goodExpr, "test"));
+ std::unique_ptr<InputParser> inputParser =
+ parser->parseString("test", goodExpr);
if (d_lang == LANG_SMTLIB_V2)
{
/* Use QF_LIA to make multiplication ("*") available */
@@ -142,9 +146,9 @@ class TestParserBlackParser : public TestInternal
ASSERT_FALSE(parser->done());
setupContext(*parser);
ASSERT_FALSE(parser->done());
- api::Term e = parser->nextExpression();
+ api::Term e = inputParser->nextExpression();
ASSERT_FALSE(e.isNull());
- e = parser->nextExpression();
+ e = inputParser->nextExpression();
ASSERT_TRUE(parser->done());
ASSERT_TRUE(e.isNull());
}
@@ -166,10 +170,11 @@ class TestParserBlackParser : public TestInternal
.withInputLanguage(d_lang)
.withStrictMode(strictMode)
.build());
- parser->setInput(Input::newStringInput(d_lang, badExpr, "test"));
+ std::unique_ptr<InputParser> inputParser =
+ parser->parseString("test", badExpr);
setupContext(*parser);
ASSERT_FALSE(parser->done());
- ASSERT_THROW(api::Term e = parser->nextExpression();
+ ASSERT_THROW(api::Term e = inputParser->nextExpression();
std::cout << std::endl
<< "Bad expr succeeded." << std::endl
<< "Input: <<" << badExpr << ">>" << std::endl
diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp
index fa532f6b6..f8d29efbe 100644
--- a/test/unit/parser/parser_builder_black.cpp
+++ b/test/unit/parser/parser_builder_black.cpp
@@ -24,6 +24,7 @@
#include "api/cpp/cvc5.h"
#include "expr/symbol_manager.h"
#include "options/language.h"
+#include "parser/input_parser.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "test_api.h"
@@ -40,18 +41,18 @@ class TestParseBlackParserBuilder : public TestApi
protected:
void SetUp() override { d_symman.reset(new SymbolManager(&d_solver)); }
- void checkEmptyInput(Parser* parser)
+ void checkEmptyInput(InputParser* inputParser)
{
- api::Term e = parser->nextExpression();
+ api::Term e = inputParser->nextExpression();
ASSERT_TRUE(e.isNull());
}
- void checkTrueInput(Parser* parser)
+ void checkTrueInput(InputParser* inputParser)
{
- api::Term e = parser->nextExpression();
+ api::Term e = inputParser->nextExpression();
ASSERT_EQ(e, d_solver.mkTrue());
- e = parser->nextExpression();
+ e = inputParser->nextExpression();
ASSERT_TRUE(e.isNull());
}
@@ -74,8 +75,8 @@ TEST_F(TestParseBlackParserBuilder, empty_file_input)
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
.withInputLanguage(LANG_CVC)
.build());
- parser->setInput(Input::newFileInput(LANG_CVC, filename, false));
- checkEmptyInput(parser.get());
+ std::unique_ptr<InputParser> inputParser = parser->parseFile(filename, false);
+ checkEmptyInput(inputParser.get());
remove(filename);
free(filename);
@@ -92,8 +93,8 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input)
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
.withInputLanguage(LANG_CVC)
.build());
- parser->setInput(Input::newFileInput(LANG_CVC, filename, false));
- checkTrueInput(parser.get());
+ std::unique_ptr<InputParser> inputParser = parser->parseFile(filename, false);
+ checkTrueInput(inputParser.get());
remove(filename);
free(filename);
@@ -104,8 +105,8 @@ TEST_F(TestParseBlackParserBuilder, empty_string_input)
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
.withInputLanguage(LANG_CVC)
.build());
- parser->setInput(Input::newStringInput(LANG_CVC, "", "foo"));
- checkEmptyInput(parser.get());
+ std::unique_ptr<InputParser> inputParser = parser->parseString("foo", "");
+ checkEmptyInput(inputParser.get());
}
TEST_F(TestParseBlackParserBuilder, true_string_input)
@@ -113,8 +114,8 @@ TEST_F(TestParseBlackParserBuilder, true_string_input)
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
.withInputLanguage(LANG_CVC)
.build());
- parser->setInput(Input::newStringInput(LANG_CVC, "TRUE", "foo"));
- checkTrueInput(parser.get());
+ std::unique_ptr<InputParser> inputParser = parser->parseString("foo", "TRUE");
+ checkTrueInput(inputParser.get());
}
TEST_F(TestParseBlackParserBuilder, empty_stream_input)
@@ -123,8 +124,8 @@ TEST_F(TestParseBlackParserBuilder, empty_stream_input)
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
.withInputLanguage(LANG_CVC)
.build());
- parser->setInput(Input::newStreamInput(LANG_CVC, ss, "foo"));
- checkEmptyInput(parser.get());
+ std::unique_ptr<InputParser> inputParser = parser->parseStream("foo", ss);
+ checkEmptyInput(inputParser.get());
}
TEST_F(TestParseBlackParserBuilder, true_stream_input)
@@ -133,8 +134,8 @@ TEST_F(TestParseBlackParserBuilder, true_stream_input)
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
.withInputLanguage(LANG_CVC)
.build());
- parser->setInput(Input::newStreamInput(LANG_CVC, ss, "foo"));
- checkTrueInput(parser.get());
+ std::unique_ptr<InputParser> inputParser = parser->parseStream("foo", ss);
+ checkTrueInput(inputParser.get());
}
} // namespace test
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback