(proof-new) Miscellaneous changes to strings for proofs (#5362)

This includes all minor remaining changes from proof-new for strings that were not merged to master.

This includes mostly minor changes to make proofs pass, including reordering assertions. It also removes some non-standard pedantic checks as these are now subsumed by standard ones.

It also makes the strings rewriter slightly more safe when checking arithmetic entailment under assumptions. This code used substitution, which was not safe when quantifiers were involved. This is replaced by capture avoiding substitution here.

diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp
index cc2c7a2e64ca65c730587d932ca53623b0b59b8a..3c58767b3560a08c21501b0adbe07d162f37c0d6 100644 (file)
--- a/src/theory/strings/arith_entail.cpp
+++ b/src/theory/strings/arith_entail.cpp
@@ -15,6 +15,7 @@
 #include "theory/strings/arith_entail.h"
 
 #include "expr/attribute.h"
+#include "expr/node_algorithm.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
@@ -555,6 +556,8 @@ bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict)
 {
   Assert(assumption.getKind() == kind::EQUAL);
   Assert(Rewriter::rewrite(assumption) == assumption);
+  Trace("strings-entail") << "checkWithEqAssumption: " << assumption << " " << a
+                          << ", strict=" << strict << std::endl;
 
   // Find candidates variables to compute substitutions for
   std::unordered_set<Node, NodeHashFunction> candVars;
@@ -615,8 +618,11 @@ bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict)
     // Could not solve for v
     return false;
   }
+  Trace("strings-entail") << "checkWithEqAssumption: subs " << v << " -> "
+                          << solution << std::endl;
 
-  a = a.substitute(TNode(v), TNode(solution));
+  // use capture avoiding substitution
+  a = expr::substituteCaptureAvoiding(a, v, solution);
   return check(a, strict);
 }
 

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index d33a7f90279e379dce8a2aea37a5da19d8f909ab..451c01f8c5c4a5a5d3a3c4f572e3f8119a9578f7 100644 (file)
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -638,9 +638,8 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
       ei->d_cardinalityLemK.set(int_k + 1);
       if (!cons.isConst() || !cons.getConst<bool>())
       {
-        std::vector<Node> emptyVec;
         d_im.sendInference(
-            emptyVec, expn, cons, Inference::CARDINALITY, true);
+            expn, expn, cons, Inference::CARDINALITY, false, true);
         return;
       }
     }
