Add elaboration for MACRO_STR_EQ_LEN_UNIFY_PREFIX (cvc5#11658)

This adds proof elaboration for MACRO_STR_EQ_LEN_UNIFY_PREFIX.

It does not require any new rules, apart from a RARE rewrite for turning
a dual implicaition into an equality.

Author: ajreynol

include/cvc5/cvc5_proof_rule.h

@@ -3636,6 +3636,8 @@ enum ENUM(ProofRewriteRule)
   EVALUE(BOOL_IMPL_TRUE2),
   /** Auto-generated from RARE rule bool-impl-elim */
   EVALUE(BOOL_IMPL_ELIM),
+  /** Auto-generated from RARE rule bool-dual-impl-eq */
+  EVALUE(BOOL_DUAL_IMPL_EQ),
   /** Auto-generated from RARE rule bool-or-true */
   EVALUE(BOOL_OR_TRUE),
   /** Auto-generated from RARE rule bool-or-flatten */

proofs/eo/cpc/rules/Rewrites.eo

@@ -291,6 +291,10 @@
   :args (t1 s1)
   :conclusion (= (=> t1 s1) (or (not t1) s1))
 )
+(declare-rule bool-dual-impl-eq ((t1 Bool) (s1 Bool))
+  :args (t1 s1)
+  :conclusion (= (and (=> t1 s1) (=> s1 t1)) (= t1 s1))
+)
 (declare-rule bool-or-true ((xs1 Bool :list) (ys1 Bool :list))
   :args (xs1 ys1)
   :conclusion (= ($singleton_elim (or xs1 true ys1)) true)

src/rewriter/basic_rewrite_rcons.cpp

@@ -224,6 +224,12 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite(CDProof* cdp,
         handledMacro = true;
       }
       break;
+    case ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY_PREFIX:
+      if (ensureProofMacroStrEqLenUnifyPrefix(cdp, eq))
+      {
+        handledMacro = true;
+      }
+      break;
     case ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY:
       if (ensureProofMacroStrEqLenUnify(cdp, eq))
       {
@@ -926,6 +932,229 @@ bool BasicRewriteRCons::ensureProofMacroSubstrStripSymLength(CDProof* cdp,
   return true;
 }
 
+
+bool BasicRewriteRCons::ensureProofMacroStrEqLenUnifyPrefix(CDProof* cdp,
+                                                            const Node& eq)
+{
+  Trace("brc-macro") << "Expand macro str eq len unify prefix " << eq
+                     << std::endl;
+  NodeManager* nm = nodeManager();
+  theory::strings::ArithEntail ae(nullptr);
+  theory::strings::StringsEntail sent(nullptr, ae);
+
+  Assert(eq[1].getKind() == Kind::AND);
+  Node eq1p = eq[1];
+  // get the equations equal empty
+  // we group (and (= s t) (= t1 "") ... (= tn "")) to
+  // (and (= s t) (and (= t1 "") ... (= tn ""))) and store in eq1p.
+  std::vector<Node> empeqs;
+  if (eq[1].getNumChildren() > 2)
+  {
+    empeqs.insert(empeqs.end(), eq[1].begin() + 1, eq[1].end());
+    Node eq1g = nm->mkAnd(empeqs);
+    eq1p = nm->mkNode(Kind::AND, eq[1][0], eq1g);
+    Node eqg = eq1p.eqNode(eq[1]);
+    cdp->addStep(eqg, ProofRule::ACI_NORM, {}, {eqg});
+  }
+  else
+  {
+    empeqs.push_back(eq[1][1]);
+  }
+
+  // prove eq[0] => eq1p in cdfwd
+  CDProof cdfwd(d_env);
+  Node eqsrc = eq[0];
+  Node ret = sent.inferEqsFromContains(eqsrc[0], eqsrc[1]);
+  Trace("brc-macro") << "[1] setup forward implication" << std::endl;
+  bool eqFlipped = false;
+  if (ret.isNull())
+  {
+    Trace("brc-macro") << "...failed " << ret << ", try flip" << std::endl;
+    eqsrc = eq[0][1].eqNode(eq[0][0]);
+    ret = sent.inferEqsFromContains(eqsrc[0], eqsrc[1]);
+    if (ret.isNull())
+    {
+      Trace("brc-macro") << "... failed to replicate " << ret << std::endl;
+      return false;
+    }
+    eqFlipped = true;
+    cdfwd.addStep(eqsrc, ProofRule::SYMM, {eq[0]}, {});
+  }
+  Node len1 = nm->mkNode(Kind::STRING_LENGTH, eqsrc[0]);
+  Node len2 = nm->mkNode(Kind::STRING_LENGTH, eqsrc[1]);
+  Node leneq = proveCong(&cdfwd, len1, {eqsrc});
+  Node li[2];
+  std::vector<Node> eqi;
+  eqi.resize(2);
+  for (size_t i = 0; i < 2; i++)
+  {
+    Node l = i == 0 ? len1 : len2;
+    TConvProofGenerator tcpg(d_env, nullptr);
+    li[i] = ae.rewriteLengthIntro(l, &tcpg);
+    if (li[i] != l)
+    {
+      Node equiv = l.eqNode(li[i]);
+      std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(equiv);
+      cdfwd.addProof(pfn);
+      eqi[i] = pfn->getResult();
+    }
+  }
+  Node leneqi = li[0].eqNode(li[1]);
+  if (leneqi != leneq)
+  {
+    Node equiv = proveCong(&cdfwd, leneq, eqi);
+    cdfwd.addStep(leneqi, ProofRule::EQ_RESOLVE, {leneq, equiv}, {});
+  }
+  Trace("brc-macro") << "...length: " << li[0] << " == " << li[1] << std::endl;
+  // based on swapping above, we should have len1i >= len2i
+  Node diff = nm->mkNode(Kind::SUB, li[1], li[0]);
+  Node diffn = theory::arith::PolyNorm::getPolyNorm(diff);
+  Trace("brc-macro") << "...norm diff " << diffn << std::endl;
+  Node diffneqz = diffn.eqNode(nm->mkConstInt(Rational(0)));
+  Node equiv = leneqi.eqNode(diffneqz);
+  if (!ensureProofArithPolyNormRel(&cdfwd, equiv))
+  {
+    Trace("brc-macro") << "... failed poly norm rel" << std::endl;
+    return false;
+  }
+  cdfwd.addStep(diffneqz, ProofRule::EQ_RESOLVE, {leneqi, equiv}, {});
+  Trace("brc-macro") << "...have " << diffneqz << std::endl;
+
+  // get the concatenation term corresponding to the components equated to empty
+  std::vector<Node> concat;
+  std::map<Node, Node> empMap;
+  Assert(eq1p.getKind() == Kind::AND && eq1p.getNumChildren() == 2);
+  for (const Node& ee : empeqs)
+  {
+    Assert(ee.getKind() == Kind::EQUAL && ee[0].getType().isStringLike());
+    concat.push_back(ee[0]);
+    empMap[ee[0]] = ee;
+  }
+  TypeNode stype = concat[0].getType();
+  Node cc = theory::strings::utils::mkConcat(concat, stype);
+  Node lcc = nm->mkNode(Kind::STRING_LENGTH, cc);
+  TConvProofGenerator tcpg(d_env, nullptr);
+  Node lcci = ae.rewriteLengthIntro(lcc, &tcpg);
+  Trace("brc-macro") << "...normalized concat length " << lcci << std::endl;
+  Node lcceq = lcc.eqNode(lcci);
+  std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(lcceq);
+  cdfwd.addProof(pfn);
+
+  // the length of the empty components should be equal to the difference
+  // the length of the equality before and after removing empty components
+  Node pnEq = lcci.eqNode(diffneqz[0]);
+  if (!cdfwd.addStep(pnEq, ProofRule::ARITH_POLY_NORM, {}, {pnEq}))
+  {
+    Trace("brc-macro") << "...fail poly norm " << pnEq << std::endl;
+    return false;
+  }
+  Node pnEq2 = lcc.eqNode(diffneqz[1]);
+  cdfwd.addStep(pnEq2, ProofRule::TRANS, {lcceq, pnEq, diffneqz}, {});
+  // now have proven (str.len (str.++ t1 ... tn)) = 0,
+  // need t1 = "" ^ ... ^ tn = ""
+  Trace("brc-macro") << "...have " << pnEq2 << std::endl;
+  Node eqconv = pnEq2.eqNode(eq1p[1]);
+  Trace("brc-macro") << "- subgoal " << eqconv << std::endl;
+  // subgoal, which can be filled with RARE rules
+  // str-len-eq-zero-concat-rec and str-len-eq-zero-base
+  cdfwd.addTrustedStep(eqconv, TrustId::MACRO_THEORY_REWRITE_RCONS, {}, {});
+  cdfwd.addStep(eq1p[1], ProofRule::EQ_RESOLVE, {pnEq2, eqconv}, {});
+
+  // proves (=> (and t="") (= (= (str.++ s t) r) (= s r)))
+  CDProof cdmid(d_env);
+  Node srcRew = eqsrc[1];
+  Trace("brc-macro") << "[2] source term to rewrite " << srcRew << std::endl;
+  Assert(srcRew.getKind() == Kind::STRING_CONCAT);
+  std::vector<Node> eqe;
+  std::map<Node, Node>::iterator it;
+  for (const Node& tc : srcRew)
+  {
+    it = empMap.find(tc);
+    if (it != empMap.end())
+    {
+      eqe.push_back(it->second);
+    }
+    else
+    {
+      eqe.push_back(Node::null());
+    }
+  }
+  Node cres = proveCong(&cdmid, srcRew, eqe);
+  if (cres.isNull())
+  {
+    Trace("brc-macro") << "...fail cong" << std::endl;
+    return false;
+  }
+  Trace("brc-macro") << "...cong to " << cres[1] << std::endl;
+  Node tgtRew = eq1p[0][eqFlipped ? 0 : 1];
+  Trace("brc-macro") << "...target is " << tgtRew << std::endl;
+
+  Node eqacin = cres[1].eqNode(tgtRew);
+  if (!cdmid.addStep(eqacin, ProofRule::ACI_NORM, {}, {eqacin}))
+  {
+    Trace("brc-macro") << "...fail aci norm" << std::endl;
+    return false;
+  }
+  Trace("brc-macro") << "...proved subs empty " << eqacin << std::endl;
+  Node teq = srcRew.eqNode(tgtRew);
+  cdmid.addStep(teq, ProofRule::TRANS, {cres, eqacin}, {});
+
+  Node eqqeq = eq[0].eqNode(eq1p[0]);
+  std::vector<Node> eqee;
+  for (size_t i = 0; i < 2; i++)
+  {
+    Node eee = eq[0][i].eqNode(eq1p[0][i]);
+    eqee.push_back(eee);
+    if (eee[0] == eee[1])
+    {
+      Node refl = eee[0].eqNode(eee[0]);
+      cdmid.addStep(refl, ProofRule::REFL, {}, {eee[0]});
+    }
+  }
+  std::vector<Node> cargs;
+  ProofRule cr = expr::getCongRule(eq[0], cargs);
+  cdmid.addStep(eqqeq, cr, eqee, cargs);
+  Node implMid = nm->mkNode(Kind::IMPLIES, eq1p[1], eqqeq);
+  cdmid.addStep(implMid, ProofRule::SCOPE, {eqqeq}, empeqs);
+  Trace("brc-macro") << "...intermediate result: " << implMid << std::endl;
+  std::shared_ptr<ProofNode> pfmid = cdmid.getProofFor(implMid);
+  Assert(implMid[1][0] == eq[0]);
+  Assert(implMid[1][1] == eq1p[0]);
+
+  // finish the forward proof
+  cdfwd.addProof(pfmid);
+  cdfwd.addStep(implMid[1], ProofRule::MODUS_PONENS, {eq1p[1], implMid}, {});
+  cdfwd.addStep(eq1p[0], ProofRule::EQ_RESOLVE, {eq[0], implMid[1]}, {});
+  cdfwd.addStep(eq1p, ProofRule::AND_INTRO, {eq1p[0], eq1p[1]}, {});
+  Node impl = nm->mkNode(Kind::IMPLIES, eq[0], eq1p);
+  cdfwd.addStep(impl, ProofRule::SCOPE, {eq1p}, {eq[0]});
+  cdp->addProof(cdfwd.getProofFor(impl));
+
+  // reverse proof is easy
+  CDProof cdrev(d_env);
+  cdrev.addProof(pfmid);
+  cdrev.addStep(implMid[1], ProofRule::MODUS_PONENS, {eq1p[1], implMid}, {});
+  Node equivs = implMid[1][1].eqNode(implMid[1][0]);
+  cdrev.addStep(equivs, ProofRule::SYMM, {implMid[1]}, {});
+  cdrev.addStep(
+      implMid[1][0], ProofRule::EQ_RESOLVE, {implMid[1][1], equivs}, {});
+  Node implrev = nm->mkNode(Kind::IMPLIES, eq1p, eq[0]);
+  cdrev.addStep(implrev, ProofRule::SCOPE, {eq[0]}, {eq1p[0], eq1p[1]});
+  cdp->addProof(cdrev.getProofFor(implrev));
+
+  // dual implication
+  Node eqfinal = proveDualImplication(cdp, impl, implrev);
+
+  // if we grouped the empty equations, we close with a transitive step
+  // which we added via ACI_NORM above
+  if (eq1p != eq[1])
+  {
+    cdp->addStep(eq, ProofRule::TRANS, {eqfinal, eq1p.eqNode(eq[1])}, {});
+  }
+
+  return true;
+}
+
 bool BasicRewriteRCons::ensureProofMacroStrEqLenUnify(CDProof* cdp,
                                                       const Node& eq)
 {

src/rewriter/basic_rewrite_rcons.h

@@ -191,6 +191,16 @@ class BasicRewriteRCons : protected EnvObj
    * @return true if added a closed proof of eq to cdp.
    */
   bool ensureProofMacroSubstrStripSymLength(CDProof* cdp, const Node& eq);
+  /**
+   * Elaborate a rewrite eq that was proven by
+   * ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY_PREFIX.
+   *
+   * @param cdp The proof to add to.
+   * @param eq The rewrite proven by
+   * ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY_PREFIX.
+   * @return true if added a closed proof of eq to cdp.
+   */
+  bool ensureProofMacroStrEqLenUnifyPrefix(CDProof* cdp, const Node& eq);
   /**
    * Elaborate a rewrite eq that was proven by
    * ProofRewriteRule::MACRO_STR_EQ_LEN_UNIFY.

src/theory/booleans/rewrites

@@ -14,6 +14,9 @@
 (define-rule bool-impl-true2 ((t Bool)) (=> true t) t)
 (define-rule bool-impl-elim ((t Bool) (s Bool)) (=> t s) (or (not t) s))
 
+; used in proof elaboration
+(define-rule bool-dual-impl-eq ((t Bool) (s Bool)) (and (=> t s) (=> s t)) (= t s))
+
 (define-rule bool-or-true ((xs Bool :list) (ys Bool :list)) (or xs true ys) true)
 (define-rule* bool-or-flatten ((xs Bool :list) (b Bool) (ys Bool :list) (zs Bool :list)) (or xs (or b ys) zs) (or xs b ys zs))