ParserBuilder parserBuilder(pExecutor->getSolver(),
pExecutor->getSymbolManager(),
- filename,
opts);
-
+ std::unique_ptr<Parser> parser(parserBuilder.build());
if( inputFromStdin ) {
- parserBuilder.withStreamInput(cin);
+ parser->setInput(
+ Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+ }
+ else
+ {
+ parser->setInput(Input::newFileInput(
+ opts.getInputLanguage(), filename, opts.getMemoryMap()));
}
vector< vector<Command*> > allCommands;
allCommands.push_back(vector<Command*>());
- std::unique_ptr<Parser> parser(parserBuilder.build());
int needReset = 0;
// true if one of the commands was interrupted
bool interrupted = false;
ParserBuilder parserBuilder(pExecutor->getSolver(),
pExecutor->getSymbolManager(),
- filename,
opts);
-
+ std::unique_ptr<Parser> parser(parserBuilder.build());
if( inputFromStdin ) {
- parserBuilder.withStreamInput(cin);
+ parser->setInput(
+ Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+ }
+ else
+ {
+ parser->setInput(Input::newFileInput(
+ opts.getInputLanguage(), filename, opts.getMemoryMap()));
}
- std::unique_ptr<Parser> parser(parserBuilder.build());
bool interrupted = false;
while (status)
{
d_out(*d_options.getOutConst()),
d_quit(false)
{
- ParserBuilder parserBuilder(solver, sm, INPUT_FILENAME, d_options);
+ ParserBuilder parserBuilder(solver, sm, d_options);
/* Create parser with bogus input. */
- d_parser = parserBuilder.withStringInput("").build();
+ d_parser = parserBuilder.build();
if(d_options.wasSetByUserForceLogicString()) {
LogicInfo tmp(d_options.getForceLogicString());
d_parser->forceLogic(tmp.getLogicString());
protected:
Cvc(api::Solver* solver,
SymbolManager* sm,
- Input* input,
bool strictMode = false,
bool parseOnly = false)
- : Parser(solver, sm, input, strictMode, parseOnly)
+ : Parser(solver, sm, strictMode, parseOnly)
{
}
};
Parser::Parser(api::Solver* solver,
SymbolManager* sm,
- Input* input,
bool strictMode,
bool parseOnly)
- : d_input(input),
- d_symman(sm),
+ : d_symman(sm),
d_symtab(sm->getSymbolTable()),
d_assertionLevel(0),
d_anonymousFunctionCount(0),
- d_done(false),
+ d_done(true),
d_checksEnabled(true),
d_strictMode(strictMode),
d_parseOnly(parseOnly),
d_forcedLogic(),
d_solver(solver)
{
- d_input->setParser(*this);
}
Parser::~Parser() {
delete command;
}
d_commandQueue.clear();
- delete d_input;
}
api::Solver* Parser::getSolver() const { return d_solver; }
#define CVC5__PARSER__PARSER_H
#include <list>
+#include <memory>
#include <set>
#include <string>
private:
/** The input that we're parsing. */
- Input* d_input;
+ std::unique_ptr<Input> d_input;
/**
* Reference to the symbol manager, which manages the symbol table used by
*/
Parser(api::Solver* solver,
SymbolManager* sm,
- Input* input,
bool strictMode = false,
bool parseOnly = false);
api::Solver* getSolver() const;
/** Get the associated input. */
- inline Input* getInput() const {
- return d_input;
- }
+ Input* getInput() const { return d_input.get(); }
/** Get unresolved sorts */
inline std::set<api::Sort>& getUnresolvedSorts() { return d_unresolved; }
/** Deletes and replaces the current parser input. */
void setInput(Input* input) {
- delete d_input;
- d_input = input;
+ d_input.reset(input);
d_input->setParser(*this);
d_done = false;
}
namespace cvc5 {
namespace parser {
-ParserBuilder::ParserBuilder(api::Solver* solver,
- SymbolManager* sm,
- const std::string& filename)
- : d_filename(filename), d_solver(solver), d_symman(sm)
+ParserBuilder::ParserBuilder(api::Solver* solver, SymbolManager* sm)
+ : d_solver(solver), d_symman(sm)
{
- init(solver, sm, filename);
+ init(solver, sm);
}
ParserBuilder::ParserBuilder(api::Solver* solver,
SymbolManager* sm,
- const std::string& filename,
const Options& options)
- : d_filename(filename), d_solver(solver), d_symman(sm)
+ : d_solver(solver), d_symman(sm)
{
- init(solver, sm, filename);
+ init(solver, sm);
withOptions(options);
}
-void ParserBuilder::init(api::Solver* solver,
- SymbolManager* sm,
- const std::string& filename)
+void ParserBuilder::init(api::Solver* solver, SymbolManager* sm)
{
- d_inputType = FILE_INPUT;
d_lang = language::input::LANG_AUTO;
- d_filename = filename;
- d_streamInput = NULL;
d_solver = solver;
d_symman = sm;
d_checksEnabled = true;
d_strictMode = false;
d_canIncludeFile = true;
- d_mmap = false;
d_parseOnly = false;
d_logicIsForced = false;
d_forcedLogic = "";
Parser* ParserBuilder::build()
{
- Input* input = NULL;
- switch( d_inputType ) {
- case FILE_INPUT:
- input = Input::newFileInput(d_lang, d_filename, d_mmap);
- break;
- case STREAM_INPUT:
- Assert(d_streamInput != NULL);
- input = Input::newStreamInput(d_lang, *d_streamInput, d_filename);
- break;
- case STRING_INPUT:
- input = Input::newStringInput(d_lang, d_stringInput, d_filename);
- break;
- }
-
- Assert(input != NULL);
-
Parser* parser = NULL;
switch (d_lang)
{
case language::input::LANG_SYGUS_V2:
- parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly);
+ parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
break;
case language::input::LANG_TPTP:
- parser = new Tptp(d_solver, d_symman, input, d_strictMode, d_parseOnly);
+ parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly);
break;
default:
if (language::isInputLang_smt2(d_lang))
{
- parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly);
+ parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
}
else
{
- parser = new Cvc(d_solver, d_symman, input, d_strictMode, d_parseOnly);
+ parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly);
}
break;
}
return *this;
}
-ParserBuilder& ParserBuilder::withSolver(api::Solver* solver)
-{
- d_solver = solver;
- return *this;
-}
-
-ParserBuilder& ParserBuilder::withFileInput() {
- d_inputType = FILE_INPUT;
- return *this;
-}
-
-ParserBuilder& ParserBuilder::withFilename(const std::string& filename) {
- d_filename = filename;
- return *this;
-}
-
ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) {
d_lang = lang;
return *this;
}
-ParserBuilder& ParserBuilder::withMmap(bool flag) {
- d_mmap = flag;
- return *this;
-}
-
ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
d_parseOnly = flag;
return *this;
ParserBuilder& retval = *this;
retval =
retval.withInputLanguage(options.getInputLanguage())
- .withMmap(options.getMemoryMap())
.withChecks(options.getSemanticChecks())
.withStrictMode(options.getStrictParsing())
.withParseOnly(options.getParseOnly())
return *this;
}
-ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) {
- d_inputType = STREAM_INPUT;
- d_streamInput = &input;
- return *this;
-}
-
-ParserBuilder& ParserBuilder::withStringInput(const std::string& input) {
- d_inputType = STRING_INPUT;
- d_stringInput = input;
- return *this;
-}
-
} // namespace parser
} // namespace cvc5
*/
class CVC5_EXPORT ParserBuilder
{
- enum InputType {
- FILE_INPUT,
- STREAM_INPUT,
- STRING_INPUT
- };
-
- /** The input type. */
- InputType d_inputType;
-
/** The input language */
InputLanguage d_lang;
- /** The file name (may not exist) */
- std::string d_filename;
-
- /** The string input, if any. */
- std::string d_stringInput;
-
- /** The stream input, if any. */
- std::istream* d_streamInput;
-
/** The API Solver object. */
api::Solver* d_solver;
/** Should we allow include-file commands? */
bool d_canIncludeFile;
- /** Should we memory-map a file input? */
- bool d_mmap;
-
/** Are we parsing only? */
bool d_parseOnly;
std::string d_forcedLogic;
/** Initialize this parser builder */
- void init(api::Solver* solver,
- SymbolManager* sm,
- const std::string& filename);
+ void init(api::Solver* solver, SymbolManager* sm);
public:
/** Create a parser builder using the given Solver and filename. */
- ParserBuilder(api::Solver* solver,
- SymbolManager* sm,
- const std::string& filename);
+ ParserBuilder(api::Solver* solver, SymbolManager* sm);
ParserBuilder(api::Solver* solver,
SymbolManager* sm,
- const std::string& filename,
const Options& options);
/** Build the parser, using the current settings. */
/** Should semantic checks be enabled in the parser? (Default: yes) */
ParserBuilder& withChecks(bool flag = true);
- /** Set the Solver to use with the parser. */
- ParserBuilder& withSolver(api::Solver* solver);
-
- /** Set the parser to read a file for its input. (Default) */
- ParserBuilder& withFileInput();
-
- /**
- * Set the filename for use by the parser. If file input is used,
- * this file will be opened and read by the parser. Otherwise, the
- * filename string (possibly a non-existent path) will only be used
- * in error messages.
- */
- ParserBuilder& withFilename(const std::string& filename);
-
/**
* Set the input language to be used by the parser.
*
*/
ParserBuilder& withInputLanguage(InputLanguage lang);
- /**
- * Should the parser memory-map its input? This is only relevant if
- * the parser will have a file input.
- *
- * (Default: no)
- */
- ParserBuilder& withMmap(bool flag = true);
-
/**
* Are we only parsing, or doing something with the resulting
* commands and expressions? This setting affects whether the
*/
ParserBuilder& withIncludeFile(bool flag = true);
- /** Set the parser to use the given stream for its input. */
- ParserBuilder& withStreamInput(std::istream& input);
-
- /** Set the parser to use the given string for its input. */
- ParserBuilder& withStringInput(const std::string& input);
-
/** Set the parser to use the given logic string. */
ParserBuilder& withForcedLogic(const std::string& logic);
}; /* class ParserBuilder */
Smt2::Smt2(api::Solver* solver,
SymbolManager* sm,
- Input* input,
bool strictMode,
bool parseOnly)
- : Parser(solver, sm, input, strictMode, parseOnly),
+ : Parser(solver, sm, strictMode, parseOnly),
d_logicSet(false),
d_seenSetLogic(false)
{
protected:
Smt2(api::Solver* solver,
SymbolManager* sm,
- Input* input,
bool strictMode = false,
bool parseOnly = false);
Tptp::Tptp(api::Solver* solver,
SymbolManager* sm,
- Input* input,
bool strictMode,
bool parseOnly)
- : Parser(solver, sm, input, strictMode, parseOnly),
- d_cnf(false),
- d_fof(false)
+ : Parser(solver, sm, strictMode, parseOnly), d_cnf(false), d_fof(false)
{
addTheory(Tptp::THEORY_CORE);
protected:
Tptp(api::Solver* solver,
SymbolManager* sm,
- Input* input,
bool strictMode = false,
bool parseOnly = false);
solver.setOption("input-language", input_language);
solver.setOption("output-language", output_language);
SymbolManager symman(&solver);
- Parser* parser = ParserBuilder(&solver, &symman, "internal-buffer")
- .withStringInput(declarations)
- .withInputLanguage(ilang)
- .build();
+ std::unique_ptr<Parser> parser(
+ ParserBuilder(&solver, &symman).withInputLanguage(ilang).build());
+ parser->setInput(
+ Input::newStringInput(ilang, declarations, "internal-buffer"));
// we don't need to execute the commands, but we DO need to parse them to
// get the declarations
while (Command* c = parser->nextCommand())
api::Term e = parser->nextExpression();
std::string s = e.toString();
assert(parser->nextExpression().isNull()); // next expr should be null
- delete parser;
return s;
}
{
std::unique_ptr<SymbolManager> symman(new SymbolManager(solver));
- ParserBuilder pb(solver, symman.get(), "<internal>", solver->getOptions());
- Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
+ 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>"));
assert(p != NULL);
Command* c = p->nextCommand();
assert(c != NULL);
stringstream ss;
c->invoke(solver, symman.get(), ss);
assert(p->nextCommand() == NULL);
- delete p;
delete c;
cout << ss.str() << endl << endl;
}
void tryGoodInput(const std::string goodInput)
{
d_symman.reset(new SymbolManager(d_solver.get()));
- Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
- .withStringInput(goodInput)
- .withOptions(d_options)
- .withInputLanguage(d_lang)
- .build();
+ std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
+ .withOptions(d_options)
+ .withInputLanguage(d_lang)
+ .build());
+ parser->setInput(Input::newStringInput(d_lang, goodInput, "test"));
ASSERT_FALSE(parser->done());
Command* cmd;
while ((cmd = parser->nextCommand()) != NULL)
}
ASSERT_TRUE(parser->done());
- delete parser;
}
void tryBadInput(const std::string badInput, bool strictMode = false)
{
d_symman.reset(new SymbolManager(d_solver.get()));
- Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
- .withStringInput(badInput)
- .withOptions(d_options)
- .withInputLanguage(d_lang)
- .withStrictMode(strictMode)
- .build();
+ std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
+ .withOptions(d_options)
+ .withInputLanguage(d_lang)
+ .withStrictMode(strictMode)
+ .build());
+ parser->setInput(Input::newStringInput(d_lang, badInput, "test"));
ASSERT_THROW(
{
Command* cmd;
std::cout << "\nBad input succeeded:\n" << badInput << std::endl;
},
ParserException);
- delete parser;
}
void tryGoodExpr(const std::string goodExpr)
{
d_symman.reset(new SymbolManager(d_solver.get()));
- Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
- .withStringInput(goodExpr)
- .withOptions(d_options)
- .withInputLanguage(d_lang)
- .build();
-
+ std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
+ .withOptions(d_options)
+ .withInputLanguage(d_lang)
+ .build());
+ parser->setInput(Input::newStringInput(d_lang, goodExpr, "test"));
if (d_lang == LANG_SMTLIB_V2)
{
/* Use QF_LIA to make multiplication ("*") available */
std::unique_ptr<Command> cmd(
- static_cast<Smt2*>(parser)->setLogic("QF_LIA"));
+ static_cast<Smt2*>(parser.get())->setLogic("QF_LIA"));
}
ASSERT_FALSE(parser->done());
e = parser->nextExpression();
ASSERT_TRUE(parser->done());
ASSERT_TRUE(e.isNull());
- delete parser;
}
/**
void tryBadExpr(const std::string badExpr, bool strictMode = false)
{
d_symman.reset(new SymbolManager(d_solver.get()));
- Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
- .withStringInput(badExpr)
- .withOptions(d_options)
- .withInputLanguage(d_lang)
- .withStrictMode(strictMode)
- .build();
+ std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
+ .withOptions(d_options)
+ .withInputLanguage(d_lang)
+ .withStrictMode(strictMode)
+ .build());
+ parser->setInput(Input::newStringInput(d_lang, badExpr, "test"));
setupContext(*parser);
ASSERT_FALSE(parser->done());
ASSERT_THROW(api::Term e = parser->nextExpression();
<< "Input: <<" << badExpr << ">>" << std::endl
<< "Output: <<" << e << ">>" << std::endl;
, ParserException);
- delete parser;
}
Options d_options;
protected:
void SetUp() override { d_symman.reset(new SymbolManager(&d_solver)); }
- void checkEmptyInput(ParserBuilder& builder)
+ void checkEmptyInput(Parser* parser)
{
- Parser* parser = builder.build();
- ASSERT_NE(parser, nullptr);
-
api::Term e = parser->nextExpression();
ASSERT_TRUE(e.isNull());
-
- delete parser;
}
- void checkTrueInput(ParserBuilder& builder)
+ void checkTrueInput(Parser* parser)
{
- Parser* parser = builder.build();
- ASSERT_NE(parser, nullptr);
-
api::Term e = parser->nextExpression();
ASSERT_EQ(e, d_solver.mkTrue());
e = parser->nextExpression();
ASSERT_TRUE(e.isNull());
- delete parser;
}
char* mkTemp()
char* filename = mkTemp();
ASSERT_NE(filename, nullptr);
- checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), filename)
- .withInputLanguage(LANG_CVC));
+ 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());
remove(filename);
free(filename);
fs << "TRUE" << std::endl;
fs.close();
- checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), filename)
- .withInputLanguage(LANG_CVC));
+ 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());
remove(filename);
free(filename);
TEST_F(TestParseBlackParserBuilder, empty_string_input)
{
- checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
- .withInputLanguage(LANG_CVC)
- .withStringInput(""));
+ 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());
}
TEST_F(TestParseBlackParserBuilder, true_string_input)
{
- checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
- .withInputLanguage(LANG_CVC)
- .withStringInput("TRUE"));
+ 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());
}
TEST_F(TestParseBlackParserBuilder, empty_stream_input)
{
std::stringstream ss("", std::ios_base::in);
- checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
- .withInputLanguage(LANG_CVC)
- .withStreamInput(ss));
+ 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());
}
TEST_F(TestParseBlackParserBuilder, true_stream_input)
{
std::stringstream ss("TRUE", std::ios_base::in);
- checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
- .withInputLanguage(LANG_CVC)
- .withStreamInput(ss));
+ 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());
}
} // namespace test
projects / cvc5.git / commitdiff