From 9df318ca1ab33001bd203c24ae57a8b5739b8f36 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 1 Nov 2014 11:31:59 +0100
Subject: [PATCH] Fix some mistakes in datatypes theory combination, disable
 two regressions.  Minor fix for fun defs.

---
 src/theory/datatypes/theory_datatypes.cpp | 31 ++++++++++++-----------
 src/theory/quantifiers/term_database.cpp  |  2 +-
 test/regress/regress0/Makefile.am         |  6 ++---
 3 files changed, 20 insertions(+), 19 deletions(-)

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 516aae0e1..77cab86a2 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -532,11 +532,11 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
 void TheoryDatatypes::addSharedTerm(TNode t) {
   Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
                      << t << " " << t.getType().isBoolean() << endl;
-  if( t.getType().isBoolean() ){
+  //if( t.getType().isBoolean() ){
     //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES);
-  }else{
-    d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
-  }
+  //}else{
+  d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
+  //}
   Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
 }
 
@@ -1059,15 +1059,14 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
 }
 
 EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){
-  if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){
-    if (d_equalityEngine.areEqual(a, b)) {
-      // The terms are implied to be equal
-      return EQUALITY_TRUE;
-    }
-    if (d_equalityEngine.areDisequal(a, b, false)) {
-      // The terms are implied to be dis-equal
-      return EQUALITY_FALSE;
-    }
+  Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
+  if (d_equalityEngine.areEqual(a, b)) {
+    // The terms are implied to be equal
+    return EQUALITY_TRUE;
+  }
+  if (d_equalityEngine.areDisequal(a, b, false)) {
+    // The terms are implied to be dis-equal
+    return EQUALITY_FALSE;
   }
   return EQUALITY_FALSE_IN_MODEL;
 }
@@ -1088,12 +1087,14 @@ void TheoryDatatypes::computeCareGraph(){
           for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
             TNode x = f1[k];
             TNode y = f2[k];
+            Assert(d_equalityEngine.hasTerm(x));
+            Assert(d_equalityEngine.hasTerm(y));            
             if( areDisequal(x, y) ){
               somePairIsDisequal = true;
               break;
-            }else if( !areEqual( x, y ) ){
+            }else if( !d_equalityEngine.areEqual( x, y ) ){
               Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
-              if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
+              if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){
                 EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y);
                 if( eqStatus!=EQUALITY_UNKNOWN ){
                   TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 3f6f2a6ed..392fc269a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1001,7 +1001,7 @@ Node TermDb::getRewriteRule( Node q ) {
 }
 
 bool TermDb::isFunDef( Node q ) {
-  if( q.getKind()==FORALL && ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF ){
+  if( q.getKind()==FORALL && ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && q.getNumChildren()==3 ){
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
       if( q[2][i].getKind()==INST_ATTRIBUTE ){
         if( q[2][i][0].getAttribute(FunDefAttribute()) ){
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index fae563973..cbaa58b3c 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -106,8 +106,7 @@ CVC_TESTS = \
 	wiki.20.cvc \
 	wiki.21.cvc \
 	queries0.cvc \
-	print_lambda.cvc \
-	trim.cvc
+	print_lambda.cvc 
 
 # Regression tests for TPTP inputs
 TPTP_TESTS =
@@ -145,7 +144,6 @@ BUG_TESTS = \
 	bug421b.smt2 \
 	bug425.cvc \
 	bug480.smt2 \
-	bug484.smt2 \
 	bug486.cvc \
 	bug507.smt2 \
 	bug512.minimized.smt2 \
@@ -171,6 +169,8 @@ 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