Avoid duplicate lemmas in datatypes (#3310)

We previously were sending e.g. dt.size >= 0 lemmas when size terms are pre-registered, which can happen multiple times in a user context. This ensures we cache whether a lemma is sent in a user-context dependent way in the datatypes solver. This ensures we don't send the same lemma twice for dt.size >= 0 lemmas.

2 files changed, 82 insertions, 70 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 609cdaf6e..8bac280b6 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -57,6 +57,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c,
       d_addedLemma(false),
       d_addedFact(false),
       d_collectTermsCache(c),
+      d_collectTermsCacheU(u),
       d_functionTerms(c),
       d_singleton_eq(u),
       d_lemmas_produced_c(u)
@@ -459,8 +460,9 @@ bool TheoryDatatypes::doSendLemma( Node lem ) {
 }
 bool TheoryDatatypes::doSendLemmas( std::vector< Node >& lemmas ){
   bool ret = false;
-  for( unsigned i=0; i<lemmas.size(); i++ ){
-    bool cret = doSendLemma( lemmas[i] );
+  for (const Node& lem : lemmas)
+  {
+    bool cret = doSendLemma(lem);
     ret = ret || cret;
   }
   lemmas.clear();
@@ -526,9 +528,6 @@ void TheoryDatatypes::preRegisterTerm(TNode n) {
     d_equalityEngine.addTriggerPredicate(n);
     break;
   default:
-    if( n.getKind()==kind::DT_SIZE ){
-      d_out->lemma( NodeManager::currentNM()->mkNode( LEQ, d_zero, n ) );
-    }
     // Function applications/predicates
     d_equalityEngine.addTerm(n);
     if( d_sygus_sym_break ){
@@ -1664,74 +1663,79 @@ Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
 }
 
 void TheoryDatatypes::collectTerms( Node n ) {
-  if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){
-    d_collectTermsCache[n] = true;
-    //for( int i=0; i<(int)n.getNumChildren(); i++ ) {
-    //  collectTerms( n[i] );
-    //}
-    if( n.getKind() == APPLY_CONSTRUCTOR ){
-      Debug("datatypes") << "  Found constructor " << n << endl;
-      if( n.getNumChildren()>0 ){
-        d_functionTerms.push_back( n );
-      }
-    }else{
+  if (d_collectTermsCache.find(n) != d_collectTermsCache.end())
+  {
+    // already processed
+    return;
+  }
+  d_collectTermsCache[n] = true;
+  Kind nk = n.getKind();
+  if (nk == APPLY_CONSTRUCTOR)
+  {
+    Debug("datatypes") << "  Found constructor " << n << endl;
+    if (n.getNumChildren() > 0)
+    {
+      d_functionTerms.push_back(n);
+    }
+    return;
+  }
+  if (nk == APPLY_SELECTOR_TOTAL || nk == DT_SIZE || nk == DT_HEIGHT_BOUND)
+  {
+    d_functionTerms.push_back(n);
+    // we must also record which selectors exist
+    Trace("dt-collapse-sel") << "  Found selector " << n << endl;
+    Node rep = getRepresentative(n[0]);
+    // record it in the selectors
+    EqcInfo* eqc = getOrMakeEqcInfo(rep, true);
+    // add it to the eqc info
+    addSelector(n, eqc, rep);
+  }
+
+  // now, do user-context-dependent lemmas
+  if (nk != DT_SIZE && nk != DT_HEIGHT_BOUND)
+  {
+    // if not one of these kinds, there are no lemmas
+    return;
+  }
+  if (d_collectTermsCacheU.find(n) != d_collectTermsCacheU.end())
+  {
+    return;
+  }
+  d_collectTermsCacheU[n] = true;
 
-      if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){
-        d_functionTerms.push_back( n );
-        //we must also record which selectors exist
-        Trace("dt-collapse-sel") << "  Found selector " << n << endl;
-        Node rep = getRepresentative( n[0] );
-        //record it in the selectors
-        EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
-        //add it to the eqc info
-        addSelector( n, eqc, rep );
-
-        if( n.getKind() == DT_SIZE ){
-  /*
-          //add size = 0 lemma
-          Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) );
-          std::vector< Node > children;
-          children.push_back( nn.negate() );
-          const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
-          for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-            if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){
-              Node test = DatatypesRewriter::mkTester( n[0], i, dt );
-              children.push_back( test );
-            }
-          }
-          conc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
-          Trace("datatypes-infer") << "DtInfer : zero size : " << conc << std::endl;
-          d_pending.push_back( conc );
-          d_pending_exp[ conc ] = d_true;
-          d_infer.push_back( conc );
-  */
-        }
+  NodeManager* nm = NodeManager::currentNM();
 
-        if( n.getKind() == DT_HEIGHT_BOUND ){
-          if( n[1].getConst<Rational>().isZero() ){
-            std::vector< Node > children;
-            const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
-            for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-              if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){
-                Node test = DatatypesRewriter::mkTester( n[0], i, dt );
-                children.push_back( test );
-              }
-            }
-            Node lem;
-            if( children.empty() ){
-              lem = n.negate();
-            }else{
-              lem = NodeManager::currentNM()->mkNode( EQUAL, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) );
-            }
-            Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
-            //d_pending.push_back( lem );
-            //d_pending_exp[ lem ] = d_true;
-            //d_infer.push_back( lem );
-            d_pending_lem.push_back( lem );
-          }
-        }
+  if (nk == DT_SIZE)
+  {
+    Node lem = nm->mkNode(LEQ, d_zero, n);
+    Trace("datatypes-infer")
+        << "DtInfer : size geq zero : " << lem << std::endl;
+    d_pending_lem.push_back(lem);
+  }
+  else if (nk == DT_HEIGHT_BOUND && n[1].getConst<Rational>().isZero())
+  {
+    std::vector<Node> children;
+    const Datatype& dt = n[0].getType().getDatatype();
+    for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+    {
+      if (DatatypesRewriter::isNullaryConstructor(dt[i]))
+      {
+        Node test = DatatypesRewriter::mkTester(n[0], i, dt);
+        children.push_back(test);
       }
     }
+    Node lem;
+    if (children.empty())
+    {
+      lem = n.negate();
+    }
+    else
+    {
+      lem = n.eqNode(children.size() == 1 ? children[0]
+                                          : nm->mkNode(OR, children));
+    }
+    Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
+    d_pending_lem.push_back(lem);
   }
 }
 
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index b4803e69a..e14a78df2 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -205,8 +205,16 @@ private:
   bool d_addedFact;
   /** The conflict node */
   Node d_conflictNode;
-  /** cache for which terms we have called collectTerms(...) on */
+  /**
+   * SAT-context dependent cache for which terms we have called
+   * collectTerms(...) on.
+   */
   BoolMap d_collectTermsCache;
+  /**
+   * User-context dependent cache for which terms we have called
+   * collectTerms(...) on.
+   */
+  BoolMap d_collectTermsCacheU;
   /** pending assertions/merges */
   std::vector< Node > d_pending_lem;
   std::vector< Node > d_pending;