diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-06-30 11:12:14 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-06-30 11:12:14 +0000 |
| commit | 4375b60d5df794b2c6193f3892185ea181a0748d (patch) | |
| tree | d346f9dc6bde42c3def6e0aac3b2711418e3d491 /src | |
| parent | 4206a75e7a1635d04bb69084404a75670e164b62 (diff) | |
* theory "tree" rewriting implemented and works
* added TheoryArith::preRewrite() to test and demonstrate
the use of pre-rewriting.
* array types and type checking now supported
* array type checking now supported
* theoryOf() dispatching properly to arrays now
* theories now required to implement a (simple) identify()
function that returns a string identifying them for
debugging/user output purposes
* added "builtin" theory to hold all built-in kinds and their
type rules and rewriting (currently only exploding distinct)
* fixed production build failure (regarding NodeSetDepth)
* removed an errant "using namespace std" in util/bitvector.h
(and made associated trivial fixes elsewhere)
* fixes to make unexpected exceptions more verbose in debug builds
* fixes to make multiple, cascading assertion fails simpler
* minor other fixes to comments etc.
Diffstat (limited to 'src')
53 files changed, 1154 insertions, 325 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/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(); } diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 2a1b1d0fc..eed542e8a 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -222,7 +222,8 @@ throw(OptionException) { 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); diff --git a/src/main/util.cpp b/src/main/util.cpp index 77274d575..eb7b56b19 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -24,6 +24,7 @@ #include <signal.h> #include "util/exception.h" +#include "util/Assert.h" #include "cvc4autoconfig.h" #include "main.h" @@ -75,6 +76,11 @@ void cvc4unexpected() { "\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); diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index d2d885ce0..ca9b2b747 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -223,7 +223,7 @@ inline std::string AntlrInput::tokenTextSubstr(pANTLR3_COMMON_TOKEN token, 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()); } diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 575f691a5..e0b144513 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -129,7 +129,7 @@ benchAttributes returns [CVC4::CommandSequence* cmd_seq] ; /** - * 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 */ @@ -261,7 +261,7 @@ builtinOp[CVC4::Kind& kind] | 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 @@ -305,9 +305,10 @@ builtinOp[CVC4::Kind& kind] | 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 ; /** @@ -437,7 +438,7 @@ sortSymbol returns [CVC4::Type t] : 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)); } ; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 0abc4c4c6..69b2eba76 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -314,7 +314,7 @@ builtinOp[CVC4::Kind& kind] | 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 ; /** @@ -482,7 +482,7 @@ fragment NUMERAL << " 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) }? diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index a7b536a57..64efedd8a 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -55,7 +55,7 @@ void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) { // 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 @@ -68,9 +68,9 @@ void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) { 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(); diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index d0d2f23d7..bb9d19b25 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -14,6 +14,7 @@ libtheory_la_SOURCES = \ theory.cpp libtheory_la_LIBADD = \ + @builddir@/builtin/libbuiltin.la \ @builddir@/booleans/libbooleans.la \ @builddir@/uf/libuf.la \ @builddir@/arith/libarith.la \ @@ -38,4 +39,4 @@ BUILT_SOURCES = @srcdir@/theoryof_table.h dist-hook: @srcdir@/theoryof_table.h MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h -SUBDIRS = booleans uf arith arrays bv +SUBDIRS = builtin booleans uf arith arrays bv diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 4e4088bb0..f270dacb4 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -148,7 +148,7 @@ public: } }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)); } } } @@ -289,7 +289,7 @@ public: 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){ @@ -299,7 +299,7 @@ public: 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); } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 26d554356..cb9dc85f7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -315,6 +315,34 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){ 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; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index ba9b5329d..465adacbc 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -41,7 +41,6 @@ namespace CVC4 { namespace theory { namespace arith { - /** * Implementation of QF_LRA. * Based upon: @@ -109,6 +108,18 @@ public: 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 preRegisterTerm(TNode n); @@ -122,6 +133,7 @@ public: void shutdown(){ } + std::string identify() const { return std::string("TheoryArith"); } private: /** @@ -254,7 +266,7 @@ private: Statistics d_statistics; -}; +};/* class TheoryArith */ }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index a995f90af..9b22b14bb 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -17,8 +17,8 @@ #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 { @@ -72,8 +72,8 @@ public: } }; -} -} -} +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif /* THEORY_ARITH_TYPE_RULES_H_ */ +#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */ diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index 84b9faaf4..0c6e9006f 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libarrays.la libarrays_la_SOURCES = \ + theory_arrays_type_rules.h \ theory_arrays.h \ theory_arrays.cpp diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 742b924c6..68daa8cb5 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -5,5 +5,11 @@ # 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" diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 52e63831c..69498cfb2 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -23,9 +23,7 @@ #include "theory/theory.h" -namespace context { -class Context; -} +#include <iostream> namespace CVC4 { namespace theory { @@ -37,10 +35,25 @@ public: ~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 */ diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h new file mode 100644 index 000000000..0eb88d800 --- /dev/null +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -0,0 +1,62 @@ +/********************* */ +/*! \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_ */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 83effa005..512dfebcc 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -45,7 +45,7 @@ public: 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 */ diff --git a/src/theory/builtin/Makefile b/src/theory/builtin/Makefile new file mode 100644 index 000000000..1dfd8a113 --- /dev/null +++ b/src/theory/builtin/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/builtin + +include $(topdir)/Makefile.subdir diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am new file mode 100644 index 000000000..5694dea84 --- /dev/null +++ b/src/theory/builtin/Makefile.am @@ -0,0 +1,13 @@ +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 diff --git a/src/expr/builtin_kinds b/src/theory/builtin/kinds index 50b858b31..1f22ebef1 100644 --- a/src/expr/builtin_kinds +++ b/src/theory/builtin/kinds @@ -1,4 +1,4 @@ -# builtin_kinds -*- sh -*- +# 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. @@ -6,7 +6,10 @@ # The first non-blank, non-comment line in this file must be a theory # declaration: # -# theory T header +# 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: # @@ -103,7 +106,7 @@ # commands. # -theory builtin +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 @@ -125,10 +128,3 @@ constant TYPE_CONSTANT \ "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/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp new file mode 100644 index 000000000..1951e438c --- /dev/null +++ b/src/theory/builtin/theory_builtin.cpp @@ -0,0 +1,69 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h new file mode 100644 index 000000000..5c0a70dea --- /dev/null +++ b/src/theory/builtin/theory_builtin.h @@ -0,0 +1,48 @@ +/********************* */ +/*! \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 */ diff --git a/src/expr/builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index afd206260..0f4fda1a6 100644 --- a/src/expr/builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -2,7 +2,7 @@ /*! \file builtin_type_rules.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** 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 @@ -10,21 +10,23 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add brief comments here ]] + ** \brief Type rules for the builtin theory ** - ** [[ Add file-specific comments here ]] + ** Type rules for the builtin theory. **/ #include "cvc4_private.h" -#ifndef __CVC4__BUILTIN_TYPE_RULES_H_ -#define __CVC4__BUILTIN_TYPE_RULES_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: @@ -51,6 +53,8 @@ public: } }; -} +}/* CVC4::theory::builtin namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4__BUILTIN_TYPE_RULES_H_ */ +#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_ */ diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index ba8fc4efd..f1b926d24 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -6,6 +6,12 @@ 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 \ diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index dc29183ea..17d0779ca 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -39,7 +39,8 @@ public: 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 */ diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 142c9c963..7dd6c3e60 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -18,8 +18,8 @@ #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 { @@ -29,7 +29,7 @@ class BitVectorConstantTypeRule { 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()); } }; @@ -42,7 +42,7 @@ public: if (!lhs.isBitVector() || lhs != rhs) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); } - return nodeManager->bitVectorType(1); + return nodeManager->mkBitVectorType(1); } }; @@ -61,7 +61,7 @@ public: } if (maxWidth < t.getBitVectorSize()) maxWidth = t.getBitVectorSize(); } - return nodeManager->bitVectorType(maxWidth); + return nodeManager->mkBitVectorType(maxWidth); } }; @@ -115,7 +115,7 @@ public: 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); } }; @@ -133,7 +133,7 @@ public: } size += t.getBitVectorSize(); } - return nodeManager->bitVectorType(size); + return nodeManager->mkBitVectorType(size); } }; @@ -146,7 +146,7 @@ public: 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()); } }; @@ -162,12 +162,12 @@ public: (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 */ diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof index 227831451..4b7dfcef5 100755 --- a/src/theory/mktheoryof +++ b/src/theory/mktheoryof @@ -51,6 +51,7 @@ function theory { 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 @@ -113,6 +114,12 @@ function check_theory_seen { 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 @@ -123,6 +130,7 @@ while [ $# -gt 0 ]; do " shift done +check_builtin_theory_seen ## output diff --git a/src/theory/theory.h b/src/theory/theory.h index 6f4effe78..bb598d410 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -29,7 +29,8 @@ #include <deque> #include <list> -#include <typeinfo> +#include <string> +#include <iostream> namespace CVC4 { @@ -37,9 +38,43 @@ class TheoryEngine; 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). @@ -121,6 +156,9 @@ protected: d_facts.clear(); } + /** + * Get the context associated to this Theory. + */ context::Context* getContext() const { return d_context; } @@ -142,21 +180,6 @@ protected: */ 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 */ @@ -230,15 +253,31 @@ public: /** * 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); } /** @@ -285,6 +324,12 @@ public: */ 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) // @@ -334,6 +379,11 @@ protected: 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 */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9dfaed68b..e41df92d0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -19,13 +19,18 @@ #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 {}; @@ -36,6 +41,50 @@ typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr; }/* 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; @@ -70,7 +119,7 @@ Node TheoryEngine::preprocess(TNode t) { * 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) { @@ -128,9 +177,11 @@ Node TheoryEngine::removeITEs(TNode node) { 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); @@ -145,66 +196,243 @@ Node TheoryEngine::removeITEs(TNode node) { 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 */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 15b406cdd..2575c4c2d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -26,6 +26,7 @@ #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" @@ -36,6 +37,18 @@ 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. @@ -116,6 +129,7 @@ class TheoryEngine { EngineOutputChannel d_theoryOut; + theory::builtin::TheoryBuiltin d_builtin; theory::booleans::TheoryBool d_bool; theory::uf::TheoryUF d_uf; theory::arith::TheoryArith d_arith; @@ -124,81 +138,101 @@ class TheoryEngine { /** - * 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: @@ -209,6 +243,7 @@ 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), @@ -216,6 +251,7 @@ public: 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); @@ -235,6 +271,7 @@ public: * ordering issues between PropEngine and Theory. */ void shutdown() { + d_builtin.shutdown(); d_bool.shutdown(); d_uf.shutdown(); d_arith.shutdown(); @@ -248,45 +285,7 @@ public: * @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 @@ -318,6 +317,7 @@ public: 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); diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index dc08788f3..cd0b4ef66 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -12,8 +12,10 @@ #include "theory/interrupted.h" #include <vector> +#include <utility> +#include <iostream> -namespace CVC4{ +namespace CVC4 { namespace theory { @@ -21,12 +23,32 @@ 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() {} @@ -34,12 +56,14 @@ public: 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) { @@ -71,11 +95,11 @@ public: 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 */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 5add2e92a..108102b9f 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -132,6 +132,13 @@ public: 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. * * Overloads void propagate(Effort level); from theory.h. @@ -147,6 +154,8 @@ public: */ 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. diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 33123cd8f..419e3d078 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -17,8 +17,8 @@ #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 { @@ -49,4 +49,4 @@ public: } -#endif /* THEORY_UF_TYPE_RULES_H_ */ +#endif /* __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_ */ diff --git a/src/util/Assert.h b/src/util/Assert.h index 5333817aa..0809257bf 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -211,9 +211,9 @@ extern __thread CVC4_PUBLIC const char* s_debugAssertionFailure; << "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; \ } \ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 0f6fb5929..e92954340 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -32,4 +32,5 @@ libutil_la_SOURCES = \ gmp_util.h \ sexpr.h \ stats.h \ - stats.cpp + stats.cpp \ + triple.h diff --git a/src/util/array.h b/src/util/array.h new file mode 100644 index 000000000..274421249 --- /dev/null +++ b/src/util/array.h @@ -0,0 +1,31 @@ +/********************* */ +/*! \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_ */ diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 746d9aaaf..0febfddfd 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -17,6 +17,8 @@ ** \todo document this file **/ +#include "cvc4_public.h" + #ifndef __CVC4__BITVECTOR_H_ #define __CVC4__BITVECTOR_H_ @@ -25,8 +27,6 @@ #include "util/gmp_util.h" #include "util/integer.h" -using namespace std; - namespace CVC4 { class BitVector { diff --git a/src/util/triple.h b/src/util/triple.h new file mode 100644 index 000000000..50bf30c4a --- /dev/null +++ b/src/util/triple.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \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 */ |