diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-25 23:44:00 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-25 23:44:00 +0000 |
commit | 97111ecb8681838f2d201420cda12ca9fc7184ed (patch) | |
tree | eee78a3ff75c1c9535b1db89ed273116a6ef3542 /src/theory | |
parent | de164c9308f6461472b95c23aae68d9d9686d8ae (diff) |
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
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/kinds | 14 | ||||
-rw-r--r-- | src/theory/arrays/kinds | 1 | ||||
-rw-r--r-- | src/theory/booleans/kinds | 9 | ||||
-rw-r--r-- | src/theory/builtin/kinds | 32 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 50 | ||||
-rw-r--r-- | src/theory/datatypes/kinds | 22 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 16 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 66 | ||||
-rwxr-xr-x | src/theory/mkrewriter | 8 | ||||
-rwxr-xr-x | src/theory/mktheorytraits | 14 | ||||
-rw-r--r-- | src/theory/uf/kinds | 6 |
12 files changed, 212 insertions, 28 deletions
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<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 */ 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<Datatype>().getCardinality()" \ + "util/datatype.h" +well-founded DATATYPE_TYPE \ + "%TYPE%.getConst<Datatype>().isWellFounded()" \ + "%TYPE%.getConst<Datatype>().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<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... @@ -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<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; 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<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> 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<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 */ 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 |