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 /src/theory | |
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.
Diffstat (limited to 'src/theory')
-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 |
5 files changed, 160 insertions, 80 deletions
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: |