diff options
Diffstat (limited to 'src/expr/command.h')
| -rw-r--r-- | src/expr/command.h | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/src/expr/command.h b/src/expr/command.h index fbb48b6b0..585e60eb4 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -2,10 +2,10 @@ /*! \file command.h ** \verbatim ** Original author: mdeters - ** Major contributors: cconway, dejan - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -28,11 +28,13 @@ #include <sstream> #include <string> #include <vector> +#include <map> #include "expr/expr.h" #include "expr/type.h" #include "util/result.h" #include "util/sexpr.h" +#include "util/datatype.h" namespace CVC4 { @@ -264,6 +266,16 @@ public: void printResult(std::ostream& out) const; };/* class GetOptionCommand */ +class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { +private: + std::vector<DatatypeType> d_datatypes; +public: + DatatypeDeclarationCommand(const DatatypeType& datatype); + DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes); + void invoke(SmtEngine* smtEngine); + void toStream(std::ostream& out) const; +};/* class DatatypeDeclarationCommand */ + class CVC4_PUBLIC CommandSequence : public Command { private: /** All the commands to be executed (in sequence) */ |