diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 19 | ||||
-rw-r--r-- | src/expr/builtin_kinds | 134 | ||||
-rw-r--r-- | src/expr/builtin_type_rules.h | 56 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 19 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 16 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 6 | ||||
-rw-r--r-- | src/expr/expr_template.h | 24 | ||||
-rw-r--r-- | src/expr/metakind_template.h | 4 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 4 | ||||
-rw-r--r-- | src/expr/node.cpp | 6 | ||||
-rw-r--r-- | src/expr/node.h | 10 | ||||
-rw-r--r-- | src/expr/node_builder.h | 18 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 23 | ||||
-rw-r--r-- | src/expr/node_manager.h | 54 | ||||
-rw-r--r-- | src/expr/type.cpp | 37 | ||||
-rw-r--r-- | src/expr/type.h | 39 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 14 | ||||
-rw-r--r-- | src/expr/type_node.h | 35 |
18 files changed, 246 insertions, 272 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 2b5bdbdb3..225624a8b 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -10,7 +10,6 @@ libexpr_la_SOURCES = \ node.cpp \ type_node.h \ type_node.cpp \ - builtin_type_rules.h \ node_builder.h \ convenience_node_builders.h \ @srcdir@/expr.h \ @@ -51,57 +50,51 @@ EXTRA_DIST = \ include @top_srcdir@/src/theory/Makefile.subdirs -@srcdir@/kind.h: kind_template.h mkkind builtin_kinds @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +@srcdir@/kind.h: kind_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkkind $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkkind \ $< \ - @srcdir@/builtin_kinds \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) -@srcdir@/metakind.h: metakind_template.h mkmetakind builtin_kinds @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +@srcdir@/metakind.h: metakind_template.h mkmetakind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkmetakind $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkmetakind \ $< \ - @srcdir@/builtin_kinds \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) -@srcdir@/expr.h: expr_template.h mkexpr builtin_kinds @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +@srcdir@/expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ - @srcdir@/builtin_kinds \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) -@srcdir@/expr.cpp: expr_template.cpp mkexpr builtin_kinds @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +@srcdir@/expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ - @srcdir@/builtin_kinds \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) -@srcdir@/expr_manager.h: expr_manager_template.h mkexpr builtin_kinds @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +@srcdir@/expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ - @srcdir@/builtin_kinds \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) -@srcdir@/expr_manager.cpp: expr_manager_template.cpp mkexpr builtin_kinds @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds +@srcdir@/expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ - @srcdir@/builtin_kinds \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds deleted file mode 100644 index 50b858b31..000000000 --- a/src/expr/builtin_kinds +++ /dev/null @@ -1,134 +0,0 @@ -# builtin_kinds -*- sh -*- -# -# This "kinds" file is written in a domain-specific language for -# declaring CVC4 kinds. Comments are marked with #, as this line is. -# -# The first non-blank, non-comment line in this file must be a theory -# declaration: -# -# theory T header -# -# There are four basic commands for declaring kinds: -# -# variable K ["comment"] -# -# This declares a kind K that has no operator (it's conceptually a -# VARIABLE). This is appropriate for things like VARIABLE and -# SKOLEM. -# -# operator K #children ["comment"] -# -# Declares a "built-in" operator kind K. Really this is the same -# as "variable" except that it has an operator (automatically -# generated by NodeManager). -# -# You can specify an exact # of children required as the second -# argument to the operator command. In debug mode, assertions are -# automatically included to ensure that no Nodes can ever be -# created violating this. (FIXME: the public Expr stuff should -# enforce them regardless of whether debugging or not.) For -# example, a binary operator could be specified as: -# -# operator LESS_THAN 2 "arithmetic comparison, x < y" -# -# Alternatively, a range can be specified for #children as -# "LB:[UB]", LB and UB representing lower and upper bounds on the -# number of children (inclusive). If there is no lower bound, put -# a "0". If there is no upper bound, leave the colon after LB, -# but omit UB. For example, an N-ary operator might be defined -# as: -# -# operator PLUS 2: "addition on two or more arguments" -# -# parameterized K #children ["comment"] -# -# Declares a "built-in" parameterized operator kind K. This is a -# theory-specific APPLY, e.g., APPLY_UF, which applies its first -# parameter (say, "f"), to its operands (say, "x" and "y", making -# the full application "f(x,y)"). Nodes with such a kind will -# have an operator (Node::hasOperator() returns true, and -# Node::getOperator() returns the Node of functional type -# representing "f" here), and the "children" are defined to be -# this operator's parameters, and don't include the operator -# itself (here, there are only two children "x" and "y"). -# -# LB and UB are the same as documented for the operator command. -# The first parameter (the function being applied) does not count -# as a child. -# -# For consistency these should start with "APPLY_", but this is -# not enforced. -# -# constant K T Hasher header ["comment"] -# -# Declares a constant kind K. T is the C++ type representing the -# constant internally (and it should be -# ::fully::qualified::like::this), and header is the header needed -# to define it. Hasher is a hash functor type defined like this: -# -# struct MyHashFcn { -# static size_t hash(const T& val); -# }; -# -# For consistency, constants taking a non-void payload should -# start with "CONST_", but this is not enforced. -# -# Lines may be broken with a backslash between arguments; for example: -# -# constant CONST_INT \ -# int IntHash \ -# "" \ -# "This is a constant representing an INT. -# Its payload is the C++ int type. -# It is used by the theory of arithmetic." -# -# As shown in the example, ["comment"] fields may be broken across -# multiple lines too. -# -# The expr package guarantees that Nodes built with kinds have the -# following constraints imposed on them. (The #children guarantee -# only holds when assertions are turned on.) -# -# Node meta-kind has operator? # children -# ================== ================= ======================= -# variable no zero -# operator yes as documented above -# parameterized yes as documented above -# constant no zero -# -# NOTE THAT This file is actually an executable Bourne shell script -# (sourced by the processing scripts after defining functions called -# "theory," "variable," "operator," "parameterized," and "constant"). -# Please don't do anything else in this file other than using these -# commands. -# - -theory builtin - -# A kind representing "inlined" operators defined with OPERATOR -# Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's -# not stored that way. If you ask for the operator of (EQUAL a b), -# you'll get a special, singleton (BUILTIN EQUAL) Node. -constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \ - "expr/kind.h" "The kind of nodes representing built-in operators" - -operator EQUAL 2 "equality" -operator DISTINCT 2: "disequality" -variable SKOLEM "skolem var" -variable VARIABLE "variable" -operator TUPLE 2: "a tuple" - -constant TYPE_CONSTANT \ - ::CVC4::TypeConstant \ - ::CVC4::TypeConstantHashStrategy \ - "expr/type_constant.h" \ - "basic types" -operator FUNCTION_TYPE 2: "function type" -variable SORT_TYPE "sort type" - -constant BITVECTOR_TYPE \ - ::CVC4::BitVectorSize \ - "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \ - "util/bitvector.h" \ - "bit-vector type" - diff --git a/src/expr/builtin_type_rules.h b/src/expr/builtin_type_rules.h deleted file mode 100644 index afd206260..000000000 --- a/src/expr/builtin_type_rules.h +++ /dev/null @@ -1,56 +0,0 @@ -/********************* */ -/*! \file builtin_type_rules.cpp - ** \verbatim - ** Original author: dejan - ** Major contributors: 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.\endverbatim - ** - ** \brief [[ Add brief comments here ]] - ** - ** [[ Add file-specific comments here ]] - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__BUILTIN_TYPE_RULES_H_ -#define __CVC4__BUILTIN_TYPE_RULES_H_ - -#include "expr/node.h" -#include "expr/type_node.h" -#include "expr/expr.h" - -namespace CVC4 { - -class EqualityTypeRule { - public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingExceptionPrivate) { - if (n[0].getType() != n[1].getType()) { - throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type"); - } - return nodeManager->booleanType(); - } -}; - -class DistinctTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) { - TNode::iterator child_it = n.begin(); - TNode::iterator child_it_end = n.end(); - TypeNode firstType = (*child_it).getType(); - for (++child_it; child_it != child_it_end; ++child_it) { - if ((*child_it).getType() != firstType) { - throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type"); - } - } - return nodeManager->booleanType(); - } -}; - -} - -#endif /* __CVC4__BUILTIN_TYPE_RULES_H_ */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 3eb2a8109..f28729b94 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -31,7 +31,7 @@ ${includes} // 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 35 "${template}" using namespace std; using namespace CVC4::context; @@ -69,11 +69,6 @@ IntegerType ExprManager::integerType() const { return Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())); } -BitVectorType ExprManager::bitVectorType(unsigned size) const { - NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->bitVectorType(size))); -} - Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { const unsigned n = 1; CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, @@ -216,7 +211,17 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { return Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))); } -SortType ExprManager::mkSort(const std::string& name) { +BitVectorType ExprManager::mkBitVectorType(unsigned size) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size))); +} + +ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))); +} + +SortType ExprManager::mkSort(const std::string& name) const { NodeManagerScope nms(d_nodeManager); return 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 707d9a26e..450d7fc4d 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -33,7 +33,7 @@ ${includes} // 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 33 "${template}" +#line 37 "${template}" namespace CVC4 { @@ -100,9 +100,6 @@ public: /** Get the type for integers */ IntegerType integerType() const; - /** The the type for bit-vectors */ - BitVectorType bitVectorType(unsigned size) const; - /** * Make a unary expression of a given kind (NOT, BVNOT, ...). * @param child1 kind the kind of expression @@ -214,8 +211,14 @@ public: */ FunctionType mkPredicateType(const std::vector<Type>& sorts); + /** 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 */ + ArrayType mkArrayType(Type indexType, Type constituentType) const; + /** Make a new sort with the given name. */ - SortType mkSort(const std::string& name); + SortType mkSort(const std::string& name) const; /** Get the type of an expression */ Type getType(const Expr& e) throw (TypeCheckingException); @@ -230,7 +233,8 @@ public: /** Returns the maximum arity of the given kind. */ static unsigned maxArity(Kind kind); - /** Signals that this expression manager will soon be destroyed. + /** + * Signals that this expression manager will soon be destroyed. * Turns off debugging assertions that may not hold as the system * is being torn down. * diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index b4359cf2a..05d31499d 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -36,6 +36,12 @@ using namespace CVC4::kind; namespace CVC4 { +namespace expr { + +const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); + +}/* CVC4::expr namespace */ + std::ostream& operator<<(std::ostream& out, const Expr& e) { e.toStream(out); return out; diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 1723f0258..1749971a5 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -32,7 +32,7 @@ ${includes} // 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 33 "${template}" +#line 36 "${template}" namespace CVC4 { @@ -43,7 +43,7 @@ class NodeTemplate; class Expr; namespace expr { - class NodeSetDepth; + class CVC4_PUBLIC ExprSetDepth; }/* CVC4::expr namespace */ /** @@ -262,7 +262,7 @@ public: * * gives "(OR a b (...))" */ - typedef expr::NodeSetDepth setdepth; + typedef expr::ExprSetDepth setdepth; /** * Very basic pretty printer for Expr. @@ -382,8 +382,6 @@ public: Expr iteExpr(const Expr& then_e, const Expr& else_e) const; }; -${getConst_instantiations} - namespace expr { /** @@ -405,7 +403,7 @@ namespace expr { * allocated word in ios_base), and serves also as the manipulator * itself (as above). */ -class NodeSetDepth { +class CVC4_PUBLIC ExprSetDepth { /** * The allocated index in ios_base for our depth setting. */ @@ -424,9 +422,9 @@ class NodeSetDepth { public: /** - * Construct a NodeSetDepth with the given depth. + * Construct a ExprSetDepth with the given depth. */ - NodeSetDepth(long depth) : d_depth(depth) {} + ExprSetDepth(long depth) : d_depth(depth) {} inline void applyDepth(std::ostream& out) { out.iword(s_iosIndex) = d_depth; @@ -446,6 +444,14 @@ public: } }; +}/* CVC4::expr namespace */ + +${getConst_instantiations} + +#line 388 "${template}" + +namespace expr { + /** * Sets the default depth when pretty-printing a Node to an ostream. * Use like this: @@ -455,7 +461,7 @@ public: * * The depth stays permanently (until set again) with the stream. */ -inline std::ostream& operator<<(std::ostream& out, NodeSetDepth sd) { +inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) { sd.applyDepth(out); return out; } diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 079199359..80bf37220 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -26,8 +26,6 @@ #include "expr/kind.h" #include "util/Assert.h" -${metakind_includes} - namespace CVC4 { namespace expr { @@ -187,6 +185,8 @@ struct NodeValuePoolEq { #endif /* __CVC4__KIND__METAKIND_H */ +${metakind_includes} + #ifdef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP namespace CVC4 { diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index cf3fb1e97..079bea861 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -75,10 +75,8 @@ function theory { fi theory_class=$1 - if [ "$1" != builtin ]; then - metakind_includes="${metakind_includes} + metakind_includes="${metakind_includes} // #include \"theory/$b/$2\"" - fi } function variable { diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 2b6417e8a..6b689034a 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -24,12 +24,6 @@ using namespace std; namespace CVC4 { -namespace expr { - -const int NodeSetDepth::s_iosIndex = std::ios_base::xalloc(); - -}/* CVC4::expr namespace */ - TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, std::string message) : Exception(message), d_node(new Node(node)) diff --git a/src/expr/node.h b/src/expr/node.h index 8618bce4d..e3fb42ead 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -99,7 +99,7 @@ class NodeValue; class AttributeManager; }/* CVC4::expr::attr namespace */ - class NodeSetDepth; + class ExprSetDepth; }/* CVC4::expr namespace */ /** @@ -304,7 +304,8 @@ public: * Returns the type of this node. * @return the type */ - TypeNode getType() const throw (CVC4::TypeCheckingExceptionPrivate); + TypeNode getType() const + throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException); /** * Returns the kind of this node. @@ -476,7 +477,7 @@ public: * * gives "(OR a b (...))" */ - typedef expr::NodeSetDepth setdepth; + typedef expr::ExprSetDepth setdepth; /** * Very basic pretty printer for Node. @@ -879,7 +880,8 @@ inline bool NodeTemplate<ref_count>::hasOperator() const { } template <bool ref_count> -TypeNode NodeTemplate<ref_count>::getType() const throw (CVC4::TypeCheckingExceptionPrivate) { +TypeNode NodeTemplate<ref_count>::getType() const + throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException) { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index d81190d7a..0cb9ed026 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -566,6 +566,24 @@ public: return append(n); } + /** + * If this Node-under-construction has a Kind set, collapse it and + * append the given Node as a child. Otherwise, simply append. + * FIXME: do we really want that collapse behavior? We had agreed + * on it but then never wrote code like that. + */ + NodeBuilder<nchild_thresh>& operator<<(TypeNode n) { + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); + /* FIXME: disable this "collapsing" for now.. + if(EXPECT_FALSE( getKind() != kind::UNDEFINED_KIND )) { + Node n2 = operator Node(); + clear(); + append(n2); + }*/ + return append(n); + } + /** Append a sequence of children to this TypeNode-under-construction. */ inline NodeBuilder<nchild_thresh>& append(const std::vector<TypeNode>& children) { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 6e2141351..8f7196e0c 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -20,10 +20,11 @@ #include "node_manager.h" -#include "expr/builtin_type_rules.h" +#include "theory/builtin/theory_builtin_type_rules.h" #include "theory/booleans/theory_bool_type_rules.h" #include "theory/uf/theory_uf_type_rules.h" #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 <ext/hash_set> @@ -181,17 +182,19 @@ void NodeManager::reclaimZombies() { } }/* NodeManager::reclaimZombies() */ -TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) { +TypeNode NodeManager::getType(TNode n) + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode typeNode; bool hasType = getAttribute(n, TypeAttr(), typeNode); - if (!hasType) { + Debug("getType") << "getting type for " << n << std::endl; + if(!hasType) { // Infer the type - switch (n.getKind()) { + switch(n.getKind()) { case kind::EQUAL: - typeNode = CVC4::EqualityTypeRule::computeType(this, n); + typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n); break; case kind::DISTINCT: - typeNode = CVC4::DistinctTypeRule::computeType(this, n); + typeNode = CVC4::theory::builtin::DistinctTypeRule::computeType(this, n); break; case kind::CONST_BOOLEAN: typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n); @@ -253,6 +256,12 @@ TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) { case kind::GEQ: typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n); break; + case kind::SELECT: + typeNode = CVC4::theory::arrays::ArraySelectTypeRule::computeType(this, n); + break; + case kind::STORE: + typeNode = CVC4::theory::arrays::ArrayStoreTypeRule::computeType(this, n); + break; case kind::BITVECTOR_CONST: typeNode = CVC4::theory::bv::BitVectorConstantTypeRule::computeType(this, n); break; @@ -362,10 +371,12 @@ TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) { typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n); break; default: + Debug("getType") << "FAILURE" << std::endl; Unhandled(n.getKind()); } setAttribute(n, TypeAttr(), typeNode); } + Debug("getType") << "type of " << n << " is " << typeNode << std::endl; return typeNode; } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 7e0cfd0cf..3586440d4 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -329,7 +329,11 @@ public: template <class NodeClass, class T> NodeClass mkConstInternal(const T&); - /** Create a node with no children. */ + /** Create a node with children. */ + TypeNode mkTypeNode(Kind kind, TypeNode child1); + TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2); + TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2, + TypeNode child3); TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children); /** @@ -472,9 +476,6 @@ public: /** Get the (singleton) type for sorts. */ inline TypeNode kindType(); - /** Get the type of bitvectors of size <code>size</code> */ - inline TypeNode bitVectorType(unsigned size); - /** * Make a function type from domain to range. * @@ -492,7 +493,8 @@ public: * @param range the range type * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range */ - inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range); + inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes, + const TypeNode& range); /** * Make a function type with input types from @@ -510,6 +512,12 @@ public: */ inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts); + /** Make the type of bitvectors of size <code>size</code> */ + inline TypeNode mkBitVectorType(unsigned size); + + /** Make the type of arrays with the given parameterization */ + inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); + /** Make a new sort. */ inline TypeNode mkSort(); @@ -519,7 +527,8 @@ public: /** * Get the type for the given node. */ - TypeNode getType(TNode n) throw (TypeCheckingExceptionPrivate); + TypeNode getType(TNode n) + throw (TypeCheckingExceptionPrivate, AssertionException); }; @@ -637,10 +646,6 @@ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE)); } -inline TypeNode NodeManager::bitVectorType(unsigned size) { - return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size))); -} - /** Make a function type from domain to range. */ inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) { std::vector<TypeNode> sorts; @@ -677,6 +682,15 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); } +inline TypeNode NodeManager::mkBitVectorType(unsigned size) { + return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size))); +} + +inline TypeNode NodeManager::mkArrayType(TypeNode indexType, + TypeNode constituentType) { + return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); +} + inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); if(find == d_nodeValuePool.end()) { @@ -836,8 +850,23 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, } +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) { + return (NodeBuilder<1>(this, kind) << child1).constructTypeNode(); +} + +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, + TypeNode child2) { + return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode(); +} + +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, + TypeNode child2, TypeNode child3) { + return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();; +} + // N-ary version for types -inline TypeNode NodeManager::mkTypeNode(Kind kind, const std::vector<TypeNode>& children) { +inline TypeNode NodeManager::mkTypeNode(Kind kind, + const std::vector<TypeNode>& children) { return NodeBuilder<>(this, kind).append(children).constructTypeNode(); } @@ -848,7 +877,8 @@ inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { return n; } -inline Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) { +inline Node* NodeManager::mkVarPtr(const std::string& name, + const TypeNode& type) { Node* n = mkVarPtr(type); n->setAttribute(expr::VarNameAttr(), name); return n; diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 3bacb4792..069f38ce0 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -150,8 +150,10 @@ bool Type::isFunction() const { return d_typeNode->isFunction(); } -/** Is this a predicate type? NOTE: all predicate types are also - function types. */ +/** + * Is this a predicate type? NOTE: all predicate types are also + * function types. + */ bool Type::isPredicate() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isPredicate(); @@ -164,6 +166,18 @@ Type::operator FunctionType() const throw (AssertionException) { return FunctionType(*this); } +/** Is this an array type? */ +bool Type::isArray() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isArray(); +} + +/** Cast to an array type */ +Type::operator ArrayType() const throw (AssertionException) { + NodeManagerScope nms(d_nodeManager); + return ArrayType(*this); +} + /** Is this a sort kind */ bool Type::isSort() const { NodeManagerScope nms(d_nodeManager); @@ -243,6 +257,12 @@ FunctionType::FunctionType(const Type& t) throw (AssertionException) Assert(isFunction()); } +ArrayType::ArrayType(const Type& t) throw (AssertionException) +: Type(t) +{ + Assert(isArray()); +} + KindType::KindType(const Type& t) throw (AssertionException) : Type(t) { @@ -255,9 +275,20 @@ SortType::SortType(const Type& t) throw (AssertionException) Assert(isSort()); } - unsigned BitVectorType::getSize() const { return d_typeNode->getBitVectorSize(); } +Type ArrayType::getIndexType() const { + return makeType(d_typeNode->getArrayIndexType()); +} + +Type ArrayType::getConstituentType() const { + return makeType(d_typeNode->getArrayConstituentType()); +} + +size_t TypeHashStrategy::hash(const Type& t) { + return TypeNodeHashStrategy::hash(*t.d_typeNode); +} + }/* CVC4 namespace */ diff --git a/src/expr/type.h b/src/expr/type.h index 2d18c2fc8..2862286ae 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -41,9 +41,17 @@ class BooleanType; class IntegerType; class RealType; class BitVectorType; +class ArrayType; class FunctionType; class KindType; class SortType; +class Type; + +/** Strategy for hashing Types */ +struct CVC4_PUBLIC TypeHashStrategy { + /** Return a hash code for type t */ + static size_t hash(const CVC4::Type& t); +};/* struct TypeHashStrategy */ /** * Class encapsulating CVC4 expression types. @@ -51,6 +59,8 @@ class SortType; class CVC4_PUBLIC Type { friend class ExprManager; + friend class TypeNode; + friend class TypeHashStrategy; protected: @@ -191,6 +201,18 @@ public: operator FunctionType() const throw (AssertionException); /** + * Is this a function type? + * @return true if the type is a Boolean type + */ + bool isArray() const; + + /** + * Cast this type to an array type + * @return the ArrayType + */ + operator ArrayType() const throw (AssertionException); + + /** * Is this a sort kind? * @return true if this is a sort kind */ @@ -273,6 +295,23 @@ public: }; /** + * Class encapsulating a function type. + */ +class CVC4_PUBLIC ArrayType : public Type { + +public: + + /** Construct from the base type */ + ArrayType(const Type& type) throw (AssertionException); + + /** Get the index type */ + Type getIndexType() const; + + /** Get the constituent type */ + Type getConstituentType() const; +}; + +/** * Class encapsulating a user-defined sort. */ class CVC4_PUBLIC SortType : public Type { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 1afaf2b89..6f8911280 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -35,6 +35,20 @@ bool TypeNode::isReal() const { && (getConst<TypeConstant>() == REAL_TYPE || getConst<TypeConstant>() == INTEGER_TYPE); } +bool TypeNode::isArray() const { + return getKind() == kind::ARRAY_TYPE; +} + +TypeNode TypeNode::getArrayIndexType() const { + Assert(isArray()); + return (*this)[0]; +} + +TypeNode TypeNode::getArrayConstituentType() const { + Assert(isArray()); + return (*this)[1]; +} + /** Is this a function type? */ bool TypeNode::isFunction() const { return getKind() == kind::FUNCTION_TYPE; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 9b67c674c..da277a382 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -39,7 +39,7 @@ namespace CVC4 { class NodeManager; namespace expr { -class NodeValue; + class NodeValue; }/* CVC4::expr namespace */ /** @@ -115,7 +115,9 @@ public: * @return true if expressions are equal, false otherwise */ bool operator==(const TypeNode& typeNode) const { - return d_nv == typeNode.d_nv || (typeNode.isReal() && this->isReal()); + return + d_nv == typeNode.d_nv + || (typeNode.isReal() && this->isReal()); } /** @@ -306,6 +308,15 @@ public: /** Is this the Real type? */ bool isReal() const; + /** Is this an array type? */ + bool isArray() const; + + /** Get the index type (for array types) */ + TypeNode getArrayIndexType() const; + + /** Get the element type (for array types) */ + TypeNode getArrayConstituentType() const; + /** Is this a function type? */ bool isFunction() const; @@ -315,8 +326,10 @@ public: /** Get the range type (i.e., the type of the result). */ TypeNode getRangeType() const; - /** Is this a predicate type? NOTE: all predicate types are also - function types. */ + /** + * Is this a predicate type? + * NOTE: all predicate types are also function types. + */ bool isPredicate() const; /** Is this a bit-vector type */ @@ -360,6 +373,13 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { return out; } +// for hash_maps, hash_sets.. +struct TypeNodeHashStrategy { + static inline size_t hash(const CVC4::TypeNode& node) { + return (size_t) node.getId(); + } +};/* struct TypeNodeHashStrategy */ + }/* CVC4 namespace */ #include <ext/hash_map> @@ -368,13 +388,6 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { namespace CVC4 { -// for hash_maps, hash_sets.. -struct TypeNodeHashFunction { - size_t operator()(const CVC4::TypeNode& node) const { - return (size_t) node.getId(); - } -}; - inline size_t TypeNode::getNumChildren() const { return d_nv->getNumChildren(); } |