// 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());
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() );
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);
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);
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;
}
}
}
+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;
/** 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 );
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 */
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) ){
** \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
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:
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.,
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) {
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);
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;
}
}
}
+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);
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");
// 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) {
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];
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
*
*/
class CVC4_PUBLIC Datatype {
+ friend class DatatypeConstructor;
public:
/**
* Get the datatype of a constructor, selector, or tester operator.
// "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
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. */
*/
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
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) :
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() {
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
--- /dev/null
+(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
//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;");
}
projects / cvc5.git / commitdiff