Lemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for datatypes model generation for UFinite datatypes when FMF.

4 files changed, 46 insertions, 23 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9ba20fcc9..35d82b2ae 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -57,7 +57,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
       d_collectTermsCache( c ),
       d_consTerms( c ),
       d_selTerms( c ),
-      d_singleton_eq( u )
+      d_singleton_eq( u ),
+      d_lemmas_produced_c( u )
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
@@ -131,6 +132,7 @@ void TheoryDatatypes::check(Effort e) {
   if (done() && !fullEffort(e)) {
     return;
   }
+  Assert( d_pending.empty() && d_pending_merge.empty() );
   d_addedLemma = false;
 
   TimerStat::CodeTimer checkTimer(d_checkTime);
@@ -221,7 +223,7 @@ void TheoryDatatypes::check(Effort e) {
                     assumptions.push_back( eq );
                     Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions );
                     Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl;
-                    d_out->lemma( lemma );
+                    doSendLemma( lemma );
                   }
                 }
               }else{
@@ -246,7 +248,7 @@ void TheoryDatatypes::check(Effort e) {
                   if( consIndex==-1 ){
                     consIndex = j;
                   }
-                  if( !dt[ j ].isFinite() && ( !options::finiteModelFind() || !dt.isUFinite() ) ) {
+                  if( options::finiteModelFind() ? !dt[ j ].isUFinite() : !dt[ j ].isFinite() ) {
                     if( !eqc || !eqc->d_selectors ){
                       needSplit = false;
                     }
@@ -281,7 +283,7 @@ void TheoryDatatypes::check(Effort e) {
                     NodeBuilder<> nb(kind::OR);
                     nb << test << test.notNode();
                     Node lemma = nb;
-                    d_out->lemma( lemma );
+                    doSendLemma( lemma );
                     d_out->requirePhase( test, true );
                   }else{
                     Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
@@ -291,7 +293,7 @@ void TheoryDatatypes::check(Effort e) {
                       d_sygus_split->getSygusSplits( n, dt, children, lemmas );
                       for( unsigned i=0; i<lemmas.size(); i++ ){
                         Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl;
-                        d_out->lemma( lemmas[i] );
+                        doSendLemma( lemmas[i] );
                       }
                     }else{
                       for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
@@ -302,7 +304,7 @@ void TheoryDatatypes::check(Effort e) {
                     Assert( !children.empty() );
                     Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children );
                     Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
-                    d_out->lemma( lemma );
+                    doSendLemma( lemma );
                   }
                   return;
                 }
@@ -339,6 +341,7 @@ void TheoryDatatypes::check(Effort e) {
     }
   }
 
+  Trace("datatypes-check") << "Finished check effort " << e << std::endl;
   if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
     Notice() << "TheoryDatatypes::check(): done" << endl;
   }
@@ -365,7 +368,7 @@ void TheoryDatatypes::flushPendingFacts(){
           lem = Rewriter::rewrite( lem );
         }
         Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
-        d_out->lemma( lem );
+        doSendLemma( lem );
         d_addedLemma = true;
       }else{
         assertFact( fact, exp );
@@ -390,6 +393,13 @@ void TheoryDatatypes::doPendingMerges(){
   d_pending_merge.clear();
 }
 
+void TheoryDatatypes::doSendLemma( Node lem ) {
+  if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
+    d_lemmas_produced_c[lem] = true;
+    d_out->lemma( lem );
+  }
+}
+
 void TheoryDatatypes::assertFact( Node fact, Node exp ){
   Assert( d_pending_merge.empty() );
   bool polarity = fact.getKind() != kind::NOT;
@@ -412,7 +422,7 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
         d_sygus_sym_break->addTester( atom );
         for( unsigned i=0; i<d_sygus_sym_break->d_lemmas.size(); i++ ){
           Trace("dt-lemma-sygus") << "Sygus symmetry breaking lemma : " << d_sygus_sym_break->d_lemmas[i] << std::endl;
-          d_out->lemma( d_sygus_sym_break->d_lemmas[i] );
+          doSendLemma( d_sygus_sym_break->d_lemmas[i] );
         }
         d_sygus_sym_break->d_lemmas.clear();
         /*
@@ -768,6 +778,7 @@ void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){
 /** called when two equivalance classes have merged */
 void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){
   if( DatatypesRewriter::isTermDatatype( t1 ) ){
+    Debug("datatypes-debug") << "NotifyPostMerge : " << t1 << " " << t2 << std::endl;
     d_pending_merge.push_back( t1.eqNode( t2 ) );
   }
 }
@@ -785,6 +796,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
       }
       EqcInfo* eqc1 = getOrMakeEqcInfo( t1 );
       if( eqc1 ){
+        Debug("datatypes-debug") << "  merge eqc info " << eqc2 << " into " << eqc1 << std::endl;
         if( !eqc1->d_constructor.get().isNull() ){
           trep1 = eqc1->d_constructor.get();
         }
@@ -793,7 +805,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         TNode cons2 = eqc2->d_constructor.get();
         //if both have constructor, then either clash or unification
         if( !cons1.isNull() && !cons2.isNull() ){
-          Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl;
+          Debug("datatypes-debug") << "  constructors : " << cons1 << " " << cons2 << std::endl;
           Node unifEq = cons1.eqNode( cons2 );
           /*
           std::vector< Node > exp;
@@ -812,6 +824,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
           if( conf ){
             exp.push_back( unifEq );
             d_conflictNode = explain( exp );
+          }
          */
           std::vector< Node > rew;
           if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){
@@ -844,12 +857,11 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
 */
           }
         }
