summaryrefslogtreecommitdiff
path: root/src/expr/command.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/command.h')
-rw-r--r--src/expr/command.h10
1 files changed, 7 insertions, 3 deletions
diff --git a/src/expr/command.h b/src/expr/command.h
index 6a4bb67ed..bb295a662 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -27,6 +27,7 @@
#include <vector>
#include "expr/expr.h"
+#include "expr/type.h"
#include "util/result.h"
namespace CVC4 {
@@ -92,10 +93,11 @@ public:
class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
public:
- DeclarationCommand(const std::vector<std::string>& ids, const Type* t);
+ DeclarationCommand(const std::vector<std::string>& ids, const Type& t);
void toStream(std::ostream& out) const;
protected:
std::vector<std::string> d_declaredSymbols;
+ Type d_type;
};
class CVC4_PUBLIC CheckSatCommand : public Command {
@@ -257,8 +259,10 @@ inline void CommandSequence::addCommand(Command* cmd) {
/* class DeclarationCommand */
-inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, const Type* t) :
- d_declaredSymbols(ids) {
+inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, const Type& t) :
+ d_declaredSymbols(ids),
+ d_type(t)
+{
}
/* class SetBenchmarkStatusCommand */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback