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 \
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; i<n.getNumChildren(); i++ ){
+ Node nc = collectRef( n[i], sk, rf, rf_pending );
+ if( nc.isNull() ){
+ return Node::null();
+ }
+ childChanged = nc!=n[i] || childChanged;
+ children.push_back( nc );
+ }
+ sk.pop_back();
+ Node ret;
+ if( childChanged ){
+ ret = NodeManager::currentNM()->mkNode( 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<UninterpretedConstant>().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 */
--- /dev/null
+/********************* */
+/*! \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<d_terms[tn].size() ){
+ ret = d_terms[tn][i];
+ }else{
+ Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
+ std::map< TypeNode, unsigned >::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( index<d_has_debruijn ){
+ ret = NodeManager::currentNM()->mkConst(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<d_sel_types.size() );
+ Assert( ctor.getNumArgs()-1<d_sel_types[index].size() );
+ 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<d_sel_types.size() );
+ Assert( index<d_sel_index.size() );
+ Assert( d_sel_types[index].size()==ctor.getNumArgs() );
+ Assert( d_sel_index[index].size()==ctor.getNumArgs()-1 );
+ for( int i=0; i<(int)(ctor.getNumArgs()-1); i++ ){
+ Node c = getTermEnum( d_sel_types[index][i], d_sel_index[index][i] );
+ Assert( !c.isNull() );
+ b << c;
+ }
+ b << lc;
+ }
+ Node nnn = Node(b);
+ Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
+ ret = nnn;
+ }
+
+ if( !d_child_enum && d_has_debruijn ){
+ Node nret = DatatypesRewriter::normalizeMuConstant( ret );
+ if( nret!=ret ){
+ Debug("dt-enum-nn") << "Non-normal constant : " << ret << std::endl;
+ return Node::null();
+ }
+ }
+
+ return ret;
+ }
+
+ void DatatypesEnumerator::init(){
+ //Assert(type.isDatatype());
+ Debug("te") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
+ Debug("te") << "datatype is kind " << d_type.getKind() << std::endl;
+ Debug("te") << "datatype is " << d_type << std::endl;
+ Debug("te") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton() << " " << d_datatype.isFinite() << std::endl;
+
+ if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
+ //start with uninterpreted constant
+ d_zeroCtor = 0;
+ d_has_debruijn = 1;
+ d_sel_types.push_back( std::vector< TypeNode >() );
+ 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_datatype.getNumConstructors(); ++i ){
+ d_sel_types.push_back( std::vector< TypeNode >() );
+ 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
** 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"
class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
/** 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 */
/** 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 */
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<d_terms[tn].size() ){
- return d_terms[tn][i];
- }else{
- Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
- std::map< TypeNode, unsigned >::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<d_sel_types.size() );
- Assert( index<d_sel_index.size() );
- Assert( d_sel_types[index].size()==ctor.getNumArgs() );
- Assert( d_sel_index[index].size()==ctor.getNumArgs()-1 );
- for( int i=0; i<(int)(ctor.getNumArgs()-1); i++ ){
- Node c = getTermEnum( d_sel_types[index][i], d_sel_index[index][i] );
- Assert( !c.isNull() );
- b << c;
- }
- b << lc;
- }
- Node nnn = Node(b);
- Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
- return nnn;
- }
+ Node getTermEnum( TypeNode tn, unsigned i );
+
+ bool increment( unsigned index );
+
+ Node getCurrentTerm( unsigned index );
+ void init();
public:
DatatypesEnumerator(TypeNode type) throw() :
TypeEnumeratorBase<DatatypesEnumerator>(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_datatype.getNumConstructors(); ++i ){
- d_sel_types.push_back( std::vector< TypeNode >() );
- 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<DatatypesEnumerator>(type),
+ d_datatype(DatatypeType(type.toType()).getDatatype()),
+ d_type(type) {
+ d_child_enum = childEnum;
+ init();
}
-
DatatypesEnumerator(const DatatypesEnumerator& de) throw() :
TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
d_datatype(de.d_datatype),
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());
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 );
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_sel_sum.size(); i++ ){
}
bool isFinished() throw() {
- return d_ctor >= d_datatype.getNumConstructors();
+ return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors();
}
};/* DatatypesEnumerator */
}
}
- ~TupleEnumerator() throw() {
+ virtual ~TupleEnumerator() throw() {
deleteEnumerators();
}
}
}
- ~RecordEnumerator() throw() {
+ virtual ~RecordEnumerator() throw() {
deleteEnumerators();
}
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();
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());
}
projects / cvc5.git / commitdiff