node.cpp \
type_node.h \
type_node.cpp \
- builtin_type_rules.h \
node_builder.h \
convenience_node_builders.h \
@srcdir@/expr.h \
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)
+++ /dev/null
-# 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"
-
+++ /dev/null
-/********************* */
-/*! \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_ */
// 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;
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,
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)));
}
// 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 {
/** 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
*/
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);
/** 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.
*
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;
// 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 {
class Expr;
namespace expr {
- class NodeSetDepth;
+ class CVC4_PUBLIC ExprSetDepth;
}/* CVC4::expr namespace */
/**
*
* gives "(OR a b (...))"
*/
- typedef expr::NodeSetDepth setdepth;
+ typedef expr::ExprSetDepth setdepth;
/**
* Very basic pretty printer for Expr.
Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
};
-${getConst_instantiations}
-
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.
*/
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;
}
};
+}/* 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:
*
* 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;
}
#include "expr/kind.h"
#include "util/Assert.h"
-${metakind_includes}
-
namespace CVC4 {
namespace expr {
#endif /* __CVC4__KIND__METAKIND_H */
+${metakind_includes}
+
#ifdef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
namespace CVC4 {
fi
theory_class=$1
- if [ "$1" != builtin ]; then
- metakind_includes="${metakind_includes}
+ metakind_includes="${metakind_includes}
// #include \"theory/$b/$2\""
- fi
}
function variable {
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))
class AttributeManager;
}/* CVC4::expr::attr namespace */
- class NodeSetDepth;
+ class ExprSetDepth;
}/* CVC4::expr namespace */
/**
* 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.
*
* gives "(OR a b (...))"
*/
- typedef expr::NodeSetDepth setdepth;
+ typedef expr::ExprSetDepth setdepth;
/**
* Very basic pretty printer for Node.
}
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 ?" );
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) {
#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>
}
}/* 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);
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;
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;
}
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);
/**
/** 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.
*
* @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
*/
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();
/**
* Get the type for the given node.
*/
- TypeNode getType(TNode n) throw (TypeCheckingExceptionPrivate);
+ TypeNode getType(TNode n)
+ throw (TypeCheckingExceptionPrivate, AssertionException);
};
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;
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()) {
}
+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();
}
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;
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();
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);
Assert(isFunction());
}
+ArrayType::ArrayType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+ Assert(isArray());
+}
+
KindType::KindType(const Type& t) throw (AssertionException)
: Type(t)
{
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 */
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.
class CVC4_PUBLIC Type {
friend class ExprManager;
+ friend class TypeNode;
+ friend class TypeHashStrategy;
protected:
*/
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
Type getRangeType() const;
};
+/**
+ * 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.
*/
&& (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;
class NodeManager;
namespace expr {
-class NodeValue;
+ class NodeValue;
}/* CVC4::expr namespace */
/**
* @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());
}
/**
/** 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;
/** 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 */
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>
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();
}
opts->strictParsing = true;
break;
- case DEFAULT_EXPR_DEPTH: {
+ case DEFAULT_EXPR_DEPTH:
+ {
int depth = atoi(optarg);
Debug.getStream() << Expr::setdepth(depth);
Trace.getStream() << Expr::setdepth(depth);
#include <signal.h>
#include "util/exception.h"
+#include "util/Assert.h"
#include "cvc4autoconfig.h"
#include "main.h"
"\n"
"CVC4 threw an \"unexpected\" exception (one that wasn't properly specified\n"
"in the throws() specifier for the throwing function).\n\n");
+ if(CVC4::s_debugAssertionFailure == NULL) {
+ fprintf(stderr, "The exception is unknown.\n\n");
+ } else {
+ fprintf(stderr, "The exception is:\n%s\n\n", CVC4::s_debugAssertionFailure);
+ }
if(segvNoSpin) {
fprintf(stderr, "No-spin requested.\n");
set_terminate(default_terminator);
ANTLR3_MARKER end = token->getStopIndex(token);
Assert( start < end );
if( index > (size_t) end - start ) {
- stringstream ss;
+ std::stringstream ss;
ss << "Out-of-bounds substring index: " << index;
throw std::invalid_argument(ss.str());
}
;
/**
- * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns
+ * Matches a benchmark attribute, such as ':logic', ':formula', and returns
* a corresponding command
* @return a command corresponding to the attribute
*/
| IFF_TOK { $kind = CVC4::kind::IFF; }
| EQUAL_TOK { $kind = CVC4::kind::EQUAL; }
| DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
- // Arithmetic
+ // Arithmetic
| GREATER_THAN_TOK
{ $kind = CVC4::kind::GT; }
| GREATER_THAN_TOK EQUAL_TOK
| BVSLE_TOK { $kind = CVC4::kind::BITVECTOR_SLE; }
| BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; }
| BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; }
- // NOTE: Theory operators go here
+ // arrays
| SELECT_TOK { $kind = CVC4::kind::SELECT; }
| STORE_TOK { $kind = CVC4::kind::STORE; }
+ // NOTE: Theory operators go here
;
/**
: sortName[name,CHECK_NONE]
{ $t = PARSER_STATE->getSort(name); }
| BITVECTOR_TOK '[' NUMERAL_TOK ']' {
- $t = EXPR_MANAGER->bitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK));
+ $t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK));
}
;
| MINUS_TOK { $kind = CVC4::kind::MINUS; }
| SELECT_TOK { $kind = CVC4::kind::SELECT; }
| STORE_TOK { $kind = CVC4::kind::STORE; }
- // NOTE: Theory operators go here
+ // NOTE: Theory operators go here
;
/**
<< " strict? " << (bool)(PARSER_STATE->strictModeEnabled())
<< " ^0? " << (bool)(*start == '0')
<< " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1))
- << endl; }
+ << std::endl; }
{ !PARSER_STATE->strictModeEnabled() ||
*start != '0' ||
start == (char*)(GETCHARINDEX() - 1) }?
// If any literals, make a clause
const unsigned i_end = outputNodes.size();
for (unsigned i = 0; i < i_end; ++ i) {
- Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << endl;
+ Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << std::endl;
// The second argument ("true") instructs the CNF stream to create
// a new literal mapping if it doesn't exist. This can happen due
// to a circular dependence, if a SAT literal "a" is asserted as a
void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) {
TNode lNode = d_cnfStream->getNode(l);
- Debug("prop-explain") << "explainPropagation(" << lNode.toString() << ")" << endl;
+ Debug("prop-explain") << "explainPropagation(" << lNode.toString() << ")" << std::endl;
Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
- Debug("prop-explain") << "explainPropagation() => " << theoryExplanation.toString() << endl;
+ Debug("prop-explain") << "explainPropagation() => " << theoryExplanation.toString() << std::endl;
if (lNode.getKind() == kind::AND) {
Node::const_iterator it = theoryExplanation.begin();
Node::const_iterator it_end = theoryExplanation.end();
theory.cpp
libtheory_la_LIBADD = \
+ @builddir@/builtin/libbuiltin.la \
@builddir@/booleans/libbooleans.la \
@builddir@/uf/libuf.la \
@builddir@/arith/libarith.la \
dist-hook: @srcdir@/theoryof_table.h
MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h
-SUBDIRS = booleans uf arith arrays bv
+SUBDIRS = builtin booleans uf arith arrays bv
}
}else{
d_nonbasic.insert(x_j);
- d_coeffs.insert(make_pair(x_j,a_sj));
+ d_coeffs.insert(std::make_pair(x_j,a_sj));
}
}
}
d_activeRows.erase(basic);
d_activeBasicVars.erase(basic);
- d_inactiveRows.insert(make_pair(basic, row));
+ d_inactiveRows.insert(std::make_pair(basic, row));
}
void reinjectBasic(TNode basic){
d_inactiveRows.erase(basic);
d_activeBasicVars.insert(basic);
- d_activeRows.insert(make_pair(basic, row));
+ d_activeRows.insert(std::make_pair(basic, row));
updateRow(row);
}
return sum;
}
+RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
+ // Look for multiplications with a 0 argument and rewrite the whole
+ // thing as 0
+ if(n.getKind() == MULT) {
+ Rational ratZero;
+ Integer intZero;
+ for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+ if((*i).getKind() == CONST_RATIONAL) {
+ if((*i).getConst<Rational>() == ratZero) {
+ n = NodeManager::currentNM()->mkConst(ratZero);
+ break;
+ }
+ } else if((*i).getKind() == CONST_INTEGER) {
+ if((*i).getConst<Integer>() == intZero) {
+ if(n.getType().isInteger()) {
+ n = NodeManager::currentNM()->mkConst(intZero);
+ break;
+ } else {
+ n = NodeManager::currentNM()->mkConst(ratZero);
+ break;
+ }
+ }
+ }
+ }
+ }
+ return RewritingComplete(Node(n));
+}
+
Node TheoryArith::rewrite(TNode n){
Debug("arith") << "rewrite(" << n << ")" << endl;
namespace theory {
namespace arith {
-
/**
* Implementation of QF_LRA.
* Based upon:
*/
Node rewrite(TNode n);
+ /**
+ * Rewriting optimizations.
+ */
+ RewriteResponse preRewrite(TNode n, bool topLevel);
+
+ /**
+ * Plug in old rewrite to the new (pre,post)rewrite interface.
+ */
+ RewriteResponse postRewrite(TNode n, bool topLevel) {
+ return RewritingComplete(topLevel ? rewrite(n) : Node(n));
+ }
+
/**
* Does non-context dependent setup for a node connected to a theory.
*/
void shutdown(){ }
+ std::string identify() const { return std::string("TheoryArith"); }
private:
/**
Statistics d_statistics;
-};
+};/* class TheoryArith */
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY_ARITH_TYPE_RULES_H_
-#define __CVC4__THEORY_ARITH_TYPE_RULES_H_
+#ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
namespace CVC4 {
namespace theory {
}
};
-}
-}
-}
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
-#endif /* THEORY_ARITH_TYPE_RULES_H_ */
+#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */
noinst_LTLIBRARIES = libarrays.la
libarrays_la_SOURCES = \
+ theory_arrays_type_rules.h \
theory_arrays.h \
theory_arrays.cpp
#
theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h"
+
+operator ARRAY_TYPE 2 "array type"
+
+# select a i is a[i]
operator SELECT 2 "array select"
+
+# store a i e is a[i] <= e
operator STORE 3 "array store"
#include "theory/theory.h"
-namespace context {
-class Context;
-}
+#include <iostream>
namespace CVC4 {
namespace theory {
~TheoryArrays();
void preRegisterTerm(TNode n) { }
void registerTerm(TNode n) { }
+
+ RewriteResponse preRewrite(TNode in, bool topLevel) {
+ Debug("arrays-rewrite") << "pre-rewriting " << in
+ << " topLevel==" << topLevel << std::endl;
+ return RewritingComplete(in);
+ }
+
+ RewriteResponse postRewrite(TNode in, bool topLevel) {
+ Debug("arrays-rewrite") << "post-rewriting " << in
+ << " topLevel==" << topLevel << std::endl;
+ return RewritingComplete(in);
+ }
+
void check(Effort e);
void propagate(Effort e) { }
void explain(TNode n, Effort e) { }
-};
+ void shutdown() { }
+ std::string identify() const { return std::string("TheoryArrays"); }
+};/* class TheoryArrays */
}/* CVC4::theory::arrays namespace */
}/* CVC4::theory namespace */
--- /dev/null
+/********************* */
+/*! \file theory_arrays_type_rules.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Theory of arrays.
+ **
+ ** Theory of arrays.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_
+#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+struct ArraySelectTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+ throw (TypeCheckingExceptionPrivate) {
+ Assert(n.getKind() == kind::SELECT);
+ TypeNode arrayType = n[0].getType();
+ TypeNode indexType = n[1].getType();
+ if(arrayType.getArrayIndexType() != indexType) {
+ throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
+ }
+ return arrayType.getArrayConstituentType();
+ }
+};/* struct ArraySelectTypeRule */
+
+struct ArrayStoreTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
+ throw (TypeCheckingExceptionPrivate) {
+ Assert(n.getKind() == kind::STORE);
+ TypeNode arrayType = n[0].getType();
+ TypeNode indexType = n[1].getType();
+ TypeNode valueType = n[2].getType();
+ if(arrayType.getArrayIndexType() != indexType) {
+ throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
+ }
+ if(arrayType.getArrayConstituentType() != valueType) {
+ throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
+ }
+ return arrayType;
+ }
+};/* struct ArrayStoreTypeRule */
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_ */
void check(Effort e) { Unimplemented(); }
void propagate(Effort e) { Unimplemented(); }
void explain(TNode n, Effort e) { Unimplemented(); }
-
+ std::string identify() const { return std::string("TheoryBool"); }
};
}/* CVC4::theory::booleans namespace */
--- /dev/null
+topdir = ../../..
+srcdir = src/theory/builtin
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libbuiltin.la
+
+libbuiltin_la_SOURCES = \
+ theory_builtin_type_rules.h \
+ theory_builtin.h \
+ theory_builtin.cpp
+
+EXTRA_DIST = kinds
--- /dev/null
+# kinds [for builtin theory] -*- 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 [builtin] T header
+#
+# The special tag "builtin" declares that this is the builtin theory.
+# There can be only one and it should be processed first.
+#
+# 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 ::CVC4::theory::builtin::TheoryBuiltin "theory_builtin.h"
+
+# 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"
--- /dev/null
+/********************* */
+/*! \file theory_builtin.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of the builtin theory.
+ **
+ ** Implementation of the builtin theory.
+ **/
+
+#include "theory/builtin/theory_builtin.h"
+#include "expr/kind.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::theory::builtin;
+
+namespace CVC4 {
+namespace theory {
+namespace builtin {
+
+Node blastDistinct(TNode in) {
+ Debug("theory-rewrite") << "blastDistinct: " << in << std::endl;
+ Assert(in.getKind() == kind::DISTINCT);
+ if(in.getNumChildren() == 2) {
+ // if this is the case exactly 1 != pair will be generated so the
+ // AND is not required
+ Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, in[0], in[1]);
+ Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
+ return neq;
+ }
+ // assume that in.getNumChildren() > 2 => diseqs.size() > 1
+ vector<Node> diseqs;
+ for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
+ TNode::iterator j = i;
+ while(++j != in.end()) {
+ Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j);
+ Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
+ diseqs.push_back(neq);
+ }
+ }
+ Node out = NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs);
+ return out;
+}
+
+RewriteResponse TheoryBuiltin::postRewrite(TNode in, bool topLevel) {
+ if(topLevel) {
+ if(in.getKind() == kind::DISTINCT) {
+ return RewritingComplete(blastDistinct(in));
+ }
+ }
+
+ // EQUAL is a special case that should never end up here
+ Assert(in.getKind() != kind::EQUAL);
+
+ return RewritingComplete(in);
+}
+
+}/* CVC4::theory::builtin namespace */
+}/* CVC4::theory */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file theory_builtin.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Built-in theory.
+ **
+ ** Built-in theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
+#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
+
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace builtin {
+
+class TheoryBuiltin : public Theory {
+public:
+ TheoryBuiltin(context::Context* c, OutputChannel& out) : Theory(c, out) { }
+ ~TheoryBuiltin() { }
+ void preRegisterTerm(TNode n) { Unreachable(); }
+ void registerTerm(TNode n) { Unreachable(); }
+ void check(Effort e) { Unreachable(); }
+ void propagate(Effort e) { Unreachable(); }
+ void explain(TNode n, Effort e) { Unreachable(); }
+ void shutdown() { }
+ RewriteResponse postRewrite(TNode n, bool topLevel);
+ std::string identify() const { return std::string("TheoryBuiltin"); }
+};/* class TheoryBuiltin */
+
+}/* CVC4::theory::builtin namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */
--- /dev/null
+/********************* */
+/*! \file builtin_type_rules.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: mdeters
+ ** 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 Type rules for the builtin theory
+ **
+ ** Type rules for the builtin theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_
+#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "expr/expr.h"
+
+namespace CVC4 {
+namespace theory {
+namespace builtin {
+
+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();
+ }
+};
+
+}/* CVC4::theory::builtin namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_ */
theory ::CVC4::theory::bv::TheoryBV "theory_bv.h"
+constant BITVECTOR_TYPE \
+ ::CVC4::BitVectorSize \
+ "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \
+ "util/bitvector.h" \
+ "bit-vector type"
+
constant BITVECTOR_CONST \
::CVC4::BitVector \
::CVC4::BitVectorHashStrategy \
void check(Effort e) { Unimplemented(); }
void propagate(Effort e) { Unimplemented(); }
void explain(TNode n, Effort e) { Unimplemented(); }
-};
+ std::string identify() const { return std::string("TheoryBV"); }
+};/* class TheoryBV */
}/* CVC4::theory::bv namespace */
}/* CVC4::theory namespace */
#include "cvc4_private.h"
-#ifndef __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_
-#define __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_
+#ifndef __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
+#define __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
namespace CVC4 {
namespace theory {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n)
throw (TypeCheckingExceptionPrivate) {
- return nodeManager->bitVectorType(n.getConst<BitVector>().getSize());
+ return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
}
};
if (!lhs.isBitVector() || lhs != rhs) {
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
}
- return nodeManager->bitVectorType(1);
+ return nodeManager->mkBitVectorType(1);
}
};
}
if (maxWidth < t.getBitVectorSize()) maxWidth = t.getBitVectorSize();
}
- return nodeManager->bitVectorType(maxWidth);
+ return nodeManager->mkBitVectorType(maxWidth);
}
};
if (extractInfo.high >= t.getBitVectorSize()) {
throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector");
}
- return nodeManager->bitVectorType(extractInfo.high - extractInfo.low + 1);
+ return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1);
}
};
}
size += t.getBitVectorSize();
}
- return nodeManager->bitVectorType(size);
+ return nodeManager->mkBitVectorType(size);
}
};
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
}
unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
- return nodeManager->bitVectorType(repeatAmount * t.getBitVectorSize());
+ return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
}
};
(unsigned) n.getOperator().getConst<BitVectorSignExtend>() :
(unsigned) n.getOperator().getConst<BitVectorZeroExtend>();
- return nodeManager->bitVectorType(extendAmount + t.getBitVectorSize());
+ return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize());
}
};
-}
-}
-}
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
-#endif /* __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ */
+#endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */
exit 1
fi
seen_theory_builtin=true
+ shift
elif [ -z "$1" -o -z "$2" ]; then
echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
exit 1
fi
}
+function check_builtin_theory_seen {
+ if ! $seen_theory_builtin; then
+ echo "$me: warning: no declaration for the builtin theory found" >&2
+ fi
+}
+
while [ $# -gt 0 ]; do
kf=$1
seen_theory=false
"
shift
done
+check_builtin_theory_seen
## output
#include <deque>
#include <list>
-#include <typeinfo>
+#include <string>
+#include <iostream>
namespace CVC4 {
namespace theory {
-// rewrite cache support
-struct RewriteCacheTag {};
-typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache;
+/**
+ * Instances of this class serve as response codes from
+ * Theory::preRewrite() and Theory::postRewrite(). Instances of
+ * derived classes RewritingComplete(n) and RewriteAgain(n) should
+ * be used for better self-documenting behavior.
+ */
+class RewriteResponse {
+protected:
+ enum Status { DONE, REWRITE };
+
+ RewriteResponse(Status s, Node n) : d_status(s), d_node(n) {}
+
+private:
+ const Status d_status;
+ const Node d_node;
+
+public:
+ bool isDone() const { return d_status == DONE; }
+ bool needsMoreRewriting() const { return d_status == REWRITE; }
+ Node getNode() const { return d_node; }
+};
+
+/**
+ * Return n, but request additional (pre,post)rewriting of it.
+ */
+class RewriteAgain : public RewriteResponse {
+public:
+ RewriteAgain(Node n) : RewriteResponse(REWRITE, n) {}
+};
+
+/**
+ * Signal that (pre,post)rewriting of the node is complete at n.
+ */
+class RewritingComplete : public RewriteResponse {
+public:
+ RewritingComplete(Node n) : RewriteResponse(DONE, n) {}
+};
/**
* Base class for T-solvers. Abstract DPLL(T).
d_facts.clear();
}
+ /**
+ * Get the context associated to this Theory.
+ */
context::Context* getContext() const {
return d_context;
}
*/
bool isShared(TNode n) throw();
- /**
- * Check whether a node is in the rewrite cache or not.
- */
- static bool inRewriteCache(TNode n) throw() {
- return n.hasAttribute(RewriteCache());
- }
-
- /**
- * Get the value of the rewrite cache (or Node::null()) if there is
- * none).
- */
- static Node getRewriteCache(TNode n) throw() {
- return n.getAttribute(RewriteCache());
- }
-
/** Tag for the "registerTerm()-has-been-called" flag on Nodes */
struct Registered {};
/** The "registerTerm()-has-been-called" flag on Nodes */
/**
* Pre-register a term. Done one time for a Node, ever.
- *
*/
virtual void preRegisterTerm(TNode) = 0;
/**
- * Rewrite a term. Done one time for a Node, ever.
+ * Pre-rewrite a term. This default base-class implementation
+ * simply returns RewritingComplete(n). A theory should never
+ * rewrite a term to a strictly larger term that contains itself, as
+ * this will cause a loop of hard Node links in the cache (and thus
+ * memory leakage).
*/
- virtual Node rewrite(TNode n) {
- return n;
+ virtual RewriteResponse preRewrite(TNode n, bool topLevel) {
+ Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl;
+ return RewritingComplete(n);
+ }
+
+ /**
+ * Post-rewrite a term. This default base-class implementation
+ * simply returns RewritingComplete(n). A theory should never
+ * rewrite a term to a strictly larger term that contains itself, as
+ * this will cause a loop of hard Node links in the cache (and thus
+ * memory leakage).
+ */
+ virtual RewriteResponse postRewrite(TNode n, bool topLevel) {
+ Debug("theory-rewrite") << "no post-rewriting to perform for " << n << std::endl;
+ return RewritingComplete(n);
}
/**
*/
virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0;
+ /**
+ * Identify this theory (for debugging, dynamic configuration,
+ * etc..)
+ */
+ virtual std::string identify() const = 0;
+
//
// CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
//
std::ostream& operator<<(std::ostream& os, Theory::Effort level);
}/* CVC4::theory namespace */
+
+inline std::ostream& operator<<(std::ostream& out, const CVC4::theory::Theory& theory) {
+ return out << theory.identify();
+}
+
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__THEORY_H */
#include "theory/theory_engine.h"
#include "expr/node.h"
#include "expr/attribute.h"
+#include "theory/theory.h"
+#include "expr/node_builder.h"
+#include <vector>
#include <list>
using namespace std;
-namespace CVC4 {
+using namespace CVC4;
+using namespace CVC4::theory;
+namespace CVC4 {
namespace theory {
struct PreRegisteredTag {};
}/* CVC4::theory namespace */
+Theory* TheoryEngine::theoryOf(TNode n) {
+ Kind k = n.getKind();
+
+ Assert(k >= 0 && k < kind::LAST_KIND);
+
+ if(n.getMetaKind() == kind::metakind::VARIABLE) {
+ TypeNode t = n.getType();
+ if(t.isBoolean()) {
+ return &d_bool;
+ } else if(t.isReal()) {
+ return &d_arith;
+ } else if(t.isArray()) {
+ return &d_arrays;
+ } else {
+ return &d_uf;
+ }
+ //Unimplemented();
+ } else if(k == kind::EQUAL) {
+ // if LHS is a variable, use theoryOf(LHS.getType())
+ // otherwise, use theoryOf(LHS)
+ TNode lhs = n[0];
+ if(lhs.getMetaKind() == kind::metakind::VARIABLE) {
+ // FIXME: we don't yet have a Type-to-Theory map. When we do,
+ // look up the type of the LHS and return that Theory (?)
+
+ //The following JUST hacks around this lack of a table
+ TypeNode type_of_n = lhs.getType();
+ if(type_of_n.isReal()) {
+ return &d_arith;
+ } else if(type_of_n.isArray()) {
+ return &d_arrays;
+ } else {
+ return &d_uf;
+ //Unimplemented();
+ }
+ } else {
+ return theoryOf(lhs);
+ }
+ } else {
+ // use our Kind-to-Theory mapping
+ return d_theoryOfTable[k];
+ }
+}
+
Node TheoryEngine::preprocess(TNode t) {
Node top = rewrite(t);
Debug("rewrite") << "rewrote: " << t << endl << "to : " << top << endl;
* and the above registration of leaves, this should ensure that
* all subterms in the entire tree were registered in
* reverse-topological order. */
- for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
+ for(list<TNode>::reverse_iterator i = toReg.rbegin();
i != toReg.rend();
++i) {
return skolem;
}
}
- std::vector<Node> newChildren;
+ vector<Node> newChildren;
bool somethingChanged = false;
- for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ for(TNode::const_iterator it = node.begin(), end = node.end();
+ it != end;
+ ++it) {
Node newChild = removeITEs(*it);
somethingChanged |= (newChild != *it);
newChildren.push_back(newChild);
nodeManager->setAttribute(node, theory::IteRewriteAttr(), Node::null());
return node;
}
-
}
-Node blastDistinct(TNode in){
- Assert(in.getKind() == kind::DISTINCT);
- if(in.getNumChildren() == 2){
- //If this is the case exactly 1 != pair will be generated so the AND is not required
- Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, in[0], in[1]);
- Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
- return neq;
- }
- //Assume that in.getNumChildren() > 2
- // => diseqs.size() > 1
- vector<Node> diseqs;
- for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
- TNode::iterator j = i;
- while(++j != in.end()) {
- Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j);
- Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
- diseqs.push_back(neq);
- }
+namespace theory {
+namespace rewrite {
+
+/**
+ * TheoryEngine::rewrite() keeps a stack of things that are being pre-
+ * and post-rewritten. Each element of the stack is a
+ * RewriteStackElement.
+ */
+struct RewriteStackElement {
+ /**
+ * The node at this rewrite level. For example (AND (OR x y) z)
+ * will have, as it's rewriting x, the stack:
+ * x
+ * (OR x y)
+ * (AND (OR x y) z)
+ */
+ Node d_node;
+
+ /**
+ * The theory associated to d_node. Cached here to avoid having to
+ * look it up again.
+ */
+ Theory* d_theory;
+
+ /**
+ * Whether or not this was a top-level rewrite. Note that at theory
+ * boundaries, topLevel is forced to true, so it's not the case that
+ * this is true only at the lowest stack level.
+ */
+ bool d_topLevel;
+
+ /**
+ * A saved index to the "next child" to pre- and post-rewrite. In
+ * the case when (AND (OR x y) z) is being rewritten, the AND, OR,
+ * and x are pre-rewritten, then (assuming they don't change), x is
+ * post-rewritten, then y is pre- and post-rewritten, then the OR is
+ * post-rewritten, then z is pre-rewritten, then the AND is
+ * post-rewritten. At each stack level, we need to remember the
+ * child index we're currently processing.
+ */
+ int d_nextChild;
+
+ /**
+ * A (re)builder for this node. As this node's children are
+ * post-rewritten, in order, they append to this builder. When this
+ * node is post-rewritten, it is reformed from d_builder since the
+ * children may have changed. Note Nodes aren't rebuilt if they
+ * have metakinds CONSTANT (which is illegal) or VARIABLE (which
+ * would create a fresh variable, not what we want)---which is fine,
+ * since those types don't have children anyway.
+ */
+ NodeBuilder<> d_builder;
+
+ /**
+ * Construct a fresh stack element.
+ */
+ RewriteStackElement(Node n, Theory* thy, bool top) :
+ d_node(n),
+ d_theory(thy),
+ d_topLevel(top),
+ d_nextChild(0) {
}
- Node out = NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs);
- return out;
-}
+};
+
+}/* CVC4::theory::rewrite namespace */
+}/* CVC4::theory namespace */
Node TheoryEngine::rewrite(TNode in) {
- if(inRewriteCache(in)) {
- return getRewriteCache(in);
- }
+ using theory::rewrite::RewriteStackElement;
+
+ Node noItes = removeITEs(in);
+ Node out;
+
+ // descend top-down into the theory rewriters
+ vector<RewriteStackElement> stack;
+ stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), true));
+ Debug("theory-rewrite") << "TheoryEngine::rewrite() starting at" << endl
+ << " " << noItes << " " << theoryOf(noItes)
+ << " TOP-LEVEL 0" << endl;
+ // This whole thing is essentially recursive, but we avoid actually
+ // doing any recursion.
+ do {// do until the stack is empty..
+ RewriteStackElement& rse = stack.back();
+ bool done;
+
+ Debug("theory-rewrite") << "rewriter looking at level " << stack.size()
+ << endl
+ << " " << rse.d_node << " " << rse.d_theory
+ << "[" << *rse.d_theory << "]"
+ << " " << (rse.d_topLevel ? "TOP-LEVEL " : "")
+ << rse.d_nextChild << endl;
+
+ if(rse.d_nextChild == 0) {
+ Node original = rse.d_node;
+ bool wasTopLevel = rse.d_topLevel;
+ Node cached = getPreRewriteCache(original, wasTopLevel);
+ if(cached.isNull()) {
+ do {
+ Debug("theory-rewrite") << "doing pre-rewrite in " << *rse.d_theory
+ << " topLevel==" << rse.d_topLevel << endl;
+ RewriteResponse response =
+ rse.d_theory->preRewrite(rse.d_node, rse.d_topLevel);
+ rse.d_node = response.getNode();
+ Assert(!rse.d_node.isNull(), "node illegally rewritten to null");
+ Theory* thy2 = theoryOf(rse.d_node);
+ Assert(thy2 != NULL, "node illegally rewritten to null theory");
+ Debug("theory-rewrite") << "got back " << rse.d_node << " "
+ << thy2 << "[" << *thy2 << "]"
+ << (response.needsMoreRewriting() ?
+ " MORE-REWRITING" : " DONE")
+ << endl;
+ if(rse.d_theory != thy2) {
+ Debug("theory-rewrite") << "pre-rewritten from " << *rse.d_theory
+ << " into " << *thy2
+ << ", marking top-level and !done" << endl;
+ rse.d_theory = thy2;
+ done = false;
+ // FIXME how to handle the "top-levelness" of a node that's
+ // rewritten from theory T1 into T2, then back to T1 ?
+ rse.d_topLevel = true;
+ } else {
+ done = !response.needsMoreRewriting();
+ }
+ } while(!done);
+ setPreRewriteCache(original, wasTopLevel, rse.d_node);
+ } else {// is in pre-rewrite cache
+ Debug("theory-rewrite") << "in pre-cache: " << cached << endl;
+ rse.d_node = cached;
+ Theory* thy2 = theoryOf(cached);
+ if(rse.d_theory != thy2) {
+ Debug("theory-rewrite") << "[cache-]pre-rewritten from "
+ << *rse.d_theory << " into " << *thy2
+ << ", marking top-level" << endl;
+ rse.d_theory = thy2;
+ rse.d_topLevel = true;
+ }
+ }
+ }
- if(in.getMetaKind() == kind::metakind::VARIABLE) {
- return in;
- }
+ // children
+ Node original = rse.d_node;
+ bool wasTopLevel = rse.d_topLevel;
+ Node cached = getPostRewriteCache(original, wasTopLevel);
+
+ if(cached.isNull()) {
+ if(rse.d_nextChild == 0 &&
+ rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ ++rse.d_nextChild;
+ Node op = rse.d_node.getOperator();
+ Theory* t = theoryOf(op);
+ Debug("theory-rewrite") << "pushing operator of " << rse.d_node << endl;
+ stack.push_back(RewriteStackElement(op, t, t != rse.d_theory));
+ continue;// break out of this node, do its operator
+ } else {
+ unsigned nch = rse.d_nextChild++;
+ if(rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ --nch;
+ }
+ if(nch < rse.d_node.getNumChildren()) {
+ Debug("theory-rewrite") << "pushing child " << nch
+ << " of " << rse.d_node << endl;
+ Node c = rse.d_node[nch];
+ Theory* t = theoryOf(c);
+ stack.push_back(RewriteStackElement(c, t, t != rse.d_theory));
+ continue;// break out of this node, do its child
+ }
+ }
- Node intermediate = removeITEs(in);
+ // incorporate the children's rewrites
+ if(rse.d_node.getMetaKind() != kind::metakind::VARIABLE &&
+ rse.d_node.getMetaKind() != kind::metakind::CONSTANT) {
+ Debug("theory-rewrite") << "builder here is " << &rse.d_builder
+ << " and it gets " << rse.d_node.getKind()
+ << endl;
+ rse.d_builder << rse.d_node.getKind();
+ rse.d_node = Node(rse.d_builder);
+ }
- // these special cases should go away when theory rewriting comes online
- if(intermediate.getKind() == kind::DISTINCT) {
- Node out = blastDistinct(intermediate);
- //setRewriteCache(intermediate, out);
- return rewrite(out); //TODO let this fall through?
- }
+ // post-rewriting
+ do {
+ Debug("theory-rewrite") << "doing post-rewrite of "
+ << rse.d_node << endl
+ << " in " << *rse.d_theory
+ << " topLevel==" << rse.d_topLevel << endl;
+ RewriteResponse response =
+ rse.d_theory->postRewrite(rse.d_node, rse.d_topLevel);
+ rse.d_node = response.getNode();
+ Assert(!rse.d_node.isNull(), "node illegally rewritten to null");
+ Theory* thy2 = theoryOf(rse.d_node);
+ Assert(thy2 != NULL, "node illegally rewritten to null theory");
+ Debug("theory-rewrite") << "got back " << rse.d_node << " "
+ << thy2 << "[" << *thy2 << "]"
+ << (response.needsMoreRewriting() ?
+ " MORE-REWRITING" : " DONE")
+ << endl;
+ if(rse.d_theory != thy2) {
+ Debug("theory-rewrite") << "post-rewritten from " << *rse.d_theory
+ << " into " << *thy2
+ << ", marking top-level and !done" << endl;
+ rse.d_theory = thy2;
+ done = false;
+ // FIXME how to handle the "top-levelness" of a node that's
+ // rewritten from theory T1 into T2, then back to T1 ?
+ rse.d_topLevel = true;
+ } else {
+ done = !response.needsMoreRewriting();
+ }
+ } while(!done);
+
+ setPostRewriteCache(original, wasTopLevel, rse.d_node);
+
+ out = rse.d_node;
+ } else {
+ Debug("theory-rewrite") << "in post-cache: " << cached << endl;
+ out = cached;
+ Theory* thy2 = theoryOf(cached);
+ if(rse.d_theory != thy2) {
+ Debug("theory-rewrite") << "[cache-]post-rewritten from "
+ << *rse.d_theory << " into " << *thy2 << endl;
+ rse.d_theory = thy2;
+ }
+ }
- theory::Theory* thy = theoryOf(intermediate);
- if(thy == NULL) {
- Node out = rewriteBuiltins(intermediate);
- //setRewriteCache(intermediate, out);
- return out;
- } else if(thy != &d_bool){
- Node out = thy->rewrite(intermediate);
- //setRewriteCache(intermediate, out);
- return out;
- }else{
- Node out = rewriteChildren(intermediate);
- //setRewriteCache(intermediate, out);
- return out;
- }
+ stack.pop_back();
+ if(!stack.empty()) {
+ Debug("theory-rewrite") << "asserting " << out << " to previous builder "
+ << &stack.back().d_builder << endl;
+ stack.back().d_builder << out;
+ }
+ } while(!stack.empty());
- Unreachable();
-}
+ Debug("theory-rewrite") << "DONE with theory rewriter." << endl;
+ Debug("theory-rewrite") << "result is:" << endl << out << endl;
+
+ return out;
+}/* TheoryEngine::rewrite(TNode in) */
}/* CVC4 namespace */
#include "theory/theoryof_table.h"
#include "prop/prop_engine.h"
+#include "theory/builtin/theory_builtin.h"
#include "theory/booleans/theory_bool.h"
#include "theory/uf/theory_uf.h"
#include "theory/arith/theory_arith.h"
namespace CVC4 {
+namespace theory {
+
+// rewrite cache support
+template <bool topLevel> struct PreRewriteCacheTag {};
+typedef expr::Attribute<PreRewriteCacheTag<true>, Node> PreRewriteCacheTop;
+typedef expr::Attribute<PreRewriteCacheTag<false>, Node> PreRewriteCache;
+template <bool topLevel> struct PostRewriteCacheTag {};
+typedef expr::Attribute<PostRewriteCacheTag<true>, Node> PostRewriteCacheTop;
+typedef expr::Attribute<PostRewriteCacheTag<false>, Node> PostRewriteCache;
+
+}/* CVC4::theory namespace */
+
// In terms of abstraction, this is below (and provides services to)
// PropEngine.
EngineOutputChannel d_theoryOut;
+ theory::builtin::TheoryBuiltin d_builtin;
theory::booleans::TheoryBool d_bool;
theory::uf::TheoryUF d_uf;
theory::arith::TheoryArith d_arith;
/**
- * Check whether a node is in the rewrite cache or not.
+ * Check whether a node is in the pre-rewrite cache or not.
*/
- static bool inRewriteCache(TNode n) throw() {
- return n.hasAttribute(theory::RewriteCache());
+ static bool inPreRewriteCache(TNode n, bool topLevel) throw() {
+ if(topLevel) {
+ return n.hasAttribute(theory::PreRewriteCacheTop());
+ } else {
+ return n.hasAttribute(theory::PreRewriteCache());
+ }
}
/**
- * Get the value of the rewrite cache (or Node::null()) if there is
+ * Get the value of the pre-rewrite cache (or Node::null()) if there is
* none).
*/
- static Node getRewriteCache(TNode n) throw() {
- return n.getAttribute(theory::RewriteCache());
+ static Node getPreRewriteCache(TNode in, bool topLevel) throw() {
+ if(topLevel) {
+ Node out;
+ if(in.getAttribute(theory::PreRewriteCacheTop(), out)) {
+ return out.isNull() ? Node(in) : out;
+ }
+ } else {
+ Node out;
+ if(in.getAttribute(theory::PreRewriteCache(), out)) {
+ return out.isNull() ? Node(in) : out;
+ }
+ }
+ return Node::null();
}
/**
- * Get the value of the rewrite cache (or Node::null()) if there is
- * none).
+ * Set the value of the pre-rewrite cache. v cannot be a null Node.
*/
- static void setRewriteCache(TNode n, TNode v) throw() {
- return n.setAttribute(theory::RewriteCache(), v);
+ static void setPreRewriteCache(TNode n, bool topLevel, TNode v) throw() {
+ AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()");
+ AssertArgument(!v.isNull(), v, "v cannot be null in setPreRewriteCache()");
+ // mappings from n -> n are actually stored as n -> null as a
+ // special case, to avoid cycles in the reference-counting of Nodes
+ if(topLevel) {
+ n.setAttribute(theory::PreRewriteCacheTop(), n == v ? TNode::null() : v);
+ } else {
+ n.setAttribute(theory::PreRewriteCache(), n == v ? TNode::null() : v);
+ }
}
/**
- * This is the top rewrite entry point, called during preprocessing.
- * It dispatches to the proper theories to rewrite the given Node.
+ * Check whether a node is in the post-rewrite cache or not.
*/
- Node rewrite(TNode in);
+ static bool inPostRewriteCache(TNode n, bool topLevel) throw() {
+ if(topLevel) {
+ return n.hasAttribute(theory::PostRewriteCacheTop());
+ } else {
+ return n.hasAttribute(theory::PostRewriteCache());
+ }
+ }
/**
- * Convenience function to recurse through the children, rewriting,
- * while leaving the Node's kind alone.
+ * Get the value of the post-rewrite cache (or Node::null()) if there is
+ * none).
*/
- Node rewriteChildren(TNode in) {
- if(in.getMetaKind() == kind::metakind::CONSTANT) {
- return in;
- }
-
- NodeBuilder<> b(in.getKind());
- if(in.getMetaKind() == kind::metakind::PARAMETERIZED){
- Assert(in.hasOperator());
- b << in.getOperator();
- }
- for(TNode::iterator c = in.begin(); c != in.end(); ++c) {
- b << rewrite(*c);
+ static Node getPostRewriteCache(TNode in, bool topLevel) throw() {
+ if(topLevel) {
+ Node out;
+ if(in.getAttribute(theory::PostRewriteCacheTop(), out)) {
+ return out.isNull() ? Node(in) : out;
+ }
+ } else {
+ Node out;
+ if(in.getAttribute(theory::PostRewriteCache(), out)) {
+ return out.isNull() ? Node(in) : out;
+ }
}
- Debug("rewrite") << "rewrote-children of " << in << std::endl
- << "got " << b << std::endl;
- Node ret = b;
- return ret;
+ return Node::null();
}
/**
- * Rewrite Nodes with builtin kind (that is, those Nodes n for which
- * theoryOf(n) == NULL). The master list is in expr/builtin_kinds.
+ * Set the value of the post-rewrite cache. v cannot be a null Node.
*/
- Node rewriteBuiltins(TNode in) {
- switch(Kind k = in.getKind()) {
- case kind::EQUAL:
- return rewriteChildren(in);
-
- case kind::ITE:
- Unhandled(k);
-
- case kind::SKOLEM:
- case kind::VARIABLE:
- return in;
-
- case kind::TUPLE:
- return rewriteChildren(in);
-
- default:
- Unhandled(k);
+ static void setPostRewriteCache(TNode n, bool topLevel, TNode v) throw() {
+ AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()");
+ AssertArgument(!v.isNull(), v, "v cannot be null in setPostRewriteCache()");
+ // mappings from n -> n are actually stored as n -> null as a
+ // special case, to avoid cycles in the reference-counting of Nodes
+ if(topLevel) {
+ n.setAttribute(theory::PostRewriteCacheTop(), n == v ? TNode::null() : v);
+ } else {
+ n.setAttribute(theory::PostRewriteCache(), n == v ? TNode::null() : v);
}
}
+ /**
+ * This is the top rewrite entry point, called during preprocessing.
+ * It dispatches to the proper theories to rewrite the given Node.
+ */
+ Node rewrite(TNode in);
+
Node removeITEs(TNode t);
public:
TheoryEngine(context::Context* ctxt) :
d_propEngine(NULL),
d_theoryOut(this, ctxt),
+ d_builtin(ctxt, d_theoryOut),
d_bool(ctxt, d_theoryOut),
d_uf(ctxt, d_theoryOut),
d_arith(ctxt, d_theoryOut),
d_bv(ctxt, d_theoryOut),
d_statistics() {
+ d_theoryOfTable.registerTheory(&d_builtin);
d_theoryOfTable.registerTheory(&d_bool);
d_theoryOfTable.registerTheory(&d_uf);
d_theoryOfTable.registerTheory(&d_arith);
* ordering issues between PropEngine and Theory.
*/
void shutdown() {
+ d_builtin.shutdown();
d_bool.shutdown();
d_uf.shutdown();
d_arith.shutdown();
* @returns the theory, or NULL if the TNode is
* of built-in type.
*/
- theory::Theory* theoryOf(TNode n) {
- Kind k = n.getKind();
-
- Assert(k >= 0 && k < kind::LAST_KIND);
-
- if(k == kind::VARIABLE) {
- TypeNode t = n.getType();
- if(t.isBoolean()){
- return &d_bool;
- }else if(t.isReal()){
- return &d_arith;
- }else{
- return &d_uf;
- }
- //Unimplemented();
- } else if(k == kind::EQUAL) {
- // if LHS is a VARIABLE, use theoryOf(LHS.getType())
- // otherwise, use theoryOf(LHS)
- TNode lhs = n[0];
- if(lhs.getKind() == kind::VARIABLE) {
- // FIXME: we don't yet have a Type-to-Theory map. When we do,
- // look up the type of the LHS and return that Theory (?)
-
- //The following JUST hacks around this lack of a table
- TypeNode type_of_n = lhs.getType();
- if(type_of_n.isReal()){
- return &d_arith;
- }else{
- return &d_uf;
- //Unimplemented();
- }
- } else {
- return theoryOf(lhs);
- }
- } else {
- // use our Kind-to-Theory mapping
- return d_theoryOfTable[k];
- }
- }
+ theory::Theory* theoryOf(TNode n);
/**
* Preprocess a node. This involves theory-specific rewriting, then
d_theoryOut.d_propagatedLiterals.clear();
// Do the checking
try {
+ //d_builtin.check(effort);
//d_bool.check(effort);
d_uf.check(effort);
d_arith.check(effort);
#include "theory/interrupted.h"
#include <vector>
+#include <utility>
+#include <iostream>
-namespace CVC4{
+namespace CVC4 {
namespace theory {
* Very basic OutputChannel for testing simple Theory Behaviour.
* Stores a call sequence for the output channel
*/
-enum OutputChannelCallType { CONFLICT, PROPOGATE, AUG_LEMMA, LEMMA, EXPLANATION };
+enum OutputChannelCallType {
+ CONFLICT,
+ PROPAGATE,
+ AUG_LEMMA,
+ LEMMA,
+ EXPLANATION
+};
+
+}/* CVC4::theory namespace */
+
+inline std::ostream& operator<<(std::ostream& out, theory::OutputChannelCallType type) {
+ switch(type) {
+ case theory::CONFLICT: return out << "CONFLICT";
+ case theory::PROPAGATE: return out << "PROPAGATE";
+ case theory::AUG_LEMMA: return out << "AUG_LEMMA";
+ case theory::LEMMA: return out << "LEMMA";
+ case theory::EXPLANATION: return out << "EXPLANATION";
+ default: return out << "UNDEFINED-OutputChannelCallType!" << int(type);
+ }
+}
+namespace theory {
class TestOutputChannel : public theory::OutputChannel {
public:
- std::vector< pair<enum OutputChannelCallType, Node> > d_callHistory;
+ std::vector< std::pair<enum OutputChannelCallType, Node> > d_callHistory;
TestOutputChannel() {}
void safePoint() throw(Interrupted, AssertionException) {}
- void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
+ void conflict(TNode n, bool safe = false)
+ throw(Interrupted, AssertionException) {
push(CONFLICT, n);
}
- void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
- push(PROPOGATE, n);
+ void propagate(TNode n, bool safe = false)
+ throw(Interrupted, AssertionException) {
+ push(PROPAGATE, n);
}
void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
private:
void push(OutputChannelCallType call, TNode n) {
- d_callHistory.push_back(make_pair(call,n));
+ d_callHistory.push_back(std::make_pair(call,n));
}
};/* class TestOutputChannel */
-}/* namespace theory */
-}/* namespace CVC4 */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
#endif /* __CVC4__THEORY__THEORY_TEST_UTILS_H */
*/
Node rewrite(TNode n);
+ /**
+ * Plug in old rewrite to the new (pre,post)rewrite interface.
+ */
+ RewriteResponse postRewrite(TNode n, bool topLevel) {
+ return RewritingComplete(topLevel ? rewrite(n) : Node(n));
+ }
+
/**
* Propagates theory literals. Currently does nothing.
*
*/
void explain(TNode n, Effort level) {}
+ std::string identify() const { return std::string("TheoryUF"); }
+
private:
/**
* Checks whether 2 nodes are already in the same equivalence class tree.
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY_UF_TYPE_RULES_H_
-#define __CVC4__THEORY_UF_TYPE_RULES_H_
+#ifndef __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_
+#define __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_
namespace CVC4 {
namespace theory {
}
-#endif /* THEORY_UF_TYPE_RULES_H_ */
+#endif /* __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_ */
<< "An assertion failed during stack unwinding:" << std::endl \
<< AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) << std::endl \
<< "===========================================" << std::endl; \
- if(s_debugAssertionFailure != NULL) { \
+ if(s_debugAssertionFailure != NULL) { \
Warning() << "The propagating exception is:" << std::endl \
- << s_debugAssertionFailure << std::endl \
+ << s_debugAssertionFailure << std::endl \
<< "===========================================" << std::endl; \
s_debugAssertionFailure = NULL; \
} \
gmp_util.h \
sexpr.h \
stats.h \
- stats.cpp
+ stats.cpp \
+ triple.h
--- /dev/null
+/********************* */
+/*! \file array.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Array types.
+ **
+ ** Array types.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__ARRAY_H_
+#define __CVC4__ARRAY_H_
+
+#include <iostream>
+#include "util/Assert.h"
+
+// we get ArrayType right now by #including type.h.
+// array.h is still useful for the auto-generated kinds #includes.
+#include "expr/type.h"
+
+#endif /* __CVC4__ARRAY_H_ */
** \todo document this file
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__BITVECTOR_H_
#define __CVC4__BITVECTOR_H_
#include "util/gmp_util.h"
#include "util/integer.h"
-using namespace std;
-
namespace CVC4 {
class BitVector {
--- /dev/null
+/********************* */
+/*! \file triple.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Similar to std::pair<>, for triples
+ **
+ ** Similar to std::pair<>, for triples.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__TRIPLE_H
+#define __CVC4__TRIPLE_H
+
+namespace CVC4 {
+
+template <class T1, class T2, class T3>
+class triple {
+public:
+ T1 first;
+ T2 second;
+ T3 third;
+};
+
+template <class T1, class T2, class T3>
+inline triple<T1, T2, T3>
+make_triple(const T1& t1, const T2& t2, const T3& t3) {
+ return triple<T1, T2, T3>(t1, t2, t3);
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__TRIPLE_H */
:logic QF_UF
:status unsat
:extrafuns ((x U) (y U) (z U))
- :formula (not (iff (distinct x y z) (and (not (= x y)) (not (= x z)) (not (= y z))))))
\ No newline at end of file
+ :formula (not (iff (distinct x y z) (and (not (= x y)) (not (= x z)) (not (= y z))))))
#include "expr/node_manager.h"
#include "expr/attribute.h"
#include "expr/node.h"
-#include "theory/theory.h"
+#include "theory/theory_engine.h"
#include "theory/uf/theory_uf.h"
#include "util/Assert.h"
TS_ASSERT_DIFFERS(theory::Theory::RegisteredAttr::s_id, TestFlag2cd::s_id);
TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id);
- lastId = attr::LastAttributeId<TNode, false>::s_id;
- TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId);
+ lastId = attr::LastAttributeId<Node, false>::s_id;
+ TS_ASSERT_LESS_THAN(theory::PreRewriteCache::s_id, lastId);
+ TS_ASSERT_LESS_THAN(theory::PostRewriteCache::s_id, lastId);
+ TS_ASSERT_LESS_THAN(theory::PreRewriteCacheTop::s_id, lastId);
+ TS_ASSERT_LESS_THAN(theory::PostRewriteCacheTop::s_id, lastId);
+ TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PostRewriteCache::s_id);
+ TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PreRewriteCacheTop::s_id);
+ TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PostRewriteCacheTop::s_id);
+ TS_ASSERT_DIFFERS(theory::PostRewriteCache::s_id, theory::PreRewriteCacheTop::s_id);
+ TS_ASSERT_DIFFERS(theory::PostRewriteCache::s_id, theory::PostRewriteCacheTop::s_id);
+ TS_ASSERT_DIFFERS(theory::PreRewriteCacheTop::s_id, theory::PostRewriteCacheTop::s_id);
lastId = attr::LastAttributeId<TypeNode, false>::s_id;
TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
Node expectedProp = d_nm->mkNode(GEQ, x, c);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPOGATE);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE);
TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedProp);
}
d_arith->explain(rLeq1, d_level);
TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPOGATE);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPAGATE);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), EXPLANATION);
TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq1);
TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), rLt1);
d_arith->explain(rLeq1, d_level);
TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPOGATE);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPOGATE);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPAGATE);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), EXPLANATION);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), EXPLANATION);
void preRegisterTerm(TNode n) {}
void propagate(Effort level) {}
void explain(TNode n, Effort level) {}
+ string identify() const { return "DummyTheory"; }
};
class TheoryBlack : public CxxTest::TestSuite {
projects / cvc5.git / commitdiff