From 82fbac8829cbc41927216b36ab064b50e50b2fa0 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 13 Feb 2015 14:12:32 +0100 Subject: [PATCH] Handle recursive singleton case for codatatypes, add regression. Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes. --- src/parser/parser.cpp | 10 +- src/theory/datatypes/datatypes_rewriter.h | 16 +- src/theory/datatypes/theory_datatypes.cpp | 205 ++++++---- src/theory/datatypes/theory_datatypes.h | 7 + .../quantifiers/ce_guided_single_inv.cpp | 2 +- src/theory/unconstrained_simplifier.cpp | 10 +- src/util/cardinality.h | 4 + src/util/datatype.cpp | 367 +++++++++++------- src/util/datatype.h | 44 ++- test/regress/regress0/datatypes/Makefile.am | 3 +- .../regress0/datatypes/stream-singleton.smt2 | 11 + test/unit/parser/parser_black.h | 4 +- 12 files changed, 457 insertions(+), 226 deletions(-) create mode 100644 test/regress/regress0/datatypes/stream-singleton.smt2 diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index aa91a5a1e..10a729420 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -362,7 +362,15 @@ Parser::mkMutualDatatypeTypes(const std::vector& datatypes) { // complained of a bad substitution if anything is left unresolved. // Clear out the set. d_unresolved.clear(); - + + //throw exception if any datatype is not well-founded + for(unsigned i = 0; i < datatypes.size(); ++i) { + const Datatype& dt = types[i].getDatatype(); + if( !dt.isCodatatype() && !dt.isWellFounded() ){ + throw ParserException(dt.getName() + " is not well-founded"); + } + } + return types; } catch(IllegalArgumentException& ie) { throw ParserException(ie.getMessage()); diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 29a95b38f..ec9318e99 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -146,14 +146,14 @@ public: gt = *te; }else{ //check whether well-founded - bool isWellFounded = true; - if( isTypeDatatype( tn ) ){ - const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype(); - isWellFounded = dta.isWellFounded(); - } - if( isWellFounded || in[0].isConst() ){ - gt = tn.mkGroundTerm(); - } + //bool isWf = true; + //if( isTypeDatatype( tn ) ){ + // const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype(); + // isWf = dta.isWellFounded(); + //} + //if( isWf || in[0].isConst() ){ + gt = tn.mkGroundTerm(); + //} } if( !gt.isNull() ){ //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 24bd69854..299ae5678 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -56,7 +56,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_conflict( c, false ), d_collectTermsCache( c ), d_consTerms( c ), - d_selTerms( c ){ + d_selTerms( c ), + d_singleton_eq( u ){ // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); @@ -175,6 +176,7 @@ void TheoryDatatypes::check(Effort e) { Debug("datatypes-split") << "Check for splits " << e << endl; addedFact = false; do { + std::map< TypeNode, Node > rec_singletons; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node n = (*eqcs_i); @@ -186,89 +188,128 @@ void TheoryDatatypes::check(Effort e) { if( !hasLabel( eqc, n ) ){ Trace("datatypes-debug") << "No constructor..." << std::endl; const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - - std::vector< bool > pcons; - getPossibleCons( eqc, n, pcons ); - //std::cout << "pcons " << n << " = "; - //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; } - //std::cout << std::endl; - //check if we do not need to resolve the constructor type for this equivalence class. - // this is if there are no selectors for this equivalence class, its possible values are infinite, - // and we are not producing a model, then do not split. - int consIndex = -1; - bool needSplit = true; - for( unsigned int j=0; jd_selectors ) ) { - needSplit = false; + bool continueProc = true; + if( dt.isRecursiveSingleton() ){ + //handle recursive singleton case + std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn ); + if( itrs!=rec_singletons.end() ){ + Node eq = n.eqNode( itrs->second ); + if( d_singleton_eq.find( eq )==d_singleton_eq.end() ){ + d_singleton_eq[eq] = true; + // get assumptions + bool success = true; + std::vector< Node > assumptions; + //if there is at least one uninterpreted sort occurring within the datatype and the logic is not quantified, add lemmas ensuring cardinality is more than one, + // do not infer the equality if at least one sort was processed. + //otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one, + // infer the equality. + for( unsigned i=0; isecond ); + assumptions.push_back( eq ); + Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions ); + Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl; + d_out->lemma( lemma ); + } } + }else{ + rec_singletons[tn] = n; } + //do splitting for quantified logics (incomplete anyways) + continueProc = ( getQuantifiersEngine()!=NULL ); } - //d_dtfCounter++; - if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){ - //for the sake of termination, we must choose the constructor of a ground term - //NEED GUARENTEE: groundTerm should not contain any subterms of the same type - // TODO: this is probably not good enough, actually need fair enumeration strategy - if( !n.getType().isRecord() ){ //FIXME - Node groundTerm = n.getType().mkGroundTerm(); - if( groundTerm.getOperator().getType().isConstructor() ){ //FIXME - int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); - if( pcons[index] ){ - consIndex = index; + if( continueProc ){ + //all other cases + std::vector< bool > pcons; + getPossibleCons( eqc, n, pcons ); + //check if we do not need to resolve the constructor type for this equivalence class. + // this is if there are no selectors for this equivalence class, its possible values are infinite, + // and we are not producing a model, then do not split. + int consIndex = -1; + bool needSplit = true; + for( unsigned int j=0; jd_selectors ) ) { + needSplit = false; + } + } + } + //d_dtfCounter++; + if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){ + //for the sake of termination, we must choose the constructor of a ground term + //NEED GUARENTEE: groundTerm should not contain any subterms of the same type + // TODO: this is probably not good enough, actually need fair enumeration strategy + if( !n.getType().isRecord() ){ //FIXME + Node groundTerm = n.getType().mkGroundTerm(); + if( groundTerm.getOperator().getType().isConstructor() ){ //FIXME + int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); + if( pcons[index] ){ + consIndex = index; + } + needSplit = true; } - needSplit = true; } } - } - if( needSplit && consIndex!=-1 ) { - //if only one constructor, then this term must be this constructor - if( dt.getNumConstructors()==1 ){ - Node t = DatatypesRewriter::mkTester( n, 0, dt ); - d_pending.push_back( t ); - d_pending_exp[ t ] = d_true; - Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; - d_infer.push_back( t ); - }else{ - if( options::dtBinarySplit() ){ - Node test = DatatypesRewriter::mkTester( n, consIndex, dt ); - Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; - test = Rewriter::rewrite( test ); - NodeBuilder<> nb(kind::OR); - nb << test << test.notNode(); - Node lemma = nb; - d_out->lemma( lemma ); - d_out->requirePhase( test, true ); + if( needSplit && consIndex!=-1 ) { + //if only one constructor, then this term must be this constructor + if( dt.getNumConstructors()==1 ){ + Node t = DatatypesRewriter::mkTester( n, 0, dt ); + d_pending.push_back( t ); + d_pending_exp[ t ] = d_true; + Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; + d_infer.push_back( t ); }else{ - Trace("dt-split") << "*************Split for constructors on " << n << endl; - std::vector< Node > children; - if( dt.isSygus() && d_sygus_split ){ - std::vector< Node > lemmas; - d_sygus_split->getSygusSplits( n, dt, children, lemmas ); - for( unsigned i=0; ilemma( lemmas[i] ); - } + if( options::dtBinarySplit() ){ + Node test = DatatypesRewriter::mkTester( n, consIndex, dt ); + Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; + test = Rewriter::rewrite( test ); + NodeBuilder<> nb(kind::OR); + nb << test << test.notNode(); + Node lemma = nb; + d_out->lemma( lemma ); + d_out->requirePhase( test, true ); }else{ - for( unsigned i=0; i children; + if( dt.isSygus() && d_sygus_split ){ + std::vector< Node > lemmas; + d_sygus_split->getSygusSplits( n, dt, children, lemmas ); + for( unsigned i=0; ilemma( lemmas[i] ); + } + }else{ + for( unsigned i=0; imkNode( kind::OR, children ); + Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl; + d_out->lemma( lemma ); } - Assert( !children.empty() ); - Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children ); - Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl; - d_out->lemma( lemma ); + return; } - return; + }else{ + Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl; } - }else{ - Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl; } - }else{ Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl; } @@ -1415,6 +1456,30 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c } } +Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) { + int index = pol ? 0 : 1; + std::map< TypeNode, Node >::iterator it = d_singleton_lemma[index].find( tn ); + if( it==d_singleton_lemma[index].end() ){ + Node a; + if( pol ){ + Node v1 = NodeManager::currentNM()->mkBoundVar( tn ); + Node v2 = NodeManager::currentNM()->mkBoundVar( tn ); + a = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, v1, v2 ), v1.eqNode( v2 ) ); + }else{ + Node v1 = NodeManager::currentNM()->mkSkolem( "k1", tn ); + Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn ); + a = v1.eqNode( v2 ).negate(); + //send out immediately as lemma + d_out->lemma( a ); + Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl; + } + d_singleton_lemma[index][tn] = a; + return a; + }else{ + return it->second; + } +} + void TheoryDatatypes::collectTerms( Node n ) { if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){ d_collectTermsCache[n] = true; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 6604e5548..ab40f07db 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -180,6 +180,11 @@ private: /** sygus utilities */ SygusSplit * d_sygus_split; SygusSymBreak * d_sygus_sym_break; +private: + /** singleton lemmas (for degenerate co-datatype case) */ + std::map< TypeNode, Node > d_singleton_lemma[2]; + /** Cache for singleton equalities processed */ + BoolMap d_singleton_eq; private: /** assert fact */ void assertFact( Node fact, Node exp ); @@ -262,6 +267,8 @@ private: std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ); /** build model */ Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap, std::vector< Node >& fv ); + /** get singleton lemma */ + Node getSingletonLemma( TypeNode tn, bool pol ); /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 616c51f54..f9c8e42fd 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -528,7 +528,7 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) { for( unsigned k=0; k 0; } + /** Returns true iff this cardinality is one */ + bool isOne() const throw() { + return d_card == 1; + } /** * Returns true iff this cardinality is finite and large (i.e., diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 06a8187f2..cd27a897b 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -151,25 +151,100 @@ void Datatype::setSygus( Type st, Expr bvl ){ Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + std::vector< Type > processing; + computeCardinality( processing ); + return d_card; +} - // already computed? - if(!d_card.isUnknown()) { - return d_card; +Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){ + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){ + d_card = Cardinality::INTEGERS; + }else{ + processing.push_back( d_self ); + Cardinality c = 0; + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + c += (*i).computeCardinality( processing ); + } + d_card = c; + processing.pop_back(); } + return d_card; +} - RecursionBreaker breaker(__PRETTY_FUNCTION__, this); - - if(breaker.isRecursion()) { - return d_card = Cardinality::INTEGERS; +bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + if( d_card_rec_singleton==0 ){ + Assert( d_card_u_assume.empty() ); + std::vector< Type > processing; + if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){ + d_card_rec_singleton = 1; + }else{ + d_card_rec_singleton = -1; + } + if( d_card_rec_singleton==1 ){ + Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl; + for( unsigned i=0; i& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException){ + if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){ + return true; + }else{ + if( d_card_rec_singleton==0 ){ + //if not yet computed + if( d_constructors.size()==1 ){ + bool success = false; + processing.push_back( d_self ); + for(unsigned i = 0; i 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; + if( d_well_founded==0 ){ + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_self); + std::vector< Type > processing; + if( computeWellFounded( processing ) ){ + d_well_founded = 1; + }else{ + d_well_founded = -1; + } } + return d_well_founded==1; +} - 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; +bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){ + return d_isCo; + }else{ + processing.push_back( d_self ); + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if( (*i).computeWellFounded( processing ) ){ + processing.pop_back(); + return true; + }else{ + Trace("dt-wf") << "Constructor " << (*i).getName() << " is not well-founded." << std::endl; + } } + processing.pop_back(); + Trace("dt-wf") << "Datatype " << getName() << " is not well-founded." << std::endl; + return false; } - - self.setAttribute(DatatypeWellFoundedComputedAttr(), true); - self.setAttribute(DatatypeWellFoundedAttr(), false); - return false; } Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { 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); - Debug("datatypes") << "dt mkGroundTerm " << t << std::endl; TypeNode self = TypeNode::fromType(d_self); @@ -246,72 +319,18 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { if(!groundTerm.isNull()) { Debug("datatypes") << "\nin cache: " << d_self << " => " << groundTerm << std::endl; } 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( groundTerm.isNull() && (*i).getNumArgs() == 0) { - groundTerm = d_constructors[indexOf((*i).getConstructor())].mkGroundTerm( t ); - //groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor()); - self.setAttribute(DatatypeGroundTermAttr(), groundTerm); - Debug("datatypes-gt") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl; - } - } - // 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) { - if( groundTerm.isNull() ){ - DatatypeConstructor::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( t ); - // DatatypeConstructor::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 DatatypeConstructor::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; - } - } - } + std::vector< Type > processing; + groundTerm = computeGroundTerm( t, processing ); + if(!groundTerm.isNull() && !isParametric() ) { + // we found a ground-term-constructing constructor! + self.setAttribute(DatatypeGroundTermAttr(), groundTerm); + Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl; } } if( groundTerm.isNull() ){ if( !d_isCo ){ // 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!"); + CheckArgument(false, *this, "datatype is not well-founded, cannot construct a ground term!"); }else{ return groundTerm; } @@ -320,6 +339,31 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { } } +Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) { + if( std::find( processing.begin(), processing.end(), d_self )==processing.end() ){ + processing.push_back( d_self ); + for( unsigned r=0; r<2; r++ ){ + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + //do nullary constructors first + if( ((*i).getNumArgs()==0)==(r==0)){ + Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl; + Expr e = (*i).computeGroundTerm( t, processing ); + if( !e.isNull() ){ + processing.pop_back(); + return e; + }else{ + Debug("datatypes") << "...failed." << std::endl; + } + } + } + } + processing.pop_back(); + }else{ + Debug("datatypes") << "...already processing " << t << std::endl; + } + return Expr(); +} + DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) { CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); CheckArgument(!d_self.isNull(), *this); @@ -654,6 +698,35 @@ Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentExc return c; } +/** compute the cardinality of this datatype */ +Cardinality DatatypeConstructor::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){ + Cardinality c = 1; + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + Type t = SelectorType((*i).getSelector().getType()).getRangeType(); + if( t.isDatatype() ){ + const Datatype& dt = ((DatatypeType)t).getDatatype(); + c *= dt.computeCardinality( processing ); + }else{ + c *= t.getCardinality(); + } + } + return c; +} + +bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException){ + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + Type t = SelectorType((*i).getSelector().getType()).getRangeType(); + if( t.isDatatype() ){ + const Datatype& dt = ((DatatypeType)t).getDatatype(); + if( !dt.computeWellFounded( processing ) ){ + return false; + } + } + } + return true; +} + + bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); @@ -685,43 +758,8 @@ bool DatatypeConstructor::isWellFounded() const throw(IllegalArgumentException) // 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 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; + std::vector< Type > processing; + return computeWellFounded( processing ); } Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { @@ -778,6 +816,55 @@ Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(IllegalArgumentExce return groundTerm; } +Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) { +// we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_constructor); + + std::vector groundTerms; + groundTerms.push_back(getConstructor()); + + // for each selector, get a ground term + std::vector< Type > instTypes; + std::vector< Type > paramTypes; + if( DatatypeType(t).isParametric() ){ + paramTypes = DatatypeType(t).getDatatype().getParameters(); + instTypes = DatatypeType(t).getParamTypes(); + } + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + Type selType = SelectorType((*i).getSelector().getType()).getRangeType(); + if( DatatypeType(t).isParametric() ){ + selType = selType.substitute( paramTypes, instTypes ); + } + Expr arg; + if( selType.isDatatype() ){ + const Datatype & dt = DatatypeType(selType).getDatatype(); + arg = dt.computeGroundTerm( selType, processing ); + }else{ + arg = selType.mkGroundTerm(); + } + if( arg.isNull() ){ + Debug("datatypes") << "...unable to construct arg of " << (*i).getName() << std::endl; + return Expr(); + }else{ + Debug("datatypes") << "...constructed arg " << arg.getType() << std::endl; + groundTerms.push_back(arg); + } + } + + Expr groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms); + if( groundTerm.getType()!=t ){ + Assert( Datatype::datatypeOf( d_constructor ).isParametric() ); + //type is ambiguous, must apply type ascription + Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl; + groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION, + getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))), + groundTerms[0]); + groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms); + } + return groundTerm; +} + + const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const { CheckArgument(index < getNumArgs(), index, "index out of bounds"); return d_args[index]; diff --git a/src/util/datatype.h b/src/util/datatype.h index adb423c96..445048440 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -209,6 +209,13 @@ private: Type doParametricSubstitution(Type range, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements); + + /** compute the cardinality of this datatype */ + Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException); + /** compute whether this datatype is well-founded */ + bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException); + /** compute ground term */ + Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException); public: /** * Create a new Datatype constructor with the given name for the @@ -427,6 +434,7 @@ public: * */ class CVC4_PUBLIC Datatype { + friend class DatatypeConstructor; public: /** * Get the datatype of a constructor, selector, or tester operator. @@ -466,6 +474,16 @@ private: // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache mutable Cardinality d_card; + + // is this type a recursive singleton type + mutable int d_card_rec_singleton; + // if d_card_rec_singleton is true, + // infinite cardinality depends on at least one of the following uninterpreted sorts having cardinality > 1 + mutable std::vector< Type > d_card_u_assume; + // is this well-founded + mutable int d_well_founded; + // ground term for this datatype + mutable Expr d_ground_term; /** * Datatypes refer to themselves, recursively, and we have a @@ -502,6 +520,14 @@ private: throw(IllegalArgumentException, DatatypeResolutionException); friend class ExprManager;// for access to resolve() + /** compute the cardinality of this datatype */ + Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException); + /** compute whether this datatype is a recursive singleton */ + bool computeCardinalityRecSingleton( std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException); + /** compute whether this datatype is well-founded */ + bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException); + /** compute ground term */ + Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException); public: /** Create a new Datatype of the given name. */ @@ -570,6 +596,16 @@ public: */ bool isWellFounded() const throw(IllegalArgumentException); + /** + * Return true iff this datatype is a recursive singleton + */ + bool isRecursiveSingleton() const throw(IllegalArgumentException); + + + /** get number of recursive singleton argument types */ + unsigned getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException); + Type getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException); + /** * Construct and return a ground term of this Datatype. The * Datatype must be both resolved and well-founded, or else an @@ -698,7 +734,9 @@ inline Datatype::Datatype(std::string name, bool isCo) : d_resolved(false), d_self(), d_involvesExt(false), - d_card(CardinalityUnknown()) { + d_card(CardinalityUnknown()), + d_card_rec_singleton(0), + d_well_founded(0) { } inline Datatype::Datatype(std::string name, const std::vector& params, bool isCo) : @@ -709,7 +747,9 @@ inline Datatype::Datatype(std::string name, const std::vector& params, boo d_resolved(false), d_self(), d_involvesExt(false), - d_card(CardinalityUnknown()) { + d_card(CardinalityUnknown()), + d_card_rec_singleton(0), + d_well_founded(0) { } inline std::string Datatype::getName() const throw() { diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 80fea45fc..88f588aa0 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -61,7 +61,8 @@ TESTS = \ bug438b.cvc \ wrong-sel-simp.cvc \ tenum-bug.smt2 \ - cdt-non-canon-stream.smt2 + cdt-non-canon-stream.smt2 \ + stream-singleton.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/stream-singleton.smt2 b/test/regress/regress0/datatypes/stream-singleton.smt2 new file mode 100644 index 000000000..6884059ca --- /dev/null +++ b/test/regress/regress0/datatypes/stream-singleton.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) + +(declare-codatatypes () ((Stream (S (s Stream))))) + +(declare-fun x () Stream) +(declare-fun y () Stream) + +(assert (not (= x y))) + +(check-sat) \ No newline at end of file diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index c157db8c4..61da34460 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -228,8 +228,8 @@ public: //tryGoodInput("a : [0..0]; b : [-5..5]; c : [-1..1]; d : [ _ .._];"); // subranges tryGoodInput("a : [ _..1]; b : [_.. 0]; c :[_..-1];"); tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;"); - tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) END;"); - tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); + tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil END;"); + //tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); tryGoodInput("DATATYPE trex = Foo | Bar END; DATATYPE tree = node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); } -- 2.30.2