diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-22 22:50:39 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-22 22:50:39 +0000 |
commit | 3870dd8a11c1153e2db24ffe1b384b84129c2df4 (patch) | |
tree | 73524745d29dd32a160867afed4f314049211cef /src/main | |
parent | a486cdde94366aa6b4a1f558eecc0130ba25ad5e (diff) |
Using Options in ParserBuilder and InteractiveShell
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/interactive_shell.h | 10 | ||||
-rw-r--r-- | src/main/main.cpp | 41 |
2 files changed, 23 insertions, 28 deletions
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 6bd9db295..66c134ecd 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -21,6 +21,7 @@ #include <string> #include "parser/parser_builder.h" +#include "util/options.h" namespace CVC4 { @@ -34,11 +35,10 @@ class InteractiveShell { ParserBuilder d_parserBuilder; public: - InteractiveShell(std::istream& in, - std::ostream& out, - ParserBuilder& parserBuilder) : - d_in(in), - d_out(out), + InteractiveShell(ParserBuilder& parserBuilder, + const Options& options) : + d_in(*options.in), + d_out(*options.out), d_parserBuilder(parserBuilder) { } diff --git a/src/main/main.cpp b/src/main/main.cpp index 544c6fd29..8bca6190e 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -79,7 +79,7 @@ void printUsage() { << "Without an input file, or with `-', CVC4 reads from standard input." << endl << endl << "CVC4 options:" << endl; - Options::printUsage( ss.str(), options.out ); + Options::printUsage( ss.str(), *options.out ); } /** @@ -94,34 +94,34 @@ int main(int argc, char* argv[]) { return runCvc4(argc, argv); } catch(OptionException& e) { #ifdef CVC4_COMPETITION_MODE - options.out << "unknown" << endl; + *options.out << "unknown" << endl; #endif cerr << "CVC4 Error:" << endl << e << endl; printUsage(); exit(1); } catch(Exception& e) { #ifdef CVC4_COMPETITION_MODE - options.out << "unknown" << endl; + *options.out << "unknown" << endl; #endif - options.err << "CVC4 Error:" << endl << e << endl; + *options.err << "CVC4 Error:" << endl << e << endl; if(options.statistics) { - StatisticsRegistry::flushStatistics(options.err); + StatisticsRegistry::flushStatistics(*options.err); } exit(1); } catch(bad_alloc) { #ifdef CVC4_COMPETITION_MODE - options.out << "unknown" << endl; + *options.out << "unknown" << endl; #endif - options.err << "CVC4 ran out of memory." << endl; + *options.err << "CVC4 ran out of memory." << endl; if(options.statistics) { - StatisticsRegistry::flushStatistics(options.err); + StatisticsRegistry::flushStatistics(*options.err); } exit(1); } catch(...) { #ifdef CVC4_COMPETITION_MODE - options.out << "unknown" << endl; + *options.out << "unknown" << endl; #endif - options.err << "CVC4 threw an exception of unknown type." << endl; + *options.err << "CVC4 threw an exception of unknown type." << endl; exit(1); } } @@ -143,10 +143,10 @@ int runCvc4(int argc, char* argv[]) { printUsage(); exit(1); } else if( options.languageHelp ) { - Options::printLanguageHelp(options.out); + Options::printLanguageHelp(*options.out); exit(1); } else if( options.version ) { - options.out << Configuration::about().c_str() << flush; + *options.out << Configuration::about().c_str() << flush; exit(0); } @@ -154,7 +154,7 @@ int runCvc4(int argc, char* argv[]) { // If in competition mode, set output stream option to flush immediately #ifdef CVC4_COMPETITION_MODE - options.out << unitbuf; + *options.out << unitbuf; #endif // We only accept one input file @@ -230,12 +230,7 @@ int runCvc4(int argc, char* argv[]) { } ParserBuilder parserBuilder = - ParserBuilder(exprMgr, filename) - .withInputLanguage(options.inputLanguage) - .withMmap(options.memoryMap) - .withChecks(options.semanticChecks && - !Configuration::isMuzzledBuild() ) - .withStrictMode( options.strictParsing ); + ParserBuilder(exprMgr, filename, options); if( inputFromStdin ) { parserBuilder.withStreamInput(cin); @@ -244,7 +239,7 @@ int runCvc4(int argc, char* argv[]) { // Parse and execute commands until we are done Command* cmd; if( options.interactive ) { - InteractiveShell shell(options.in,options.out,parserBuilder); + InteractiveShell shell(parserBuilder,options); while((cmd = shell.readCommand())) { doCommand(smt,cmd); delete cmd; @@ -280,7 +275,7 @@ int runCvc4(int argc, char* argv[]) { StatisticsRegistry::registerStat(&s_statSatResult); if(options.statistics) { - StatisticsRegistry::flushStatistics(options.err); + StatisticsRegistry::flushStatistics(*options.err); } StatisticsRegistry::unregisterStat(&s_statSatResult); @@ -304,11 +299,11 @@ void doCommand(SmtEngine& smt, Command* cmd) { } } else { if(options.verbosity > 0) { - options.out << "Invoking: " << *cmd << endl; + *options.out << "Invoking: " << *cmd << endl; } if(options.verbosity >= 0) { - cmd->invoke(&smt, options.out); + cmd->invoke(&smt, *options.out); } else { cmd->invoke(&smt); } |