1 files changed, 82 insertions, 76 deletions

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 9d0042694..bf1143647 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -31,12 +31,8 @@
 #include "expr/pickler.h"
 #include "main/main.h"
 #include "main/portfolio.h"
-#include "options/base_options.h"
-#include "options/main_options.h"
 #include "options/options.h"
-#include "options/printer_options.h"
 #include "options/set_language.h"
-#include "options/smt_options.h"
 #include "smt_util/command.h"
 
 
@@ -45,25 +41,26 @@ using namespace std;
 namespace CVC4 {
 namespace main {
 
-CommandExecutorPortfolio::CommandExecutorPortfolio
-(ExprManager &exprMgr, Options &options, vector<Options>& tOpts):
-  CommandExecutor(exprMgr, options),
-  d_numThreads(options[options::threads]),
-  d_smts(),
-  d_seq(new CommandSequence()),
-  d_threadOptions(tOpts),
-  d_vmaps(),
-  d_lastWinner(0),
-  d_channelsOut(),
-  d_channelsIn(),
-  d_ostringstreams(),
-  d_statLastWinner("portfolio::lastWinner"),
-  d_statWaitTime("portfolio::waitTime")
+CommandExecutorPortfolio::CommandExecutorPortfolio(
+    ExprManager &exprMgr, Options &options, OptionsList& tOpts)
+    : CommandExecutor(exprMgr, options),
+      d_numThreads(options.getThreads()),
+      d_smts(),
+      d_seq(new CommandSequence()),
+      d_threadOptions(tOpts),
+      d_vmaps(),
+      d_lastWinner(0),
+      d_channelsOut(),
+      d_channelsIn(),
+      d_ostringstreams(),
+      d_statLastWinner("portfolio::lastWinner"),
+      d_statWaitTime("portfolio::waitTime")
 {
   assert(d_threadOptions.size() == d_numThreads);
 
   d_statLastWinner.setData(d_lastWinner);
   d_stats.registerStat(&d_statLastWinner);
+
   d_stats.registerStat(&d_statWaitTime);
 
   /* Duplication, individualization */
@@ -111,7 +108,7 @@ void CommandExecutorPortfolio::lemmaSharingInit()
 
   if(d_numThreads == 1) {
     // Disable sharing
-    d_threadOptions[0].set(options::sharingFilterByLength, 0);
+    d_threadOptions[0].setSharingFilterByLength(0);
   } else {
     // Setup sharing channels
     const unsigned int sharingChannelSize = 1000000;
@@ -125,34 +122,34 @@ void CommandExecutorPortfolio::lemmaSharingInit()
 
     /* Lemma I/O channels */
     for(unsigned i = 0; i < d_numThreads; ++i) {
-      string tag = "thread #" +
-        boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
+      int thread_id = d_threadOptions[i].getThreadId();
+      string tag = "thread #" + boost::lexical_cast<string>(thread_id);
       LemmaOutputChannel* outputChannel =
           new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i],
                                           d_vmaps[i]->d_from, d_vmaps[i]->d_to);
       LemmaInputChannel* inputChannel =
           new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i],
                                          d_vmaps[i]->d_from, d_vmaps[i]->d_to);
-      d_smts[i]->globals()->setLemmaInputChannel(inputChannel);
-      d_smts[i]->globals()->setLemmaOutputChannel(outputChannel);
+      d_smts[i]->channels()->setLemmaInputChannel(inputChannel);
+      d_smts[i]->channels()->setLemmaOutputChannel(outputChannel);
     }
 
     /* Output to string stream  */
     assert(d_ostringstreams.size() == 0);
     for(unsigned i = 0; i < d_numThreads; ++i) {
       d_ostringstreams.push_back(new ostringstream);
-      d_threadOptions[i].set(options::out, d_ostringstreams[i]);
+      d_threadOptions[i].setOut(d_ostringstreams[i]);
 
+      OutputLanguage outputLanguage = d_threadOptions[i].getOutputLanguage();
       // important even for muzzled builds (to get result output right)
-      *d_threadOptions[i][options::out]
-        << language::SetLanguage(d_threadOptions[i][options::outputLanguage]);
+      *(d_threadOptions[i].getOut()) << language::SetLanguage(outputLanguage);
     }
   }
 }/* CommandExecutorPortfolio::lemmaSharingInit() */
 
 void CommandExecutorPortfolio::lemmaSharingCleanup()
 {
-  assert(d_numThreads == d_options[options::threads]);
+  assert(d_numThreads == d_options.getThreads());
 
   if(d_numThreads == 1)
     return;
@@ -163,10 +160,10 @@ void CommandExecutorPortfolio::lemmaSharingCleanup()
   for(unsigned i = 0; i < d_numThreads; ++i) {
     delete d_channelsIn[i];
     delete d_channelsOut[i];
-    delete d_smts[i]->globals()->getLemmaInputChannel();
-    d_smts[i]->globals()->setLemmaInputChannel(NULL);
-    delete d_smts[i]->globals()->getLemmaOutputChannel();
-    d_smts[i]->globals()->setLemmaOutputChannel(NULL);
+    delete d_smts[i]->channels()->getLemmaInputChannel();
+    d_smts[i]->channels()->setLemmaInputChannel(NULL);
+    delete d_smts[i]->channels()->getLemmaOutputChannel();
+    d_smts[i]->channels()->setLemmaOutputChannel(NULL);
   }
   d_channelsIn.clear();
   d_channelsOut.clear();
@@ -175,7 +172,7 @@ void CommandExecutorPortfolio::lemmaSharingCleanup()
   if(d_ostringstreams.size() != 0) {
     assert(d_ostringstreams.size() == d_numThreads);
     for(unsigned i = 0; i < d_numThreads; ++i) {
-      d_threadOptions[i].set(options::out, d_options[options::out]);
+      d_threadOptions[i].setOut(d_options.getOut());
       delete d_ostringstreams[i];
     }
     d_ostringstreams.clear();
@@ -225,9 +222,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     Command* cmdExported =
       d_lastWinner == 0 ?
       cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) );