@@ -675,7 +674,7 @@ Node BaseSolver::explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp)
     }
     if (!bei.d_exp.isNull())
     {
-      exp.push_back(bei.d_exp);
+      utils::flattenOp(AND, bei.d_exp, exp);
     }
     if (!bei.d_base.isNull())
     {
@@ -695,7 +694,7 @@ Node BaseSolver::explainBestContentEqc(Node n, Node eqc, std::vector<Node>& exp)
     Assert(!bei.d_bestContent.isNull());
     if (!bei.d_exp.isNull())
     {
-      exp.push_back(bei.d_exp);
+      utils::flattenOp(AND, bei.d_exp, exp);
     }
     if (!bei.d_base.isNull())
     {

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index c5275cc430f799102a1676d169d9cf7afec5a08d..66f71bf14f26ecea8ecae2cd47c47ba5e8fa7826 100644 (file)
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -878,17 +878,6 @@ void InferProofCons::convert(Inference infer,
     ps.d_rule = PfRule::STRING_TRUST;
     // add to stats
     d_statistics.d_inferencesNoPf << infer;
-    if (options::proofNewPedantic() > 0)
-    {
-      std::stringstream serr;
-      serr << "InferProofCons::convert: Failed " << infer
-           << (isRev ? " :rev " : " ") << conc << std::endl;
-      for (const Node& ec : exp)
-      {
-        serr << "    e: " << ec << std::endl;
-      }
-      Unhandled() << serr.str();
-    }
   }
   if (Trace.isOn("strings-ipc-debug"))
   {

diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp
index 372b07f56371c18c74e7eb759d16a1cb73d69f0f..7724b5137e69c6834a73fc4c77fc41d29302fbe2 100644 (file)
--- a/src/theory/strings/normal_form.cpp
+++ b/src/theory/strings/normal_form.cpp
@@ -83,6 +83,7 @@ void NormalForm::addToExplanation(Node exp,
                                   unsigned new_val,
                                   unsigned new_rev_val)
 {
+  Assert(!exp.isConst());
   if (std::find(d_exp.begin(), d_exp.end(), exp) == d_exp.end())
   {
     d_exp.push_back(exp);
@@ -177,11 +178,9 @@ void NormalForm::getExplanationForPrefixEq(NormalForm& nfi,
   Trace("strings-explain-prefix")
       << "Included " << curr_exp.size() << " / "
       << (nfi.d_exp.size() + nfj.d_exp.size()) << std::endl;
-  if (nfi.d_base != nfj.d_base)
-  {
-    Node eq = nfi.d_base.eqNode(nfj.d_base);
-    curr_exp.push_back(eq);
-  }
+  // add explanation for why they are equal
+  Node eq = nfi.d_base.eqNode(nfj.d_base);
+  curr_exp.push_back(eq);
 }
 
 }  // namespace strings

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 76230bcffb0812a80c23b2d20ebbd9aec8291198..8274b7dc0c086b291cd23e7f77b26fa734d5ce14 100644 (file)
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -462,11 +462,6 @@ TrustNode TermRegistry::getRegisterTermAtomicLemma(
     Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
                            << std::endl;
     Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
-    if (options::proofNewPedantic() > 0)
-    {
-      Unhandled() << "Unhandled lemma Strings::Lemma SK-GEQ-ONE : "
-                  << len_geq_one << std::endl;
-    }
     return TrustNode::mkTrustLemma(len_geq_one, nullptr);
   }
 
@@ -476,11 +471,6 @@ TrustNode TermRegistry::getRegisterTermAtomicLemma(
     Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
                            << std::endl;
     Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
-    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);

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index a8c1a6573088abad3d161810a7b88140c48902fb..936f60ed2a3efab0a7920024a229194b326ae881 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -875,7 +875,7 @@ Node StringsPreprocess::reduce(Node t,
   {
     Node ltp = sc->mkTypedSkolemCached(
         nm->booleanType(), t, SkolemCache::SK_PURIFY, "ltp");
-    Node k = nm->mkSkolem("k", nm->integerType());
+    Node k = SkolemCache::mkIndexVar(t);
 
     std::vector<Node> conj;
     conj.push_back(nm->mkNode(GEQ, k, zero));
@@ -899,6 +899,8 @@ Node StringsPreprocess::reduce(Node t,
     }
     conj.push_back(nm->mkNode(ITE, ite_ch));
 
+    Node conjn = nm->mkNode(
+        EXISTS, nm->mkNode(BOUND_VAR_LIST, k), nm->mkNode(AND, conj));
     // Intuitively, the reduction says either x and y are equal, or they have
     // some (maximal) common prefix after which their characters at position k
     // are distinct, and the comparison of their code matches the return value
@@ -912,13 +914,13 @@ Node StringsPreprocess::reduce(Node t,
     // assert:
     //  IF x=y
     //  THEN: ltp
-    //  ELSE: k >= 0 AND k <= len( x ) AND k <= len( y ) AND
+    //  ELSE: exists k.
+    //        k >= 0 AND k <= len( x ) AND k <= len( y ) AND
     //        substr( x, 0, k ) = substr( y, 0, k ) AND
     //        IF    ltp
     //        THEN: str.code(substr( x, k, 1 )) < str.code(substr( y, k, 1 ))
     //        ELSE: str.code(substr( x, k, 1 )) > str.code(substr( y, k, 1 ))
-    Node assert =
-        nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, nm->mkNode(AND, conj));
+    Node assert = nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, conjn);
     asserts.push_back(assert);
 
     // Thus, str.<=( x, y ) = ltp