diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/driver_unified.cpp | 35 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 68 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 2 |
3 files changed, 48 insertions, 57 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index de6f614e1..f68545d00 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -158,32 +158,32 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver) } const char* filename = filenameStr.c_str(); - if (opts->base.inputLanguage == Language::LANG_AUTO) + if (solver->getOption("input-language") == "LANG_AUTO") { if( inputFromStdin ) { // We can't do any fancy detection on stdin - opts->base.inputLanguage = Language::LANG_CVC; + solver->setOption("input-language", "cvc"); } else { size_t len = filenameStr.size(); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - opts->base.inputLanguage = Language::LANG_SMTLIB_V2_6; + solver->setOption("input-language", "smt2"); } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { - opts->base.inputLanguage = Language::LANG_TPTP; + solver->setOption("input-language", "tptp"); } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - opts->base.inputLanguage = Language::LANG_CVC; + solver->setOption("input-language", "cvc"); } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) || (len >= 3 && !strcmp(".sl", filename + len - 3))) { // version 2 sygus is the default - opts->base.inputLanguage = Language::LANG_SYGUS_V2; + solver->setOption("input-language", "sygus2"); } } } - if (opts->base.outputLanguage == Language::LANG_AUTO) + if (solver->getOption("output-language") == "LANG_AUTO") { - opts->base.outputLanguage = opts->base.inputLanguage; + solver->setOption("output-language", solver->getOption("input-language")); } pExecutor->storeOptionsAsOriginal(); @@ -197,11 +197,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver) WarningChannel.setStream(&cvc5::null_os); } - // important even for muzzled builds (to get result output right) - (*opts->base.out) - << language::SetLanguage(opts->base.outputLanguage); - - int returnValue = 0; { // notify SmtEngine that we are starting to parse @@ -259,19 +254,19 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver) pExecutor->doCommand(cmd); } - ParserBuilder parserBuilder(pExecutor->getSolver(), - pExecutor->getSymbolManager(), - *opts); + ParserBuilder parserBuilder( + pExecutor->getSolver(), pExecutor->getSymbolManager(), true); std::unique_ptr<Parser> parser(parserBuilder.build()); if( inputFromStdin ) { parser->setInput(Input::newStreamInput( - opts->base.inputLanguage, cin, filename)); + solver->getOption("input-language"), cin, filename)); } else { - parser->setInput(Input::newFileInput(opts->base.inputLanguage, - filename, - opts->parser.memoryMap)); + parser->setInput( + Input::newFileInput(solver->getOption("input-language"), + filename, + solver->getOption("mmap") == "true")); } bool interrupted = false; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 14a507aee..8cb40cfdb 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -91,17 +91,17 @@ static set<string> s_declarations; #endif /* HAVE_LIBEDITLINE */ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) - : d_options(solver->getOptions()), - d_in(*d_options.base.in), - d_out(*d_options.base.out), + : d_solver(solver), + d_in(*solver->getOptions().base.in), + d_out(*solver->getOptions().base.out), d_quit(false) { - ParserBuilder parserBuilder(solver, sm, d_options); + ParserBuilder parserBuilder(solver, sm, true); /* Create parser with bogus input. */ d_parser = parserBuilder.build(); - if (d_options.parser.forceLogicStringWasSetByUser) + if (d_solver->getOptions().parser.forceLogicStringWasSetByUser) { - LogicInfo tmp(d_options.parser.forceLogicString); + LogicInfo tmp(d_solver->getOption("force-logic")); d_parser->forceLogic(tmp.getLogicString()); } @@ -116,34 +116,30 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) #endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */ ::using_history(); - Language lang = d_options.base.inputLanguage; - switch(lang) { - case Language::LANG_CVC: - d_historyFilename = string(getenv("HOME")) + "/.cvc5_history"; - commandsBegin = cvc_commands; - commandsEnd = - cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); - break; - case Language::LANG_TPTP: - d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_tptp"; - commandsBegin = tptp_commands; - commandsEnd = - tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands); - break; - default: - if (language::isLangSmt2(lang)) - { - d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2"; - commandsBegin = smt2_commands; - commandsEnd = - smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); - } - else - { - std::stringstream ss; - ss << "internal error: unhandled language " << lang; - throw Exception(ss.str()); - } + std::string lang = solver->getOption("input-language"); + if (lang == "LANG_CVC") + { + d_historyFilename = string(getenv("HOME")) + "/.cvc5_history"; + commandsBegin = cvc_commands; + commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); + } + else if (lang == "LANG_TPTP") + { + d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_tptp"; + commandsBegin = tptp_commands; + commandsEnd = + tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands); + } + else if (lang == "LANG_SMTLIB_V2_6") + { + d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2"; + commandsBegin = smt2_commands; + commandsEnd = + smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); + } + else + { + throw Exception("internal error: unhandled language " + lang); } d_usingEditline = true; int err = ::read_history(d_historyFilename.c_str()); @@ -313,7 +309,7 @@ restart: } d_parser->setInput(Input::newStringInput( - d_options.base.inputLanguage, input, INPUT_FILENAME)); + d_solver->getOption("input-language"), input, INPUT_FILENAME)); /* There may be more than one command in the input. Build up a sequence. */ @@ -364,7 +360,7 @@ restart: } catch (ParserException& pe) { - if (language::isLangSmt2(d_options.base.outputLanguage)) + if (d_solver->getOption("output-language") == "LANG_SMTLIB_V2_6") { d_out << "(error \"" << pe << "\")" << endl; } diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index cf5f22b51..d4736470f 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -40,7 +40,7 @@ class SymbolManager; class InteractiveShell { - const Options& d_options; + api::Solver* d_solver; std::istream& d_in; std::ostream& d_out; parser::Parser* d_parser; |