From: Christopher L. Conway Date: Fri, 22 Oct 2010 22:50:39 +0000 (+0000) Subject: Using Options in ParserBuilder and InteractiveShell X-Git-Tag: cvc5-1.0.0~8788 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3870dd8a11c1153e2db24ffe1b384b84129c2df4;p=cvc5.git Using Options in ParserBuilder and InteractiveShell --- 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 #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); } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 31f402df1..348fb6e6d 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -56,15 +56,36 @@ public: } };*/ -ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename) : - d_inputType(FILE_INPUT), - d_lang(language::input::LANG_AUTO), - d_filename(filename), - d_streamInput(NULL), - d_exprManager(exprManager), - d_checksEnabled(true), - d_strictMode(false), - d_mmap(false) { +ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename)// : + // d_inputType(FILE_INPUT), + // d_lang(language::input::LANG_AUTO), + : d_filename(filename), + // d_streamInput(NULL), + d_exprManager(exprManager) + // d_checksEnabled(true), + // d_strictMode(false), + // d_mmap(false) +{ + init(exprManager,filename); +} + + ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename, const Options& options) : + d_filename(filename), + d_exprManager(exprManager) +{ + init(exprManager,filename); + withOptions(options); +} + + void ParserBuilder::init(ExprManager& exprManager, const std::string& filename) { + d_inputType = FILE_INPUT; + d_lang = language::input::LANG_AUTO; + d_filename = filename; + d_streamInput = NULL; + d_exprManager = exprManager; + d_checksEnabled = true; + d_strictMode = false; + d_mmap = false; } Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) { @@ -135,6 +156,14 @@ ParserBuilder& ParserBuilder::withMmap(bool flag) { return *this; } +ParserBuilder& ParserBuilder::withOptions(const Options& options) { + return + withInputLanguage(options.inputLanguage) + .withMmap(options.memoryMap) + .withChecks(options.semanticChecks) + .withStrictMode(options.strictParsing); + } + ParserBuilder& ParserBuilder::withStrictMode(bool flag) { d_strictMode = flag; return *this; diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 2e0af677e..4e8c06f78 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -23,8 +23,10 @@ #include -#include "parser/input.h" -#include "parser/parser_options.h" +#include "input.h" +#include "parser_options.h" + +#include "util/options.h" namespace CVC4 { @@ -87,11 +89,16 @@ class CVC4_PUBLIC ParserBuilder { /** Should we memory-map a file input? */ bool d_mmap; + void init(ExprManager& exprManager, const std::string& filename); + public: /** Create a parser builder using the given ExprManager and filename. */ ParserBuilder(ExprManager& exprManager, const std::string& filename); + ParserBuilder(ExprManager& exprManager, const std::string& filename, + const Options& options); + /** Build the parser, using the current settings. */ Parser *build() throw (InputStreamException,AssertionException); @@ -118,6 +125,9 @@ public: * the parser will have a file input. (Default: no) */ ParserBuilder& withMmap(bool flag = true); + /** Derive settings from the given options. */ + ParserBuilder& withOptions(const Options& options); + /** Should the parser use strict mode? (Default: no) */ ParserBuilder& withStrictMode(bool flag = true); diff --git a/src/util/options.h b/src/util/options.h index b56741fba..e232176b5 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -27,6 +27,12 @@ # define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false #endif /* CVC4_DEBUG */ +#ifdef CVC4_MUZZLED +# define DO_SEMANTIC_CHECKS_BY_DEFAULT false +#else +# define DO_SEMANTIC_CHECKS_BY_DEFAULT true +#endif + #include #include @@ -49,9 +55,9 @@ struct CVC4_PUBLIC Options { bool statistics; - std::istream& in; - std::ostream& out; - std::ostream& err; + std::istream* in; + std::ostream* out; + std::ostream* err; /* -1 means no output */ /* 0 is normal (and default) -- warnings only */ @@ -120,14 +126,14 @@ struct CVC4_PUBLIC Options { Options() : binary_name(), statistics(false), - in(std::cin), - out(std::cout), - err(std::cerr), + in(&std::cin), + out(&std::cout), + err(&std::cerr), verbosity(0), inputLanguage(language::input::LANG_AUTO), uf_implementation(MORGAN), parseOnly(false), - semanticChecks(true), + semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT), memoryMap(false), strictParsing(false), lazyDefinitionExpansion(false), @@ -136,7 +142,7 @@ struct CVC4_PUBLIC Options { segvNoSpin(false), produceModels(false), produceAssignments(false), - typeChecking(true), + typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT), earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) { }