From: Andrew Reynolds Date: Tue, 9 Oct 2012 17:44:02 +0000 (+0000) Subject: made datatypes rewrite incorrect selectors to ground term. this feature can be turne... X-Git-Tag: cvc5-1.0.0~7718 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=680d9e20d412afe24a23dcaf3a4e440bcf208fbe;p=cvc5.git made datatypes rewrite incorrect selectors to ground term. this feature can be turned off by --disable-dt-rewrite-error-sel. changed regression answer to reflect new default behavior. --- diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 5bae534e1..fae2c5bff 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -22,6 +22,7 @@ #define __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H #include "theory/rewriter.h" +#include "theory/datatypes/options.h" namespace CVC4 { namespace theory { @@ -74,21 +75,22 @@ public: << "Rewrite trivial selector " << in << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); - } - /* - Node gt = in.getType().mkGroundTerm(); - TypeNode gtt = gt.getType(); - //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); - if( !gtt.isInstantiatedDatatype() ){ - gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); + }else{ + if( options::dtRewriteErrorSel() ){ + Node gt = in.getType().mkGroundTerm(); + TypeNode gtt = gt.getType(); + //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); + if( !gtt.isInstantiatedDatatype() ){ + gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); + } + Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + << "Rewrite trivial selector " << in + << " to distinguished ground term " + << in.getType().mkGroundTerm() << std::endl; + return RewriteResponse(REWRITE_DONE,gt ); } - Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " - << "Rewrite trivial selector " << in - << " to distinguished ground term " - << in.getType().mkGroundTerm() << std::endl; - return RewriteResponse(REWRITE_DONE,gt ); - */ + } } if(in.getKind() == kind::EQUAL && in[0] == in[1]) { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index f1c8fd657..ba0dcc348 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -93,6 +93,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_infer_exp(c), d_notify( *this ), d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"), + d_selector_apps( c ), d_labels( c ), d_conflict( c, false ){ @@ -211,9 +212,15 @@ void TheoryDatatypes::check(Effort e) { ++eqcs_i; } flushPendingFacts(); - //if( !d_conflict ){ - // printModelDebug(); - //} + if( !d_conflict ){ + if( options::dtRewriteErrorSel() ){ + collapseSelectors(); + flushPendingFacts(); + } + } + if( !d_conflict ){ + // printModelDebug(); + } } if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) { @@ -710,18 +717,21 @@ void TheoryDatatypes::collectTerms( Node n ) { d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); } }else if( n.getKind() == APPLY_SELECTOR ){ - //we must also record which selectors exist - Debug("datatypes") << " Found selector " << n << endl; - if (n.getType().isBoolean()) { - d_equalityEngine.addTriggerPredicate( n ); - }else{ - d_equalityEngine.addTerm( n ); - } - Node rep = getRepresentative( n[0] ); - EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); - if( !eqc->d_selectors ){ - eqc->d_selectors = true; - instantiate( eqc, rep ); + if( d_selector_apps.find( n )==d_selector_apps.end() ){ + d_selector_apps[n] = false; + //we must also record which selectors exist + Debug("datatypes") << " Found selector " << n << endl; + if (n.getType().isBoolean()) { + d_equalityEngine.addTriggerPredicate( n ); + }else{ + d_equalityEngine.addTerm( n ); + } + Node rep = getRepresentative( n[0] ); + EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); + if( !eqc->d_selectors ){ + eqc->d_selectors = true; + instantiate( eqc, rep ); + } } } } @@ -770,6 +780,32 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index //} } +void TheoryDatatypes::collapseSelectors(){ + //must check incorrect applications of selectors + for( BoolMap::iterator it = d_selector_apps.begin(); it != d_selector_apps.end(); ++it ){ + if( !(*it).second ){ + Node n = (*it).first[0]; + EqcInfo* ei = getOrMakeEqcInfo( n ); + if( ei ){ + if( !ei->d_constructor.get().isNull() ){ + Node op = (*it).first.getOperator(); + Node cons = ei->d_constructor; + Node sn = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, op, cons ); + Node s = Rewriter::rewrite( sn ); + if( sn!=s ){ + Node eq = s.eqNode( sn ); + d_pending.push_back( eq ); + d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true ); + Trace("datatypes-infer") << "DtInfer : " << eq << ", by rewrite" << std::endl; + d_infer.push_back( eq ); + } + d_selector_apps[ (*it).first ] = true; + } + } + } + } +} + void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ //add constructor to equivalence class if not done so already if( hasLabel( eqc, n ) && !eqc->d_inst ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 17638b00a..f93599fe9 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -139,6 +139,8 @@ private: eq::EqualityEngine d_equalityEngine; /** information necessary for equivalence classes */ std::map< Node, EqcInfo* > d_eqc_info; + /** selector applications */ + BoolMap d_selector_apps; /** map from nodes to their instantiated equivalent for each constructor type */ std::map< Node, std::map< int, Node > > d_inst_map; /** which instantiation lemmas we have sent */ @@ -225,6 +227,8 @@ private: void processNewTerm( Node n ); /** check instantiate */ void instantiate( EqcInfo* eqc, Node n ); + /** collapse selectors */ + void collapseSelectors(); /** must specify model * This returns true when the datatypes theory is expected to specify the constructor * type for all equivalence classes. diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc index 3ba3249f1..c033903b5 100644 --- a/test/regress/regress0/datatypes/wrong-sel-simp.cvc +++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc @@ -1,5 +1,5 @@ -% EXPECT: invalid -% EXIT: 10 +% EXPECT: valid +% EXIT: 20 DATATYPE nat = succ(pred : nat) | zero END;