summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/driver_unified.cpp35
-rw-r--r--src/main/interactive_shell.cpp68
-rw-r--r--src/main/interactive_shell.h2
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback