Fix bug with incremental+datatypes. Minor cleanup. Disable regression bug484, enabl...

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 72d0c6b2b0c9d4b4969fcdc4b59476784c2f7855..f4c399c129310a9be85ff528922affd3af65a4f9 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -49,7 +49,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"),
   d_labels( c ),
   d_selector_apps( c ),
-  d_consEqc( c ),
+  //d_consEqc( c ),
   d_conflict( c, false ),
   d_collectTermsCache( c ),
   d_consTerms( c ),
@@ -649,7 +649,7 @@ void TheoryDatatypes::eqNotifyNewClass(TNode t){
       }
     }
 */
-    d_consEqc[t] = true;
+    //d_consEqc[t] = true;
   }
 }
 
@@ -749,9 +749,9 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             if( d_conflict ){
               return;
             }
-            d_consEqc[t1] = true;
+            //d_consEqc[t1] = true;
           }
-          d_consEqc[t2] = false;
+          //d_consEqc[t2] = false;
         }
       }else{
         Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl;
@@ -1119,6 +1119,7 @@ void TheoryDatatypes::computeCareGraph(){
       TNode f1 = r==0 ? d_consTerms[i] : d_selTerms[i];
       for( unsigned j=i+1; j<functionTerms; j++ ){
         TNode f2 = r==0 ? d_consTerms[j] : d_selTerms[j];
+        Trace("dt-cg-debug") << "dt-cg: " << f1 << " and " << f2 << " " << (f1.getOperator()==f2.getOperator()) << " " << areEqual( f1, f2 ) << std::endl;
         if( f1.getOperator()==f2.getOperator() && !areEqual( f1, f2 ) ){
           Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
           bool somePairIsDisequal = false;
@@ -1183,6 +1184,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
         Node c = ei->d_constructor.get();
         cons.push_back( c );
         eqc_cons[ eqc ] = c;
+        Trace("dt-cmi") << "Datatypes : assert representative " << c << " for " << eqc << std::endl;
         m->assertRepresentative( c );
       }else{
         //if eqc contains a symbol known to datatypes (a selector), then we must assign
@@ -1303,6 +1305,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
       Trace("dt-cmi") << "Assign : " << neqc << std::endl;
       m->assertEquality( eqc, neqc, true );
       eqc_cons[ eqc ] = neqc;
+      Trace("dt-cmi") << "Datatypes : assert representative " << neqc << " for " << eqc << std::endl;
       m->assertRepresentative( neqc );
     }
     //m->assertRepresentative( neqc );
@@ -1369,6 +1372,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
       collectTerms( n[i] );
     }
     if( n.getKind() == APPLY_CONSTRUCTOR ){
+      Debug("datatypes") << "  Found constructor " << n << endl;
       d_consTerms.push_back( n );
     }else if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE ){
       d_selTerms.push_back( n );
@@ -1758,7 +1762,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
   if( n.getKind()==EQUAL || n.getKind()==IFF ){
     /*
     for( unsigned i=0; i<2; i++ ){
-      if( n[i].getKind()!=APPLY_SELECTOR_TOTAL && n[i].getKind()!=APPLY_CONSTRUCTOR ){
+      if( !n[i].isVar() && n[i].getKind()!=APPLY_SELECTOR_TOTAL && n[i].getKind()!=APPLY_CONSTRUCTOR ){
         addLemma = true;
       }
     }
@@ -1783,14 +1787,14 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
   }
   if( addLemma ){
     //check if we have already added this lemma
-    if( std::find( d_inst_lemmas[ n[0] ].begin(), d_inst_lemmas[ n[0] ].end(), n[1] )==d_inst_lemmas[ n[0] ].end() ){
-      d_inst_lemmas[ n[0] ].push_back( n[1] );
-      Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
-      return true;
-    }else{
-      Trace("dt-lemma-debug") << "Already communicated " << n << std::endl;
-      return false;
-    }
+    //if( std::find( d_inst_lemmas[ n[0] ].begin(), d_inst_lemmas[ n[0] ].end(), n[1] )==d_inst_lemmas[ n[0] ].end() ){
+    //  d_inst_lemmas[ n[0] ].push_back( n[1] );
+    Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
+    return true;
+    //}else{
+    //  Trace("dt-lemma-debug") << "Already communicated " << n << std::endl;
+    //  return false;
+    //}
   }
   //else if( exp.getKind()==APPLY_TESTER ){
     //if( n.getKind()==EQUAL && !DatatypesRewriter::isTermDatatype( n[0] ) ){

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 2777e775a673ce08e76e6586eb5008b5398760d9..84d894098a5cf5174bb8eeacebd22a41e9ef1a73 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -143,7 +143,7 @@ private:
   /** map from nodes to their instantiated equivalent for each constructor type */
   std::map< Node, std::map< int, Node > > d_inst_map;
   /** which instantiation lemmas we have sent */
-  std::map< Node, std::vector< Node > > d_inst_lemmas;
+  //std::map< Node, std::vector< Node > > d_inst_lemmas;
   /** labels for each equivalence class
    * for each eqc n, d_labels[n] is testers that hold for this equivalence class, either:
    * a list of equations of the form
@@ -157,7 +157,7 @@ private:
   /** selector apps for eqch equivalence class */
   NodeListMap d_selector_apps;
   /** constructor terms */
-  BoolMap d_consEqc;
+  //BoolMap d_consEqc;
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
   /** The conflict node */
@@ -168,14 +168,14 @@ private:
   std::vector< Node > d_pending;
   std::map< Node, Node > d_pending_exp;
   std::vector< Node > d_pending_merge;
-  /** expand definition skolem functions */
-  std::map< Node, Node > d_exp_def_skolem;
   /** All the constructor terms that the theory has seen */
   context::CDList<TNode> d_consTerms;
   /** All the selector terms that the theory has seen */
   context::CDList<TNode> d_selTerms;
   /** counter for forcing assignments (ensures fairness) */
   unsigned d_dtfCounter;
+  /** expand definition skolem functions */
+  std::map< Node, Node > d_exp_def_skolem;
 private:
   /** assert fact */
   void assertFact( Node fact, Node exp );

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 33f6ca9c898e5cb7fb0b93d0e6e3e3dc1f32bef8..1c62717c8fb494e1df4541403334260022694cdf 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -372,6 +372,7 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
 void TheoryModel::assertRepresentative(TNode n )
 {
   Trace("model-builder-reps") << "Assert rep : " << n << std::endl;
+  Trace("model-builder-reps") << "Rep eqc is : " << getRepresentative( n ) << std::endl;
   d_reps[ n ] = n;
 }
 
@@ -684,7 +685,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       if(t.isTuple() || t.isRecord()) {
         t = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
       }
-      TypeNode tb = t.getBaseType();      
+      TypeNode tb = t.getBaseType();
       if (!assignOne) {
         set<Node>* repSet = typeRepSet.getSet(tb);
         if (repSet != NULL && !repSet->empty()) {

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index ad4e8a6021aedf91b43e04667ae509de6b1211ec..7ffcff4e334eba090624f8a25a7ab0ada81b9ad9 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -145,7 +145,6 @@ BUG_TESTS = \
        bug421b.smt2 \
        bug425.cvc \
        bug480.smt2 \
-       bug484.smt2 \
        bug486.cvc \
        bug507.smt2 \
        bug512.minimized.smt2 \
@@ -175,6 +174,8 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
 # bug512 -- taking too long, --time-per not working perhaps? in any case,
 # we have a minimized version still getting tested
+# disabled for now (dt sharing issue):
+#    bug484.smt2 
 DISABLED_TESTS = \
        bug512.smt2
 

diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index a1232196e4d97a3ea4e9f2a92b1f2fd9dc05a868..a90b238e2eb9c468b973a70d98281b101ac2d907 100644 (file)
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -47,7 +47,8 @@ TESTS =       \
        constarr3.smt2 \
        constarr.cvc \
        constarr2.cvc \
-       constarr3.cvc
+       constarr3.cvc \
+       parsing_ringer.cvc
 
 EXTRA_DIST = $(TESTS)
 
@@ -60,8 +61,6 @@ EXTRA_DIST = $(TESTS)
 # and make sure to distribute it
 #EXTRA_DIST += \
 #      error.cvc
-# disabled for now (problem is related to records in model):
-#   parsing_ringer.cvc
 
 # synonyms for "check"
 .PHONY: regress regress0 test