summaryrefslogtreecommitdiff
path: root/src/main/main.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r--src/main/main.cpp30
1 files changed, 10 insertions, 20 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 19e1d0cff..a16db2411 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -22,8 +22,8 @@
#include "cvc4autoconfig.h"
#include "main.h"
#include "usage.h"
-#include "parser/input.h"
#include "parser/parser.h"
+#include "parser/parser_builder.h"
#include "expr/expr_manager.h"
#include "smt/smt_engine.h"
#include "expr/command.h"
@@ -149,29 +149,19 @@ int runCvc4(int argc, char* argv[]) {
}
}
- // Create the parser
- Input* input;
-
/* TODO: Hack ANTLR3 to support input from streams */
-// if(inputFromStdin) {
- // parser = Parser::getNewParser(&exprMgr, options.lang, cin, "<stdin>");
-// } else {
- input = Input::newFileInput(options.lang, argv[firstArgIndex],
- options.memoryMap);
-// }
- Parser parser(&exprMgr, input);
-
- if(!options.semanticChecks || Configuration::isMuzzledBuild()) {
- parser.disableChecks();
- }
+ ParserBuilder parserBuilder(options.lang, argv[firstArgIndex]);
- if( options.strictParsing ) {
- parser.enableStrictMode();
- }
+ Parser *parser =
+ parserBuilder.withExprManager(exprMgr)
+ .withMmap(options.memoryMap)
+ .withChecks(options.semanticChecks && !Configuration::isMuzzledBuild() )
+ .withStrictMode( options.strictParsing )
+ .build();
// Parse and execute commands until we are done
Command* cmd;
- while((cmd = parser.nextCommand())) {
+ while((cmd = parser->nextCommand())) {
if( !options.parseOnly ) {
doCommand(smt, cmd);
}
@@ -179,7 +169,7 @@ int runCvc4(int argc, char* argv[]) {
}
// Remove the parser
- delete input;
+ delete parser;
switch(lastResult.asSatisfiabilityResult().isSAT()) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback