From: ajreynol Date: Wed, 24 Sep 2014 11:33:31 +0000 (+0200) Subject: Partial support for codatatype models. X-Git-Tag: cvc5-1.0.0~6622 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cb1c193049fc8ac1bf5522fc6a114e9a804039a3;p=cvc5.git Partial support for codatatype models. --- diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 508106106..44474c18a 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -302,9 +302,6 @@ operator SEXPR 0: "a symbolic expression (any arity)" operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body" -## for co-datatypes, not yet supported -# operator MU 2 "mu" - parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjuction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator" constant CHAIN_OP \ ::CVC4::Chain \ @@ -336,7 +333,6 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule -#typerule MU ::CVC4::theory::builtin::MuTypeRule typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 045f440e6..977a097d0 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -164,27 +164,6 @@ public: } };/* class LambdaTypeRule */ -/* For co-datatypes, not yet supported-- -** -class MuTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - if( n[0].getType(check) != nodeManager->boundVarListType() ) { - std::stringstream ss; - ss << "expected a bound var list for MU expression, got `" - << n[0].getType().toString() << "'"; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - std::vector argTypes; - for(TNode::iterator i = n[0].begin(); i != n[0].end(); ++i) { - argTypes.push_back((*i).getType()); - } - TypeNode rangeType = n[1].getType(check); - return nodeManager->mkFunctionType(argTypes, rangeType); - } -}; -**/ - class ChainTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index d8b42111c..faaf78fe4 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -89,6 +89,12 @@ typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionType # constructor applications are constant if they are applied only to constants construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule +## for co-datatypes +operator MU 2 "a mu operator, first argument is a bound variable, second argument is body" +typerule MU ::CVC4::theory::datatypes::DatatypeMuTypeRule +# mu applications are constant expressions +construle MU ::CVC4::theory::datatypes::DatatypeMuTypeRule + operator TUPLE_TYPE 0: "tuple type" cardinality TUPLE_TYPE \ "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index d3f0dac9b..145cd32dd 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1321,32 +1321,44 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); if( dt.isCodatatype() ){ std::map< Node, Node > vmap; - Node v = getCodatatypesValue( it->first, eqc_cons, eqc_mu, vmap ); - Trace("dt-cmi-cod") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << std::endl; + std::vector< Node > fv; + Node v = getCodatatypesValue( it->first, eqc_cons, eqc_mu, vmap, fv ); + Trace("dt-cmi-cdt") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl; + m->assertEquality( eqc, v, true ); } } } -Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap ){ +Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap, std::vector< Node >& fv ){ std::map< Node, Node >::iterator itv = vmap.find( n ); if( itv!=vmap.end() ){ + if( std::find( fv.begin(), fv.end(), itv->second )==fv.end() ){ + fv.push_back( itv->second ); + } return itv->second; }else if( DatatypesRewriter::isTermDatatype( n ) ){ - Node nv = NodeManager::currentNM()->mkBoundVar( n.getType() ); + std::stringstream ss; + ss << "$x" << vmap.size(); + Node nv = NodeManager::currentNM()->mkBoundVar( ss.str().c_str(), n.getType() ); vmap[n] = nv; - Trace("dt-cmi-cod-debug") << " map " << n << " -> " << nv << std::endl; + Trace("dt-cmi-cdt-debug") << " map " << n << " -> " << nv << std::endl; Node nc = eqc_cons[n]; Assert( nc.getKind()==APPLY_CONSTRUCTOR ); std::vector< Node > children; children.push_back( nc.getOperator() ); for( unsigned i=0; imkNode( APPLY_CONSTRUCTOR, children ); + Node v = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + //add mu if we found a circular reference + if( std::find( fv.begin(), fv.end(), nv )!=fv.end() ){ + v = NodeManager::currentNM()->mkNode( MU, nv, v ); + } + return v; }else{ return n; } @@ -1464,7 +1476,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ void TheoryDatatypes::checkCycles() { Debug("datatypes-cycle-check") << "Check cycles" << std::endl; - std::vector< Node > cod_eqc; + std::vector< Node > cdt_eqc; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); @@ -1495,30 +1507,30 @@ void TheoryDatatypes::checkCycles() { } }else{ //indexing - cod_eqc.push_back( eqc ); + cdt_eqc.push_back( eqc ); } } ++eqcs_i; } //process codatatypes - if( cod_eqc.size()>1 && options::cdtBisimilar() ){ - Trace("dt-cod-debug") << "Process " << cod_eqc.size() << " co-datatypes" << std::endl; + if( cdt_eqc.size()>1 && options::cdtBisimilar() ){ + Trace("dt-cdt-debug") << "Process " << cdt_eqc.size() << " co-datatypes" << std::endl; std::vector< std::vector< Node > > part_out; std::vector< TNode > exp; std::map< Node, Node > cn; std::map< Node, std::map< Node, int > > dni; - for( unsigned i=0; i part; part.push_back( part_out[i][0] ); for( unsigned j=1; j > tpart_out; exp.clear(); @@ -1530,16 +1542,16 @@ void TheoryDatatypes::checkCycles() { Assert( tpart_out.size()==1 && tpart_out[0].size()==2 ); part.pop_back(); //merge based on explanation - Trace("dt-cod") << " exp is : "; + Trace("dt-cdt") << " exp is : "; for( unsigned k=0; k& part, std::vector< std::map< Node, Node >& cn, std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ){ if( !mkExp ){ - Trace("dt-cod-debug") << "Separate bisimilar : " << std::endl; + Trace("dt-cdt-debug") << "Separate bisimilar : " << std::endl; for( unsigned i=0; isecond << std::endl; } + if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is looping at index " << it_rec->second << std::endl; } new_part_rec[ it_rec->second ].push_back( part[j] ); }else{ if( DatatypesRewriter::isTermDatatype( c ) ){ @@ -1582,14 +1594,14 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector< explainEquality( c, ncons, true, exp ); } new_part[cc].push_back( part[j] ); - if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is datatype " << ncons << "." << std::endl; } + if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is datatype " << ncons << "." << std::endl; } }else{ new_part_c[c].push_back( part[j] ); - if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is unspecified datatype." << std::endl; } + if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is unspecified datatype." << std::endl; } } }else{ //add equivalences - if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is term " << c << "." << std::endl; } + if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is term " << c << "." << std::endl; } new_part_c[c].push_back( part[j] ); } } @@ -1631,7 +1643,7 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector< //for each child of constructor unsigned cindex = 0; while( cindexfirst << "..." << std::endl; } + if( !mkExp ){ Trace("dt-cdt-debug") << "Split argument #" << cindex << " of " << it->first << "..." << std::endl; } std::vector< std::vector< Node > > next_split_new_part; for( unsigned j=0; j& cn, 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 ); + 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 ); /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index ddad913fe..8ce8ee7df 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -209,6 +209,49 @@ struct DatatypeAscriptionTypeRule { } };/* struct DatatypeAscriptionTypeRule */ +/* For co-datatypes */ +class DatatypeMuTypeRule { +private: + //a Mu-expression is constant iff its body is composed of constructors applied to constant expr and bound variables only + inline static bool computeIsConstNode(TNode n, std::vector< TNode >& fv ){ + if( n.getKind()==kind::MU ){ + fv.push_back( n[0] ); + bool ret = computeIsConstNode( n[1], fv ); + fv.pop_back(); + return ret; + }else if( n.isConst() || std::find( fv.begin(), fv.end(), n )!=fv.end() ){ + return true; + }else if( n.getKind()==kind::APPLY_CONSTRUCTOR ){ + for( unsigned i=0; i fv; + return computeIsConstNode( n, fv ); + } +}; + + struct ConstructorProperties { inline static Cardinality computeCardinality(TypeNode type) { // Constructors aren't exactly functions, they're like