summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/Makefile.am19
-rw-r--r--src/expr/builtin_kinds134
-rw-r--r--src/expr/builtin_type_rules.h56
-rw-r--r--src/expr/expr_manager_template.cpp19
-rw-r--r--src/expr/expr_manager_template.h16
-rw-r--r--src/expr/expr_template.cpp6
-rw-r--r--src/expr/expr_template.h24
-rw-r--r--src/expr/metakind_template.h4
-rwxr-xr-xsrc/expr/mkmetakind4
-rw-r--r--src/expr/node.cpp6
-rw-r--r--src/expr/node.h10
-rw-r--r--src/expr/node_builder.h18
-rw-r--r--src/expr/node_manager.cpp23
-rw-r--r--src/expr/node_manager.h54
-rw-r--r--src/expr/type.cpp37
-rw-r--r--src/expr/type.h39
-rw-r--r--src/expr/type_node.cpp14
-rw-r--r--src/expr/type_node.h35
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();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback