Some minor changes after reviewing the portfolio "unified driver" commit.

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 93 insertions, 0 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
new file mode 100644
index 000000000..1bffd5e35
--- /dev/null
+++ b/src/main/command_executor.cpp
@@ -0,0 +1,93 @@
+/*********************                                                        */
+/*! \file command_executor.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An additional layer between commands and invoking them.
+ **/
+
+#include <iostream>
+
+#include "main/command_executor.h"
+#include "expr/command.h"
+
+#include "main/main.h"
+
+namespace CVC4 {
+namespace main {
+
+
+CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options):
+  d_exprMgr(exprMgr),
+  d_smtEngine(SmtEngine(&exprMgr)),
+  d_options(options) {
+  
+  // signal handlers need access
+  main::pStatistics = d_smtEngine.getStatisticsRegistry();
+  d_exprMgr.getStatisticsRegistry()->setName("ExprManager");
+  main::pStatistics->registerStat_(d_exprMgr.getStatisticsRegistry());
+}
+
+bool CommandExecutor::doCommand(Command* cmd)
+{
+  if( d_options[options::parseOnly] ) {
+    return true;
+  }
+
+  CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
+  if(seq != NULL) {
+    // assume no error
+    bool status = true;
+
+    for(CommandSequence::iterator subcmd = seq->begin();
+        status && subcmd != seq->end();
+        ++subcmd) {
+      status = doCommand(*subcmd);
+    }
+
+    return status;
+  } else {
+    if(d_options[options::verbosity] > 0) {
+      *d_options[options::out] << "Invoking: " << *cmd << std::endl;
+    }
+
+    return doCommandSingleton(cmd);
+  }
+}
+
+bool CommandExecutor::doCommandSingleton(Command *cmd)
+{
+  bool status = true;
+  if(d_options[options::verbosity] >= 0) {
+    status = smtEngineInvoke(&d_smtEngine, cmd, d_options[options::out]);
+  } else {
+    status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
+  }
+  return status;
+}
+
+std::string CommandExecutor::getSmtEngineStatus()
+{
+  return d_smtEngine.getInfo("status").getValue();
+}
+
+bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
+{
+  if(out == NULL) {
+    cmd->invoke(smt);
+  } else {
+    cmd->invoke(smt, *out);
+  }
+  return !cmd->fail();
+}
+
+}/*main namespace*/
+}/*CVC4 namespace*/