From: ajreynol Date: Fri, 11 Sep 2015 13:16:12 +0000 (+0200) Subject: Minor cleanup related to codatatypes. X-Git-Tag: cvc5-1.0.0~6241 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ace360b4da1edef06088a366dc21b58f9431efc2;p=cvc5.git Minor cleanup related to codatatypes. --- diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 4f9e497ea..0f5e020d8 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -582,6 +582,9 @@ public: /** Is this a parameterized datatype type */ bool isParametricDatatype() const; + /** Is this a codatatype type */ + bool isCodatatype() const; + /** Is this a fully instantiated datatype type */ bool isInstantiatedDatatype() const; @@ -985,6 +988,15 @@ inline bool TypeNode::isParametricDatatype() const { ( isPredicateSubtype() && getSubtypeParentType().isParametricDatatype() ); } +/** Is this a codatatype type */ +inline bool TypeNode::isCodatatype() const { + if( isDatatype() ){ + return getDatatype().isCodatatype(); + }else{ + return false; + } +} + /** Is this a constructor type */ inline bool TypeNode::isConstructor() const { return getKind() == kind::CONSTRUCTOR_TYPE; @@ -1004,7 +1016,7 @@ inline bool TypeNode::isTester() const { and sig significand bits */ inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const { return - ( getKind() == kind::FLOATINGPOINT_TYPE && + ( getKind() == kind::FLOATINGPOINT_TYPE && getConst().exponent() == exp && getConst().significand() == sig ) || ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint(exp,sig) ); diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index c342e488a..4b60044d0 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -60,8 +60,9 @@ public: } if( in.isConst() ){ Node inn = normalizeConstant( in ); + Assert( !inn.isNull() ); if( inn!=in ){ - Trace("datatypes-rewrite-debug") << "Normalized constant " << in << " -> " << inn << std::endl; + Trace("datatypes-rewrite") << "Normalized constant " << in << " -> " << inn << std::endl; return RewriteResponse(REWRITE_DONE, inn); } } @@ -399,8 +400,7 @@ private: Node ret = n; bool isCdt = false; if( tn.isDatatype() ){ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( !dt.isCodatatype() ){ + if( !tn.isCodatatype() ){ //nested datatype within codatatype : can be normalized independently since all loops should be self-contained ret = normalizeConstant( n ); }else{ @@ -592,10 +592,9 @@ public: } //normalize constant : apply to top-level codatatype constants static Node normalizeConstant( Node n ){ - if( n.getType().isDatatype() ){ - Assert( n.getType().isDatatype() ); - const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); - if( dt.isCodatatype() ){ + TypeNode tn = n.getType(); + if( tn.isDatatype() ){ + if( tn.isCodatatype() ){ return normalizeCodatatypeConstant( n ); }else{ std::vector< Node > children; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 72717f974..af8e5c503 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -190,6 +190,7 @@ void TheoryDatatypes::check(Effort e) { const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); bool continueProc = true; if( dt.isRecursiveSingleton() ){ + Trace("datatypes-debug") << "Check recursive singleton..." << std::endl; //handle recursive singleton case std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn ); if( itrs!=rec_singletons.end() ){ @@ -230,6 +231,7 @@ void TheoryDatatypes::check(Effort e) { continueProc = ( getQuantifiersEngine()!=NULL ); } if( continueProc ){ + Trace("datatypes-debug") << "Get possible cons..." << std::endl; //all other cases std::vector< bool > pcons; getPossibleCons( eqc, n, pcons ); @@ -237,32 +239,30 @@ void TheoryDatatypes::check(Effort e) { // 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; + int fconsIndex = -1; bool needSplit = true; for( unsigned int j=0; jd_selectors ) ) { - needSplit = false; + if( !dt[ j ].isFinite() ) { + if( !eqc || !eqc->d_selectors ){ + needSplit = false; + } + }else{ + if( fconsIndex==-1 ){ + fconsIndex = j; + } } } } + //if we want to force an assignment of constructors to all ground eqc //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; - } - } + Trace("datatypes-force-assign") << "Force assignment for " << n << std::endl; + needSplit = true; + consIndex = fconsIndex!=-1 ? fconsIndex : consIndex; } if( needSplit && consIndex!=-1 ) { @@ -1391,8 +1391,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ for( std::map< Node, Node >::iterator it = eqc_cons.begin(); it != eqc_cons.end(); ++it ){ Node eqc = it->first; - const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); - if( dt.isCodatatype() ){ + if( eqc.getType().isCodatatype() ){ //until models are implemented for codatatypes //throw Exception("Models for codatatypes are not supported in this version."); //must proactive expand to avoid looping behavior in model builder @@ -1583,7 +1582,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ int index = getLabelIndex( eqc, n ); const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype(); //must be finite or have a selector - //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment() + //if( eqc->d_selectors || dt[ index ].isFinite() ){ //instantiate this equivalence class eqc->d_inst = true; Node tt_cons = getInstantiateCons( tt, dt, index ); @@ -1613,8 +1612,7 @@ void TheoryDatatypes::checkCycles() { Node eqc = (*eqcs_i); TypeNode tn = eqc.getType(); if( DatatypesRewriter::isTypeDatatype( tn ) ) { - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( !dt.isCodatatype() ){ + if( !tn.isCodatatype() ){ if( options::dtCyclic() ){ //do cycle checks std::map< TNode, bool > visited; @@ -1846,8 +1844,7 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on, }else{ TypeNode tn = nn.getType(); if( DatatypesRewriter::isTypeDatatype( tn ) ) { - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( !dt.isCodatatype() ){ + if( !tn.isCodatatype() ){ return nn; } } @@ -1855,15 +1852,6 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on, } } -bool TheoryDatatypes::mustSpecifyAssignment(){ - //FIXME: the condition finiteModelFind is an over-approximation in this function - // we still may not want to specify assignments for datatypes that are truly infinite - // the fix for this is to correctly compute the cardinality for datatypes containing uninterpered sorts in fmf (i.e. by assuming they are finite) - return options::finiteModelFind() || options::produceModels() || options::dtForceAssignment(); - //return options::produceModels(); - //return false; -} - bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ //the datatypes decision procedure makes "internal" inferences apart from the equality engine : // (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index a221153a3..b452e02d1 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -277,11 +277,6 @@ private: void processNewTerm( Node n ); /** check instantiate */ void instantiate( EqcInfo* eqc, Node n ); - /** must specify model - * This returns true when the datatypes theory is expected to specify the constructor - * type for all equivalence classes. - */ - bool mustSpecifyAssignment(); /** must communicate fact */ bool mustCommunicateFact( Node n, Node exp ); /** check clash mod eq */ diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index da3c0cce0..3cf603100 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1044,8 +1044,15 @@ Node ConjectureGenerator::getPredicateForType( TypeNode tn ) { void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) { if( n.getNumChildren()>0 ){ std::vector< int > vec; + std::vector< TypeNode > types; for( unsigned i=0; igetEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){ + if( vec_sumgetEnumerateTerm( types[index], vec[index]+1 ).isNull() ){ vec[index]++; vec_sum++; vec.push_back( size_limit - vec_sum ); @@ -1074,7 +1081,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< } if( success ){ if( vec.size()==n.getNumChildren() ){ - Node lc = getTermDatabase()->getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] ); + Node lc = getTermDatabase()->getEnumerateTerm( types[vec.size()-1], vec[vec.size()-1] ); if( !lc.isNull() ){ for( unsigned i=0; i children; children.push_back( n.getOperator() ); for( unsigned i=0; i<(vec.size()-1); i++ ){ - Node nn = getTermDatabase()->getEnumerateTerm( n[i].getType(), vec[i] ); + Node nn = getTermDatabase()->getEnumerateTerm( types[i], vec[i] ); Assert( !nn.isNull() ); Assert( nn.getType()==n[i].getType() ); children.push_back( nn ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 9985d3cdb..d076c6510 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -594,7 +594,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ Node mbt; if( tn.isInteger() || tn.isReal() ){ mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) ); - }else if( !tn.isArray() && !tn.isSort() ){ + }else if( isClosedEnumerableType( tn ) ){ mbt = tn.mkGroundTerm(); }else{ if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){ @@ -963,6 +963,9 @@ Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { return d_enum_terms[tn][index]; } +bool TermDb::isClosedEnumerableType( TypeNode tn ) { + return !tn.isArray() && !tn.isSort() && !tn.isCodatatype(); +} Node TermDb::getFreeVariableForInstConstant( Node n ){ return getFreeVariableForType( n.getType() ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 136d77268..fb80cb8a8 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -282,6 +282,8 @@ private: public: //get nth term for type Node getEnumerateTerm( TypeNode tn, unsigned index ); + //does this type have an enumerator that produces constants that are handled by ground theory solvers + static bool isClosedEnumerableType( TypeNode tn ); //miscellaneous public: