1 files changed, 24 insertions, 20 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 6888d3af5..19e4859b0 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -40,10 +40,7 @@
 
 #include "base/output.h"
 #include "options/language.h"
-#include "options/base_options.h"
-#include "options/main_options.h"
 #include "options/options.h"
-#include "options/smt_options.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -92,16 +89,18 @@ static set<string> s_declarations;
 #endif /* HAVE_LIBREADLINE */
 
 InteractiveShell::InteractiveShell(ExprManager& exprManager,
-                                   const Options& options) :
-  d_in(*options[options::in]),
-  d_out(*options[options::out]),
-  d_options(options),
-  d_quit(false) {
+                                   const Options& options)
+    : d_in(*options.getIn()),
+      d_out(*options.getOutConst()),
+      d_options(options),
+      d_quit(false)
+{
   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(d_options.wasSetByUserForceLogicString()) {
+    LogicInfo tmp(d_options.getForceLogicString());
+    d_parser->forceLogic(tmp.getLogicString());
   }
 
 #if HAVE_LIBREADLINE
@@ -114,7 +113,8 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
 #endif /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */
     ::using_history();
 
-    switch(OutputLanguage lang = toOutputLanguage(d_options[options::inputLanguage])) {
+    OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage());
+    switch(lang) {
     case output::LANG_CVC4:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history";
       commandsBegin = cvc_commands;
@@ -195,7 +195,8 @@ restart:
   /* Prompt the user for input. */
   if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-    lineBuf = ::readline(d_options[options::interactivePrompt] ? (line == "" ? "CVC4> " : "... > ") : "");
+    lineBuf = ::readline(d_options.getInteractivePrompt()
+                         ? (line == "" ? "CVC4> " : "... > ") : "");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
       ::add_history(lineBuf);
     }
@@ -203,7 +204,7 @@ restart:
     free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
   } else {
-    if(d_options[options::interactivePrompt]) {
+    if(d_options.getInteractivePrompt()) {
       if(line == "") {
         d_out << "CVC4> " << flush;
       } else {
@@ -219,7 +220,8 @@ restart:
 
   string input = "";
   while(true) {
-    Debug("interactive") << "Input now '" << input << line << "'" << endl << flush;
+    Debug("interactive") << "Input now '" << input << line << "'" << endl
+                         << flush;
 
     assert( !(d_in.fail() && !d_in.eof()) || line.empty() );
 
@@ -260,7 +262,8 @@ restart:
       /* Extract the newline delimiter from the stream too */
       int c CVC4_UNUSED = d_in.get();
       assert(c == '\n');
-      Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush;
+      Debug("interactive") << "Next char is '" << (char)c << "'" << endl
+                           << flush;
     }
 
     input += line;
@@ -271,7 +274,7 @@ restart:
       input[n] = '\n';
       if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-        lineBuf = ::readline(d_options[options::interactivePrompt] ? "... > " : "");
+        lineBuf = ::readline(d_options.getInteractivePrompt() ? "... > " : "");
         if(lineBuf != NULL && lineBuf[0] != '\0') {
           ::add_history(lineBuf);
         }
@@ -279,7 +282,7 @@ restart:
         free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
       } else {
-        if(d_options[options::interactivePrompt]) {
+        if(d_options.getInteractivePrompt()) {
           d_out << "... > " << flush;
         }
 
@@ -295,7 +298,8 @@ restart:
     }
   }
 
-  d_parser->setInput(Input::newStringInput(d_options[options::inputLanguage], input, INPUT_FILENAME));
+  d_parser->setInput(Input::newStringInput(d_options.getInputLanguage(),
+                                           input, INPUT_FILENAME));
 
   /* There may be more than one command in the input. Build up a
      sequence. */
@@ -326,8 +330,8 @@ restart:
     line += "\n";
     goto restart;
   } catch(ParserException& pe) {
-    if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_0 ||
-       d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_5) {
+    if(d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_0 ||
+       d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_5) {
       d_out << "(error \"" << pe << "\")" << endl;
     } else {
       d_out << pe << endl;