made datatypes rewrite incorrect selectors to ground term. this feature can be turne...

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 5bae534e1f5a40552daa64280011f30ef1fc36e3..fae2c5bffe1917117f207716e63d3ba68979d6fa 100644 (file)
--- 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 f1c8fd657309bb4de90ef894a99cbe054e9bc032..ba0dcc348c467f9f99e089a41101d4eebb976bb6 100644 (file)
--- 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 17638b00a8a96244813b40e43e5df11ac2a0143a..f93599fe947c44f791e8dd5c152bb57fdcb0dc78 100644 (file)
--- 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 3ba3249f18eebe4d19ed394805d0852abd756a69..c033903b55fa19da5d35d35cdbeb2e50224cebc0 100644 (file)
--- 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;