src/main/command_executor.cpp

   1 /*********************                                                        */
   2 /*! \file command_executor.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Andrew Reynolds, Kshitij Bansal
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief An additional layer between commands and invoking them.
  13  **/
  14
  15 #include <iostream>
  16 #include <string>
  17
  18 #include "main/command_executor.h"
  19 #include "expr/command.h"
  20
  21 #include "main/main.h"
  22
  23 #include "main/options.h"
  24 #include "smt/options.h"
  25
  26 #ifndef __WIN32__
  27 #  include <sys/resource.h>
  28 #endif /* ! __WIN32__ */
  29
  30 namespace CVC4 {
  31 namespace main {
  32
  33 // Function to cancel any (externally-imposed) limit on CPU time.
  34 // This is used for competitions while a solution (proof or model)
  35 // is being dumped (so that we don't give "sat" or "unsat" then get
  36 // interrupted partway through outputting a proof!).
  37 void setNoLimitCPU() {
  38   // Windows doesn't have these things, just ignore
  39 #ifndef __WIN32__
  40   struct rlimit rlc;
  41   int st = getrlimit(RLIMIT_CPU, &rlc);
  42   if(st == 0) {
  43     rlc.rlim_cur = rlc.rlim_max;
  44     setrlimit(RLIMIT_CPU, &rlc);
  45   }
  46 #endif /* ! __WIN32__ */
  47 }
  48
  49
  50 void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString);
  51
  52 CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
  53   d_exprMgr(exprMgr),
  54   d_smtEngine(new SmtEngine(&exprMgr)),
  55   d_options(options),
  56   d_stats("driver"),
  57   d_result() {
  58 }
  59
  60 bool CommandExecutor::doCommand(Command* cmd)
  61 {
  62   if( d_options[options::parseOnly] ) {
  63     return true;
  64   }
  65
  66   CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
  67   if(seq != NULL) {
  68     // assume no error
  69     bool status = true;
  70
  71     for(CommandSequence::iterator subcmd = seq->begin();
  72         (status || d_options[options::continuedExecution]) && subcmd != seq->end();
  73         ++subcmd) {
  74       status = doCommand(*subcmd);
  75     }
  76
  77     return status;
  78   } else {
  79     if(d_options[options::verbosity] > 2) {
  80       *d_options[options::out] << "Invoking: " << *cmd << std::endl;
  81     }
  82
  83     return doCommandSingleton(cmd);
  84   }
  85 }
  86
  87 void CommandExecutor::reset()
  88 {
  89   if(d_options[options::statistics]) {
  90     flushStatistics(*d_options[options::err]);
  91   }
  92   delete d_smtEngine;
  93   d_smtEngine = new SmtEngine(&d_exprMgr);
  94 }
  95
  96 bool CommandExecutor::doCommandSingleton(Command* cmd)
  97 {
  98   bool status = true;
  99   if(d_options[options::verbosity] >= -1) {
 100     status = smtEngineInvoke(d_smtEngine, cmd, d_options[options::out]);
 101   } else {
 102     status = smtEngineInvoke(d_smtEngine, cmd, NULL);
 103   }
 104
 105   Result res;
 106   CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
 107   if(cs != NULL) {
 108     d_result = res = cs->getResult();
 109   }
 110   QueryCommand* q = dynamic_cast<QueryCommand*>(cmd);
 111   if(q != NULL) {
 112     d_result = res = q->getResult();
 113   }
 114
 115   if((cs != NULL || q != NULL) && d_options[options::statsEveryQuery]) {
 116     std::ostringstream ossCurStats;
 117     flushStatistics(ossCurStats);
 118     printStatsIncremental(*d_options[options::err], d_lastStatistics, ossCurStats.str());
 119     d_lastStatistics = ossCurStats.str();
 120   }
 121
 122   // dump the model/proof if option is set
 123   if(status) {
 124     Command * g = NULL;
 125     if( d_options[options::produceModels] &&
 126         d_options[options::dumpModels] &&
 127         ( res.asSatisfiabilityResult() == Result::SAT ||
 128           (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
 129       g = new GetModelCommand();
 130     } else if( d_options[options::proof] &&
 131                d_options[options::dumpProofs] &&
 132                res.asSatisfiabilityResult() == Result::UNSAT ) {
 133       g = new GetProofCommand();
 134     } else if( d_options[options::dumpInstantiations] &&
 135                res.asSatisfiabilityResult() == Result::UNSAT ) {
 136       g = new GetInstantiationsCommand();
 137     }
 138     if( g ){
 139       //set no time limit during dumping if applicable
 140       if( d_options[options::forceNoLimitCpuWhileDump] ){
 141         setNoLimitCPU();
 142       }
 143       status = doCommandSingleton(g);
 144     }
 145   }
 146   return status;
 147 }
 148
 149 bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
 150 {
 151   if(out == NULL) {
 152     cmd->invoke(smt);
 153   } else {
 154     cmd->invoke(smt, *out);
 155   }
 156   // ignore the error if the command-verbosity is 0 for this command
 157   if(smt->getOption(std::string("command-verbosity:") + cmd->getCommandName()).getIntegerValue() == 0) {
 158     return true;
 159   }
 160   return !cmd->fail();
 161 }
 162
 163 void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString) {
 164   if(prvsStatsString == "") {
 165       out << curStatsString;
 166       return;
 167   }
 168
 169   // read each line
 170   // if a number, subtract and add that to parantheses
 171   std::istringstream issPrvs(prvsStatsString);
 172   std::istringstream issCur(curStatsString);
 173
 174   std::string prvsStatName, prvsStatValue, curStatName, curStatValue;
 175
 176   std::getline(issPrvs, prvsStatName, ',');
 177   std::getline(issCur, curStatName, ',');
 178
 179   /**
 180    * Stat are assumed to one-per line: "<statName>, <statValue>"
 181    *   e.g. "sat::decisions, 100"
 182    * Output is of the form: "<statName>, <statValue> (<statDiffFromPrvs>)"
 183    *   e.g. "sat::decisions, 100 (20)"
 184    * If the value is not numeric, no change is made.
 185    */
 186   while( !issCur.eof() ) {
 187
 188     std::getline(issCur, curStatValue, '\n');
 189
 190     if(curStatName == prvsStatName) {
 191       std::getline(issPrvs, prvsStatValue, '\n');
 192
 193       double prvsFloat, curFloat;
 194       bool isFloat =
 195         (std::istringstream(prvsStatValue) >> prvsFloat) &&
 196         (std::istringstream(curStatValue) >> curFloat);
 197
 198       if(isFloat) {
 199         out << curStatName << ", " << curStatValue << " "
 200             << "(" << std::setprecision(8) << (curFloat-prvsFloat) << ")"
 201             << std::endl;
 202       } else {
 203         out << curStatName << ", " << curStatValue << std::endl;
 204       }
 205
 206       std::getline(issPrvs, prvsStatName, ',');
 207     } else {
 208       out << curStatName << ", " << curStatValue << std::endl;
 209     }
 210
 211     std::getline(issCur, curStatName, ',');
 212   }
 213 }
 214
 215 }/* CVC4::main namespace */
 216 }/* CVC4 namespace */