Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemmas being...

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 77cab86a24298631fbecb383b438c902c218f587..2b5e52415ba22bfec470191cc63d2ae009517c32 100644 (file)
--- 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 cbaa58b3c3d0e1a45c01d1a510bb79f1adbe5dfd..b2724e89aa712fdb90f8a75fd9e950f36ee33d8c 100644 (file)
--- 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