summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/command.cpp35
-rw-r--r--src/expr/command.h18
-rw-r--r--src/expr/expr_manager_template.cpp65
-rw-r--r--src/expr/expr_manager_template.h30
-rw-r--r--src/expr/expr_template.h88
-rwxr-xr-xsrc/expr/mkexpr23
-rwxr-xr-xsrc/expr/mkkind2
-rw-r--r--src/expr/node.h2
-rw-r--r--src/expr/node_manager.cpp32
-rw-r--r--src/expr/node_manager.h23
-rw-r--r--src/expr/type.cpp104
-rw-r--r--src/expr/type.h134
-rw-r--r--src/expr/type_node.cpp48
-rw-r--r--src/expr/type_node.h42
14 files changed, 584 insertions, 62 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 7c08293be..bcc96637f 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -2,10 +2,10 @@
/*! \file command.cpp
** \verbatim
** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
** 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
@@ -498,6 +498,35 @@ void GetOptionCommand::toStream(std::ostream& out) const {
out << "GetOption(" << d_flag << ")";
}
+/* class DatatypeDeclarationCommand */
+
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) :
+ d_datatypes() {
+ d_datatypes.push_back(datatype);
+ Debug("datatypes") << "Create datatype command." << endl;
+}
+
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) :
+ d_datatypes(datatypes) {
+ Debug("datatypes") << "Create datatype command." << endl;
+}
+
+void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
+ Debug("datatypes") << "Invoke datatype command." << endl;
+ //smtEngine->addDatatypeDefinitions(d_datatype);
+}
+
+void DatatypeDeclarationCommand::toStream(std::ostream& out) const {
+ out << "DatatypeDeclarationCommand([";
+ for(vector<DatatypeType>::const_iterator i = d_datatypes.begin(),
+ i_end = d_datatypes.end();
+ i != i_end;
+ ++i) {
+ out << *i << ";" << endl;
+ }
+ out << "])";
+}
+
/* output stream insertion operator for benchmark statuses */
std::ostream& operator<<(std::ostream& out,
BenchmarkStatus status) {
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) */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6e8b6c63c..21fc0a4a1 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -2,10 +2,10 @@
/*! \file expr_manager_template.cpp
** \verbatim
** Original author: dejan
- ** Major contributors: mdeters, cconway
+ ** Major contributors: cconway, mdeters
** 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)
+ ** 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
@@ -22,13 +22,15 @@
#include "util/options.h"
#include "util/stats.h"
+#include <map>
+
${includes}
// This is a hack, but an important one: if there's an error, the
// compiler directs the user to the template file instead of the
// generated one. We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
-#line 32 "${template}"
+#line 34 "${template}"
#ifdef CVC4_STATISTICS_ON
#define INC_STAT(kind) \
@@ -340,6 +342,63 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
}
+DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
+ NodeManagerScope nms(d_nodeManager);
+ TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(datatype));
+ Type type(d_nodeManager, typeNode);
+ DatatypeType dtt(type);
+ const Datatype& dt = typeNode->getConst<Datatype>();
+ if(!dt.isResolved()) {
+ std::map<std::string, DatatypeType> resolutions;
+ resolutions.insert(std::make_pair(datatype.getName(), dtt));
+ const_cast<Datatype&>(dt).resolve(this, resolutions);
+ }
+ return dtt;
+}
+
+std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
+ NodeManagerScope nms(d_nodeManager);
+ std::map<std::string, DatatypeType> resolutions;
+ std::vector<DatatypeType> dtts;
+ for(std::vector<Datatype>::const_iterator i = datatypes.begin(), i_end = datatypes.end();
+ i != i_end;
+ ++i) {
+ TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
+ Type type(d_nodeManager, typeNode);
+ DatatypeType dtt(type);
+ CheckArgument(resolutions.find((*i).getName()) == resolutions.end(),
+ datatypes,
+ "cannot construct two datatypes at the same time with the same name `%s'",
+ (*i).getName().c_str());
+ resolutions.insert(std::make_pair((*i).getName(), dtt));
+ dtts.push_back(dtt);
+ }
+ for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end();
+ i != i_end;
+ ++i) {
+ const Datatype& dt = (*i).getDatatype();
+ if(!dt.isResolved()) {
+ const_cast<Datatype&>(dt).resolve(this, resolutions);
+ }
+ }
+ return dtts;
+}
+
+ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& constructor, Type range) const {
+ NodeManagerScope nms(d_nodeManager);
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
+}
+
+SelectorType ExprManager::mkSelectorType(Type domain, Type range) const {
+ NodeManagerScope nms(d_nodeManager);
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode)));
+}
+
+TesterType ExprManager::mkTesterType(Type domain) const {
+ NodeManagerScope nms(d_nodeManager);
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode)));
+}
+
SortType ExprManager::mkSort(const std::string& name) const {
NodeManagerScope nms(d_nodeManager);
return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index f51d6fa28..415d05878 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -5,7 +5,7 @@
** Major contributors: mdeters
** Minor contributors (to current version): taking, 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
@@ -241,20 +241,40 @@ public:
*/
TupleType mkTupleType(const std::vector<Type>& types);
- /** Make a type representing a bit-vector of the given size */
+ /** Make a type representing a bit-vector of the given size. */
BitVectorType mkBitVectorType(unsigned size) const;
- /** Make the type of arrays with the given parameterization */
+ /** Make the type of arrays with the given parameterization. */
ArrayType mkArrayType(Type indexType, Type constituentType) const;
+ /** Make a type representing the given datatype. */
+ DatatypeType mkDatatypeType(const Datatype& datatype);
+
+ /**
+ * Make a set of types representing the given datatypes, which may be
+ * mutually recursive.
+ */
+ std::vector<DatatypeType> mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
+
+ /**
+ * Make a type representing a constructor with the given parameterization.
+ */
+ ConstructorType mkConstructorType(const Datatype::Constructor& constructor, Type range) const;
+
+ /** Make a type representing a selector with the given parameterization. */
+ SelectorType mkSelectorType(Type domain, Type range) const;
+
+ /** Make a type representing a tester with the given parameterization. */
+ TesterType mkTesterType(Type domain) const;
+
/** Make a new sort with the given name. */
SortType mkSort(const std::string& name) const;
- /** Make a new sort from a constructor */
+ /** Make a new sort from a constructor. */
SortType mkSort(SortConstructorType constructor,
const std::vector<TypeNode>& children) const;
- /** Make a sort constructor from a name and arity */
+ /** Make a sort constructor from a name and arity. */
SortConstructorType mkSortConstructor(const std::string& name,
size_t arity) const;
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 1a9722939..489564d5f 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -18,6 +18,13 @@
#include "cvc4_public.h"
+// putting the constant-payload #includes up here allows circularity
+// (some of them may require a completely-defined Expr type). This
+// way, those #includes can forward-declare some stuff to get Expr's
+// getConst<> template instantiations correct, and then #include
+// "expr.h" safely, then go on to completely declare their own stuff.
+${includes}
+
#ifndef __CVC4__EXPR_H
#define __CVC4__EXPR_H
@@ -28,13 +35,11 @@
#include "util/exception.h"
#include "util/language.h"
-${includes}
-
// This is a hack, but an important one: if there's an error, the
// compiler directs the user to the template file instead of the
// generated one. We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
-#line 38 "${template}"
+#line 43 "${template}"
namespace CVC4 {
@@ -576,6 +581,31 @@ public:
static inline void setDepth(std::ostream& out, long depth) {
out.iword(s_iosIndex) = depth;
}
+
+ /**
+ * Set the expression depth on the output stream for the current
+ * stack scope. This makes sure the old depth is reset on the stream
+ * after normal OR exceptional exit from the scope, using the RAII
+ * C++ idiom.
+ */
+ class Scope {
+ std::ostream& d_out;
+ long d_oldDepth;
+
+ public:
+
+ inline Scope(std::ostream& out, long depth) :
+ d_out(out),
+ d_oldDepth(ExprSetDepth::getDepth(out)) {
+ ExprSetDepth::setDepth(out, depth);
+ }
+
+ inline ~Scope() {
+ ExprSetDepth::setDepth(d_out, d_oldDepth);
+ }
+
+ };/* class ExprSetDepth::Scope */
+
};/* class ExprSetDepth */
/**
@@ -621,6 +651,31 @@ public:
static inline void setPrintTypes(std::ostream& out, bool printTypes) {
out.iword(s_iosIndex) = printTypes;
}
+
+ /**
+ * Set the print-types state on the output stream for the current
+ * stack scope. This makes sure the old state is reset on the
+ * stream after normal OR exceptional exit from the scope, using the
+ * RAII C++ idiom.
+ */
+ class Scope {
+ std::ostream& d_out;
+ bool d_oldPrintTypes;
+
+ public:
+
+ inline Scope(std::ostream& out, bool printTypes) :
+ d_out(out),
+ d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) {
+ ExprPrintTypes::setPrintTypes(out, printTypes);
+ }
+
+ inline ~Scope() {
+ ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes);
+ }
+
+ };/* class ExprPrintTypes::Scope */
+
};/* class ExprPrintTypes */
/**
@@ -668,13 +723,38 @@ public:
// (offset by one to detect whether default has been set yet)
out.iword(s_iosIndex) = int(l) + 1;
}
+
+ /**
+ * Set a language on the output stream for the current stack scope.
+ * This makes sure the old language is reset on the stream after
+ * normal OR exceptional exit from the scope, using the RAII C++
+ * idiom.
+ */
+ class Scope {
+ std::ostream& d_out;
+ OutputLanguage d_oldLanguage;
+
+ public:
+
+ inline Scope(std::ostream& out, OutputLanguage language) :
+ d_out(out),
+ d_oldLanguage(ExprSetLanguage::getLanguage(out)) {
+ ExprSetLanguage::setLanguage(out, language);
+ }
+
+ inline ~Scope() {
+ ExprSetLanguage::setLanguage(d_out, d_oldLanguage);
+ }
+
+ };/* class ExprSetLanguage::Scope */
+
};/* class ExprSetLanguage */
}/* CVC4::expr namespace */
${getConst_instantiations}
-#line 676 "${template}"
+#line 682 "${template}"
namespace expr {
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 40bf9992c..da2847d84 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -138,25 +138,26 @@ function constant {
includes="${includes}
#include \"$4\""
mkConst_instantiations="${mkConst_instantiations}
-template <>
-Expr ExprManager::mkConst($2 const& val);
+#line $lineno \"$kf\"
+template <> Expr ExprManager::mkConst($2 const& val);
"
mkConst_implementations="${mkConst_implementations}
-template <>
-Expr ExprManager::mkConst($2 const& val) {
+#line $lineno \"$kf\"
+template <> Expr ExprManager::mkConst($2 const& val) {
+#line $lineno \"$kf\"
return Expr(this, new Node(d_nodeManager->mkConst< $2 >(val)));
}
"
getConst_instantiations="${getConst_instantiations}
-template <>
-$2 const & Expr::getConst< $2 >() const;
+#line $lineno \"$kf\"
+template <> $2 const & Expr::getConst< $2 >() const;
"
getConst_implementations="${getConst_implementations}
-template <>
-$2 const & Expr::getConst() const {
- // check even for production builds
- CheckArgument(getKind() == ::CVC4::kind::$1, *this,
- \"Improper kind for getConst<$2>()\");
+#line $lineno \"$kf\"
+template <> $2 const & Expr::getConst() const {
+#line $lineno \"$kf\"
+ CheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\");
+#line $lineno \"$kf\"
return d_node->getConst< $2 >();
}
"
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 631f73a89..f7f6ba836 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -74,7 +74,7 @@ function theory {
theory_id="$1"
theory_enum="$1,
- ${theory_enum}"
+ ${theory_enum}"
theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break;
"
}
diff --git a/src/expr/node.h b/src/expr/node.h
index 2509640e0..d3775cb3f 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -813,7 +813,7 @@ namespace CVC4 {
// for hash_maps, hash_sets..
struct NodeHashFunction {
- size_t operator()(const CVC4::Node& node) const {
+ size_t operator()(CVC4::Node node) const {
return (size_t) node.getId();
}
};/* struct NodeHashFunction */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 793b701f8..9449594e3 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -2,10 +2,10 @@
/*! \file node_manager.cpp
** \verbatim
** Original author: mdeters
- ** Major contributors: cconway, dejan
- ** Minor contributors (to current version): acsys, taking
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): acsys, taking, dejan
** 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
@@ -26,6 +26,7 @@
#include "theory/arith/theory_arith_type_rules.h"
#include "theory/arrays/theory_arrays_type_rules.h"
#include "theory/bv/theory_bv_type_rules.h"
+#include "theory/datatypes/theory_datatypes_type_rules.h"
#include "util/Assert.h"
#include "util/options.h"
@@ -434,6 +435,15 @@ TypeNode NodeManager::computeType(TNode n, bool check)
case kind::BITVECTOR_SIGN_EXTEND:
typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n, check);
break;
+ case kind::APPLY_CONSTRUCTOR:
+ typeNode = CVC4::theory::datatypes::DatatypeConstructorTypeRule::computeType(this, n, check);
+ break;
+ case kind::APPLY_SELECTOR:
+ typeNode = CVC4::theory::datatypes::DatatypeSelectorTypeRule::computeType(this, n, check);
+ break;
+ case kind::APPLY_TESTER:
+ typeNode = CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(this, n, check);
+ break;
default:
Debug("getType") << "FAILURE" << std::endl;
Unhandled(n.getKind());
@@ -509,4 +519,20 @@ TypeNode NodeManager::getType(TNode n, bool check)
return typeNode;
}
+TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor, TypeNode range) {
+ std::vector<TypeNode> sorts;
+ Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl;
+ for(Datatype::Constructor::const_iterator i = constructor.begin();
+ i != constructor.end();
+ ++i) {
+ Debug("datatypes") << *(*i).getSelector().getType().d_typeNode << std::endl;
+ TypeNode sort = (*(*i).getSelector().getType().d_typeNode)[1];
+ Debug("datatypes") << "ctor sort: " << sort << std::endl;
+ sorts.push_back(sort);
+ }
+ Debug("datatypes") << "ctor range: " << range << std::endl;
+ sorts.push_back(range);
+ return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
+}
+
}/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1760f48c7..7f7d37a52 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -5,7 +5,7 @@
** Major contributors: cconway, dejan
** Minor contributors (to current version): acsys, taking
** 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
@@ -55,8 +55,8 @@ namespace attr {
struct SortArityTag {};
}/* CVC4::expr::attr namespace */
-typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr;
-typedef expr::Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
+typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
+typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
}/* CVC4::expr namespace */
@@ -542,6 +542,15 @@ public:
/** Make the type of arrays with the given parameterization */
inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
+ /** Make a type representing a constructor with the given parameterization */
+ TypeNode mkConstructorType(const Datatype::Constructor& constructor, TypeNode range);
+
+ /** Make a type representing a selector with the given parameterization */
+ inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
+
+ /** Make a type representing a tester with given parameterization */
+ inline TypeNode mkTesterType(TypeNode domain);
+
/** Make a new (anonymous) sort of arity 0. */
inline TypeNode mkSort();
@@ -796,6 +805,14 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
}
+inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
+ return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
+}
+
+inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
+ return mkTypeNode(kind::TESTER_TYPE, domain );
+}
+
inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
if(find == d_nodeValuePool.end()) {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 78554f61f..6dd9c5cec 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -2,10 +2,10 @@
/*! \file type.cpp
** \verbatim
** Original author: cconway
- ** Major contributors: mdeters, dejan
+ ** Major contributors: dejan, mdeters
** 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)
+ ** 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
@@ -186,6 +186,58 @@ Type::operator BitVectorType() const throw(AssertionException) {
return BitVectorType(*this);
}
+/** Cast to a Constructor type */
+Type::operator DatatypeType() const throw(AssertionException) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert(isDatatype());
+ return DatatypeType(*this);
+}
+
+/** Is this the Datatype type? */
+bool Type::isDatatype() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->isDatatype();
+}
+
+/** Cast to a Constructor type */
+Type::operator ConstructorType() const throw(AssertionException) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert(isConstructor());
+ return ConstructorType(*this);
+}
+
+/** Is this the Constructor type? */
+bool Type::isConstructor() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->isConstructor();
+}
+
+/** Cast to a Selector type */
+Type::operator SelectorType() const throw(AssertionException) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert(isSelector());
+ return SelectorType(*this);
+}
+
+/** Is this the Selector type? */
+bool Type::isSelector() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->isSelector();
+}
+
+/** Cast to a Tester type */
+Type::operator TesterType() const throw(AssertionException) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert(isTester());
+ return TesterType(*this);
+}
+
+/** Is this the Tester type? */
+bool Type::isTester() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->isTester();
+}
+
/** Is this a function type? */
bool Type::isFunction() const {
NodeManagerScope nms(d_nodeManager);
@@ -349,6 +401,26 @@ BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
Assert(isBitVector());
}
+DatatypeType::DatatypeType(const Type& t) throw(AssertionException) :
+ Type(t) {
+ Assert(isDatatype());
+}
+
+ConstructorType::ConstructorType(const Type& t) throw(AssertionException) :
+ Type(t) {
+ Assert(isConstructor());
+}
+
+SelectorType::SelectorType(const Type& t) throw(AssertionException) :
+ Type(t) {
+ Assert(isSelector());
+}
+
+TesterType::TesterType(const Type& t) throw(AssertionException) :
+ Type(t) {
+ Assert(isTester());
+}
+
FunctionType::FunctionType(const Type& t) throw(AssertionException) :
Type(t) {
Assert(isFunction());
@@ -392,8 +464,32 @@ Type ArrayType::getConstituentType() const {
return makeType(d_typeNode->getArrayConstituentType());
}
-size_t TypeHashStrategy::hash(const Type& t) {
- return TypeNodeHashStrategy::hash(*t.d_typeNode);
+Type ConstructorType::getReturnType() const {
+ return makeType(d_typeNode->getConstructorReturnType());
+}
+
+const Datatype& DatatypeType::getDatatype() const {
+ return d_typeNode->getConst<Datatype>();
+}
+
+DatatypeType SelectorType::getDomain() const {
+ return DatatypeType(makeType((*d_typeNode)[0]));
+}
+
+Type SelectorType::getRangeType() const {
+ return makeType((*d_typeNode)[1]);
+}
+
+DatatypeType TesterType::getDomain() const {
+ return DatatypeType(makeType((*d_typeNode)[0]));
+}
+
+BooleanType TesterType::getRangeType() const {
+ return BooleanType(makeType(d_nodeManager->booleanType()));
+}
+
+size_t TypeHashFunction::operator()(const Type& t) {
+ return TypeNodeHashFunction()(NodeManager::fromType(t));
}
}/* CVC4 namespace */
diff --git a/src/expr/type.h b/src/expr/type.h
index 130aa3122..3b476ddf5 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -5,7 +5,7 @@
** Major contributors: mdeters, 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)
+ ** 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
@@ -36,6 +36,8 @@ class TypeNode;
class SmtEngine;
+class Datatype;
+
template <bool ref_count>
class NodeTemplate;
@@ -44,6 +46,10 @@ class IntegerType;
class RealType;
class BitVectorType;
class ArrayType;
+class DatatypeType;
+class ConstructorType;
+class SelectorType;
+class TesterType;
class FunctionType;
class TupleType;
class KindType;
@@ -52,10 +58,10 @@ class SortConstructorType;
class Type;
/** Strategy for hashing Types */
-struct CVC4_PUBLIC TypeHashStrategy {
+struct CVC4_PUBLIC TypeHashFunction {
/** Return a hash code for type t */
- static size_t hash(const CVC4::Type& t);
-};/* struct TypeHashStrategy */
+ size_t operator()(const CVC4::Type& t);
+};/* struct TypeHashFunction */
/**
* Output operator for types
@@ -259,6 +265,54 @@ public:
operator ArrayType() const throw(AssertionException);
/**
+ * Is this a datatype type?
+ * @return true if the type is a datatype type
+ */
+ bool isDatatype() const;
+
+ /**
+ * Cast this type to a datatype type
+ * @return the DatatypeType
+ */
+ operator DatatypeType() const throw(AssertionException);
+
+ /**
+ * Is this a constructor type?
+ * @return true if the type is a constructor type
+ */
+ bool isConstructor() const;
+
+ /**
+ * Cast this type to a constructor type
+ * @return the ConstructorType
+ */
+ operator ConstructorType() const throw(AssertionException);
+
+ /**
+ * Is this a selector type?
+ * @return true if the type is a selector type
+ */
+ bool isSelector() const;
+
+ /**
+ * Cast this type to a selector type
+ * @return the SelectorType
+ */
+ operator SelectorType() const throw(AssertionException);
+
+ /**
+ * Is this a tester type?
+ * @return true if the type is a tester type
+ */
+ bool isTester() const;
+
+ /**
+ * Cast this type to a tester type
+ * @return the TesterType
+ */
+ operator TesterType() const throw(AssertionException);
+
+ /**
* Is this a sort kind?
* @return true if this is a sort kind
*/
@@ -449,6 +503,78 @@ public:
unsigned getSize() const;
};/* class BitVectorType */
+
+/**
+ * Class encapsulating the datatype type
+ */
+class CVC4_PUBLIC DatatypeType : public Type {
+
+public:
+
+ /** Construct from the base type */
+ DatatypeType(const Type& type) throw(AssertionException);
+
+ /** Get the underlying datatype */
+ const Datatype& getDatatype() const;
+
+};/* class DatatypeType */
+
+
+/**
+ * Class encapsulating the constructor type
+ */
+class CVC4_PUBLIC ConstructorType : public Type {
+
+public:
+
+ /** Construct from the base type */
+ ConstructorType(const Type& type) throw(AssertionException);
+
+ /** Get the return type */
+ Type getReturnType() const;
+
+};/* class ConstructorType */
+
+
+/**
+ * Class encapsulating the Selector type
+ */
+class CVC4_PUBLIC SelectorType : public Type {
+
+public:
+
+ /** Construct from the base type */
+ SelectorType(const Type& type) throw(AssertionException);
+
+ /** Get the domain type for this selector (the datatype type) */
+ DatatypeType getDomain() const;
+
+ /** Get the range type for this selector (the field type) */
+ Type getRangeType() const;
+
+};/* class SelectorType */
+
+/**
+ * Class encapsulating the Tester type
+ */
+class CVC4_PUBLIC TesterType : public Type {
+
+public:
+
+ /** Construct from the base type */
+ TesterType(const Type& type) throw(AssertionException);
+
+ /** Get the type that this tester tests (the datatype type) */
+ DatatypeType getDomain() const;
+
+ /**
+ * Get the range type for this tester (included for sake of
+ * interface completeness), but doesn't give useful information).
+ */
+ BooleanType getRangeType() const;
+
+};/* class TesterType */
+
}/* CVC4 namespace */
#endif /* __CVC4__TYPE_H */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index badc3b72f..7549af895 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -5,7 +5,7 @@
** Major contributors: mdeters
** Minor contributors (to current version): taking
** 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
@@ -76,28 +76,38 @@ TypeNode TypeNode::getArrayConstituentType() const {
return (*this)[1];
}
-/** Is this a function type? */
+TypeNode TypeNode::getConstructorReturnType() const {
+ Assert(isConstructor());
+ return (*this)[getNumChildren()-1];
+}
+
bool TypeNode::isFunction() const {
return getKind() == kind::FUNCTION_TYPE;
}
-/** Is this a predicate type? NOTE: all predicate types are also
- function types. */
bool TypeNode::isPredicate() const {
return isFunction() && getRangeType().isBoolean();
}
-vector<TypeNode> TypeNode::getArgTypes() const {
- Assert(isFunction());
+std::vector<TypeNode> TypeNode::getArgTypes() const {
vector<TypeNode> args;
- for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
- args.push_back((*this)[i]);
+ if(isTester()) {
+ Assert(getNumChildren() == 1);
+ args.push_back((*this)[0]);
+ } else {
+ Assert(isFunction() || isConstructor() || isSelector());
+ for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
+ args.push_back((*this)[i]);
+ }
}
return args;
}
TypeNode TypeNode::getRangeType() const {
- Assert(isFunction());
+ if(isTester()) {
+ return NodeManager::currentNM()->booleanType();
+ }
+ Assert(isFunction() || isConstructor() || isSelector());
return (*this)[getNumChildren()-1];
}
@@ -137,6 +147,26 @@ bool TypeNode::isBitVector() const {
return getKind() == kind::BITVECTOR_TYPE;
}
+/** Is this a datatype type */
+bool TypeNode::isDatatype() const {
+ return getKind() == kind::DATATYPE_TYPE;
+}
+
+/** Is this a constructor type */
+bool TypeNode::isConstructor() const {
+ return getKind() == kind::CONSTRUCTOR_TYPE;
+}
+
+/** Is this a selector type */
+bool TypeNode::isSelector() const {
+ return getKind() == kind::SELECTOR_TYPE;
+}
+
+/** Is this a tester type */
+bool TypeNode::isTester() const {
+ return getKind() == kind::TESTER_TYPE;
+}
+
/** Is this a bit-vector type of size <code>size</code> */
bool TypeNode::isBitVector(unsigned size) const {
return getKind() == kind::BITVECTOR_TYPE &&
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index ead85cd19..049173867 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -5,7 +5,7 @@
** Major contributors: mdeters
** Minor contributors (to current version): taking
** 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
@@ -360,18 +360,32 @@ public:
/** Get the element type (for array types) */
TypeNode getArrayConstituentType() const;
- /** Is this a function type? */
+ /** Get the return type (for constructor types) */
+ TypeNode getConstructorReturnType() const;
+
+ /**
+ * Is this a function type? Function-like things (e.g. datatype
+ * selectors) that aren't actually functions are NOT considered
+ * functions, here.
+ */
bool isFunction() const;
- /** Get the argument types */
+ /**
+ * Get the argument types of a function, datatype constructor,
+ * datatype selector, or datatype tester.
+ */
std::vector<TypeNode> getArgTypes() const;
- /** Get the range type (i.e., the type of the result). */
+ /**
+ * Get the range type (i.e., the type of the result) of a function,
+ * datatype constructor, datatype selector, or datatype tester.
+ */
TypeNode getRangeType() const;
/**
* Is this a predicate type?
- * NOTE: all predicate types are also function types.
+ * NOTE: all predicate types are also function types (so datatype
+ * testers are not considered "predicates" for the purpose of this function).
*/
bool isPredicate() const;
@@ -387,6 +401,18 @@ public:
/** Is this a bit-vector type of size <code>size</code> */
bool isBitVector(unsigned size) const;
+ /** Is this a datatype type */
+ bool isDatatype() const;
+
+ /** Is this a constructor type */
+ bool isConstructor() const;
+
+ /** Is this a selector type */
+ bool isSelector() const;
+
+ /** Is this a tester type */
+ bool isTester() const;
+
/** Get the size of this bit-vector type */
unsigned getBitVectorSize() const;
@@ -430,11 +456,11 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
}
// for hash_maps, hash_sets..
-struct TypeNodeHashStrategy {
- static inline size_t hash(const TypeNode& node) {
+struct TypeNodeHashFunction {
+ size_t operator()(TypeNode node) const {
return (size_t) node.getId();
}
-};/* struct TypeNodeHashStrategy */
+};/* struct TypeNodeHashFunction */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback