From 03c1daa126ecd86d1434c7512b73723687ea8ca0 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 29 Apr 2014 17:57:17 -0400 Subject: [PATCH] Fix for --force-logic to extend its reach to the parser. --- src/main/interactive_shell.cpp | 4 ++++ src/parser/parser.cpp | 4 +++- src/parser/parser.h | 14 ++++++++++++++ src/parser/parser_builder.cpp | 22 ++++++++++++++++++++-- src/parser/parser_builder.h | 9 +++++++++ src/parser/smt1/smt1.cpp | 6 +++++- src/parser/smt2/smt2.cpp | 6 +++++- 7 files changed, 60 insertions(+), 5 deletions(-) diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 90229861f..a19e23725 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -32,6 +32,7 @@ #include "parser/parser.h" #include "parser/parser_builder.h" #include "options/options.h" +#include "smt/options.h" #include "main/options.h" #include "util/language.h" #include "util/output.h" @@ -93,6 +94,9 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options); /* Create parser with bogus input. */ d_parser = parserBuilder.withStringInput("").build(); + if(d_options.wasSetByUser(options::forceLogic)) { + d_parser->forceLogic(d_options[options::forceLogic].getLogicString()); + } #if HAVE_LIBREADLINE if(d_in == cin) { diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c3019966a..c40c352d9 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -48,7 +48,9 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par d_checksEnabled(true), d_strictMode(strictMode), d_parseOnly(parseOnly), - d_canIncludeFile(true) { + d_canIncludeFile(true), + d_logicIsForced(false), + d_forcedLogic() { d_input->setParser(*this); } diff --git a/src/parser/parser.h b/src/parser/parser.h index b6ba482b7..3f5e66492 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -164,6 +164,16 @@ class CVC4_PUBLIC Parser { */ bool d_canIncludeFile; + /** + * Whether the logic has been forced with --force-logic. + */ + bool d_logicIsForced; + + /** + * The logic, if d_logicIsForced == true. + */ + std::string d_forcedLogic; + /** The set of operators available in the current logic. */ std::set d_logicOperators; @@ -262,6 +272,10 @@ public: void disallowIncludeFile() { d_canIncludeFile = false; } bool canIncludeFile() const { return d_canIncludeFile; } + void forceLogic(const std::string& logic) { assert(!d_logicIsForced); d_logicIsForced = true; d_forcedLogic = logic; } + const std::string& getForcedLogic() const { return d_forcedLogic; } + bool logicIsForced() const { return d_logicIsForced; } + /** * Returns a variable, given a name. * diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 7d0a0c4b9..c8171d180 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -25,6 +25,7 @@ #include "expr/expr_manager.h" #include "parser/options.h" +#include "smt/options.h" namespace CVC4 { namespace parser { @@ -57,6 +58,8 @@ void ParserBuilder::init(ExprManager* exprManager, d_canIncludeFile = true; d_mmap = false; d_parseOnly = false; + d_logicIsForced = false; + d_forcedLogic = ""; } Parser* ParserBuilder::build() @@ -109,6 +112,10 @@ Parser* ParserBuilder::build() parser->disallowIncludeFile(); } + if( d_logicIsForced ) { + parser->forceLogic(d_forcedLogic); + } + return parser; } @@ -148,14 +155,19 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) { } ParserBuilder& ParserBuilder::withOptions(const Options& options) { - return - withInputLanguage(options[options::inputLanguage]) + ParserBuilder& retval = *this; + retval = + retval.withInputLanguage(options[options::inputLanguage]) .withMmap(options[options::memoryMap]) .withChecks(options[options::semanticChecks]) .withStrictMode(options[options::strictParsing]) .withParseOnly(options[options::parseOnly]) .withIncludeFile(options[options::filesystemAccess]); + if(options.wasSetByUser(options::forceLogic)) { + retval = retval.withForcedLogic(options[options::forceLogic].getLogicString()); } + return retval; +} ParserBuilder& ParserBuilder::withStrictMode(bool flag) { d_strictMode = flag; @@ -167,6 +179,12 @@ ParserBuilder& ParserBuilder::withIncludeFile(bool flag) { return *this; } +ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic) { + d_logicIsForced = true; + d_forcedLogic = logic; + return *this; +} + ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) { d_inputType = STREAM_INPUT; d_streamInput = &input; diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index b6e15b2ff..96590eb3e 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -80,6 +80,12 @@ class CVC4_PUBLIC ParserBuilder { /** Are we parsing only? */ bool d_parseOnly; + /** Is the logic forced by the user? */ + bool d_logicIsForced; + + /** The forced logic name */ + std::string d_forcedLogic; + /** Initialize this parser builder */ void init(ExprManager* exprManager, const std::string& filename); @@ -164,6 +170,9 @@ public: /** Set the parser to use the given string for its input. */ ParserBuilder& withStringInput(const std::string& input); + + /** Set the parser to use the given logic string. */ + ParserBuilder& withForcedLogic(const std::string& logic); };/* class ParserBuilder */ }/* CVC4::parser namespace */ diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index 19be199fd..73838e3cc 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -178,7 +178,11 @@ bool Smt1::logicIsSet() { void Smt1::setLogic(const std::string& name) { d_logicSet = true; - d_logic = toLogic(name); + if(logicIsForced()) { + d_logic = toLogic(getForcedLogic()); + } else { + d_logic = toLogic(name); + } switch(d_logic) { case QF_S: diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e9e6ba857..5baa0b16f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -233,7 +233,11 @@ bool Smt2::logicIsSet() { void Smt2::setLogic(const std::string& name) { d_logicSet = true; - d_logic = name; + if(logicIsForced()) { + d_logic = getForcedLogic(); + } else { + d_logic = name; + } // Core theory belongs to every logic addTheory(THEORY_CORE); -- 2.30.2