Minor fix to avoid rewriting datatype equalities into non-equalitiers, as required. Add APPLY_UF to congruence types to avoid model construction bugs.

2 files changed, 20 insertions, 8 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index e884248e7..75d1f2b2e 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -207,13 +207,10 @@ public:
       std::vector< Node > rew;
       if( checkClash(in[0], in[1], rew) ){
         Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl;
-        return RewriteResponse(REWRITE_DONE,
-                               NodeManager::currentNM()->mkConst(false));
-      }else if( rew.size()!=1 || rew[0]!=in ){
-        Node nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) :
-                    ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
-        Trace("datatypes-rewrite") << "Rewrite equality to " << nn << std::endl;
-        return RewriteResponse(REWRITE_AGAIN_FULL, nn );
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
+      }else if( rew.size()==1 && rew[0]!=in ){
+        Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << rew[0] << std::endl;
+        return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] );
       }
     }
 
@@ -242,7 +239,7 @@ public:
           }
         }
       }
-    }else{
+    }else if( n1!=n2 ){
       Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
       rew.push_back( eq );
     }
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 8afcbb1de..2fb1a2679 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -56,6 +56,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
   d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
+  d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 }
 
 TheoryDatatypes::~TheoryDatatypes() {
@@ -412,6 +413,19 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
         NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
       }
     }
+
+    if( in.getKind()==EQUAL ){
+      Node nn;
+      std::vector< Node > rew;
+      if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
+        nn = NodeManager::currentNM()->mkConst(false);
+      }else{
+        nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) :
+                  ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
+      }
+      return nn;
+    }
+
     // nothing to do
     return in;
   }
@@ -465,6 +479,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
 
   Assert(!n.isNull());
 
+
   Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl;
 
   return n;