-        if( !eqc1->d_inst && eqc2->d_inst ){
-          eqc1->d_inst = true;
-        }
+        Debug("datatypes-debug") << "  instantiated : " << eqc1->d_inst << " " << eqc2->d_inst << std::endl;
+        eqc1->d_inst = eqc1->d_inst || eqc2->d_inst;
         if( !cons2.isNull() ){
           if( cons1.isNull() ){
-            Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl;
+            Debug("datatypes-debug") << "  must check if it is okay to set the constructor." << std::endl;
             checkInst = true;
             addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
             if( d_conflict ){
@@ -860,7 +872,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
           //d_consEqc[t2] = false;
         }
       }else{
-        Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl;
+        Debug("datatypes-debug") << "  no eqc info for " << t1 << ", must create" << std::endl;
         //just copy the equivalence class information
         eqc1 = getOrMakeEqcInfo( t1, true );
         eqc1->d_inst.set( eqc2->d_inst );
@@ -872,12 +884,12 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
       //merge labels
       NodeListMap::iterator lbl_i = d_labels.find( t2 );
       if( lbl_i != d_labels.end() ){
-        Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl;
+        Debug("datatypes-debug") << "  merge labels from " << eqc2 << " " << t2 << std::endl;
         NodeList* lbl = (*lbl_i).second;
         for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){
           addTester( *j, eqc1, t1 );
           if( d_conflict ){
-            Debug("datatypes-debug") << "Conflict!" << std::endl;
+            Debug("datatypes-debug") << "  conflict!" << std::endl;
             return;
           }
         }
@@ -889,19 +901,21 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
       }
       NodeListMap::iterator sel_i = d_selector_apps.find( t2 );
       if( sel_i != d_selector_apps.end() ){
-        Debug("datatypes-debug") << "Merge selectors from " << eqc2 << " " << t2 << std::endl;
+        Debug("datatypes-debug") << "  merge selectors from " << eqc2 << " " << t2 << std::endl;
         NodeList* sel = (*sel_i).second;
         for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
           addSelector( *j, eqc1, t1, eqc2->d_constructor.get().isNull() );
         }
       }
       if( checkInst ){
+        Debug("datatypes-debug") << "  checking instantiate" << std::endl;
         instantiate( eqc1, t1 );
         if( d_conflict ){
           return;
         }
       }
     }
+    Debug("datatypes-debug") << "Finished Merge " << t1 << " " << t2 << std::endl;
   }
 }
 
@@ -1363,7 +1377,8 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
         if( neqc.isNull() ){
           for( unsigned i=0; i<pcons.size(); i++ ){
             //must try the infinite ones first
-            if( pcons[i] && (r==1)==dt[ i ].isFinite() ){
+            bool cfinite = options::finiteModelFind() ? dt[ i ].isUFinite() : dt[ i ].isFinite();
+            if( pcons[i] && (r==1)==cfinite ){
               neqc = DatatypesRewriter::getInstCons( eqc, dt, i );
               //for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
               //  //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
@@ -1447,7 +1462,7 @@ Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
       Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
       a = v1.eqNode( v2 ).negate();
       //send out immediately as lemma
-      d_out->lemma( a );
+      doSendLemma( a );
       Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl;
     }
     d_singleton_lemma[index][tn] = a;
@@ -1554,7 +1569,9 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index
       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 );
+      //doSendLemma( eq );
+      d_pending.push_back( eq );
+      d_pending_exp[ eq ] = d_true;
     }
     Node n_ic = DatatypesRewriter::getInstCons( k, dt, index );
     //Assert( n_ic==Rewriter::rewrite( n_ic ) );
@@ -1592,6 +1609,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
       Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl;
       d_pending.push_back( eq );
       d_pending_exp[ eq ] = exp;
+      Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl;
       Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl;
       //eqc->d_inst.set( eq );
       d_infer.push_back( eq );
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index fc6e435cc..212b9d7cf 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -184,10 +184,11 @@ private:
 private:
   /** singleton lemmas (for degenerate co-datatype case) */
   std::map< TypeNode, Node > d_singleton_lemma[2];
-
   /** Cache for singleton equalities processed */
   BoolMap d_singleton_eq;
-
+  /** list of all lemmas produced */
+  BoolMap d_lemmas_produced_c;
+private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
 
@@ -196,7 +197,8 @@ private:
 
   /** do pending merged */
   void doPendingMerges();
-
+  /** do send lemma */
+  void doSendLemma( Node lem );
   /** get or make eqc info */
   EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 3813d7cd2..e7a87927a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -95,6 +95,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_term_db = new quantifiers::TermDb( c, u, this );
   d_tr_trie = new inst::TriggerTrie;
   d_hasAddedLemma = false;
+  //don't add true lemma
+  d_lemmas_produced_c[d_term_db->d_true] = true;
 
   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4405fe406..07a170a08 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4023,6 +4023,7 @@ void TheoryStrings::checkExtendedFuncs() {
           addMembership( it->first ? it->second[i] : it->second[i].negate() );
         }
       }
+      Trace("strings-process") << "Checking memberships..." << std::endl;
       checkMemberships();
       Trace("strings-process") << "Done check memberships, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
     }