-    bool ret = smtEngineInvoke(d_smts[d_lastWinner],
-                               cmdExported,
-                               d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL);
+    std::ostream* winnersOut =  d_options.getVerbosity() >= -1 ?
+        (d_threadOptions[d_lastWinner]).getOut() : NULL;
+    bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported, winnersOut);
     if(d_lastWinner != 0) delete cmdExported;
     return ret;
   } else if(mode == 1) {               // portfolio
@@ -260,13 +257,15 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
           cmd->exportTo(d_exprMgrs[i], *(d_vmaps[i])) :
           d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) );
       } catch(ExportUnsupportedException& e) {
-        if(d_options[options::fallbackSequential]) {
-          Notice() << "Unsupported theory encountered, switching to sequential mode.";
+        if(d_options.getFallbackSequential()) {
+          Notice() << "Unsupported theory encountered."
+                   << "Switching to sequential mode.";
           return CommandExecutor::doCommandSingleton(cmd);
         }
         else
-          throw Exception("Certain theories (e.g., datatypes) are (currently) unsupported in portfolio\n"
-                          "mode. Please see option --fallback-sequential to make this a soft error.");
+          throw Exception("Certain theories (e.g., datatypes) are (currently)"
+                          " unsupported in portfolio\n mode. Please see option"
+                          " --fallback-sequential to make this a soft error.");
       }
     }
 
@@ -289,11 +288,11 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     /* Portfolio */
     boost::function<bool()>* fns = new boost::function<bool()>[d_numThreads];
     for(unsigned i = 0; i < d_numThreads; ++i) {
-      fns[i] = boost::bind(smtEngineInvoke,
-                           d_smts[i],
-                           seqs[i],
-                           d_options[options::verbosity] >= -1 ? d_threadOptions[i][options::out] : NULL
-                           );
+      std::ostream* current_out_or_null = d_options.getVerbosity() >= -1 ?
+          d_threadOptions[i].getOut() : NULL;
+
+      fns[i] = boost::bind(smtEngineInvoke, d_smts[i], seqs[i],
+                           current_out_or_null);
     }
 
     assert(d_channelsIn.size() == d_numThreads
@@ -311,12 +310,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
                          &d_channelsIn[0],
                          &d_smts[0]);
 
-    size_t threadStackSize = d_options[options::threadStackSize];
+    size_t threadStackSize = d_options.getThreadStackSize();
     threadStackSize *= 1024 * 1024;
 
     pair<int, bool> portfolioReturn =
         runPortfolio(d_numThreads, smFn, fns, threadStackSize,
-                     d_options[options::waitToJoin], d_statWaitTime);
+                     d_options.getWaitToJoin(), d_statWaitTime);
 
 #ifdef CVC4_STATISTICS_ON
     assert( d_statWaitTime.running() );
