From d78d47eafdad2d76f681463787647cdf5892a2fd Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 9 Sep 2015 09:48:26 +0200 Subject: [PATCH] Working towards a fair enumerator for codatatypes. --- src/Makefile.am | 1 + src/theory/datatypes/datatypes_rewriter.h | 70 +++++++- src/theory/datatypes/type_enumerator.cpp | 208 ++++++++++++++++++++++ src/theory/datatypes/type_enumerator.h | 196 +++++--------------- src/theory/type_enumerator.h | 2 + src/util/uninterpreted_constant.h | 2 +- 6 files changed, 321 insertions(+), 158 deletions(-) create mode 100755 src/theory/datatypes/type_enumerator.cpp diff --git a/src/Makefile.am b/src/Makefile.am index 0cd4cff44..90a4d6f5b 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -232,6 +232,7 @@ libcvc4_la_SOURCES = \ theory/builtin/theory_builtin.cpp \ theory/datatypes/theory_datatypes_type_rules.h \ theory/datatypes/type_enumerator.h \ + theory/datatypes/type_enumerator.cpp \ theory/datatypes/theory_datatypes.h \ theory/datatypes/datatypes_rewriter.h \ theory/datatypes/theory_datatypes.cpp \ diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 6fafbca42..14d966458 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -384,7 +384,75 @@ public: return tn.isDatatype() || tn.isParametricDatatype() || tn.isTuple() || tn.isRecord(); } - +private: + static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending ){ + Assert( n.isConst() ); + TypeNode tn = n.getType(); + if( tn.isDatatype() ){ + if( n.getKind()==kind::APPLY_CONSTRUCTOR ){ + sk.push_back( n ); + rf_pending.push_back( Node::null() ); + std::vector< Node > children; + children.push_back( n.getOperator() ); + bool childChanged = false; + for( unsigned i=0; imkNode( kind::APPLY_CONSTRUCTOR, children ); + if( !rf_pending.back().isNull() ){ + rf[rf_pending.back()] = ret; + } + }else{ + ret = n; + Assert( rf_pending.back().isNull() ); + } + rf_pending.pop_back(); + return ret; + }else{ + const Integer& i = n.getConst().getIndex(); + uint32_t index = i.toUnsignedInt(); + if( index>=sk.size() ){ + return Node::null(); + }else{ + Assert( sk.size()==rf_pending.size() ); + Node r = rf_pending[ rf_pending.size()-1-index ]; + if( r.isNull() ){ + r = NodeManager::currentNM()->mkBoundVar( sk[ rf_pending.size()-1-index ].getType() ); + rf_pending[ rf_pending.size()-1-index ] = r; + } + return r; + } + } + }else{ + return n; + } + } +public: + static Node normalizeMuConstant( Node n ){ + Trace("dt-nconst") << "Normalize " << n << std::endl; + std::map< Node, Node > rf; + std::vector< Node > sk; + std::vector< Node > rf_pending; + Node s = collectRef( n, sk, rf, rf_pending ); + if( !s.isNull() ){ + Trace("dt-nconst") << "...symbolic normalized is : " << s << std::endl; + for( std::map< Node, Node >::iterator it = rf.begin(); it != rf.end(); ++it ){ + Trace("dt-nconst") << " " << it->first << " = " << it->second << std::endl; + } + return n; + }else{ + Trace("dt-nconst") << "...invalid." << std::endl; + return Node::null(); + } + } };/* class DatatypesRewriter */ }/* CVC4::theory::datatypes namespace */ diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp new file mode 100755 index 000000000..a4af183c5 --- /dev/null +++ b/src/theory/datatypes/type_enumerator.cpp @@ -0,0 +1,208 @@ +/********************* */ +/*! \file type_enumerator.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Enumerators for datatypes + ** + ** Enumerators for datatypes. + **/ + + #include "theory/datatypes/type_enumerator.h" + #include "theory/datatypes/datatypes_rewriter.h" + +using namespace CVC4; +using namespace theory; +using namespace datatypes; + +Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ + Node ret; + if( i::iterator it = d_te_index.find( tn ); + unsigned tei; + if( it==d_te_index.end() ){ + //initialize child enumerator for type + tei = d_children.size(); + d_te_index[tn] = tei; + if( tn.isDatatype() && d_has_debruijn ){ + //must indicate that this is a child enumerator (do not normalize constants for it) + DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true ); + d_children.push_back( TypeEnumerator( dte ) ); + }else{ + d_children.push_back( TypeEnumerator( tn ) ); + } + d_terms[tn].push_back( *d_children[tei] ); + }else{ + tei = it->second; + } + //enumerate terms until index is reached + while( i>=d_terms[tn].size() ){ + ++d_children[tei]; + if( d_children[tei].isFinished() ){ + Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl; + return Node::null(); + } + d_terms[tn].push_back( *d_children[tei] ); + } + Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl; + ret = d_terms[tn][i]; + } + return ret; + } + + bool DatatypesEnumerator::increment( unsigned index ){ + Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl; + if( d_sel_sum[index]==-1 ){ + //first time + d_sel_sum[index] = 0; + //special case: no children to iterate + if( index>=d_has_debruijn && d_sel_types[index].empty() ){ + Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl; + return d_size_limit==0; + }else{ + Debug("dt-enum") << "...success" << std::endl; + return true; + } + }else{ + unsigned i = 0; + while( i < d_sel_index[index].size() ){ + //increment if the sum of iterations on arguments is less than the limit + if( d_sel_sum[index]<(int)d_size_limit ){ + //also check if child enumerator has enough terms + if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){ + Debug("dt-enum") << "...success increment child " << i << std::endl; + d_sel_index[index][i]++; + d_sel_sum[index]++; + return true; + } + } + Debug("dt-enum") << "......failed increment child " << i << std::endl; + //reset child, iterate next + d_sel_sum[index] -= d_sel_index[index][i]; + d_sel_index[index][i] = 0; + i++; + } + Debug("dt-enum") << "...failure." << std::endl; + return false; + } + } + + Node DatatypesEnumerator::getCurrentTerm( unsigned index ){ + Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type << std::endl; + Node ret; + if( indexmkConst(UninterpretedConstant(d_type.toType(), d_size_limit)); + }else{ + Debug("dt-enum-debug") << "Look at constructor " << (index - d_has_debruijn) << std::endl; + DatatypeConstructor ctor = d_datatype[index - d_has_debruijn]; + Debug("dt-enum-debug") << "Check last term..." << std::endl; + //we first check if the last argument (which is forced to make sum of iterated arguments equal to d_size_limit) is defined + Node lc; + if( ctor.getNumArgs()>0 ){ + Assert( index b(kind::APPLY_CONSTRUCTOR); + Type typ; + if( d_datatype.isParametric() ){ + typ = ctor.getSpecializedConstructorType(d_type.toType()); + b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) ); + }else{ + b << ctor.getConstructor(); + } + Debug("dt-enum-debug") << "Get arguments..." << std::endl; + if( ctor.getNumArgs()>0 ){ + Assert( index() ); + d_sel_index.push_back( std::vector< unsigned >() ); + d_sel_sum.push_back( -1 ); + }else{ + // find the "zero" constructor via mkGroundTerm + Node t = d_type.mkGroundTerm(); + Assert( t.getKind()==kind::APPLY_CONSTRUCTOR ); + // start with the constructor for which a ground term is constructed + d_zeroCtor = Datatype::indexOf( t.getOperator().toExpr() ); + d_has_debruijn = 0; + } + d_ctor = d_zeroCtor; + for( unsigned i=0; i() ); + d_sel_index.push_back( std::vector< unsigned >() ); + d_sel_sum.push_back( -1 ); + DatatypeConstructor ctor = d_datatype[i]; + Type typ; + if( d_datatype.isParametric() ){ + typ = ctor.getSpecializedConstructorType(d_type.toType()); + } + for( unsigned a = 0; a < ctor.getNumArgs(); ++a ){ + TypeNode tn; + if( d_datatype.isParametric() ){ + tn = TypeNode::fromType( typ )[a]; + }else{ + tn = Node::fromExpr(ctor[a].getSelector()).getType()[1]; + } + d_sel_types.back().push_back( tn ); + d_sel_index.back().push_back( 0 ); + } + if( !d_sel_index.back().empty() ){ + d_sel_index.back().pop_back(); + } + } + d_size_limit = 0; + //set up initial conditions (should always succeed) + ++*this; //increment( d_ctor ); + AlwaysAssert( !isFinished() ); +} \ No newline at end of file diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index dc2a83841..0e5aad640 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -9,9 +9,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief An enumerator for bitvectors + ** \brief An enumerator for datatypes ** - ** An enumerator for bitvectors. + ** An enumerator for datatypes. **/ #include "cvc4_private.h" @@ -32,6 +32,8 @@ namespace datatypes { class DatatypesEnumerator : public TypeEnumeratorBase { /** The datatype we're enumerating */ const Datatype& d_datatype; + /** extra cons */ + unsigned d_has_debruijn; /** type */ TypeNode d_type; /** The datatype constructor we're currently enumerating */ @@ -41,6 +43,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase { /** list of type enumerators (one for each type in a selector argument) */ std::map< TypeNode, unsigned > d_te_index; std::vector< TypeEnumerator > d_children; + //std::vector< DatatypesEnumerator > d_dt_children; /** terms produced for types */ std::map< TypeNode, std::vector< Node > > d_terms; /** arg type of each selector, for each constructor */ @@ -51,165 +54,44 @@ class DatatypesEnumerator : public TypeEnumeratorBase { std::vector< int > d_sel_sum; /** current bound on the number of times we can iterate argument enumerators */ unsigned d_size_limit; + /** child */ + bool d_child_enum; - Node getTermEnum( TypeNode tn, unsigned i ){ - if( i::iterator it = d_te_index.find( tn ); - unsigned tei; - if( it==d_te_index.end() ){ - //initialize child enumerator for type - tei = d_children.size(); - d_te_index[tn] = tei; - d_children.push_back( TypeEnumerator( tn ) ); - d_terms[tn].push_back( *d_children[tei] ); - }else{ - tei = it->second; - } - //enumerate terms until index is reached - while( i>=d_terms[tn].size() ){ - ++d_children[tei]; - if( d_children[tei].isFinished() ){ - Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl; - return Node::null(); - } - d_terms[tn].push_back( *d_children[tei] ); - } - Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl; - return d_terms[tn][i]; - } + bool hasCyclesDt( const Datatype& dt ) { + return dt.isRecursiveSingleton() || !dt.isFinite(); } - - bool increment( unsigned index ){ - Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl; - if( d_sel_sum[index]==-1 ){ - //first time - d_sel_sum[index] = 0; - //special case: no children to iterate - if( d_sel_types[index].size()==0 ){ - Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl; - return d_size_limit==0; - }else{ - Debug("dt-enum") << "...success" << std::endl; - return true; - } + bool hasCycles( TypeNode tn ){ + if( tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + return hasCyclesDt( dt ); }else{ - unsigned i = 0; - while( i < d_sel_index[index].size() ){ - //increment if the sum of iterations on arguments is less than the limit - if( d_sel_sum[index]<(int)d_size_limit ){ - //also check if child enumerator has enough terms - if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){ - Debug("dt-enum") << "...success increment child " << i << std::endl; - d_sel_index[index][i]++; - d_sel_sum[index]++; - return true; - } - } - Debug("dt-enum") << "......failed increment child " << i << std::endl; - //reset child, iterate next - d_sel_sum[index] -= d_sel_index[index][i]; - d_sel_index[index][i] = 0; - i++; - } - Debug("dt-enum") << "...failure." << std::endl; return false; } } - Node getCurrentTerm( unsigned index ){ - Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type << "..." << std::endl; - DatatypeConstructor ctor = d_datatype[index]; - Debug("dt-enum-debug") << "Check last term..." << std::endl; - //we first check if the last argument (which is forced to make sum of iterated arguments equal to d_size_limit) is defined - Node lc; - if( ctor.getNumArgs()>0 ){ - lc = getTermEnum( d_sel_types[index][ctor.getNumArgs()-1], d_size_limit - d_sel_sum[index] ); - if( lc.isNull() ){ - Debug("dt-enum-debug") << "Current infeasible." << std::endl; - return Node::null(); - } - } - Debug("dt-enum-debug") << "Get constructor..." << std::endl; - NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); - Type typ; - if( d_datatype.isParametric() ){ - typ = ctor.getSpecializedConstructorType(d_type.toType()); - b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) ); - }else{ - b << ctor.getConstructor(); - } - Debug("dt-enum-debug") << "Get arguments..." << std::endl; - if( ctor.getNumArgs()>0 ){ - Assert( index(type), d_datatype(DatatypeType(type.toType()).getDatatype()), - d_type(type), - d_ctor(0), - d_zeroCtor(0) { - - //Assert(type.isDatatype()); - Debug("te") << "datatype is datatype? " << type.isDatatype() << std::endl; - Debug("te") << "datatype is kind " << type.getKind() << std::endl; - Debug("te") << "datatype is " << type << std::endl; - - /* find the "zero" constructor via mkGroundTerm */ - Node t = type.mkGroundTerm(); - Assert( t.getKind()==kind::APPLY_CONSTRUCTOR ); - d_zeroCtor = Datatype::indexOf( t.getOperator().toExpr() ); - /* start with the constructor for which a ground term is constructed */ - d_ctor = d_zeroCtor; - - for( unsigned i=0; i() ); - d_sel_index.push_back( std::vector< unsigned >() ); - d_sel_sum.push_back( -1 ); - DatatypeConstructor ctor = d_datatype[i]; - Type typ; - if( d_datatype.isParametric() ){ - typ = ctor.getSpecializedConstructorType(d_type.toType()); - } - for( unsigned a = 0; a < ctor.getNumArgs(); ++a ){ - TypeNode tn; - if( d_datatype.isParametric() ){ - tn = TypeNode::fromType( typ )[a]; - }else{ - tn = Node::fromExpr(ctor[a].getSelector()).getType()[1]; - } - d_sel_types[i].push_back( tn ); - d_sel_index[i].push_back( 0 ); - } - if( !d_sel_index[i].empty() ){ - d_sel_index[i].pop_back(); - } - } - d_size_limit = 0; - //set up initial conditions (should always succeed) - bool init_inc = increment( d_ctor ); - AlwaysAssert( init_inc ); + d_type(type) { + d_child_enum = false; + init(); + } + DatatypesEnumerator(TypeNode type, bool childEnum) throw() : + TypeEnumeratorBase(type), + d_datatype(DatatypeType(type.toType()).getDatatype()), + d_type(type) { + d_child_enum = childEnum; + init(); } - DatatypesEnumerator(const DatatypesEnumerator& de) throw() : TypeEnumeratorBase(de.getType()), d_datatype(de.d_datatype), @@ -235,14 +117,16 @@ public: d_children.insert( d_children.end(), de.d_children.begin(), de.d_children.end() ); d_sel_sum.insert( d_sel_sum.end(), de.d_sel_sum.begin(), de.d_sel_sum.end() ); d_size_limit = de.d_size_limit; + d_has_debruijn = de.d_has_debruijn; + d_child_enum = de.d_child_enum; } - ~DatatypesEnumerator() throw() { + virtual ~DatatypesEnumerator() throw() { } Node operator*() throw(NoMoreValuesException) { Debug("dt-enum-debug") << ": get term " << this << std::endl; - if(d_ctor < d_datatype.getNumConstructors()) { + if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) { return getCurrentTerm( d_ctor ); } else { throw NoMoreValuesException(getType()); @@ -252,7 +136,7 @@ public: DatatypesEnumerator& operator++() throw() { Debug("dt-enum-debug") << ": increment " << this << std::endl; unsigned prevSize = d_size_limit; - while(d_ctor < d_datatype.getNumConstructors()) { + while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) { //increment at index while( increment( d_ctor ) ){ Node n = getCurrentTerm( d_ctor ); @@ -267,9 +151,9 @@ public: if(d_ctor == d_zeroCtor) { ++d_ctor; } - if( d_ctor>=d_datatype.getNumConstructors() ){ - //try next size limit as long as new terms were generated at last size - if( prevSize==d_size_limit ){ + if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){ + //try next size limit as long as new terms were generated at last size, or other cases + if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isFinite() ){ d_size_limit++; d_ctor = d_zeroCtor; for( unsigned i=0; i= d_datatype.getNumConstructors(); + return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors(); } };/* DatatypesEnumerator */ @@ -328,7 +212,7 @@ public: } } - ~TupleEnumerator() throw() { + virtual ~TupleEnumerator() throw() { deleteEnumerators(); } @@ -413,7 +297,7 @@ public: } } - ~RecordEnumerator() throw() { + virtual ~RecordEnumerator() throw() { deleteEnumerators(); } diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index f0a76ee8a..d8006a5a4 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -89,6 +89,8 @@ public: TypeEnumerator(const TypeEnumerator& te) : d_te(te.d_te->clone()) { } + TypeEnumerator(TypeEnumeratorInterface* te) : d_te(te){ + } TypeEnumerator& operator=(const TypeEnumerator& te) { delete d_te; d_te = te.d_te->clone(); diff --git a/src/util/uninterpreted_constant.h b/src/util/uninterpreted_constant.h index c4fb776bc..13a80a19d 100644 --- a/src/util/uninterpreted_constant.h +++ b/src/util/uninterpreted_constant.h @@ -32,7 +32,7 @@ public: UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException) : d_type(type), d_index(index) { - CheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str()); + //CheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str()); CheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str()); } -- 2.30.2