Remove ref skolem datatype option (#4185)

Fixes #4180, fixes CVC4/cvc4-projects#133, fixes CVC4/cvc4-projects#134.

diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 82e8335061edaf490c0943cc51f11f415420d432..ac371efeb7f2389428639ba82d5a770e11dae37b 100644 (file)
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -31,15 +31,6 @@ header = "options/datatypes_options.h"
   read_only  = true
   help       = "do binary splits for datatype constructor types"
 
-[[option]]
-  name       = "dtRefIntro"
-  category   = "regular"
-  long       = "dt-ref-sk-intro"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "introduce reference skolems for shorter explanations"
-
 [[option]]
   name       = "cdtBisimilar"
   category   = "regular"

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index d202648f4939a838e98db22866308b0dff4ae5e2..7fbe5bc68188d6864b88a4bb81857ece88842755 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1306,15 +1306,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
   Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl;
   Node r;
   bool wrong = false;
-  Node use_s;
-  Node eq_exp;
-  if( options::dtRefIntro() ){
-    eq_exp = d_true;
-    use_s = getTermSkolemFor( c );
-  }else{
-    eq_exp = c.eqNode( s[0] );
-    use_s = s;
-  }
+  Node eq_exp = c.eqNode(s[0]);
   if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
     Node selector = s.getOperator();
     size_t constructorIndex = utils::indexOf(c.getOperator());
@@ -1322,14 +1314,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
     const DTypeConstructor& dtc = dt[constructorIndex];
     int selectorIndex = dtc.getSelectorIndexInternal(selector);
     wrong = selectorIndex<0;
-    
-    //if( wrong ){
-    //  return;
-    //}
     r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
-    if( options::dtRefIntro() ){
-      use_s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), use_s );
-    }
   }
   if( !r.isNull() ){
     Node rr = Rewriter::rewrite( r );
@@ -1341,14 +1326,10 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
       std::map< Node, Node > visited;
       rrs = removeUninterpretedConstants( rr, visited );
     }
-    if( use_s!=rrs ){
-      Node eq = use_s.eqNode( rrs );
-      Node peq;
-      if( options::dtRefIntro() ){
-        peq = d_true;
-      }else{
-        peq = c.eqNode(s[0]);
-      }
+    if (s != rrs)
+    {
+      Node eq = s.eqNode(rrs);
+      Node peq = c.eqNode(s[0]);
       Trace("datatypes-infer") << "DtInfer : collapse sel";
       //Trace("datatypes-infer") << ( wrong ? " wrong" : "");
       Trace("datatypes-infer") << " : " << eq << " by " << peq << std::endl;