diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-13 14:12:32 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-13 14:12:41 +0100 |
commit | 82fbac8829cbc41927216b36ab064b50e50b2fa0 (patch) | |
tree | 346361d002c109b8ac2254f4f215a12dfc7643d2 | |
parent | 3ba153b4be4c2fe8ad7decf8ebc7cf5d8815a0e9 (diff) |
Handle recursive singleton case for codatatypes, add regression. Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
-rw-r--r-- | src/parser/parser.cpp | 10 | ||||
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 16 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 205 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 2 | ||||
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 10 | ||||
-rw-r--r-- | src/util/cardinality.h | 4 | ||||
-rw-r--r-- | src/util/datatype.cpp | 367 | ||||
-rw-r--r-- | src/util/datatype.h | 44 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/stream-singleton.smt2 | 11 | ||||
-rw-r--r-- | test/unit/parser/parser_black.h | 4 |
12 files changed, 457 insertions, 226 deletions
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<Datatype>& 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; j<pcons.size(); j++ ) { - if( pcons[j] ) { - if( consIndex==-1 ){ - consIndex = j; - } - if( !dt[ j ].isFinite() && ( !eqc || !eqc->d_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; i<dt.getNumRecursiveSingletonArgTypes(); i++ ){ + TypeNode tn = TypeNode::fromType( dt.getRecursiveSingletonArgType( i ) ); + if( getQuantifiersEngine() ){ + // under the assumption that the cardinality of this type is one + Node a = getSingletonLemma( tn, true ); + assumptions.push_back( a.negate() ); + }else{ + success = false; + // assert that the cardinality of this type is more than one + getSingletonLemma( tn, false ); + } + } + if( success ){ + Node eq = n.eqNode( itrs->second ); + 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; j<pcons.size(); j++ ) { + if( pcons[j] ) { + if( consIndex==-1 ){ + consIndex = j; + } + if( !dt[ j ].isFinite() && ( !eqc || !eqc->d_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; i<lemmas.size(); i++ ){ - Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl; - d_out->lemma( 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<dt.getNumConstructors(); i++ ){ - Node test = DatatypesRewriter::mkTester( n, i, dt ); - children.push_back( test ); + 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; i<lemmas.size(); i++ ){ + Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl; + d_out->lemma( lemmas[i] ); + } + }else{ + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + Node test = DatatypesRewriter::mkTester( n, i, dt ); + children.push_back( test ); + } } + 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 ); } - 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 @@ -181,6 +181,11 @@ private: 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 ); /** flush pending facts */ @@ -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<vars[lhs].size(); k++ ){ int v = vars[lhs][k]; Trace("cegqi-si-debug") << " variable " << v << std::endl; - Assert( vars[lhs].size()==vn ); + Assert( (int)vars[lhs].size()==vn ); //check if already processed bool proc = d_eq_processed[lhs][rhs].find( v )!=d_eq_processed[lhs][rhs].end(); if( proc==(p==1) ){ diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index d37aa1b7d..244cb303d 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Clark Barrett ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Tim King, Liana Hadarean, Peter Collingbourne + ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Tim King, Liana Hadarean, Peter Collingbourne, Andrew Reynolds ** 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 @@ -197,6 +197,14 @@ void UnconstrainedSimplifier::processUnconstrained() break; } } + if( parent[0].getType().isDatatype() ){ + TypeNode tn = parent[0].getType(); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + if( dt.isRecursiveSingleton() ){ + //domain size may be 1 + break; + } + } case kind::BITVECTOR_COMP: case kind::LT: case kind::LEQ: diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 524d9cda4..113cb954c 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -156,6 +156,10 @@ public: bool isFinite() const throw() { return d_card > 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<const Datatype*, DatatypeHashFunction> 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<d_card_u_assume.size(); i++ ){ + Trace("dt-card") << " " << d_card_u_assume [i] << std::endl; + } + Trace("dt-card") << std::endl; + } } + return d_card_rec_singleton==1; +} - Cardinality c = 0; - for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - // We can't just add to d_card here, since this function is reentrant - c += (*i).getCardinality(); - } +unsigned Datatype::getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException) { + return d_card_u_assume.size(); +} +Type Datatype::getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException) { + return d_card_u_assume[i]; +} - return d_card = c; +bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& 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<d_constructors[0].getNumArgs(); i++ ) { + Type t = ((SelectorType)d_constructors[0][i].getType()).getRangeType(); + //if it is an uninterpreted sort, then we depend on it having cardinality one + if( t.isSort() ){ + if( std::find( u_assume.begin(), u_assume.end(), t )==u_assume.end() ){ + u_assume.push_back( t ); + } + //if it is a datatype, recurse + }else if( t.isDatatype() ){ + const Datatype & dt = ((DatatypeType)t).getDatatype(); + if( !dt.computeCardinalityRecSingleton( processing, u_assume ) ){ + return false; + }else{ + success = true; + } + //if it is a builtin type, it must have cardinality one + }else if( !t.getCardinality().isOne() ){ + return false; + } + } + processing.pop_back(); + return success; + }else{ + return false; + } + }else if( d_card_rec_singleton==-1 ){ + return false; + }else{ + for( unsigned i=0; i<d_card_u_assume.size(); i++ ){ + if( std::find( u_assume.begin(), u_assume.end(), d_card_u_assume[i] )==u_assume.end() ){ + u_assume.push_back( d_card_u_assume[i] ); + } + } + return true; + } + } } bool Datatype::isFinite() const throw(IllegalArgumentException) { @@ -200,44 +275,42 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) { bool Datatype::isWellFounded() 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); - - TypeNode self = TypeNode::fromType(d_self); - - // is this already in the cache ? - if(self.getAttribute(DatatypeWellFoundedComputedAttr())) { - return self.getAttribute(DatatypeWellFoundedAttr()); - } - - RecursionBreaker<const Datatype*, DatatypeHashFunction> 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<const DatatypeConstructor*, DatatypeHashFunction> 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<Expr> 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<Type>& params, bool isCo) : @@ -709,7 +747,9 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& 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;"); } |