(proof-new) Updates to strings term registry (#4599)

This makes it so that methods for constructing term registration lemmas are made into static methods, so that they can be used by both the term registry and proof checker.

3 files changed, 118 insertions, 56 deletions

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 90ebc4f8b..b4fbbed98 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -15,6 +15,7 @@
 #include "theory/strings/term_registry.h"
 
 #include "expr/attribute.h"
+#include "options/smt_options.h"
 #include "options/strings_options.h"
 #include "smt/logic_exception.h"
 #include "theory/rewriter.h"
@@ -35,23 +36,25 @@ struct StringsProxyVarAttributeId
 typedef expr::Attribute<StringsProxyVarAttributeId, bool>
     StringsProxyVarAttribute;
 
-TermRegistry::TermRegistry(context::Context* c,
-                           context::UserContext* u,
+TermRegistry::TermRegistry(SolverState& s,
                            eq::EqualityEngine& ee,
                            OutputChannel& out,
-                           SequencesStatistics& statistics)
-    : d_ee(ee),
+                           SequencesStatistics& statistics,
+                           ProofNodeManager* pnm)
+    : d_state(s),
+      d_ee(ee),
       d_out(out),
       d_statistics(statistics),
       d_hasStrCode(false),
-      d_functionsTerms(c),
-      d_inputVars(u),
-      d_preregisteredTerms(u),
-      d_registeredTerms(u),
-      d_registeredTypes(u),
-      d_proxyVar(u),
-      d_proxyVarToLength(u),
-      d_lengthLemmaTermsCache(u)
+      d_functionsTerms(s.getSatContext()),
+      d_inputVars(s.getUserContext()),
+      d_preregisteredTerms(s.getUserContext()),
+      d_registeredTerms(s.getUserContext()),
+      d_registeredTypes(s.getUserContext()),
+      d_proxyVar(s.getUserContext()),
+      d_proxyVarToLength(s.getUserContext()),
+      d_lengthLemmaTermsCache(s.getUserContext()),
+      d_epg(nullptr)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_zero = nm->mkConst(Rational(0));
@@ -62,6 +65,64 @@ TermRegistry::TermRegistry(context::Context* c,
 
 TermRegistry::~TermRegistry() {}
 
+Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node lemma;
+  Kind tk = t.getKind();
+  if (tk == STRING_TO_CODE)
+  {
+    // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 )
+    Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConst(Rational(1)));
+    Node code_eq_neg1 = t.eqNode(nm->mkConst(Rational(-1)));
+    Node code_range = nm->mkNode(
+        AND,
+        nm->mkNode(GEQ, t, nm->mkConst(Rational(0))),
+        nm->mkNode(
+            LT, t, nm->mkConst(Rational(utils::getAlphabetCardinality()))));
+    lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
+  }
+  else if (tk == STRING_STRIDOF)
+  {
+    // (and (>= (str.indexof x y n) (- 1)) (<= (str.indexof x y n) (str.len
+    // x)))
+    Node l = utils::mkNLength(t[0]);
+    lemma = nm->mkNode(AND,
+                       nm->mkNode(GEQ, t, nm->mkConst(Rational(-1))),
+                       nm->mkNode(LEQ, t, l));
+  }
+  else if (tk == STRING_STOI)
+  {
+    // (>= (str.to_int x) (- 1))
+    lemma = nm->mkNode(GEQ, t, nm->mkConst(Rational(-1)));
+  }
+  else if (tk == STRING_STRCTN)
+  {
+    // ite( (str.contains s r), (= s (str.++ sk1 r sk2)), (not (= s r)))
+    Node sk1 =
+        sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1");
+    Node sk2 =
+        sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2");
+    lemma = t[0].eqNode(utils::mkNConcat(sk1, t[1], sk2));
+    lemma = nm->mkNode(ITE, t, lemma, t[0].eqNode(t[1]).notNode());
+  }
+  return lemma;
+}
+
+Node TermRegistry::lengthPositive(Node t)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node zero = nm->mkConst(Rational(0));
+  Node emp = Word::mkEmptyWord(t.getType());
+  Node tlen = nm->mkNode(STRING_LENGTH, t);
+  Node tlenEqZero = tlen.eqNode(zero);
+  Node tEqEmp = t.eqNode(emp);
+  Node caseEmpty = nm->mkNode(AND, tlenEqZero, tEqEmp);
+  Node caseNEmpty = nm->mkNode(GT, tlen, zero);
+  // (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
+  return nm->mkNode(OR, caseEmpty, caseNEmpty);
+}
+
 void TermRegistry::preRegisterTerm(TNode n)
 {
   if (d_preregisteredTerms.find(n) != d_preregisteredTerms.end())
@@ -202,7 +263,6 @@ void TermRegistry::registerTerm(Node n, int effort)
   d_registeredTerms.insert(n);
   // ensure the type is registered
   registerType(tn);
-  NodeManager* nm = NodeManager::currentNM();
   Debug("strings-register") << "TheoryStrings::registerTerm() " << n
                             << ", effort = " << effort << std::endl;
   Node regTermLem;
@@ -213,28 +273,10 @@ void TermRegistry::registerTerm(Node n, int effort)
     //  for concat/const/replace, introduce proxy var and state length relation
     regTermLem = getRegisterTermLemma(n);
   }
