Fix for --force-logic to extend its reach to the parser.

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<Kind> 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);