@@ -327,25 +326,24 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     d_result = d_smts[d_lastWinner]->getStatusOfLastCommand();
 
     if(d_ostringstreams.size() != 0) {
-      assert(d_numThreads == d_options[options::threads]);
+      assert(d_numThreads == d_options.getThreads());
       assert(portfolioReturn.first >= 0);
       assert(unsigned(portfolioReturn.first) < d_numThreads);
 
+      std::ostream& out = *d_options.getOut();
       if(Debug.isOn("treat-unknown-error")) {
         if(d_ostringstreams[portfolioReturn.first]->str() == "unknown\n") {
-          *d_options[options::out]
-            << "portfolioReturn = (" << portfolioReturn.first << ", " << portfolioReturn.second
-            << ")\n";
+          out << "portfolioReturn = (" << portfolioReturn.first << ", "
+              << portfolioReturn.second << ")\n";
           for(unsigned i = 0; i < d_numThreads; ++i)
-            *d_options[options::out]
-              << "thread " << i << ": " << d_ostringstreams[i]->str() << std::endl;
+            out << "thread " << i << ": " << d_ostringstreams[i]->str()
+                << std::endl;
           throw Exception("unknown encountered");
         }
       }
 
-      *d_options[options::out]
-        << d_ostringstreams[portfolioReturn.first]->str()
-        << std::flush;
+      out << d_ostringstreams[portfolioReturn.first]->str()
+          << std::flush;
 
 #ifdef CVC4_COMPETITION_MODE
       // We use CVC4 in competition with --no-wait-to-join. If
@@ -366,27 +364,32 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
     // dump the model/proof/unsat core if option is set
     if(status) {
-      if( d_options[options::produceModels] &&
-          d_options[options::dumpModels] &&
+      if( d_options.getProduceModels() &&
+          d_options.getDumpModels() &&
           ( d_result.asSatisfiabilityResult() == Result::SAT ||
-            (d_result.isUnknown() && d_result.whyUnknown() == Result::INCOMPLETE) ) ) {
+            (d_result.isUnknown() &&
+             d_result.whyUnknown() == Result::INCOMPLETE) ) )
+      {
         Command* gm = new GetModelCommand();
         status = doCommandSingleton(gm);
-      } else if( d_options[options::proof] &&
-                 d_options[options::dumpProofs] &&
+      } else if( d_options.getProof() &&
+                 d_options.getDumpProofs() &&
                  d_result.asSatisfiabilityResult() == Result::UNSAT ) {
         Command* gp = new GetProofCommand();
         status = doCommandSingleton(gp);
-      } else if( d_options[options::dumpInstantiations] &&
-                 ( ( d_options[options::instFormatMode]!=INST_FORMAT_MODE_SZS && 
-                   ( d_result.asSatisfiabilityResult() == Result::SAT || (d_result.isUnknown() && d_result.whyUnknown() == Result::INCOMPLETE) ) ) || 
-                 d_result.asSatisfiabilityResult() == Result::UNSAT ) ) {
+      } else if( d_options.getDumpInstantiations() &&
+                 ( ( d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS &&
+                   ( d_result.asSatisfiabilityResult() == Result::SAT ||
+                     (d_result.isUnknown() &&
+                      d_result.whyUnknown() == Result::INCOMPLETE) ) ) ||
+                   d_result.asSatisfiabilityResult() == Result::UNSAT ) ) {
         Command* gi = new GetInstantiationsCommand();
         status = doCommandSingleton(gi);
-      } else if( d_options[options::dumpSynth] && d_result.asSatisfiabilityResult() == Result::UNSAT ){
+      } else if( d_options.getDumpSynth() &&
+                 d_result.asSatisfiabilityResult() == Result::UNSAT ){
         Command* gi = new GetSynthSolutionCommand();
         status = doCommandSingleton(gi);
-      } else if( d_options[options::dumpUnsatCores] &&
+      } else if( d_options.getDumpUnsatCores() &&
                  d_result.asSatisfiabilityResult() == Result::UNSAT ) {
         Command* guc = new GetUnsatCoreCommand();
         status = doCommandSingleton(guc);
@@ -395,13 +398,15 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
     return status;
   } else if(mode == 2) {
-    Command* cmdExported =
-      d_lastWinner == 0 ?
-      cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) );
-    bool ret = smtEngineInvoke(d_smts[d_lastWinner],
-                               cmdExported,
-                               d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL);
-    if(d_lastWinner != 0) delete cmdExported;
+    Command* cmdExported = d_lastWinner == 0 ?
+        cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]));
+    std::ostream* winner_out_if_verbose = d_options.getVerbosity() >= -1 ?
+        d_threadOptions[d_lastWinner].getOut() : NULL;
+    bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported,
+                               winner_out_if_verbose);
+    if(d_lastWinner != 0){
+      delete cmdExported;
+    }
     return ret;
   } else {
     // Unreachable();
@@ -412,16 +417,17 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 }/* CommandExecutorPortfolio::doCommandSingleton() */
 
 void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const {
-  assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
+  assert(d_numThreads == d_exprMgrs.size() &&
+         d_exprMgrs.size() == d_smts.size());
   for(size_t i = 0; i < d_numThreads; ++i) {
     string emTag = "thread#"
-      + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
+        + boost::lexical_cast<string>(d_threadOptions[i].getThreadId());
     Statistics stats = d_exprMgrs[i]->getStatistics();
     stats.setPrefix(emTag);
     stats.flushInformation(out);
 
     string smtTag = "thread#"
-      + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
+        + boost::lexical_cast<string>(d_threadOptions[i].getThreadId());
     stats = d_smts[i]->getStatistics();
     stats.setPrefix(smtTag);
     stats.flushInformation(out);