-  else if (n.getKind() == STRING_TO_CODE)
-  {
-    // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 )
-    Node code_len = utils::mkNLength(n[0]).eqNode(d_one);
-    Node code_eq_neg1 = n.eqNode(d_negOne);
-    Node code_range = nm->mkNode(
-        AND,
-        nm->mkNode(GEQ, n, d_zero),
-        nm->mkNode(
-            LT, n, nm->mkConst(Rational(utils::getAlphabetCardinality()))));
-    regTermLem = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
-  }
-  else if (n.getKind() == STRING_STRIDOF)
+  else if (n.getKind() != STRING_STRCTN)
   {
-    Node len = utils::mkNLength(n[0]);
-    regTermLem = nm->mkNode(AND,
-                            nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
-                            nm->mkNode(LEQ, n, len));
-  }
-  else if (n.getKind() == STRING_STOI)
-  {
-    regTermLem = nm->mkNode(GEQ, n, nm->mkConst(Rational(-1)));
+    // we don't send out eager reduction lemma for str.contains currently
+    regTermLem = eagerReduce(n, &d_skCache);
   }
   if (!regTermLem.isNull())
   {
@@ -324,7 +366,9 @@ Node TermRegistry::getRegisterTermLemma(Node n)
   d_proxyVarToLength[sk] = lsum;
   Node ceq = Rewriter::rewrite(skl.eqNode(lsum));
 
-  return nm->mkNode(AND, eq, ceq);
+  Node ret = nm->mkNode(AND, eq, ceq);
+
+  return ret;
 }
 
 void TermRegistry::registerTermAtomic(Node n, LengthStatus s)
@@ -407,17 +451,15 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n,
   }
   Assert(s == LENGTH_SPLIT);
 
-  std::vector<Node> lems;
+  // get the positive length lemma
+  Node lenLemma = lengthPositive(n);
   // split whether the string is empty
   Node n_len_eq_z = n_len.eqNode(d_zero);
   Node n_len_eq_z_2 = n.eqNode(emp);
   Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
-  case_empty = Rewriter::rewrite(case_empty);
-  Node case_nempty = nm->mkNode(GT, n_len, d_zero);
-  if (!case_empty.isConst())
+  Node case_emptyr = Rewriter::rewrite(case_empty);
+  if (!case_emptyr.isConst())
   {
-    Node lem = nm->mkNode(OR, case_empty, case_nempty);
-    lems.push_back(lem);
     // prefer trying the empty case first
     // notice that requirePhase must only be called on rewritten literals that
     // occur in the CNF stream.
@@ -428,24 +470,15 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n,
     Assert(!n_len_eq_z_2.isConst());
     reqPhase[n_len_eq_z_2] = true;
   }
