TheoryIds for UF theory. (#5901)

This PR introduces new InferenceId for the uf theory and uses them instead of InferenceId::UNKNOWN.

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 5a2158d00bad90db9bed16c680f7359ab669f295..81c34cf3f73496aff8d6ba00f49feee90eded04c 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -141,6 +141,13 @@ const char* toString(InferenceId i)
     case InferenceId::STRINGS_REDUCTION: return "REDUCTION";
     case InferenceId::STRINGS_PREFIX_CONFLICT: return "PREFIX_CONFLICT";
 
+    case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE";
+    case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM";
+    case InferenceId::UF_HO_EXTENSIONALITY: return "UF_HO_EXTENSIONALITY";
+    case InferenceId::UF_HO_MODEL_APP_ENCODE: return "UF_HO_MODEL_APP_ENCODE";
+    case InferenceId::UF_HO_MODEL_EXTENSIONALITY:
+      return "UF_HO_MODEL_EXTENSIONALITY";
+
     default: return "?";
   }
 }

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index f28faa0371030f5703a7cff6243b5e2ffb55d620..a48a8c366c2ad2ced80b00c199f395e2a09fb35f 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -404,7 +404,40 @@ enum class InferenceId
   STRINGS_PREFIX_CONFLICT,
   //-------------------------------------- end prefix conflict
 
