From 20e58d420e4985ecc2cb76b5fcd55d4db8d9adc6 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 23 Oct 2020 13:24:05 -0500
Subject: [PATCH] Change datatypes lemma policy for equalities not coming from
 instantiate (#5325)

Recently, the policy for lemma vs fact changed for instantiate rule in datatypes to ensure that other theories were notified of terms having external finite type. This PR further refines the policy so that the instantiate rule is the only rule whose conclusion is an equality that is sent out as a lemma.

This means that equalities from unification and collapsing selectors are always kept internal. The justification for this is that the instantiate rule is applied for all terms with the proper policy, and hence it already covers all cases where we may need to introduce new terms.
---
 src/theory/datatypes/inference.cpp | 34 ++++++++++++------------------
 src/theory/datatypes/inference.h   |  6 +++---
 2 files changed, 17 insertions(+), 23 deletions(-)

diff --git a/src/theory/datatypes/inference.cpp b/src/theory/datatypes/inference.cpp
index f8dbd1153..9c49b2a4e 100644
--- a/src/theory/datatypes/inference.cpp
+++ b/src/theory/datatypes/inference.cpp
@@ -63,32 +63,26 @@ DatatypesInference::DatatypesInference(InferenceManager* im,
 bool DatatypesInference::mustCommunicateFact(Node n, Node exp)
 {
   Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
-  bool addLemma = false;
-  if (options::dtInferAsLemmas() && !exp.isConst())
+  // Force lemmas if option is set
+  if (options::dtInferAsLemmas())
   {
-    // all units are lemmas
-    addLemma = true;
-  }
-  else if (n.getKind() == EQUAL)
-  {
-    // Note that equalities due to instantiate are forced as lemmas if
-    // necessary as they are created. This ensures that terms are shared with
-    // external theories when necessary. We send the lemma here only if
-    // the equality is not for datatype terms, which can happen for collapse
-    // selector / term size or unification.
-    TypeNode tn = n[0].getType();
-    addLemma = !tn.isDatatype();
+    Trace("dt-lemma-debug")
+        << "Communicate " << n << " due to option" << std::endl;
+    return true;
   }
+  // Note that equalities due to instantiate are forced as lemmas if
+  // necessary as they are created. This ensures that terms are shared with
+  // external theories when necessary. We send the lemma here only if the
+  // conclusion has kind LEQ (for datatypes size) or OR. Notice that
+  // all equalities are kept internal, apart from those forced as lemmas
+  // via instantiate.
   else if (n.getKind() == LEQ || n.getKind() == OR)
   {
-    addLemma = true;
-  }
-  if (addLemma)
-  {
-    Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
+    Trace("dt-lemma-debug")
+        << "Communicate " << n << " due to kind" << std::endl;
     return true;
   }
-  Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl;
+  Trace("dt-lemma-debug") << "Do not communicate " << n << std::endl;
   return false;
 }
 
diff --git a/src/theory/datatypes/inference.h b/src/theory/datatypes/inference.h
index 31ede087b..6923d8a1e 100644
--- a/src/theory/datatypes/inference.h
+++ b/src/theory/datatypes/inference.h
@@ -96,9 +96,9 @@ class DatatypesInference : public SimpleTheoryInternalFact
    * size( tn )
    *  (6) non-negative size : 0 <= size(t)
    * This method returns true if the fact must be sent out as a lemma. If it
-   * returns false, then we assert the fact internally. We may need to
-   * communicate outwards if the conclusions involve other theories.  Also
-   * communicate (6) and OR conclusions.
+   * returns false, then we assert the fact internally. We return true for (6)
+   * and OR conclusions. We also return true if the option dtInferAsLemmas is
+   * set to true.
    */
   static bool mustCommunicateFact(Node n, Node exp);
   /**
-- 
2.30.2