-  else if (!case_empty.getConst<bool>())
-  {
-    // the rewriter knows that n is non-empty
-    lems.push_back(case_nempty);
-  }
   else
   {
     // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
     // n ---> "". Since this method is only called on non-constants n, it must
     // be that n = "" ^ len( n ) = 0 does not rewrite to true.
-    Assert(false);
+    Assert(!case_emptyr.getConst<bool>());
   }
 
-  if (lems.empty())
-  {
-    return Node::null();
-  }
-  return lems.size() == 1 ? lems[0] : nm->mkNode(AND, lems);
+  return lenLemma;
 }
 
 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 f0b4a74c6..d0589be90 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -19,10 +19,13 @@
 
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
+#include "expr/proof_node_manager.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/output_channel.h"
 #include "theory/strings/infer_info.h"
 #include "theory/strings/sequences_stats.h"
 #include "theory/strings/skolem_cache.h"
+#include "theory/strings/solver_state.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
@@ -46,12 +49,34 @@ class TermRegistry
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 
  public:
-  TermRegistry(context::Context* c,
-               context::UserContext* u,
+  TermRegistry(SolverState& s,
                eq::EqualityEngine& ee,
                OutputChannel& out,
-               SequencesStatistics& statistics);
+               SequencesStatistics& statistics,
+               ProofNodeManager* pnm);
   ~TermRegistry();
+  /** The eager reduce routine
+   *
+   * Constructs a lemma for t that is incomplete, but communicates pertinent
+   * information about t. This is analogous to StringsPreprocess::reduce.
+   *
+   * In practice, we send this lemma eagerly, as soon as t is registered.
+   *
+   * @param t The node to reduce,
+   * @param sc The Skolem cache to use for new variables,
+   * @return The eager reduction for t.
+   */
+  static Node eagerReduce(Node t, SkolemCache* sc);
+  /**
+   * Returns a lemma indicating that the length of a term t whose type is
+   * string-like has positive length. The exact form of this lemma depends
+   * on what works best in practice, currently:
+   *   (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
+   *
+   * @param t The node to reduce,
+   * @return The positive length lemma for t.
+   */
+  static Node lengthPositive(Node t);
   /**
    * Preregister term, called when TheoryStrings::preRegisterTerm(n) is called.
    * This does the following:
@@ -184,6 +209,8 @@ class TermRegistry
   Node d_negOne;
   /** the cardinality of the alphabet */
   uint32_t d_cardSize;
+  /** Reference to the solver state of the theory of strings. */
+  SolverState& d_state;
   /** Reference to equality engine of the theory of strings. */
   eq::EqualityEngine& d_ee;
   /** Reference to the output channel of the theory of strings. */
@@ -224,6 +251,8 @@ class TermRegistry
   NodeNodeMap d_proxyVarToLength;
   /** List of terms that we have register length for */
   NodeSet d_lengthLemmaTermsCache;
+  /** Proof generator, manages proofs for lemmas generated by this class */
+  std::unique_ptr<EagerProofGenerator> d_epg;
   /** Register type
    *
    * Ensures the theory solver is setup to handle string-like type tn. In
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 562d8eab8..ae8b3b682 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -44,7 +44,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_statistics(),
       d_equalityEngine(d_notify, c, "theory::strings::ee", true),
       d_state(c, u, d_equalityEngine, d_valuation),
-      d_termReg(c, u, d_equalityEngine, out, d_statistics),
+      d_termReg(d_state, d_equalityEngine, out, d_statistics, nullptr),
       d_im(nullptr),
       d_rewriter(&d_statistics.d_rewrites),
       d_bsolver(nullptr),