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.

diff --git a/src/theory/datatypes/inference.cpp b/src/theory/datatypes/inference.cpp
index f8dbd115324e13c828e34959128022564f1d2534..9c49b2a4e76d4e5d4671432eecfb938c296a70bb 100644 (file)
--- 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 31ede087b1c1caf210ba10a3d6d80aa54916e045..6923d8a1e75849b1f698e859d59cffee98b02cbc 100644 (file)
--- 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);
   /**