summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/main/driver_unified.cpp35
-rw-r--r--src/main/interactive_shell.cpp68
-rw-r--r--src/main/interactive_shell.h2
-rw-r--r--src/options/base_options.toml1
-rw-r--r--src/options/options_handler.cpp8
-rw-r--r--src/options/options_handler.h4
-rw-r--r--src/parser/antlr_input.cpp49
-rw-r--r--src/parser/antlr_input.h3
-rw-r--r--src/parser/input.cpp6
-rw-r--r--src/parser/input.h6
-rw-r--r--src/parser/parser_builder.cpp46
-rw-r--r--src/parser/parser_builder.h10
-rw-r--r--src/parser/smt2/smt2.cpp9
-rw-r--r--src/parser/smt2/smt2.h4
14 files changed, 118 insertions, 133 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;
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index a049348a6..bf0134200 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -49,6 +49,7 @@ public = true
type = "Language"
default = "Language::LANG_AUTO"
handler = "stringToLanguage"
+ predicates = ["applyOutputLanguage"]
includes = ["options/language.h"]
help = "force output language (default is \"auto\"; see --output-lang help)"
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 149aa767b..1b6cff519 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -34,6 +34,7 @@
#include "options/didyoumean.h"
#include "options/language.h"
#include "options/option_exception.h"
+#include "options/set_language.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "smt/command.h"
@@ -513,6 +514,13 @@ Language OptionsHandler::stringToLanguage(const std::string& option,
Unreachable();
}
+void OptionsHandler::applyOutputLanguage(const std::string& option,
+ const std::string& flag,
+ Language lang)
+{
+ d_options->base.out << language::SetLanguage(lang);
+}
+
void OptionsHandler::languageIsNotAST(const std::string& option,
const std::string& flag,
Language lang)
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 3b8eb724f..0d625c5da 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -153,6 +153,10 @@ public:
Language stringToLanguage(const std::string& option,
const std::string& flag,
const std::string& optarg);
+ /** Apply the output language to the default output stream */
+ void applyOutputLanguage(const std::string& option,
+ const std::string& flag,
+ Language lang);
/** Check that lang is not LANG_AST (which is not allowed as input language). */
void languageIsNotAST(const std::string& option,
const std::string& flag,
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 6d5cbb5cc..c190fe7f0 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -185,35 +185,30 @@ AntlrInputStream::newStringInputStream(const std::string& input,
return new AntlrInputStream(name, inputStream, false, input_duplicate, NULL);
}
-AntlrInput* AntlrInput::newInput(Language lang, AntlrInputStream& inputStream)
+AntlrInput* AntlrInput::newInput(const std::string& lang,
+ AntlrInputStream& inputStream)
{
- AntlrInput* input;
-
- switch(lang) {
- case Language::LANG_CVC:
- {
- input = new CvcInput(inputStream);
- break;
- }
-
- case Language::LANG_SYGUS_V2: input = new SygusInput(inputStream); break;
-
- case Language::LANG_TPTP: input = new TptpInput(inputStream); break;
-
- default:
- if (language::isLangSmt2(lang))
- {
- input = new Smt2Input(inputStream);
- }
- else
- {
- std::stringstream ss;
- ss << "unable to detect input file format, try --lang ";
- throw InputStreamException(ss.str());
- }
+ if (lang == "LANG_CVC")
+ {
+ return new CvcInput(inputStream);
+ }
+ else if (lang == "LANG_SYGUS_V2")
+ {
+ return new SygusInput(inputStream);
+ }
+ else if (lang == "LANG_TPTP")
+ {
+ return new TptpInput(inputStream);
+ }
+ else if (lang == "LANG_SMTLIB_V2_6")
+ {
+ return new Smt2Input(inputStream);
+ }
+ else
+ {
+ throw InputStreamException(
+ "unable to detect input file format, try --lang ");
}
-
- return input;
}
AntlrInput::AntlrInput(AntlrInputStream& inputStream, unsigned int lookahead) :
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 52650f561..7799d279d 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -155,7 +155,8 @@ public:
* @param inputStream the input stream
*
* */
- static AntlrInput* newInput(Language lang, AntlrInputStream& inputStream);
+ static AntlrInput* newInput(const std::string& lang,
+ AntlrInputStream& inputStream);
/** Retrieve the text associated with a token. */
static std::string tokenText(pANTLR3_COMMON_TOKEN token);
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 9d4c65eae..c8c005b36 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -51,7 +51,7 @@ InputStream *Input::getInputStream() {
return d_inputStream;
}
-Input* Input::newFileInput(Language lang,
+Input* Input::newFileInput(const std::string& lang,
const std::string& filename,
bool useMmap)
{
@@ -60,7 +60,7 @@ Input* Input::newFileInput(Language lang,
return AntlrInput::newInput(lang, *inputStream);
}
-Input* Input::newStreamInput(Language lang,
+Input* Input::newStreamInput(const std::string& lang,
std::istream& input,
const std::string& name)
{
@@ -69,7 +69,7 @@ Input* Input::newStreamInput(Language lang,
return AntlrInput::newInput(lang, *inputStream);
}
-Input* Input::newStringInput(Language lang,
+Input* Input::newStringInput(const std::string& lang,
const std::string& str,
const std::string& name)
{
diff --git a/src/parser/input.h b/src/parser/input.h
index 94bbe1d8a..7d7254339 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -100,7 +100,7 @@ class CVC5_EXPORT Input
* @param filename the input filename
* @param useMmap true if the parser should use memory-mapped I/O (default: false)
*/
- static Input* newFileInput(Language lang,
+ static Input* newFileInput(const std::string& lang,
const std::string& filename,
bool useMmap = false);
@@ -113,7 +113,7 @@ class CVC5_EXPORT Input
* (false, the default, means that the entire Input might be read
* before being lexed and parsed)
*/
- static Input* newStreamInput(Language lang,
+ static Input* newStreamInput(const std::string& lang,
std::istream& input,
const std::string& name);
@@ -123,7 +123,7 @@ class CVC5_EXPORT Input
* @param input the input string
* @param name the name of the stream, for use in error messages
*/
- static Input* newStringInput(Language lang,
+ static Input* newStringInput(const std::string& lang,
const std::string& input,
const std::string& name);
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 1ac03fb83..665836402 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -33,24 +33,21 @@
namespace cvc5 {
namespace parser {
-ParserBuilder::ParserBuilder(api::Solver* solver, SymbolManager* sm)
- : d_solver(solver), d_symman(sm)
-{
- init(solver, sm);
-}
-
ParserBuilder::ParserBuilder(api::Solver* solver,
SymbolManager* sm,
- const Options& options)
+ bool useOptions)
: d_solver(solver), d_symman(sm)
{
init(solver, sm);
- withOptions(options);
+ if (useOptions)
+ {
+ withOptions(solver->getOptions());
+ }
}
void ParserBuilder::init(api::Solver* solver, SymbolManager* sm)
{
- d_lang = Language::LANG_AUTO;
+ d_lang = "LANG_AUTO";
d_solver = solver;
d_symman = sm;
d_checksEnabled = true;
@@ -64,24 +61,17 @@ void ParserBuilder::init(api::Solver* solver, SymbolManager* sm)
Parser* ParserBuilder::build()
{
Parser* parser = NULL;
- switch (d_lang)
+ if (d_lang == "LANG_SYGUS_V2" || d_lang == "LANG_SMTLIB_V2_6")
+ {
+ parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
+ }
+ else if (d_lang == "LANG_TPTP")
+ {
+ parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly);
+ }
+ else
{
- case Language::LANG_SYGUS_V2:
- parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
- break;
- case Language::LANG_TPTP:
- parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly);
- break;
- default:
- if (language::isLangSmt2(d_lang))
- {
- parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
- }
- else
- {
- parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly);
- }
- break;
+ parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly);
}
if( d_checksEnabled ) {
@@ -108,7 +98,7 @@ ParserBuilder& ParserBuilder::withChecks(bool flag) {
return *this;
}
-ParserBuilder& ParserBuilder::withInputLanguage(Language lang)
+ParserBuilder& ParserBuilder::withInputLanguage(const std::string& lang)
{
d_lang = lang;
return *this;
@@ -122,7 +112,7 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
ParserBuilder& ParserBuilder::withOptions(const Options& opts)
{
ParserBuilder& retval = *this;
- retval = retval.withInputLanguage(opts.base.inputLanguage)
+ retval = retval.withInputLanguage(d_solver->getOption("input-language"))
.withChecks(opts.parser.semanticChecks)
.withStrictMode(opts.parser.strictParsing)
.withParseOnly(opts.base.parseOnly)
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 61819a8f9..23a9daae2 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -45,7 +45,7 @@ class Parser;
class CVC5_EXPORT ParserBuilder
{
/** The input language */
- Language d_lang;
+ std::string d_lang;
/** The API Solver object. */
api::Solver* d_solver;
@@ -76,11 +76,7 @@ class CVC5_EXPORT ParserBuilder
public:
/** Create a parser builder using the given Solver and filename. */
- ParserBuilder(api::Solver* solver, SymbolManager* sm);
-
- ParserBuilder(api::Solver* solver,
- SymbolManager* sm,
- const Options& options);
+ ParserBuilder(api::Solver* solver, SymbolManager* sm, bool useOptions);
/** Build the parser, using the current settings. */
Parser* build();
@@ -93,7 +89,7 @@ class CVC5_EXPORT ParserBuilder
*
* (Default: LANG_AUTO)
*/
- ParserBuilder& withInputLanguage(Language lang);
+ ParserBuilder& withInputLanguage(const std::string& lang);
/**
* Are we only parsing, or doing something with the resulting
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index fe777fe27..39492a98c 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -334,7 +334,7 @@ api::Term Smt2::getExpressionForNameAndType(const std::string& name,
bool Smt2::getTesterName(api::Term cons, std::string& name)
{
- if ((v2_6() || sygus_v2()) && strictModeEnabled())
+ if ((v2_6() || sygus()) && strictModeEnabled())
{
// 2.6 or above uses indexed tester symbols, if we are in strict mode,
// we do not automatically define is-cons for constructor cons.
@@ -711,9 +711,10 @@ api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars,
return d_allocGrammars.back().get();
}
-bool Smt2::sygus() const { return language::isLangSygus(getLanguage()); }
-
-bool Smt2::sygus_v2() const { return getLanguage() == Language::LANG_SYGUS_V2; }
+bool Smt2::sygus() const
+{
+ return d_solver->getOption("input-language") == "LANG_SYGUS_V2";
+}
void Smt2::checkThatLogicIsSet()
{
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 50b4a4efc..c3f93708d 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -230,12 +230,10 @@ class Smt2 : public Parser
*/
bool v2_6(bool exact = false) const
{
- return language::isLangSmt2(getLanguage());
+ return d_solver->getOption("input-language") == "LANG_SMTLIB_V2_6";
}
/** Are we using a sygus language? */
bool sygus() const;
- /** Are we using the sygus version 2.0 format? */
- bool sygus_v2() const;
/**
* Returns true if the language that we are parsing (SMT-LIB version >=2.5
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback