From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 24 Jul 2013 18:41:29 +0000 (-0400)
Subject: some portfolio driver cleanup
X-Git-Tag: cvc5-1.0.0~7287^2~47
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=028b3ee2dce5ae7491f1019c32ac6faf6c4d6ef1;p=cvc5.git

some portfolio driver cleanup
---

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 48dcc17ef..2cdcc344c 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -214,7 +214,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
     // We currently don't support changing number of threads for each
     // command, but things have been architected in a way so that this
-    // can be acheived with not a lot of work
+    // can be achieved without a lot of work.
     Command *seqs[d_numThreads];
 
     if(d_lastWinner == 0)
@@ -238,7 +238,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
           int(i) == d_lastWinner ?
           cmd->exportTo(d_exprMgrs[i], *(d_vmaps[i])) :
           d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) );
-      }catch(ExportUnsupportedException& e){
+      } catch(ExportUnsupportedException& e) {
         if(d_options[options::fallbackSequential]) {
           Notice() << "Unsupported theory encountered, switching to sequential mode.";
           return CommandExecutor::doCommandSingleton(cmd);
@@ -292,20 +292,11 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
         runPortfolio(d_numThreads, smFn, fns,
                      d_options[options::waitToJoin]);
 
-    d_seq = NULL;
     delete d_seq;
     d_seq = new CommandSequence();
 
     d_lastWinner = portfolioReturn.first;
-
-    CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
-    if(cs != NULL) {
-      d_result = cs->getResult();
-    }
-    QueryCommand* q = dynamic_cast<QueryCommand*>(cmd);
-    if(q != NULL) {
-      d_result = q->getResult();
-    }
+    d_result = d_smts[d_lastWinner]->getStatusOfLastCommand();
 
     if(d_ostringstreams.size() != 0) {
       assert(d_numThreads == d_options[options::threads]);