(proof-new) Proof support in the strings term registry. (#4876)

Adds basic support for proofs in the strings term registry. This code is not yet active until further parts of proof-new are merged.

2 files changed, 54 insertions, 21 deletions

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index ed20406df..f28db4c35 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -265,7 +265,7 @@ void TermRegistry::registerTerm(Node n, int effort)
   registerType(tn);
   Debug("strings-register") << "TheoryStrings::registerTerm() " << n
                             << ", effort = " << effort << std::endl;
-  Node regTermLem;
+  TrustNode regTermLem;
   if (tn.isStringLike())
   {
     // register length information:
@@ -276,15 +276,29 @@ void TermRegistry::registerTerm(Node n, int effort)
   else if (n.getKind() != STRING_STRCTN)
   {
     // we don't send out eager reduction lemma for str.contains currently
-    regTermLem = eagerReduce(n, &d_skCache);
+    Node eagerRedLemma = eagerReduce(n, &d_skCache);
+    if (!eagerRedLemma.isNull())
+    {
+      // if there was an eager reduction, we make the trust node for it
+      if (d_epg != nullptr)
+      {
+        regTermLem = d_epg->mkTrustNode(
+            eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {n});
+      }
+      else
+      {
+        regTermLem = TrustNode::mkTrustLemma(eagerRedLemma, nullptr);
+      }
+    }
   }
   if (!regTermLem.isNull())
   {
     Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem
                            << std::endl;
-    Trace("strings-assert") << "(assert " << regTermLem << ")" << std::endl;
+    Trace("strings-assert")
+        << "(assert " << regTermLem.getNode() << ")" << std::endl;
     ++(d_statistics.d_lemmasRegisterTerm);
-    d_out.lemma(regTermLem);
+    d_out.trustedLemma(regTermLem);
   }
 }
 
@@ -306,7 +320,7 @@ void TermRegistry::registerType(TypeNode tn)
   }
 }
 
-Node TermRegistry::getRegisterTermLemma(Node n)
+TrustNode TermRegistry::getRegisterTermLemma(Node n)
 {
   Assert(n.getType().isStringLike());
   NodeManager* nm = NodeManager::currentNM();
@@ -322,7 +336,7 @@ Node TermRegistry::getRegisterTermLemma(Node n)
     if (lsum == lsumb)
     {
       registerTermAtomic(n, LENGTH_SPLIT);
-      return Node::null();
+      return TrustNode::null();
     }
   }
   Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
@@ -368,7 +382,12 @@ Node TermRegistry::getRegisterTermLemma(Node n)
 
   Node ret = nm->mkNode(AND, eq, ceq);
 
-  return ret;
+  // it is a simple rewrite to justify this
+  if (d_epg != nullptr)
+  {
+    return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {ret});
+  }
+  return TrustNode::mkTrustLemma(ret, nullptr);
 }
 
 void TermRegistry::registerTermAtomic(Node n, LengthStatus s)
@@ -385,14 +404,15 @@ void TermRegistry::registerTermAtomic(Node n, LengthStatus s)
     return;
   }
   std::map<Node, bool> reqPhase;
-  Node lenLem = getRegisterTermAtomicLemma(n, s, reqPhase);
+  TrustNode lenLem = getRegisterTermAtomicLemma(n, s, reqPhase);
   if (!lenLem.isNull())
   {
     Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem
                            << std::endl;
-    Trace("strings-assert") << "(assert " << lenLem << ")" << std::endl;
+    Trace("strings-assert")
+        << "(assert " << lenLem.getNode() << ")" << std::endl;
     ++(d_statistics.d_lemmasRegisterTermAtomic);
-    d_out.lemma(lenLem);
+    d_out.trustedLemma(lenLem);
   }
   for (const std::pair<const Node, bool>& rp : reqPhase)
   {
@@ -415,16 +435,15 @@ const context::CDHashSet<Node, NodeHashFunction>& TermRegistry::getInputVars()
 
 bool TermRegistry::hasStringCode() const { return d_hasStrCode; }
 
-Node TermRegistry::getRegisterTermAtomicLemma(Node n,
-                                              LengthStatus s,
-                                              std::map<Node, bool>& reqPhase)
+TrustNode TermRegistry::getRegisterTermAtomicLemma(
+    Node n, LengthStatus s, std::map<Node, bool>& reqPhase)
 {
   if (n.isConst())
   {
     // No need to send length for constant terms. This case may be triggered
     // for cases where the skolem cache automatically replaces a skolem by
     // a constant.
-    return Node::null();
+    return TrustNode::null();
   }
   Assert(n.getType().isStringLike());
   NodeManager* nm = NodeManager::currentNM();
@@ -438,7 +457,12 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n,
     Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
                            << std::endl;
     Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
-    return len_geq_one;
+    if (options::proofNewPedantic() > 0)
+    {
+      Unhandled() << "Unhandled lemma Strings::Lemma SK-GEQ-ONE : "
+                  << len_geq_one << std::endl;
+    }
+    return TrustNode::mkTrustLemma(len_geq_one, nullptr);
   }
 
   if (s == LENGTH_ONE)
@@ -447,7 +471,12 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n,
     Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
                            << std::endl;
     Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
-    return len_one;
+    if (options::proofNewPedantic() > 0)
+    {
+      Unhandled() << "Unhandled lemma Strings::Lemma SK-ONE : " << len_one
+                  << std::endl;
+    }
+    return TrustNode::mkTrustLemma(len_one, nullptr);
   }
   Assert(s == LENGTH_SPLIT);
 
@@ -478,7 +507,11 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n,
     Assert(!case_emptyr.getConst<bool>());
   }
 
-  return lenLemma;
+  if (d_epg != nullptr)
+  {
+    return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {n});
+  }
+  return TrustNode::mkTrustLemma(lenLemma, nullptr);
 }
 
 Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index 9a66690b8..2048abec1 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -278,7 +278,7 @@ class TermRegistry
    * If n is an atomic term, the method registerTermAtomic is called for n
    * and s = LENGTH_SPLIT and no lemma is returned.
    */
-  Node getRegisterTermLemma(Node n);
+  TrustNode getRegisterTermLemma(Node n);
   /**
    * Get the lemma required for registering the length information for
    * atomic term n given length status s. For details, see registerTermAtomic.
@@ -287,9 +287,9 @@ class TermRegistry
    * argument reqPhase, which should be processed by a call to requiredPhase by
    * the caller of this method.
    */
-  Node getRegisterTermAtomicLemma(Node n,
-                                  LengthStatus s,
-                                  std::map<Node, bool>& reqPhase);
+  TrustNode getRegisterTermAtomicLemma(Node n,
+                                       LengthStatus s,
+                                       std::map<Node, bool>& reqPhase);
 };
 
 }  // namespace strings