-  UNKNOWN,
+  // Clause from the uf symmetry breaker
+  UF_BREAK_SYMMETRY,
+  UF_CARD_CLIQUE,
+  UF_CARD_COMBINED,
+  UF_CARD_ENFORCE_NEGATIVE,
+  UF_CARD_EQUIV,
+  UF_CARD_MONOTONE_COMBINED,
+  UF_CARD_SIMPLE_CONFLICT,
+  UF_CARD_SPLIT,
+  //-------------------------------------- begin HO extension to UF
+  // Encodes an n-ary application as a chain of binary HO_APPLY applications
+  //   (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
+  UF_HO_APP_ENCODE,
+  UF_HO_APP_CONV_SKOLEM,
+  // Adds an extensionality lemma to witness that disequal functions have
+  // different applications
+  //   (not (= (f sk1 .. skn) (g sk1 .. skn))
+  UF_HO_EXTENSIONALITY,
+  //-------------------------------------- begin model-construction specific part
+  // These rules are necessary to ensure that we build models properly. For more
+  // details see Section 3.3 of Barbosa et al. CADE'19.
+  //
+  // Enforces that a regular APPLY_UF term in the model is equal to its HO_APPLY
+  // equivalent by adding the equality as a lemma
+  //   (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
+  UF_HO_MODEL_APP_ENCODE,
+  // Adds an extensionality lemma to witness that disequal functions have
+  // different applications
+  //   (not (= (f sk1 .. skn) (g sk1 .. skn))
+  UF_HO_MODEL_EXTENSIONALITY,
+  //-------------------------------------- end model-construction specific part
+  //-------------------------------------- end HO extension to UF
+
+  UNKNOWN
 };
 
 /**

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 697a828a4dfe7a1b2d922b53d41c5208577055dd..861da355895a4a601ed00fd3a616a2cda4fdabbe 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1037,7 +1037,7 @@ int SortModel::addSplit(Region* r)
     //split on the equality s
     Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
     // send lemma, with caching
-    if (d_im.lemma(lem, InferenceId::UNKNOWN))
+    if (d_im.lemma(lem, InferenceId::UF_CARD_SPLIT))
     {
       Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
       //tell the sat solver to explore the equals branch first
@@ -1070,7 +1070,7 @@ void SortModel::addCliqueLemma(std::vector<Node>& clique)
   eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
   Node lem = NodeManager::currentNM()->mkNode(OR, eqs);
   // send lemma, with caching
-  if (d_im.lemma(lem, InferenceId::UNKNOWN))
+  if (d_im.lemma(lem, InferenceId::UF_CARD_CLIQUE))
   {
     Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
     ++(d_thss->d_statistics.d_clique_lemmas);
@@ -1082,7 +1082,7 @@ void SortModel::simpleCheckCardinality() {
     Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ),
                                                       getCardinalityLiteral( d_maxNegCard.get() ).negate() );
     Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl;
-    d_im.conflict(lem, InferenceId::UNKNOWN);
+    d_im.conflict(lem, InferenceId::UF_CARD_SIMPLE_CONFLICT);
   }
 }
 
@@ -1179,7 +1179,7 @@ bool SortModel::checkLastCall()
         Node lem = NodeManager::currentNM()->mkNode(
             OR, cl, NodeManager::currentNM()->mkAnd(force_cl));
         Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
-        d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
+        d_im.lemma(lem, InferenceId::UF_CARD_ENFORCE_NEGATIVE, LemmaProperty::NONE, false);
         return false;
       }
     }
@@ -1399,7 +1399,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
           Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
           eqv_lit = lit.eqNode( eqv_lit );
           Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
-          d_im.lemma(eqv_lit, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
+          d_im.lemma(eqv_lit, InferenceId::UF_CARD_EQUIV, LemmaProperty::NONE, false);
           d_card_assertions_eqv_lemma[lit] = true;
         }
       }
@@ -1528,7 +1528,7 @@ void CardinalityExtension::check(Theory::Effort level)
                     Node eq = Rewriter::rewrite( a.eqNode( b ) );
                     Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
                     Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
-                    d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
+                    d_im.lemma(lem, InferenceId::UF_CARD_SPLIT, LemmaProperty::NONE, false);
                     d_im.requirePhase(eq, true);
                     type_proc[tn] = true;
                     break;
@@ -1707,7 +1707,7 @@ void CardinalityExtension::checkCombinedCardinality()
                              << " : " << cf << std::endl;
         Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
                                 << " : " << cf << std::endl;
-        d_im.conflict(cf, InferenceId::UNKNOWN);
+        d_im.conflict(cf, InferenceId::UF_CARD_MONOTONE_COMBINED);
         return;
       }
     }
@@ -1745,7 +1745,7 @@ void CardinalityExtension::checkCombinedCardinality()
                            << std::endl;
       Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
                               << std::endl;
-      d_im.conflict(cf, InferenceId::UNKNOWN);
+      d_im.conflict(cf, InferenceId::UF_CARD_COMBINED);
     }
   }
 }

diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 55e2500af0b626f8493a953484e52e2b139846b8..a9e48d7ca9b47883a4ded539a9bdce8e428e2566 100644 (file)
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -107,7 +107,7 @@ unsigned HoExtension::applyExtensionality(TNode deq)
     Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc);
     Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
                          << std::endl;
-    d_im.lemma(lem, InferenceId::UNKNOWN);
+    d_im.lemma(lem, InferenceId::UF_HO_EXTENSIONALITY);
     return 1;
   }
   return 0;
@@ -167,7 +167,7 @@ Node HoExtension::getApplyUfForHoApply(Node node)
       Trace("uf-ho-lemma")
           << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem
           << std::endl;
-      d_im.lemma(lem, InferenceId::UNKNOWN);
+      d_im.lemma(lem, InferenceId::UF_HO_APP_CONV_SKOLEM);
       d_uf_std_skolem[f] = new_f;
     }
     else
@@ -256,7 +256,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
               Node lem = nm->mkNode(OR, deq.negate(), eq);
               Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
                              << std::endl;
-              d_im.lemma(lem, InferenceId::UNKNOWN);
+              d_im.lemma(lem, InferenceId::UF_HO_MODEL_EXTENSIONALITY);
               return 1;
             }
           }
@@ -284,7 +284,12 @@ unsigned HoExtension::applyAppCompletion(TNode n)
     Node eq = n.eqNode(ret);
     Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
                          << std::endl;
-    d_im.assertInternalFact(eq, true, InferenceId::UNKNOWN, PfRule::HO_APP_ENCODE, {}, {n});
+    d_im.assertInternalFact(eq,
+                            true,
+                            InferenceId::UF_HO_APP_ENCODE,
+                            PfRule::HO_APP_ENCODE,
+                            {},
+                            {n});
     return 1;
   }
   Trace("uf-ho-debug") << "    ...already have " << ret << " == " << n << "."
@@ -441,7 +446,7 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
       Node eq = n.eqNode(hn);
       Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
                      << std::endl;
-      d_im.lemma(eq, InferenceId::UNKNOWN);
+      d_im.lemma(eq, InferenceId::UF_HO_MODEL_APP_ENCODE);
       return false;
     }
   }

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index c8cfe295e3a2ea1a7230d61d9759d86ed8bb398a..3ad94c57136b5c535a49e13afb2d58fcb3e210b5 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -315,7 +315,7 @@ void TheoryUF::presolve() {
         ++i) {
       Debug("uf") << "uf: generating a lemma: " << *i << std::endl;
       // no proof generator provided
-      d_im.lemma(*i, InferenceId::UNKNOWN);
+      d_im.lemma(*i, InferenceId::UF_BREAK_SYMMETRY);
     }
   }
   if( d_thss ){