src/expr/command.cpp

   1 /*********************                                                        */
   2 /** command.cpp
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** Implementation of command objects.
  14  **/
  15
  16 #include "expr/command.h"
  17 #include "smt/smt_engine.h"
  18
  19 using namespace std;
  20
  21 namespace CVC4 {
  22
  23 ostream& operator<<(ostream& out, const Command* command) {
  24   if (command == NULL) {
  25     out << "null";
  26   } else {
  27     command->toStream(out);
  28   }
  29   return out;
  30 }
  31
  32 CommandSequence::~CommandSequence() {
  33   for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
  34     delete d_commandSequence[i];
  35   }
  36 }
  37
  38 void CommandSequence::invoke(SmtEngine* smtEngine) {
  39   for(; d_index < d_commandSequence.size(); ++d_index) {
  40     d_commandSequence[d_index]->invoke(smtEngine);
  41     delete d_commandSequence[d_index];
  42   }
  43 }
  44
  45 void CheckSatCommand::toStream(ostream& out) const {
  46   if(d_expr.isNull()) {
  47     out << "CheckSat()";
  48   } else {
  49     out << "CheckSat(" << d_expr << ")";
  50   }
  51 }
  52
  53 void CommandSequence::toStream(ostream& out) const {
  54   out << "CommandSequence[" << endl;
  55   for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
  56     out << *d_commandSequence[i] << endl;
  57   }
  58   out << "]";
  59 }
  60
  61 void DeclarationCommand::toStream(std::ostream& out) const {
  62   out << "Declare(";
  63   bool first = true;
  64   for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) {
  65     if(!first) {
  66       out << ", ";
  67     }
  68     out << d_declaredSymbols[i];
  69     first = false;
  70   }
  71   out << ")";
  72 }
  73
  74 void PushCommand::invoke(SmtEngine* smtEngine) {
  75   smtEngine->push();
  76 }
  77
  78 void PushCommand::toStream(ostream& out) const {
  79   out << "Push()";
  80 }
  81
  82 void PopCommand::invoke(SmtEngine* smtEngine) {
  83   smtEngine->pop();
  84 }
  85
  86 void PopCommand::toStream(ostream& out) const {
  87   out << "Pop()";
  88 }
  89
  90 }/* CVC4 namespace */