From 97111ecb8681838f2d201420cda12ca9fc7184ed Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 25 Apr 2011 23:44:00 +0000 Subject: [PATCH] Monday tasks: * new "well-foundedness" type property (like cardinality) specified in Theory kinds files; specifies well-foundedness and a ground term * well-foundedness / finite checks in Datatypes now superseded by type system isFinite(), isWellFounded(), mkGroundTerm(). * new "RecursionBreaker" template class, a convenient class that keeps a "seen" trail without you having to pass it around (which is difficult in cases of mutual recursion) of the idea of passing around a "seen" trail --- src/expr/expr_manager_scope.h | 7 +- src/expr/expr_manager_template.cpp | 2 +- src/expr/mkexpr | 8 +- src/expr/mkkind | 100 +++++- src/expr/mkmetakind | 8 +- src/expr/type.cpp | 14 +- src/expr/type.h | 17 +- src/expr/type_node.cpp | 10 +- src/expr/type_node.h | 37 ++- src/expr/type_properties_template.h | 64 +++- src/smt/smt_engine.cpp | 2 +- src/theory/arith/kinds | 14 +- src/theory/arrays/kinds | 1 + src/theory/booleans/kinds | 9 +- src/theory/builtin/kinds | 32 +- .../builtin/theory_builtin_type_rules.h | 50 ++- src/theory/datatypes/kinds | 22 ++ src/theory/datatypes/theory_datatypes.cpp | 16 +- src/theory/datatypes/theory_datatypes.h | 2 +- .../datatypes/theory_datatypes_type_rules.h | 66 +++- src/theory/mkrewriter | 8 +- src/theory/mktheorytraits | 14 +- src/theory/uf/kinds | 6 +- src/util/Makefile.am | 1 + src/util/datatype.cpp | 303 +++++++++++++++++- src/util/datatype.h | 78 ++++- src/util/recursion_breaker.h | 133 ++++++++ test/unit/Makefile.am | 1 + test/unit/util/datatype_black.h | 277 +++++++++++++++- test/unit/util/recursion_breaker_black.h | 57 ++++ 30 files changed, 1294 insertions(+), 65 deletions(-) create mode 100644 src/util/recursion_breaker.h create mode 100644 test/unit/util/recursion_breaker_black.h diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h index c1da288a4..7a5bdbfb4 100644 --- a/src/expr/expr_manager_scope.h +++ b/src/expr/expr_manager_scope.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -56,6 +56,11 @@ public: ? NodeManager::currentNM() : e.getExprManager()->getNodeManager()) { } + inline ExprManagerScope(const Type& t) : + d_nms(t.getExprManager() == NULL + ? NodeManager::currentNM() + : t.getExprManager()->getNodeManager()) { + } inline ExprManagerScope(const ExprManager& exprManager) : d_nms(exprManager.getNodeManager()) { } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index b116a4671..f0c90ebdb 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -585,7 +585,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { Type ctorType CVC4_UNUSED = c.getConstructor().getType(); Assert(ctorType.isConstructor() && ConstructorType(ctorType).getArity() == c.getNumArgs() && - ConstructorType(ctorType).getReturnType() == dtt, + ConstructorType(ctorType).getRangeType() == dtt, "malformed constructor in datatype post-resolution"); // for all selectors... for(Datatype::Constructor::const_iterator j = c.begin(), j_end = c.end(); diff --git a/src/expr/mkexpr b/src/expr/mkexpr index a7302da26..479ef6d11 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -108,7 +108,7 @@ function endtheory { } function sort { - # sort TYPE cardinality ["comment"] + # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen } @@ -119,6 +119,12 @@ function cardinality { check_theory_seen } +function well-founded { + # well-founded TYPE wellfoundedness-computer [header] + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function variable { # variable K ["comment"] lineno=${BASH_LINENO[0]} diff --git a/src/expr/mkkind b/src/expr/mkkind index 08d874c79..47d02863e 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -63,7 +63,11 @@ type_constant_list= type_constant_to_theory_id= type_cardinalities= type_constant_cardinalities= -type_cardinalities_includes= +type_wellfoundednesses= +type_constant_wellfoundednesses= +type_groundterms= +type_constant_groundterms= +type_properties_includes= seen_theory=false seen_theory_builtin=false @@ -121,10 +125,24 @@ function rewriter { } function sort { - # sort TYPE cardinality ["comment"] + # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen - register_sort "$1" "$2" "$3" + if [ "$3" = well-founded ]; then + wf=true + groundterm="$4" + header="$5" + comment="$6" + elif [ "$3" = not-well-founded ]; then + wf=false + groundterm= + header= + comment="$4" + else + echo "$kf:$lineno: expected third argument to be \"well-founded\" or \"not-well-founded\"" >&2 + exit 1 + fi + register_sort "$1" "$2" "$wf" "$groundterm" "$header" "$comment" } function cardinality { @@ -134,6 +152,13 @@ function cardinality { register_cardinality "$1" "$2" "$3" } +function well-founded { + # well-founded TYPE wellfoundedness-computer groundterm-computer [header] + lineno=${BASH_LINENO[0]} + check_theory_seen + register_wellfoundedness "$1" "$2" "$3" "$4" +} + function variable { # variable K ["comment"] @@ -173,7 +198,10 @@ function constant { function register_sort { id=$1 cardinality=$2 - comment=$3 + wellfoundedness=$3 + groundterm=$4 + header=$5 + comment=$6 type_constant_list="${type_constant_list} ${id}, /**< ${comment} */ " @@ -184,6 +212,23 @@ function register_sort { type_constant_cardinalities="${type_constant_cardinalities}#line $lineno \"$kf\" case $id: return Cardinality($cardinality); " + type_constant_wellfoundednesses="${type_constant_wellfoundednesses}#line $lineno \"$kf\" + case $id: return $wellfoundedness; +" + if [ -n "$groundterm" ]; then + type_constant_groundterms="${type_constant_groundterms}#line $lineno \"$kf\" + case $id: return $groundterm; +" + if [ -n "$header" ]; then + type_properties_includes="${type_properties_includes}#line $lineno \"$kf\" +#include \"$header\" +" + fi + else + type_constant_groundterms="${type_constant_groundterms}#line $lineno \"$kf\" + case $id: Unhandled(tc); +" + fi } function register_cardinality { @@ -195,7 +240,46 @@ function register_cardinality { case $id: return $cardinality_computer; " if [ -n "$header" ]; then - type_cardinalities_includes="${type_cardinalities_includes}#line $lineno \"$kf\" + type_properties_includes="${type_properties_includes}#line $lineno \"$kf\" +#include \"$header\" +" + fi +} + +function register_wellfoundedness { + id=$1 + wellfoundedness_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$2") + groundterm_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$3") + header=$4 + + # "false" is a special well-foundedness computer that doesn't + # require an associated groundterm-computer; anything else does + if [ "$wellfoundedness_computer" != false ]; then + if [ -z "$groundterm_computer" ]; then + echo "$kf:$lineno: ground-term computer missing in command \"well-founded\"" >&2 + exit 1 + fi + else + if [ -n "$groundterm_computer" ]; then + echo "$kf:$lineno: ground-term computer specified for not-well-founded type" >&2 + exit 1 + fi + fi + + type_wellfoundednesses="${type_wellfoundednesses}#line $lineno \"$kf\" + case $id: return $wellfoundedness_computer; +" + if [ -n "$groundterm_computer" ]; then + type_groundterms="${type_groundterms}#line $lineno \"$kf\" + case $id: return $groundterm_computer; +" + else + type_groundterms="${type_groundterms}#line $lineno \"$kf\" + case $id: Unhandled(typeNode); +" + fi + if [ -n "$header" ]; then + type_properties_includes="${type_properties_includes}#line $lineno \"$kf\" #include \"$header\" " fi @@ -272,7 +356,11 @@ for var in \ type_constant_to_theory_id \ type_cardinalities \ type_constant_cardinalities \ - type_cardinalities_includes \ + type_wellfoundednesses \ + type_constant_wellfoundednesses \ + type_groundterms \ + type_constant_groundterms \ + type_properties_includes \ theory_descriptions \ template \ ; do diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 00599c5a0..46a69dee5 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -100,7 +100,7 @@ function rewriter { } function sort { - # sort TYPE cardinality ["comment"] + # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen } @@ -111,6 +111,12 @@ function cardinality { check_theory_seen } +function well-founded { + # well-founded TYPE wellfoundedness-computer [header] + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function variable { # variable K ["comment"] diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 27a3f9da7..0df385a29 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -73,6 +73,16 @@ Cardinality Type::getCardinality() const { return d_typeNode->getCardinality(); } +bool Type::isWellFounded() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isWellFounded(); +} + +Expr Type::mkGroundTerm() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->mkGroundTerm().toExpr(); +} + Type& Type::operator=(const Type& t) { Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!"); Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!"); @@ -489,8 +499,8 @@ Type ArrayType::getConstituentType() const { return makeType(d_typeNode->getArrayConstituentType()); } -Type ConstructorType::getReturnType() const { - return makeType(d_typeNode->getConstructorReturnType()); +DatatypeType ConstructorType::getRangeType() const { + return DatatypeType(makeType(d_typeNode->getConstructorRangeType())); } size_t ConstructorType::getArity() const { diff --git a/src/expr/type.h b/src/expr/type.h index 89cb994e7..682e5fbcd 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -33,6 +33,7 @@ namespace CVC4 { class NodeManager; class ExprManager; +class Expr; class TypeNode; class SmtEngine; @@ -142,6 +143,18 @@ public: */ Cardinality getCardinality() const; + /** + * Is this a well-founded type? (I.e., do there exist ground + * terms?) + */ + bool isWellFounded() const; + + /** + * Construct and return a ground term for this Type. Throws an + * exception if this type is not well-founded. + */ + Expr mkGroundTerm() const; + /** * Substitution of Types. */ @@ -541,8 +554,8 @@ public: /** Construct from the base type */ ConstructorType(const Type& type) throw(AssertionException); - /** Get the return type */ - Type getReturnType() const; + /** Get the range type */ + DatatypeType getRangeType() const; /** Get the argument types */ std::vector getArgTypes() const; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index e48a92321..7b0adaa95 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -51,6 +51,14 @@ Cardinality TypeNode::getCardinality() const { return kind::getCardinality(*this); } +bool TypeNode::isWellFounded() const { + return kind::isWellFounded(*this); +} + +Node TypeNode::mkGroundTerm() const { + return kind::mkGroundTerm(*this); +} + bool TypeNode::isBoolean() const { return getKind() == kind::TYPE_CONSTANT && getConst() == BOOLEAN_TYPE; @@ -81,7 +89,7 @@ TypeNode TypeNode::getArrayConstituentType() const { return (*this)[1]; } -TypeNode TypeNode::getConstructorReturnType() const { +TypeNode TypeNode::getConstructorRangeType() const { Assert(isConstructor()); return (*this)[getNumChildren()-1]; } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index f51d7a9ba..b9fea939e 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -343,6 +343,17 @@ public: return d_nv == &expr::NodeValue::s_null; } + /** + * Convert this TypeNode into a Type using the currently-in-scope + * manager. + */ + inline Type toType(); + + /** + * Convert a Type into a TypeNode. + */ + inline static TypeNode fromType(const Type& t); + /** * Returns the cardinality of this type. * @@ -350,6 +361,22 @@ public: */ Cardinality getCardinality() const; + /** + * Returns whether this type is well-founded. A type is + * well-founded if there exist ground terms. + * + * @return true iff the type is well-founded + */ + bool isWellFounded() const; + + /** + * Construct and return a ground term of this type. If the type is + * not well founded, this function throws an exception. + * + * @return a ground term of the type + */ + Node mkGroundTerm() const; + /** Is this the Boolean type? */ bool isBoolean() const; @@ -369,7 +396,7 @@ public: TypeNode getArrayConstituentType() const; /** Get the return type (for constructor types) */ - TypeNode getConstructorReturnType() const; + TypeNode getConstructorRangeType() const; /** * Is this a function type? Function-like things (e.g. datatype @@ -492,6 +519,14 @@ struct TypeNodeHashFunction { namespace CVC4 { +inline Type TypeNode::toType() { + return NodeManager::currentNM()->toType(*this); +} + +inline TypeNode TypeNode::fromType(const Type& t) { + return NodeManager::fromType(t); +} + template TypeNode TypeNode::substitute(Iterator1 typesBegin, Iterator1 typesEnd, diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index b6fd644c8..28aa2f884 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -31,7 +31,7 @@ #include -${type_cardinalities_includes} +${type_properties_includes} #line 37 "${template}" @@ -81,6 +81,68 @@ ${type_cardinalities} } }/* getCardinality(TypeNode) */ +inline bool isWellFounded(TypeConstant tc) { + switch(tc) { +${type_constant_wellfoundednesses} +#line 88 "${template}" + default: { + std::stringstream ss; + ss << "No well-foundedness status known for type constant: " << tc; + InternalError(ss.str()); + } + } +}/* isWellFounded(TypeConstant) */ + +inline bool isWellFounded(TypeNode typeNode) { + AssertArgument(!typeNode.isNull(), typeNode); + switch(Kind k = typeNode.getKind()) { + case TYPE_CONSTANT: + return isWellFounded(typeNode.getConst()); +${type_wellfoundednesses} +#line 103 "${template}" + default: { + std::stringstream ss; + ss << Expr::setlanguage(language::toOutputLanguage + ( Options::current()->inputLanguage )); + ss << "A theory kinds file did not provide a well-foundedness " + << "or well-foundedness computer for type:\n" << typeNode + << "\nof kind " << k; + InternalError(ss.str()); + } + } +}/* isWellFounded(TypeNode) */ + +inline Node mkGroundTerm(TypeConstant tc) { + switch(tc) { +${type_constant_groundterms} +#line 119 "${template}" + default: { + std::stringstream ss; + ss << "No ground term known for type constant: " << tc; + InternalError(ss.str()); + } + } +}/* mkGroundTerm(TypeConstant) */ + +inline Node mkGroundTerm(TypeNode typeNode) { + AssertArgument(!typeNode.isNull(), typeNode); + switch(Kind k = typeNode.getKind()) { + case TYPE_CONSTANT: + return mkGroundTerm(typeNode.getConst()); +${type_groundterms} +#line 134 "${template}" + default: { + std::stringstream ss; + ss << Expr::setlanguage(language::toOutputLanguage + ( Options::current()->inputLanguage )); + ss << "A theory kinds file did not provide a ground term " + << "or ground term computer for type:\n" << typeNode + << "\nof kind " << k; + InternalError(ss.str()); + } + } +}/* mkGroundTerm(TypeNode) */ + }/* CVC4::kind namespace */ }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f98d60702..45c697d0b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -508,7 +508,7 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) // process without any error notice. stringstream ss; ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)) - << "A bad expression was produced. Original exception follows:\n" + << "A bad expression was produced internally. Original exception follows:\n" << tcep; InternalError(ss.str().c_str()); } diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index a0fc71ab4..1871e897a 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -18,8 +18,18 @@ operator MINUS 2 "arithmetic binary subtraction operator" operator UMINUS 1 "arithmetic unary negation" operator DIVISION 2 "arithmetic division" -sort REAL_TYPE Cardinality::REALS "Real type" -sort INTEGER_TYPE Cardinality::INTEGERS "Integer type" +sort REAL_TYPE \ + Cardinality::REALS \ + well-founded \ + "NodeManager::currentNM()->mkConst(Rational(0))" \ + "expr/node_manager.h" \ + "Real type" +sort INTEGER_TYPE \ + Cardinality::INTEGERS \ + well-founded \ + "NodeManager::currentNM()->mkConst(Integer(0))" \ + "expr/node_manager.h" \ + "Integer type" constant CONST_RATIONAL \ ::CVC4::Rational \ diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 533145dc2..4c68fb5cb 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -15,6 +15,7 @@ operator ARRAY_TYPE 2 "array type" cardinality ARRAY_TYPE \ "::CVC4::theory::arrays::CardinalityComputer::computeCardinality(%TYPE%)" \ "theory/arrays/theory_arrays_type_rules.h" +well-founded ARRAY_TYPE false # select a i is a[i] operator SELECT 2 "array select" diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index ce7c9111a..d540d57f5 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -10,7 +10,12 @@ properties finite rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h" -sort BOOLEAN_TYPE 2 "Boolean type" +sort BOOLEAN_TYPE \ + 2 \ + well-founded \ + "NodeManager::currentNM()->mkConst(false)" \ + "expr/node_manager.h" \ + "Boolean type" constant CONST_BOOLEAN \ bool \ @@ -26,4 +31,4 @@ operator OR 2: "logical or" operator XOR 2 "exclusive or" operator ITE 3 "if-then-else" -endtheory \ No newline at end of file +endtheory diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index a170ba145..f5195e256 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -122,7 +122,7 @@ # For consistency, constants taking a non-void payload should # start with "CONST_", but this is not enforced. # -# sort K cardinality ["comment"] +# sort K cardinality [well-founded ground-term header | not-well-founded] ["comment"] # # This creates a kind K that represents a sort (a "type constant"). # These kinds of types are "atomic" types; if you need to describe @@ -138,6 +138,13 @@ # cardinality as the integers, or Cardinality::REALS if the sort # has the same cardinality as the reals. # +# If the sort is well-founded (i.e., there exist ground terms), +# then the argument should be the string "well-founded"; if not, +# it should be the string "not-well-founded". If well-founded, +# two extra arguments immediately follow---a C++ expression that +# constructs a ground term (as a Node), and the header that must +# be #included for that expression to compile. +# # For consistency, sorts should end with "_TYPE", but this is not # enforced. # @@ -168,6 +175,15 @@ # ::CVC4::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \ # "theory/foo/theory_foo_type_rules.h" # +# well-founded K wellfoundedness-computer ground-term-computer [header] +# +# Analogous to the "cardinality" command above, the well-founded +# command provides a well-foundedness computer for the type. A +# ground term computer is required unless the +# wellfoundedness-computer is the constant "false". The ground +# term computer should return a Node, and it should return the +# same Node each time for a given type (although usually it's only +# ever called once anyway since the result is cached). # # # Lines may be broken with a backslash between arguments; for example: @@ -207,7 +223,10 @@ properties stable-infinite # Rewriter responisble for all the terms of the theory rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h" -sort BUILTIN_OPERATOR_TYPE Cardinality::INTEGERS "Built in type for built in operators" +sort BUILTIN_OPERATOR_TYPE \ + Cardinality::INTEGERS \ + not-well-founded \ + "Built in type for built in operators" # A kind representing "inlined" operators defined with OPERATOR # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's @@ -235,11 +254,16 @@ constant TYPE_CONSTANT \ "basic types" operator FUNCTION_TYPE 2: "function type" cardinality FUNCTION_TYPE \ - "::CVC4::theory::builtin::FunctionCardinality::computeCardinality(%TYPE%)" \ + "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" +well-founded FUNCTION_TYPE false operator TUPLE_TYPE 2: "tuple type" cardinality TUPLE_TYPE \ - "::CVC4::theory::builtin::TupleCardinality::computeCardinality(%TYPE%)" \ + "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" +well-founded TUPLE_TYPE \ + "::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" endtheory diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index bebfca9ab..cffc95ab2 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -128,10 +128,13 @@ public: } };/* class TupleTypeRule */ -class FunctionCardinality { +class FunctionProperties { public: inline static Cardinality computeCardinality(TypeNode type) { - Assert(type.getKind() == kind::FUNCTION_TYPE); + // Don't assert this; allow other theories to use this cardinality + // computation. + // + // Assert(type.getKind() == kind::FUNCTION_TYPE); Cardinality argsCard(1); // get the largest cardinality of function arguments/return type @@ -143,12 +146,15 @@ public: return valueCard ^ argsCard; } -};/* class FuctionCardinality */ +};/* class FuctionProperties */ -class TupleCardinality { +class TupleProperties { public: inline static Cardinality computeCardinality(TypeNode type) { - Assert(type.getKind() == kind::TUPLE_TYPE); + // Don't assert this; allow other theories to use this cardinality + // computation. + // + // Assert(type.getKind() == kind::TUPLE_TYPE); Cardinality card(1); for(TypeNode::iterator i = type.begin(), @@ -160,7 +166,39 @@ public: return card; } -};/* class TupleCardinality */ + + inline static bool isWellFounded(TypeNode type) { + // Don't assert this; allow other theories to use this + // wellfoundedness computation. + // + // Assert(type.getKind() == kind::TUPLE_TYPE); + + for(TypeNode::iterator i = type.begin(), + i_end = type.end(); + i != i_end; + ++i) { + if(! (*i).isWellFounded()) { + return false; + } + } + + return true; + } + + inline static Node mkGroundTerm(TypeNode type) { + Assert(type.getKind() == kind::TUPLE_TYPE); + + std::vector children; + for(TypeNode::iterator i = type.begin(), + i_end = type.end(); + i != i_end; + ++i) { + children.push_back((*i).mkGroundTerm()); + } + + return NodeManager::currentNM()->mkNode(kind::TUPLE, children); + } +};/* class TupleProperties */ }/* CVC4::theory::builtin namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 8cac2da62..37a65a2b0 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -12,12 +12,27 @@ rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatype # constructor type has a list of selector types followed by a return type operator CONSTRUCTOR_TYPE 1: "constructor" +cardinality CONSTRUCTOR_TYPE \ + "::CVC4::theory::datatypes::ConstructorProperties::computeCardinality(%TYPE%)" \ + "theory/datatypes/theory_datatypes_type_rules.h" +well-founded CONSTRUCTOR_TYPE \ + "::CVC4::theory::datatypes::ConstructorProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::datatypes::ConstructorProperties::mkGroundTerm(%TYPE%)" \ + "theory/datatypes/theory_datatypes_type_rules.h" # selector type has domain type and a range type operator SELECTOR_TYPE 2 "selector" +# can re-use function cardinality +cardinality SELECTOR_TYPE \ + "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" # tester type has a constructor type operator TESTER_TYPE 1 "tester" +# can re-use function cardinality +cardinality TESTER_TYPE \ + "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" parameterized APPLY_CONSTRUCTOR CONSTRUCTOR_TYPE 0: "constructor application" @@ -30,5 +45,12 @@ constant DATATYPE_TYPE \ "::CVC4::DatatypeHashStrategy" \ "util/datatype.h" \ "datatype type" +cardinality DATATYPE_TYPE \ + "%TYPE%.getConst().getCardinality()" \ + "util/datatype.h" +well-founded DATATYPE_TYPE \ + "%TYPE%.getConst().isWellFounded()" \ + "%TYPE%.getConst().mkGroundTerm()" \ + "util/datatype.h" endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 5e813b125..ee6f175dd 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -66,7 +66,7 @@ void TheoryDatatypes::checkFiniteWellFounded() { vector::iterator itc; // for each datatype... for( it = d_cons.begin(); it != d_cons.end(); ++it ) { - d_distinguishTerms[it->first] = Node::null(); + //d_distinguishTerms[it->first] = Node::null(); d_finite[it->first] = false; d_wellFounded[it->first] = false; // for each ctor of that datatype... @@ -137,15 +137,15 @@ void TheoryDatatypes::checkFiniteWellFounded() { for( int c=0; c<(int)ct.getNumChildren()-1; c++ ) { TypeNode ts = ct[c]; if( ts.isDatatype() ) { - children.push_back( d_distinguishTerms[ts] ); + //children.push_back( d_distinguishTerms[ts] ); } else { //fix? this should be a ground term children.push_back( nm->mkVar( ts ) ); } } - Node dgt = nm->mkNode( APPLY_CONSTRUCTOR, children ); - Debug("datatypes-finite") << "set distinguished ground term " << t << " to " << dgt << endl; - d_distinguishTerms[t] = dgt; + //Node dgt = nm->mkNode( APPLY_CONSTRUCTOR, children ); + //Debug("datatypes-finite") << "set distinguished ground term " << t << " to " << dgt << endl; + //d_distinguishTerms[t] = dgt; } } } @@ -882,8 +882,8 @@ Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) { } else { Debug("datatypes") << "Applied selector " << t << " to wrong constructor " << endl; Debug("datatypes") << "Return distinguished term "; - Debug("datatypes") << d_distinguishTerms[ selType[1] ] << " of type " << selType[1] << endl; - retNode = d_distinguishTerms[ selType[1] ]; + Debug("datatypes") << selType[1].mkGroundTerm() << " of type " << selType[1] << endl; + retNode = selType[1].mkGroundTerm(); } if( useContext ) { Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t ); @@ -900,7 +900,7 @@ Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) { checkTester( tester, false ); if( !d_conflict.isNull() ) { Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl; - retNode = d_distinguishTerms[ selType[1] ]; + retNode = selType[1].mkGroundTerm(); Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t ); NodeBuilder<> nb(kind::AND); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 36d1b3311..c3b9a0baf 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -56,7 +56,7 @@ private: /** map from selectors to the constructors they are for */ std::map d_sel_cons; /** the distinguished ground term for each type */ - std::map d_distinguishTerms; + //std::map d_distinguishTerms; /** finite datatypes/constructor */ std::map< TypeNode, bool > d_finite; std::map< Node, bool > d_cons_finite; diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 1fd24cf53..bc1581f14 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -22,9 +22,18 @@ #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H namespace CVC4 { + +namespace expr { + namespace attr { + struct DatatypeConstructorTypeGroundTermTag {}; + }/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ + namespace theory { namespace datatypes { +typedef expr::Attribute GroundTermAttr; + struct DatatypeConstructorTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw(TypeCheckingExceptionPrivate) { @@ -47,7 +56,7 @@ struct DatatypeConstructorTypeRule { } } } - return consType.getConstructorReturnType(); + return consType.getConstructorRangeType(); } };/* struct DatatypeConstructorTypeRule */ @@ -91,6 +100,61 @@ struct DatatypeTesterTypeRule { } };/* struct DatatypeSelectorTypeRule */ +struct ConstructorProperties { + inline static Cardinality computeCardinality(TypeNode type) { + // Constructors aren't exactly functions, they're like + // parameterized ground terms. So the cardinality is more like + // that of a tuple than that of a function. + AssertArgument(type.isConstructor(), type); + Cardinality c = 1; + for(unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) { + c *= type[i].getCardinality(); + } + return c; + } + + inline static bool isWellFounded(TypeNode type) { + // Constructors aren't exactly functions, they're like + // parameterized ground terms. So the wellfoundedness is more + // like that of a tuple than that of a function. + AssertArgument(type.isConstructor(), type); + for(unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) { + if(!type[i].isWellFounded()) { + return false; + } + } + return true; + } + + inline static Node mkGroundTerm(TypeNode type) { + AssertArgument(type.isConstructor(), type); + + // is this already in the cache ? + Node groundTerm = type.getAttribute(GroundTermAttr()); + if(!groundTerm.isNull()) { + return groundTerm; + } + + // This is a bit tricky; Constructors have a unique index within + // their datatype, but Constructor *types* do not; multiple + // Constructors within the same Datatype could share the same + // type. So we scan through the datatype to find one that + // matches. + const Datatype& dt = type[type.getNumChildren() - 1].getConst(); + for(Datatype::const_iterator i = dt.begin(), + i_end = dt.end(); + i != i_end; + ++i) { + if(TypeNode::fromType((*i).getConstructor().getType()) == type) { + groundTerm = Node::fromExpr((*i).mkGroundTerm()); + type.setAttribute(GroundTermAttr(), groundTerm); + return groundTerm; + } + } + + InternalError("couldn't find a matching constructor?!"); + } +};/* struct ConstructorProperties */ }/* CVC4::theory::datatypes namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index 78fc39984..ec659d0bb 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -125,7 +125,7 @@ function rewriter { } function sort { - # sort TYPE cardinality ["comment"] + # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen } @@ -136,6 +136,12 @@ function cardinality { check_theory_seen } +function well-founded { + # well-founded TYPE wellfoundedness-computer [header] + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function variable { # variable K ["comment"] lineno=${BASH_LINENO[0]} diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 9672fc871..2056c6306 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -197,10 +197,14 @@ function properties { } function sort { - # sort TYPE cardinality ["comment"] + # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen - register_sort "$1" "$2" "$3" + if [ "$3" = well-founded ]; then + register_sort "$1" "$2" "$6" + else + register_sort "$1" "$2" "$4" + fi } function cardinality { @@ -209,6 +213,12 @@ function cardinality { check_theory_seen } +function well-founded { + # well-founded TYPE wellfoundedness-computer [header] + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function variable { # variable K ["comment"] lineno=${BASH_LINENO[0]} diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index d7f542038..9498fa6fb 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -13,7 +13,10 @@ rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" # Justified because we can have an unbounded-but-finite number of # sorts. Assuming we have |Z| is probably ok for now.. -sort KIND_TYPE Cardinality::INTEGERS "Uninterpreted Sort" +sort KIND_TYPE \ + Cardinality::INTEGERS \ + not-well-founded \ + "Uninterpreted Sort" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" @@ -23,5 +26,6 @@ parameterized SORT_TYPE SORT_TAG 0: "sort type" # enough (for now) ? Once we support quantifiers, maybe reconsider # this.. cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)" +well-founded SORT_TYPE false endtheory diff --git a/src/util/Makefile.am b/src/util/Makefile.am index a6ff0ea40..27b9e42d2 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -47,6 +47,7 @@ libutil_la_SOURCES = \ language.h \ language.cpp \ triple.h \ + recursion_breaker.h \ subrange_bound.h \ cardinality.h \ cardinality.cpp \ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index afd5af703..20d63995f 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -23,7 +23,10 @@ #include "util/datatype.h" #include "expr/type.h" #include "expr/expr_manager.h" +#include "expr/expr_manager_scope.h" +#include "expr/node_manager.h" #include "expr/node.h" +#include "util/recursion_breaker.h" using namespace std; @@ -32,10 +35,20 @@ namespace CVC4 { namespace expr { namespace attr { struct DatatypeIndexTag {}; - } -} + struct DatatypeFiniteTag {}; + struct DatatypeWellFoundedTag {}; + struct DatatypeFiniteComputedTag {}; + struct DatatypeWellFoundedComputedTag {}; + struct DatatypeGroundTermTag {}; + }/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ typedef expr::Attribute DatatypeIndexAttr; +typedef expr::Attribute DatatypeFiniteAttr; +typedef expr::Attribute DatatypeWellFoundedAttr; +typedef expr::Attribute DatatypeFiniteComputedAttr; +typedef expr::Attribute DatatypeWellFoundedComputedAttr; +typedef expr::Attribute DatatypeGroundTermAttr; const Datatype& Datatype::datatypeOf(Expr item) { TypeNode t = Node::fromExpr(item).getType(); @@ -73,6 +86,7 @@ void Datatype::resolve(ExprManager* em, "Datatype::resolve(): resolutions doesn't contain me!"); AssertArgument(placeholders.size() == replacements.size(), placeholders, "placeholders and replacements must be the same size"); + CheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors"); DatatypeType self = (*resolutions.find(d_name)).second; AssertArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!"); d_resolved = true; @@ -83,6 +97,7 @@ void Datatype::resolve(ExprManager* em, Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); } + d_self = self; Assert(index == getNumConstructors()); } @@ -92,6 +107,166 @@ void Datatype::addConstructor(const Constructor& c) { d_constructors.push_back(c); } +Cardinality Datatype::getCardinality() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + RecursionBreaker breaker(__PRETTY_FUNCTION__, this); + if(breaker.isRecursion()) { + return Cardinality::INTEGERS; + } + Cardinality c = 0; + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + c += (*i).getCardinality(); + } + return c; +} + +bool Datatype::isFinite() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_self); + + TypeNode self = TypeNode::fromType(d_self); + + // is this already in the cache ? + if(self.getAttribute(DatatypeFiniteComputedAttr())) { + return self.getAttribute(DatatypeFiniteAttr()); + } + + Cardinality c = 0; + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if(! (*i).isFinite()) { + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), false); + return false; + } + } + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), true); + return true; +} + +bool Datatype::isWellFounded() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_self); + + TypeNode self = TypeNode::fromType(d_self); + + // is this already in the cache ? + if(self.getAttribute(DatatypeWellFoundedComputedAttr())) { + return self.getAttribute(DatatypeWellFoundedAttr()); + } + + RecursionBreaker breaker(__PRETTY_FUNCTION__, this); + if(breaker.isRecursion()) { + // This *path* is cyclic, so may not be well-founded. The + // datatype itself might still be well-founded, though (we'll find + // the well-foundedness along another path). + return false; + } + + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if((*i).isWellFounded()) { + self.setAttribute(DatatypeWellFoundedComputedAttr(), true); + self.setAttribute(DatatypeWellFoundedAttr(), true); + return true; + } + } + + self.setAttribute(DatatypeWellFoundedComputedAttr(), true); + self.setAttribute(DatatypeWellFoundedAttr(), false); + return false; +} + +Expr Datatype::mkGroundTerm() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_self); + + TypeNode self = TypeNode::fromType(d_self); + + // is this already in the cache ? + Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr(); + if(!groundTerm.isNull()) { + Debug("datatypes") << "\nin cache: " << d_self << " => " << groundTerm << std::endl; + return groundTerm; + } else { + Debug("datatypes") << "\nNOT in cache: " << d_self << std::endl; + } + + // look for a nullary ctor and use that + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + // prefer the nullary constructor + if((*i).getNumArgs() == 0) { + groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor()); + self.setAttribute(DatatypeGroundTermAttr(), groundTerm); + Debug("datatypes") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl; + return groundTerm; + } + } + + // No ctors are nullary, but we can't just use the first ctor + // because that might recurse! In fact, since this datatype is + // well-founded by assumption, we know that at least one constructor + // doesn't contain a self-reference. We search for that one and use + // it to construct the ground term, as that is often a simpler + // ground term (e.g. in a tree datatype, something like "(leaf 0)" + // is simpler than "(node (leaf 0) (leaf 0))". + // + // Of course this check doesn't always work, if the self-reference + // is through other Datatypes (or other non-Datatype types), but it + // does simplify a common case. It requires a bit of extra work, + // but since we cache the results of these, it only happens once, + // ever, per Datatype. + // + // If the datatype is not actually well-founded, something below + // will throw an exception. + for(const_iterator i = begin(), i_end = end(); + i != i_end; + ++i) { + Constructor::const_iterator j = (*i).begin(), j_end = (*i).end(); + for(; j != j_end; ++j) { + SelectorType stype((*j).getSelector().getType()); + if(stype.getDomain() == stype.getRangeType()) { + Debug("datatypes") << "self-reference, skip " << getName() << "::" << (*i).getName() << std::endl; + // the constructor contains a direct self-reference + break; + } + } + + if(j == j_end && (*i).isWellFounded()) { + groundTerm = (*i).mkGroundTerm(); + // Constructor::mkGroundTerm() doesn't ever return null when + // called from the outside. But in recursive invocations, it + // can: say you have dt = a(one:dt) | b(two:INT), and you ask + // the "a" constructor for a ground term. It asks "dt" for a + // ground term, which in turn asks the "a" constructor for a + // ground term! Thus, even though "a" is a well-founded + // constructor, it cannot construct a ground-term by itself. We + // have to skip past it, and we do that with a + // RecursionBreaker<> in Constructor::mkGroundTerm(). In the + // case of recursion, it returns null. + if(!groundTerm.isNull()) { + // we found a ground-term-constructing constructor! + self.setAttribute(DatatypeGroundTermAttr(), groundTerm); + Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl; + return groundTerm; + } + } + } + // if we get all the way here, we aren't well-founded + CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!"); +} + +DatatypeType Datatype::getDatatypeType() const throw(AssertionException) { + CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); + Assert(!d_self.isNull()); + return DatatypeType(d_self); +} + bool Datatype::operator==(const Datatype& other) const throw() { // two datatypes are == iff the name is the same and they have // exactly matching constructors (in the same order) @@ -279,15 +454,131 @@ std::string Datatype::Constructor::getName() const throw() { } Expr Datatype::Constructor::getConstructor() const { - CheckArgument(isResolved(), this, "this datatype constructor not yet resolved"); + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_constructor; } Expr Datatype::Constructor::getTester() const { - CheckArgument(isResolved(), this, "this datatype constructor not yet resolved"); + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_tester; } +Cardinality Datatype::Constructor::getCardinality() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + + Cardinality c = 1; + + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + c *= SelectorType((*i).getSelector().getType()).getRangeType().getCardinality(); + } + + return c; +} + +bool Datatype::Constructor::isFinite() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_constructor); + + TNode self = Node::fromExpr(d_constructor); + + // is this already in the cache ? + if(self.getAttribute(DatatypeFiniteComputedAttr())) { + return self.getAttribute(DatatypeFiniteAttr()); + } + + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if(! SelectorType((*i).getSelector().getType()).getRangeType().getCardinality().isFinite()) { + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), false); + return false; + } + } + + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), true); + return true; +} + +bool Datatype::Constructor::isWellFounded() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_constructor); + + TNode self = Node::fromExpr(d_constructor); + + // is this already in the cache ? + if(self.getAttribute(DatatypeWellFoundedComputedAttr())) { + return self.getAttribute(DatatypeWellFoundedAttr()); + } + + RecursionBreaker breaker(__PRETTY_FUNCTION__, this); + if(breaker.isRecursion()) { + // This *path* is cyclic, sso may not be well-founded. The + // constructor itself might still be well-founded, though (we'll + // find the well-foundedness along another path). + return false; + } + + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if(! SelectorType((*i).getSelector().getType()).getRangeType().isWellFounded()) { + /* FIXME - we can't cache a negative result here, because a + Datatype might tell us it's not well founded along this + *path*, due to recursion, when it really is well-founded. + This should be fixed by creating private functions to do the + recursion here, and leaving the (public-facing) + isWellFounded() call as the base of that recursion. Then we + can distinguish the cases. + */ + /* + self.setAttribute(DatatypeWellFoundedComputedAttr(), true); + self.setAttribute(DatatypeWellFoundedAttr(), false); + */ + return false; + } + } + + self.setAttribute(DatatypeWellFoundedComputedAttr(), true); + self.setAttribute(DatatypeWellFoundedAttr(), true); + return true; +} + +Expr Datatype::Constructor::mkGroundTerm() const throw(AssertionException) { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_constructor); + + TNode self = Node::fromExpr(d_constructor); + + // is this already in the cache ? + Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr(); + if(!groundTerm.isNull()) { + return groundTerm; + } + + RecursionBreaker breaker(__PRETTY_FUNCTION__, this); + if(breaker.isRecursion()) { + // Recursive path, we should skip and go to the next constructor; + // see lengthy comments in Datatype::mkGroundTerm(). + return Expr(); + } + + std::vector groundTerms; + groundTerms.push_back(getConstructor()); + + // for each selector, get a ground term + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + groundTerms.push_back(SelectorType((*i).getSelector().getType()).getRangeType().mkGroundTerm()); + } + + groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms); + self.setAttribute(DatatypeGroundTermAttr(), groundTerm); + return groundTerm; +} + const Datatype::Constructor::Arg& Datatype::Constructor::operator[](size_t index) const { CheckArgument(index < getNumArgs(), index, "index out of bounds"); return d_args[index]; @@ -346,7 +637,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { // These datatype things are recursive! Be very careful not to // print an infinite chain of them. long& printNameOnly = os.iword(s_printDatatypeNamesOnly); - Debug("datatypes") << "printNameOnly is " << printNameOnly << std::endl; + Debug("datatypes-output") << "printNameOnly is " << printNameOnly << std::endl; if(printNameOnly) { return os << dt.getName(); } @@ -360,7 +651,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { } scope(printNameOnly, 1); // when scope is destructed, the value pops back - Debug("datatypes") << "printNameOnly is now " << printNameOnly << std::endl; + Debug("datatypes-output") << "printNameOnly is now " << printNameOnly << std::endl; // can only output datatypes in the CVC4 native language Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); diff --git a/src/util/datatype.h b/src/util/datatype.h index 74bff1843..df7dd1814 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -99,8 +99,17 @@ public: */ class CVC4_PUBLIC Datatype { public: - static const Datatype& datatypeOf(Expr item); - static size_t indexOf(Expr item); + /** + * Get the datatype of a constructor, selector, or tester operator. + */ + static const Datatype& datatypeOf(Expr item) CVC4_PUBLIC; + + /** + * Get the index of a constructor or tester in its datatype, or the + * index of a selector in its constructor. (Zero is always the + * first index.) + */ + static size_t indexOf(Expr item) CVC4_PUBLIC; /** * A holder type (used in calls to Datatype::Constructor::addArg()) @@ -243,6 +252,33 @@ public: */ inline size_t getNumArgs() const throw(); + /** + * Return the cardinality of this constructor (the product of the + * cardinalities of its arguments). + */ + Cardinality getCardinality() const throw(AssertionException); + + /** + * Return true iff this constructor is finite (it is nullary or + * each of its argument types are finite). This function can + * only be called for resolved constructors. + */ + bool isFinite() const throw(AssertionException); + + /** + * Return true iff this constructor is well-founded (there exist + * ground terms). The constructor must be resolved or an + * exception is thrown. + */ + bool isWellFounded() const throw(AssertionException); + + /** + * Construct and return a ground term of this constructor. The + * constructor must be both resolved and well-founded, or else an + * exception is thrown. + */ + Expr mkGroundTerm() const throw(AssertionException); + /** * Returns true iff this Datatype constructor has already been * resolved. @@ -272,6 +308,7 @@ private: std::string d_name; std::vector d_constructors; bool d_resolved; + Type d_self; /** * Datatypes refer to themselves, recursively, and we have a @@ -302,6 +339,40 @@ public: /** Get the number of constructors (so far) for this Datatype. */ inline size_t getNumConstructors() const throw(); + /** + * Return the cardinality of this datatype (the sum of the + * cardinalities of its constructors). The Datatype must be + * resolved. + */ + Cardinality getCardinality() const throw(AssertionException); + + /** + * Return true iff this Datatype is finite (all constructors are + * finite, i.e., there are finitely many ground terms). If the + * datatype is not well-founded, this function returns false. The + * Datatype must be resolved or an exception is thrown. + */ + bool isFinite() const throw(AssertionException); + + /** + * Return true iff this datatype is well-founded (there exist ground + * terms). The Datatype must be resolved or an exception is thrown. + */ + bool isWellFounded() const throw(AssertionException); + + /** + * Construct and return a ground term of this Datatype. The + * Datatype must be both resolved and well-founded, or else an + * exception is thrown. + */ + Expr mkGroundTerm() const throw(AssertionException); + + /** + * Get the DatatypeType associated to this Datatype. Can only be + * called post-resolution. + */ + DatatypeType getDatatypeType() const throw(AssertionException); + /** * Return true iff the two Datatypes are the same. * @@ -372,7 +443,8 @@ inline std::string Datatype::UnresolvedType::getName() const throw() { inline Datatype::Datatype(std::string name) : d_name(name), d_constructors(), - d_resolved(false) { + d_resolved(false), + d_self() { } inline std::string Datatype::getName() const throw() { diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h new file mode 100644 index 000000000..6f82eec5c --- /dev/null +++ b/src/util/recursion_breaker.h @@ -0,0 +1,133 @@ +/********************* */ +/*! \file recursion_breaker.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, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A utility class to help with detecting recursion in a + ** computation + ** + ** A utility class to help with detecting recursion in a computation. + ** A breadcrumb trail is left, and a function can query the breaker + ** to see if recursion has occurred. For example: + ** + ** int foo(int x) { + ** RecursionBreaker breaker("foo", x); + ** if(breaker.isRecursion()) { + ** ++d_count; + ** return 0; + ** } + ** int xfactor = x * x; + ** if(x > 0) { + ** xfactor = -xfactor; + ** } + ** int y = foo(11 * x + xfactor); + ** int z = y < 0 ? y : x * y; + ** cout << "x == " << x << ", y == " << y << " ==> " << z << endl; + ** return z; + ** } + ** + ** Recursion occurs after a while in this example, and the recursion + ** is broken by the RecursionBreaker. + ** + ** RecursionBreaker is really just a thread-local set of "what has + ** been seen." The above example is trivial, easily fixed by + ** allocating such a set at the base of the recursion, and passing a + ** reference to it to each invocation. But other cases of + ** nontrivial, mutual recursion exist that aren't so easily broken, + ** and that's what the RecursionBreaker is for. See + ** Datatype::getCardinality(), for example. A Datatype's cardinality + ** depends on the cardinalities of the types it references---but + ** these, in turn can reference the original datatype in a cyclic + ** fashion. Where that happens, we need to break the recursion. + ** + ** Several RecursionBreakers can be used at once; each is identified + ** by the string tag in its constructor. If a single function is + ** involved in the detection of recursion, a good choice is to use + ** __FUNCTION__: + ** + ** RecursionBreaker(__FUNCTION__, this) breaker; + ** + ** Of course, if you're using GNU, you might prefer + ** __PRETTY_FUNCTION__, since it's robust to overloading, namespaces, + ** and containing classes. But neither is a good choice if two + ** functions need to access the same RecursionBreaker mechanism. + ** + ** For non-primitive datatypes, it might be a good idea to use a + ** pointer type to instantiate RecursionBreaker<>, for example with + ** RecursionBreaker. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__RECURSION_BREAKER_H +#define __CVC4__RECURSION_BREAKER_H + +#include +#include +#include +#include "util/hash.h" +#include "util/tls.h" +#include "util/Assert.h" + +namespace CVC4 { + +template +class RecursionBreaker { + //typedef std::hash_set Set; + typedef std::set Set; + typedef std::map Map; + static CVC4_THREADLOCAL(Map*) s_maps; + + std::string d_tag; + const T& d_item; + bool d_firstToTag; + bool d_recursion; + +public: + RecursionBreaker(std::string tag, const T& item) : + d_tag(tag), + d_item(item) { + if(s_maps == NULL) { + s_maps = new Map(); + } + d_firstToTag = s_maps->find(tag) == s_maps->end(); + Set& set = (*s_maps)[tag]; + d_recursion = (set.find(item) != set.end()); + Assert(!d_recursion || !d_firstToTag); + if(!d_recursion) { + set.insert(item); + } + } + + ~RecursionBreaker() { + Assert(s_maps->find(d_tag) != s_maps->end()); + if(!d_recursion) { + (*s_maps)[d_tag].erase(d_item); + } + if(d_firstToTag) { + Assert((*s_maps)[d_tag].empty()); + s_maps->erase(d_tag); + Assert(s_maps->find(d_tag) == s_maps->end()); + } + } + + bool isRecursion() const throw() { + return d_recursion; + } + +};/* class RecursionBreaker */ + +template +CVC4_THREADLOCAL(typename RecursionBreaker::Map*) RecursionBreaker::s_maps; + +}/* CVC4 namespace */ + +#endif /* __CVC4__RECURSION_BREAKER_H */ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index f50cc32db..691f33406 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -48,6 +48,7 @@ UNIT_TESTS = \ util/boolean_simplification_black \ util/subrange_bound_white \ util/cardinality_public \ + util/recursion_breaker_black \ main/interactive_shell_black export VERBOSE = 1 diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 991d71364..1ac4caaec 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -35,12 +35,54 @@ public: void setUp() { d_em = new ExprManager(); + Debug.on("datatypes"); + Debug.on("groundterms"); } void tearDown() { delete d_em; } + void testEnumeration() { + Datatype colors("colors"); + + Datatype::Constructor yellow("yellow", "is_yellow"); + Datatype::Constructor blue("blue", "is_blue"); + Datatype::Constructor green("green", "is_green"); + Datatype::Constructor red("red", "is_red"); + + colors.addConstructor(yellow); + colors.addConstructor(blue); + colors.addConstructor(green); + colors.addConstructor(red); + + Debug("datatypes") << colors << std::endl; + DatatypeType colorsType = d_em->mkDatatypeType(colors); + Debug("datatypes") << colorsType << std::endl; + + Expr ctor = colorsType.getDatatype()[1].getConstructor(); + Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor); + Debug("datatypes") << apply << std::endl; + + TS_ASSERT(colorsType.getDatatype().isFinite()); + TS_ASSERT(colorsType.getDatatype().getCardinality() == 4); + TS_ASSERT(ctor.getType().getCardinality() == 1); + TS_ASSERT(colorsType.getDatatype().isWellFounded()); + Debug("groundterms") << "ground term of " << colorsType.getDatatype().getName() << endl + << " is " << colorsType.mkGroundTerm() << endl; + TS_ASSERT(colorsType.mkGroundTerm().getType() == colorsType); + // all ctors should be well-founded too + for(Datatype::const_iterator i = colorsType.getDatatype().begin(), + i_end = colorsType.getDatatype().end(); + i != i_end; + ++i) { + TS_ASSERT((*i).isWellFounded()); + Debug("groundterms") << "ground term of " << *i << endl + << " is " << (*i).mkGroundTerm() << endl; + TS_ASSERT((*i).mkGroundTerm().getType() == colorsType); + } + } + void testNat() { Datatype nat("nat"); @@ -51,13 +93,31 @@ public: Datatype::Constructor zero("zero", "is_zero"); nat.addConstructor(zero); - cout << nat << std::endl; + Debug("datatypes") << nat << std::endl; DatatypeType natType = d_em->mkDatatypeType(nat); - cout << natType << std::endl; + Debug("datatypes") << natType << std::endl; Expr ctor = natType.getDatatype()[1].getConstructor(); Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor); - cout << apply << std::endl; + Debug("datatypes") << apply << std::endl; + + TS_ASSERT(! natType.getDatatype().isFinite()); + TS_ASSERT(natType.getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(natType.getDatatype().isWellFounded()); + Debug("groundterms") << "ground term of " << natType.getDatatype().getName() << endl + << " is " << natType.mkGroundTerm() << endl; + TS_ASSERT(natType.mkGroundTerm().getType() == natType); + // all ctors should be well-founded too + for(Datatype::const_iterator i = natType.getDatatype().begin(), + i_end = natType.getDatatype().end(); + i != i_end; + ++i) { + Debug("datatypes") << "checking " << (*i).getName() << endl; + TS_ASSERT((*i).isWellFounded()); + Debug("groundterms") << "ground term of " << *i << endl + << " is " << (*i).mkGroundTerm() << endl; + TS_ASSERT((*i).mkGroundTerm().getType() == natType); + } } void testTree() { @@ -73,12 +133,29 @@ public: leaf.addArg("leaf", integerType); tree.addConstructor(leaf); - cout << tree << std::endl; + Debug("datatypes") << tree << std::endl; DatatypeType treeType = d_em->mkDatatypeType(tree); - cout << treeType << std::endl; + Debug("datatypes") << treeType << std::endl; + + TS_ASSERT(! treeType.getDatatype().isFinite()); + TS_ASSERT(treeType.getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(treeType.getDatatype().isWellFounded()); + Debug("groundterms") << "ground term of " << treeType.getDatatype().getName() << endl + << " is " << treeType.mkGroundTerm() << endl; + TS_ASSERT(treeType.mkGroundTerm().getType() == treeType); + // all ctors should be well-founded too + for(Datatype::const_iterator i = treeType.getDatatype().begin(), + i_end = treeType.getDatatype().end(); + i != i_end; + ++i) { + TS_ASSERT((*i).isWellFounded()); + Debug("groundterms") << "ground term of " << *i << endl + << " is " << (*i).mkGroundTerm() << endl; + TS_ASSERT((*i).mkGroundTerm().getType() == treeType); + } } - void testList() { + void testListInt() { Datatype list("list"); Type integerType = d_em->integerType(); @@ -90,9 +167,94 @@ public: Datatype::Constructor nil("nil", "is_nil"); list.addConstructor(nil); - cout << list << std::endl; + Debug("datatypes") << list << std::endl; + DatatypeType listType = d_em->mkDatatypeType(list); + Debug("datatypes") << listType << std::endl; + + TS_ASSERT(! listType.getDatatype().isFinite()); + TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(listType.getDatatype().isWellFounded()); + Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl + << " is " << listType.mkGroundTerm() << endl; + TS_ASSERT(listType.mkGroundTerm().getType() == listType); + // all ctors should be well-founded too + for(Datatype::const_iterator i = listType.getDatatype().begin(), + i_end = listType.getDatatype().end(); + i != i_end; + ++i) { + TS_ASSERT((*i).isWellFounded()); + Debug("groundterms") << "ground term of " << *i << endl + << " is " << (*i).mkGroundTerm() << endl; + TS_ASSERT((*i).mkGroundTerm().getType() == listType); + } + } + + void testListReal() { + Datatype list("list"); + Type realType = d_em->realType(); + + Datatype::Constructor cons("cons", "is_cons"); + cons.addArg("car", realType); + cons.addArg("cdr", Datatype::SelfType()); + list.addConstructor(cons); + + Datatype::Constructor nil("nil", "is_nil"); + list.addConstructor(nil); + + Debug("datatypes") << list << std::endl; DatatypeType listType = d_em->mkDatatypeType(list); - cout << listType << std::endl; + Debug("datatypes") << listType << std::endl; + + TS_ASSERT(! listType.getDatatype().isFinite()); + TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::REALS); + TS_ASSERT(listType.getDatatype().isWellFounded()); + Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl + << " is " << listType.mkGroundTerm() << endl; + TS_ASSERT(listType.mkGroundTerm().getType() == listType); + // all ctors should be well-founded too + for(Datatype::const_iterator i = listType.getDatatype().begin(), + i_end = listType.getDatatype().end(); + i != i_end; + ++i) { + TS_ASSERT((*i).isWellFounded()); + Debug("groundterms") << "ground term of " << *i << endl + << " is " << (*i).mkGroundTerm() << endl; + TS_ASSERT((*i).mkGroundTerm().getType() == listType); + } + } + + void testListBoolean() { + Datatype list("list"); + Type booleanType = d_em->booleanType(); + + Datatype::Constructor cons("cons", "is_cons"); + cons.addArg("car", booleanType); + cons.addArg("cdr", Datatype::SelfType()); + list.addConstructor(cons); + + Datatype::Constructor nil("nil", "is_nil"); + list.addConstructor(nil); + + Debug("datatypes") << list << std::endl; + DatatypeType listType = d_em->mkDatatypeType(list); + Debug("datatypes") << listType << std::endl; + + TS_ASSERT(! listType.getDatatype().isFinite()); + TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(listType.getDatatype().isWellFounded()); + Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl + << " is " << listType.mkGroundTerm() << endl; + TS_ASSERT(listType.mkGroundTerm().getType() == listType); + // all ctors should be well-founded too + for(Datatype::const_iterator i = listType.getDatatype().begin(), + i_end = listType.getDatatype().end(); + i != i_end; + ++i) { + TS_ASSERT((*i).isWellFounded()); + Debug("groundterms") << "ground term of " << *i << endl + << " is " << (*i).mkGroundTerm() << endl; + TS_ASSERT((*i).mkGroundTerm().getType() == listType); + } } void testMutualListTrees() { @@ -114,7 +276,7 @@ public: leaf.addArg("leaf", Datatype::UnresolvedType("list")); tree.addConstructor(leaf); - cout << tree << std::endl; + Debug("datatypes") << tree << std::endl; Datatype list("list"); Datatype::Constructor cons("cons", "is_cons"); @@ -125,7 +287,7 @@ public: Datatype::Constructor nil("nil", "is_nil"); list.addConstructor(nil); - cout << list << std::endl; + Debug("datatypes") << list << std::endl; TS_ASSERT(! tree.isResolved()); TS_ASSERT(! node.isResolved()); @@ -142,6 +304,40 @@ public: TS_ASSERT(dtts[0].getDatatype().isResolved()); TS_ASSERT(dtts[1].getDatatype().isResolved()); + TS_ASSERT(! dtts[0].getDatatype().isFinite()); + TS_ASSERT(dtts[0].getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(dtts[0].getDatatype().isWellFounded()); + Debug("groundterms") << "ground term of " << dtts[0].getDatatype().getName() << endl + << " is " << dtts[0].mkGroundTerm() << endl; + TS_ASSERT(dtts[0].mkGroundTerm().getType() == dtts[0]); + // all ctors should be well-founded too + for(Datatype::const_iterator i = dtts[0].getDatatype().begin(), + i_end = dtts[0].getDatatype().end(); + i != i_end; + ++i) { + TS_ASSERT((*i).isWellFounded()); + Debug("groundterms") << "ground term of " << *i << endl + << " is " << (*i).mkGroundTerm() << endl; + TS_ASSERT((*i).mkGroundTerm().getType() == dtts[0]); + } + + TS_ASSERT(! dtts[1].getDatatype().isFinite()); + TS_ASSERT(dtts[1].getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(dtts[1].getDatatype().isWellFounded()); + Debug("groundterms") << "ground term of " << dtts[1].getDatatype().getName() << endl + << " is " << dtts[1].mkGroundTerm() << endl; + TS_ASSERT(dtts[1].mkGroundTerm().getType() == dtts[1]); + // all ctors should be well-founded too + for(Datatype::const_iterator i = dtts[1].getDatatype().begin(), + i_end = dtts[1].getDatatype().end(); + i != i_end; + ++i) { + TS_ASSERT((*i).isWellFounded()); + Debug("groundterms") << "ground term of " << *i << endl + << " is " << (*i).mkGroundTerm() << endl; + TS_ASSERT((*i).mkGroundTerm().getType() == dtts[1]); + } + // add another constructor to list datatype resulting in an // "otherNil-list" Datatype::Constructor otherNil("otherNil", "is_otherNil"); @@ -155,6 +351,67 @@ public: // tree is also different because it's a tree of otherNil-lists TS_ASSERT_DIFFERS(dtts[0], dtts2[0]); + + TS_ASSERT(! dtts2[0].getDatatype().isFinite()); + TS_ASSERT(dtts2[0].getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(dtts2[0].getDatatype().isWellFounded()); + Debug("groundterms") << "ground term of " << dtts2[0].getDatatype().getName() << endl + << " is " << dtts2[0].mkGroundTerm() << endl; + TS_ASSERT(dtts2[0].mkGroundTerm().getType() == dtts2[0]); + // all ctors should be well-founded too + for(Datatype::const_iterator i = dtts2[0].getDatatype().begin(), + i_end = dtts2[0].getDatatype().end(); + i != i_end; + ++i) { + TS_ASSERT((*i).isWellFounded()); + Debug("groundterms") << "ground term of " << *i << endl + << " is " << (*i).mkGroundTerm() << endl; + TS_ASSERT((*i).mkGroundTerm().getType() == dtts2[0]); + } + + TS_ASSERT(! dtts2[1].getDatatype().isFinite()); + TS_ASSERT(dtts2[1].getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(dtts2[1].getDatatype().isWellFounded()); + Debug("groundterms") << "ground term of " << dtts2[1].getDatatype().getName() << endl + << " is " << dtts2[1].mkGroundTerm() << endl; + TS_ASSERT(dtts2[1].mkGroundTerm().getType() == dtts2[1]); + // all ctors should be well-founded too + for(Datatype::const_iterator i = dtts2[1].getDatatype().begin(), + i_end = dtts2[1].getDatatype().end(); + i != i_end; + ++i) { + TS_ASSERT((*i).isWellFounded()); + Debug("groundterms") << "ground term of " << *i << endl + << " is " << (*i).mkGroundTerm() << endl; + TS_ASSERT((*i).mkGroundTerm().getType() == dtts2[1]); + } + } + + void testNotSoWellFounded() { + Datatype tree("tree"); + + Datatype::Constructor node("node", "is_node"); + node.addArg("left", Datatype::SelfType()); + node.addArg("right", Datatype::SelfType()); + tree.addConstructor(node); + + Debug("datatypes") << tree << std::endl; + DatatypeType treeType = d_em->mkDatatypeType(tree); + Debug("datatypes") << treeType << std::endl; + + TS_ASSERT(! treeType.getDatatype().isFinite()); + TS_ASSERT(treeType.getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(! treeType.getDatatype().isWellFounded()); + TS_ASSERT_THROWS_ANYTHING( treeType.mkGroundTerm() ); + TS_ASSERT_THROWS_ANYTHING( treeType.getDatatype().mkGroundTerm() ); + // all ctors should be not-well-founded either + for(Datatype::const_iterator i = treeType.getDatatype().begin(), + i_end = treeType.getDatatype().end(); + i != i_end; + ++i) { + TS_ASSERT(! (*i).isWellFounded()); + TS_ASSERT_THROWS_ANYTHING( (*i).mkGroundTerm() ); + } } };/* class DatatypeBlack */ diff --git a/test/unit/util/recursion_breaker_black.h b/test/unit/util/recursion_breaker_black.h new file mode 100644 index 000000000..41e498919 --- /dev/null +++ b/test/unit/util/recursion_breaker_black.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file recursion_breaker_black.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, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Black-box testing of RecursionBreaker + ** + ** Black-box testing of RecursionBreaker. + **/ + +#include +#include + +#include "util/recursion_breaker.h" + +using namespace CVC4; +using namespace std; + +class RecursionBreakerBlack : public CxxTest::TestSuite { + int d_count; + +public: + + void setUp() { + d_count = 0; + } + + int foo(int x) { + RecursionBreaker breaker("foo", x); + if(breaker.isRecursion()) { + ++d_count; + return 0; + } + int xfactor = x * x; + if(x > 0) { + xfactor = -xfactor; + } + int y = foo(11 * x + xfactor); + int z = y < 0 ? y : x * y; + cout << "x == " << x << ", y == " << y << " ==> " << z << endl; + return z; + } + + void testFoo() { + foo(5); + TS_ASSERT( d_count == 1 ); + } + +};/* class RecursionBreakerBlack */ -- 2.30.2