From 97111ecb8681838f2d201420cda12ca9fc7184ed Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 25 Apr 2011 23:44:00 +0000 Subject: 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/theory/builtin/kinds | 32 ++++++++++++++--- src/theory/builtin/theory_builtin_type_rules.h | 50 ++++++++++++++++++++++---- 2 files changed, 72 insertions(+), 10 deletions(-) (limited to 'src/theory/builtin') 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 */ -- cgit v1.2.3