From 6b652f7239aaf7ef1793eb115a6e7371a3ec54eb Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 1 Nov 2014 13:01:31 +0100
Subject: [PATCH] Fix bug 592: introduce skolem for dt instantiate lemma
 (avoids terms in lemmas being rewritten).  Minor improvement to dt care
 graph.  Reenable regressions.

---
 src/theory/datatypes/theory_datatypes.cpp | 20 ++++++++++++++++----
 test/regress/regress0/Makefile.am         |  4 ++--
 2 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 77cab86a2..2b5e52415 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1096,7 +1096,10 @@ void TheoryDatatypes::computeCareGraph(){
               Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
               if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){
                 EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y);
-                if( eqStatus!=EQUALITY_UNKNOWN ){
+                if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_UNKNOWN ){
+                  somePairIsDisequal = true;
+                  break;
+                }else{
                   TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
                   TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
                   Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
@@ -1433,10 +1436,19 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index,
     return it->second;
   }else{
     //add constructor to equivalence class
-    Node n_ic = DatatypesRewriter::getInstCons( n, dt, index );
+    Node k = n;
+    if( n.getKind()==APPLY_CONSTRUCTOR ){
+      //must construct variable to refer to n, add lemma immediately
+      k = NodeManager::currentNM()->mkSkolem( "k", n.getType(), "for dt instantiation" );
+      Node eq = k.eqNode( n );
+      Trace("datatypes-infer") << "DtInfer : instantiation ref : " << eq << std::endl;
+      d_out->lemma( eq );
+    }
+    Node n_ic = DatatypesRewriter::getInstCons( k, dt, index );
     if( isActive ){
       for( unsigned i = 0; i<n_ic.getNumChildren(); i++ ){
-        processNewTerm( n_ic[i] );
+        Assert( n_ic[i]==Rewriter::rewrite( n_ic[i] ) );
+        //processNewTerm( n_ic[i] );
       }
       collectTerms( n_ic );
     }
@@ -1760,7 +1772,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
     //    break;
     //  }
     //}
-  }else if( n.getKind()==EQUAL && ( n[0].getKind()==DT_SIZE || n[1].getKind()==DT_SIZE ) ){
+  }else if( n.getKind()==EQUAL && !n[0].getType().isDatatype() ){
     addLemma = true;
   }else if( n.getKind()==LEQ ){
     addLemma = true;
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index cbaa58b3c..b2724e89a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -106,6 +106,7 @@ CVC_TESTS = \
 	wiki.20.cvc \
 	wiki.21.cvc \
 	queries0.cvc \
+	trim.cvc \
 	print_lambda.cvc 
 
 # Regression tests for TPTP inputs
@@ -144,6 +145,7 @@ BUG_TESTS = \
 	bug421b.smt2 \
 	bug425.cvc \
 	bug480.smt2 \
+	bug484.smt2 \
 	bug486.cvc \
 	bug507.smt2 \
 	bug512.minimized.smt2 \
@@ -169,8 +171,6 @@ BUG_TESTS = \
 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
 # bug512 -- taking too long, --time-per not working perhaps? in any case,
-# bug484.smt2 
-# trim.cvc
 # we have a minimized version still getting tested
 DISABLED_TESTS = \
 	bug512.smt2
-- 
2.30.2