** 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
? 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()) {
}
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();
}
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
}
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]}
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
}
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 {
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"]
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} */
"
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 {
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
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
}
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
}
check_theory_seen
}
+function well-founded {
+ # well-founded TYPE wellfoundedness-computer [header]
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
function variable {
# variable K ["comment"]
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!");
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 {
class NodeManager;
class ExprManager;
+class Expr;
class TypeNode;
class SmtEngine;
*/
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.
*/
/** 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<Type> getArgTypes() 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<TypeConstant>() == BOOLEAN_TYPE;
return (*this)[1];
}
-TypeNode TypeNode::getConstructorReturnType() const {
+TypeNode TypeNode::getConstructorRangeType() const {
Assert(isConstructor());
return (*this)[getNumChildren()-1];
}
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.
*
*/
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;
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
namespace CVC4 {
+inline Type TypeNode::toType() {
+ return NodeManager::currentNM()->toType(*this);
+}
+
+inline TypeNode TypeNode::fromType(const Type& t) {
+ return NodeManager::fromType(t);
+}
+
template <class Iterator1, class Iterator2>
TypeNode TypeNode::substitute(Iterator1 typesBegin,
Iterator1 typesEnd,
#include <sstream>
-${type_cardinalities_includes}
+${type_properties_includes}
#line 37 "${template}"
}
}/* 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<TypeConstant>());
+${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<TypeConstant>());
+${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 */
// 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());
}
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 \
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"
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 \
operator XOR 2 "exclusive or"
operator ITE 3 "if-then-else"
-endtheory
\ No newline at end of file
+endtheory
# 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
# 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.
#
# ::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:
# 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
"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
}
};/* 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
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(),
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<Node> 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 */
# 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"
"::CVC4::DatatypeHashStrategy" \
"util/datatype.h" \
"datatype type"
+cardinality DATATYPE_TYPE \
+ "%TYPE%.getConst<Datatype>().getCardinality()" \
+ "util/datatype.h"
+well-founded DATATYPE_TYPE \
+ "%TYPE%.getConst<Datatype>().isWellFounded()" \
+ "%TYPE%.getConst<Datatype>().mkGroundTerm()" \
+ "util/datatype.h"
endtheory
vector<Node>::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...
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;
}
}
}
} 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 );
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);
/** map from selectors to the constructors they are for */
std::map<Node, Node > d_sel_cons;
/** the distinguished ground term for each type */
- std::map<TypeNode, Node > d_distinguishTerms;
+ //std::map<TypeNode, Node > d_distinguishTerms;
/** finite datatypes/constructor */
std::map< TypeNode, bool > d_finite;
std::map< Node, bool > d_cons_finite;
#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<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> GroundTermAttr;
+
struct DatatypeConstructorTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw(TypeCheckingExceptionPrivate) {
}
}
}
- return consType.getConstructorReturnType();
+ return consType.getConstructorRangeType();
}
};/* struct DatatypeConstructorTypeRule */
}
};/* 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<Datatype>();
+ 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 */
}
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
}
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]}
}
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 {
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]}
# 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"
# enough (for now) ? Once we support quantifiers, maybe reconsider
# this..
cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
+well-founded SORT_TYPE false
endtheory
language.h \
language.cpp \
triple.h \
+ recursion_breaker.h \
subrange_bound.h \
cardinality.h \
cardinality.cpp \
#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;
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<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr;
+typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr;
+typedef expr::Attribute<expr::attr::DatatypeWellFoundedTag, bool> DatatypeWellFoundedAttr;
+typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr;
+typedef expr::Attribute<expr::attr::DatatypeWellFoundedComputedTag, bool> DatatypeWellFoundedComputedAttr;
+typedef expr::Attribute<expr::attr::DatatypeGroundTermTag, Node> DatatypeGroundTermAttr;
const Datatype& Datatype::datatypeOf(Expr item) {
TypeNode t = Node::fromExpr(item).getType();
"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;
Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
}
+ d_self = self;
Assert(index == getNumConstructors());
}
d_constructors.push_back(c);
}
+Cardinality Datatype::getCardinality() const throw(AssertionException) {
+ CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+ RecursionBreaker<const Datatype*> 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<const Datatype*> 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)
}
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<const Datatype::Constructor*> 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<const Datatype::Constructor*> 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<Expr> 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];
// 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();
}
} 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);
*/
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())
*/
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.
std::string d_name;
std::vector<Constructor> d_constructors;
bool d_resolved;
+ Type d_self;
/**
* Datatypes refer to themselves, recursively, and we have a
/** 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.
*
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() {
--- /dev/null
+/********************* */
+/*! \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<int> 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<Foo*>(__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<Foo*>.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__RECURSION_BREAKER_H
+#define __CVC4__RECURSION_BREAKER_H
+
+#include <string>
+#include <map>
+#include <ext/hash_set>
+#include "util/hash.h"
+#include "util/tls.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+template <class T>
+class RecursionBreaker {
+ //typedef std::hash_set<T> Set;
+ typedef std::set<T> Set;
+ typedef std::map<std::string, Set> 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<T> */
+
+template <class T>
+CVC4_THREADLOCAL(typename RecursionBreaker<T>::Map*) RecursionBreaker<T>::s_maps;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RECURSION_BREAKER_H */
util/boolean_simplification_black \
util/subrange_bound_white \
util/cardinality_public \
+ util/recursion_breaker_black \
main/interactive_shell_black
export VERBOSE = 1
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");
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() {
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();
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() {
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");
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());
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");
// 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 */
--- /dev/null
+/********************* */
+/*! \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<T>
+ **
+ ** Black-box testing of RecursionBreaker<T>.
+ **/
+
+#include <iostream>
+#include <string>
+
+#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<int> 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 */
projects / cvc5.git / commitdiff