diff options
Diffstat (limited to 'src/parser/smt/smt.cpp')
-rw-r--r-- | src/parser/smt/smt.cpp | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index a8dabeffe..a6e716b77 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -2,8 +2,8 @@ /*! \file smt.cpp ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -20,6 +20,7 @@ namespace std { } #include "expr/type.h" +#include "expr/command.h" #include "parser/parser.h" #include "parser/smt/smt.h" @@ -80,6 +81,10 @@ void Smt::addTheory(Theory theory) { case THEORY_ARRAYS_EX: { Type indexType = mkSort("Index"); Type elementType = mkSort("Element"); + DeclarationSequence* seq = new DeclarationSequence(); + seq->addCommand(new DeclareTypeCommand("Index", 0, indexType)); + seq->addCommand(new DeclareTypeCommand("Element", 0, elementType)); + preemptCommand(seq); defineType("Array", getExprManager()->mkArrayType(indexType,elementType)); @@ -88,9 +93,11 @@ void Smt::addTheory(Theory theory) { break; } - case THEORY_EMPTY: - mkSort("U"); + case THEORY_EMPTY: { + Type sort = mkSort("U"); + preemptCommand(new DeclareTypeCommand("U", 0, sort)); break; + } case THEORY_REALS_INTS: defineType("Real", getExprManager()->realType()); |