diff options
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r-- | src/expr/command.cpp | 74 |
1 files changed, 74 insertions, 0 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp new file mode 100644 index 000000000..2f8dd789e --- /dev/null +++ b/src/expr/command.cpp @@ -0,0 +1,74 @@ +/********************* -*- C++ -*- */ +/** command.cpp + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Implementation of command objects. + **/ + +#include "expr/command.h" +#include "smt/smt_engine.h" + +using namespace std; + +namespace CVC4 { + +ostream& operator<<(ostream& out, const Command* c) { + if (c == NULL) { + out << "null"; + } else { + c->toStream(out); + } + return out; +} + +CommandSequence::~CommandSequence() { + for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { + delete d_commandSequence[i]; + } +} + +void CommandSequence::invoke(SmtEngine* smtEngine) { + for(; d_index < d_commandSequence.size(); ++d_index) { + d_commandSequence[d_index]->invoke(smtEngine); + delete d_commandSequence[d_index]; + } +} + +void CheckSatCommand::toStream(ostream& out) const { + if(d_expr.isNull()) { + out << "CheckSat()"; + } else { + out << "CheckSat(" << d_expr << ")"; + } +} + +void CommandSequence::toStream(ostream& out) const { + out << "CommandSequence[" << endl; + for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { + out << *d_commandSequence[i] << endl; + } + out << "]"; +} + +void DeclarationCommand::toStream(std::ostream& out) const { + out << "Declare("; + bool first = true; + for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) { + if(!first) { + out << ", "; + } + out << d_declaredSymbols[i]; + first = false; + } + out << ")"; +} + +}/* CVC4 namespace */ |