Merge branch 'main' of https://github.com/cvc5/cvc5 into seqEvalOp

include/cvc5/cvc5_proof_rule.h

@@ -4034,6 +4034,10 @@ enum ENUM(ProofRewriteRule)
   EVALUE(BV_ZERO_EXTEND_EQ_CONST_1),
   /** Auto-generated from RARE rule bv-zero-extend-eq-const-2 */
   EVALUE(BV_ZERO_EXTEND_EQ_CONST_2),
+  /** Auto-generated from RARE rule bv-zero-extend-ult-const-1 */
+  EVALUE(BV_ZERO_EXTEND_ULT_CONST_1),
+  /** Auto-generated from RARE rule bv-zero-extend-ult-const-2 */
+  EVALUE(BV_ZERO_EXTEND_ULT_CONST_2),
   /** Auto-generated from RARE rule bv-sign-extend-ult-const-1 */
   EVALUE(BV_SIGN_EXTEND_ULT_CONST_1),
   /** Auto-generated from RARE rule bv-sign-extend-ult-const-2 */

proofs/eo/cpc/rules/Rewrites.eo

@@ -603,10 +603,10 @@
   :args (xs1 ys1 zs1 x1)
   :conclusion (= (bvxor xs1 (bvnot x1) ys1 x1 zs1) (bvnot ($singleton_elim (bvxor xs1 ys1 zs1))))
 )
-(declare-rule bv-ult-add-one ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (c1 (BitVec @n2)) (w1 Int))
-  :premises ((= c1 (@bv 1 w1)) (= w1 (@bvsize y1)))
-  :args (x1 y1 c1 w1)
-  :conclusion (= (bvult x1 (bvadd y1 c1)) (and (not (= y1 (bvnot (@bv 0 w1)))) (not (bvult y1 x1))))
+(declare-rule bv-ult-add-one ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (x1 (BitVec @n0)) (ys1 (BitVec @n1) :list) (zs1 (BitVec @n2) :list) (c1 (BitVec @n3)) (w1 Int))
+  :premises ((= c1 (@bv 1 w1)) (= w1 (@bvsize x1)))
+  :args (x1 ys1 zs1 c1 w1)
+  :conclusion (= (bvult x1 ($singleton_elim (bvadd ys1 c1 zs1))) (eo::define ((_let_1 ($singleton_elim (bvadd ys1 zs1)))) (and (not (= _let_1 (bvnot (@bv 0 w1)))) (not (bvult _let_1 x1)))))
 )
 (declare-rule bv-concat-to-mult ((@n0 Int) (x1 (BitVec @n0)) (i1 Int) (m1 Int) (n1 Int) (w1 Int))
   :premises ((= (+ 1 i1 m1) (@bvsize x1)) (= n1 0) (= w1 (@bvsize x1)))
@@ -830,7 +830,7 @@
 (declare-rule bv-smod-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (w1 Int) (wm1 Int))
   :premises ((= w1 (@bvsize x1)) (= wm1 (- (@bvsize x1) 1)))
   :args (x1 y1 w1 wm1)
-  :conclusion (= (bvsmod x1 y1) (eo::define ((_let_1 (@bv 1 1))) (eo::define ((_let_2 (= (extract wm1 wm1 y1) _let_1))) (eo::define ((_let_3 (= (extract wm1 wm1 x1) _let_1))) (eo::define ((_let_4 (bvurem (ite _let_3 (bvneg x1) x1) (ite _let_2 (bvneg y1) y1)))) (eo::define ((_let_5 (bvneg _let_4))) (eo::define ((_let_6 (not _let_3))) (eo::define ((_let_7 (not _let_2))) (ite (= _let_4 (@bv 0 w1)) _let_4 (ite (and _let_6 _let_7) _let_4 (ite (and _let_3 _let_7) (bvadd _let_5 y1) (ite (and _let_6 _let_2) (bvadd _let_4 y1) _let_5))))))))))))
+  :conclusion (= (bvsmod x1 y1) (eo::define ((_let_1 (@bv 0 1))) (eo::define ((_let_2 (extract wm1 wm1 y1))) (eo::define ((_let_3 (= _let_2 _let_1))) (eo::define ((_let_4 (extract wm1 wm1 x1))) (eo::define ((_let_5 (= _let_4 _let_1))) (eo::define ((_let_6 (bvurem (ite _let_5 x1 (bvneg x1)) (ite _let_3 y1 (bvneg y1))))) (eo::define ((_let_7 (bvneg _let_6))) (eo::define ((_let_8 (@bv 1 1))) (ite (= _let_6 (@bv 0 w1)) _let_6 (ite (and _let_5 _let_3) _let_6 (ite (and (= _let_4 _let_8) _let_3) (bvadd _let_7 y1) (ite (and _let_5 (= _let_2 _let_8)) (bvadd _let_6 y1) _let_7)))))))))))))
 )
 (declare-rule bv-smod-eliminate-fewer-bitwise-ops ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (w1 Int) (wm1 Int))
   :premises ((= w1 (@bvsize x1)) (= wm1 (- (@bvsize x1) 1)))
@@ -840,7 +840,7 @@
 (declare-rule bv-srem-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (nm1 Int))
   :premises ((= nm1 (- (@bvsize x1) 1)))
   :args (x1 y1 nm1)
-  :conclusion (= (bvsrem x1 y1) (eo::define ((_let_1 (extract nm1 nm1 x1))) (eo::define ((_let_2 (bvurem (bvite _let_1 (bvneg x1) x1) (bvite (extract nm1 nm1 y1) (bvneg y1) y1)))) (bvite _let_1 (bvneg _let_2) _let_2))))
+  :conclusion (= (bvsrem x1 y1) (eo::define ((_let_1 (@bv 1 1))) (eo::define ((_let_2 (= (extract nm1 nm1 x1) _let_1))) (eo::define ((_let_3 (bvurem (ite _let_2 (bvneg x1) x1) (ite (= (extract nm1 nm1 y1) _let_1) (bvneg y1) y1)))) (ite _let_2 (bvneg _let_3) _let_3)))))
 )
 (declare-rule bv-srem-eliminate-fewer-bitwise-ops ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (nm1 Int))
   :premises ((= nm1 (- (@bvsize x1) 1)))
@@ -891,7 +891,7 @@
 )
 (declare-rule bv-ite-merge-then-else ((@n0 Int) (@n1 Int) (c1 (_ BitVec 1)) (c2 (_ BitVec 1)) (t1 (BitVec @n0)) (e1 (BitVec @n1)))
   :args (c1 c2 t1 e1)
-  :conclusion (= (bvite c1 t1 (bvite c2 t1 e1)) (bvite (bvnor c1 c2) e1 t1))
+  :conclusion (= (bvite c1 t1 (bvite c2 t1 e1)) (bvite (bvand (bvnot c1) (bvnot c2)) e1 t1))
 )
 (declare-rule bv-ite-merge-else-else ((@n0 Int) (@n1 Int) (c1 (_ BitVec 1)) (c2 (_ BitVec 1)) (t1 (BitVec @n0)) (t2 (BitVec @n1)))
   :args (c1 c2 t1 t2)
@@ -1136,14 +1136,13 @@
   :conclusion (= (sign_extend i1 (sign_extend j1 x1)) (sign_extend k1 x1))
 )
 (declare-rule bv-merge-sign-extend-2 ((@n0 Int) (x1 (BitVec @n0)) (i1 Int) (j1 Int) (k1 Int))
-  :premises ((= (> j1 1) true) (= k1 (+ i1 j1)))
+  :premises ((= (> j1 0) true) (= k1 (+ i1 j1)))
   :args (x1 i1 j1 k1)
   :conclusion (= (sign_extend i1 (zero_extend j1 x1)) (zero_extend k1 x1))
 )
-(declare-rule bv-merge-sign-extend-3 ((@n0 Int) (x1 (BitVec @n0)) (i1 Int) (n1 Int))
-  :premises ((= n1 0))
-  :args (x1 i1 n1)
-  :conclusion (= (sign_extend i1 (zero_extend n1 x1)) (sign_extend i1 x1))
+(declare-rule bv-merge-sign-extend-3 ((@n0 Int) (x1 (BitVec @n0)) (i1 Int))
+  :args (x1 i1)
+  :conclusion (= (sign_extend i1 (zero_extend 0 x1)) (sign_extend i1 x1))
 )
 (declare-rule bv-sign-extend-eq-const-1 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (mp1 Int) (nm2 Int) (nmm1 Int))
   :premises ((= mp1 (+ m1 1)) (= nm2 (- (@bvsize x1) 1)) (= nmm1 (- nm1 1)))
@@ -1165,6 +1164,16 @@
   :args (x1 m1 c1 nm1 nm2 nmm1)
   :conclusion (= (= (@bv c1 nm1) (zero_extend m1 x1)) (eo::define ((_let_1 (@bv c1 nm1))) (and (= (extract nmm1 nm2 _let_1) (@bv 0 m1)) (= x1 (extract nm2 0 _let_1)))))
 )
+(declare-rule bv-zero-extend-ult-const-1 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int))
+  :premises ((= nm2 (- (@bvsize x1) 1)) (eo::define ((_let_1 (@bv c1 nm1))) (= _let_1 (zero_extend m1 (extract nm2 0 _let_1)))))
+  :args (x1 m1 c1 nm1 nm2)
+  :conclusion (= (bvult (zero_extend m1 x1) (@bv c1 nm1)) (bvult x1 (extract nm2 0 (@bv c1 nm1))))
+)
+(declare-rule bv-zero-extend-ult-const-2 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int))
+  :premises ((= nm2 (- (@bvsize x1) 1)) (eo::define ((_let_1 (@bv c1 nm1))) (= _let_1 (zero_extend m1 (extract nm2 0 _let_1)))))
+  :args (x1 m1 c1 nm1 nm2)
+  :conclusion (= (bvult (@bv c1 nm1) (zero_extend m1 x1)) (bvult (extract nm2 0 (@bv c1 nm1)) x1))
+)
 (declare-rule bv-sign-extend-ult-const-1 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int))
   :premises ((eo::define ((_let_1 (@bv (- (@bvsize x1) 1) nm1))) (eo::define ((_let_2 (@bv c1 nm1))) (= (or (bvule _let_2 (bvshl (@bv 1 nm1) _let_1)) (bvuge _let_2 (bvshl (bvnot (@bv 0 nm1)) _let_1))) true))) (= nm2 (- (@bvsize x1) 1)))
   :args (x1 m1 c1 nm1 nm2)

src/rewriter/basic_rewrite_rcons.cpp

@@ -36,8 +36,10 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"
+#include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/strings_entail.h"
 #include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
 #include "util/rational.h"
 
 using namespace cvc5::internal::kind;
@@ -222,6 +224,13 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite(CDProof* cdp,
         handledMacro = true;
       }
       break;
+    case ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS:
+    case ProofRewriteRule::MACRO_STR_SPLIT_CTN:
+      if (ensureProofMacroOverlap(id, cdp, eq))
+      {
+        handledMacro = true;
+      }
+      break;
     case ProofRewriteRule::MACRO_QUANT_MERGE_PRENEX:
       if (ensureProofMacroQuantMergePrenex(cdp, eq))
       {
@@ -911,6 +920,205 @@ bool BasicRewriteRCons::ensureProofMacroSubstrStripSymLength(CDProof* cdp,
   return true;
 }
 
+bool BasicRewriteRCons::ensureProofMacroOverlap(ProofRewriteRule id,
+                                                CDProof* cdp,
+                                                const Node& eq)
+{
+  Trace("brc-macro") << "Expand macro overlap (" << id << ") for " << eq
+                     << std::endl;
+  NodeManager* nm = nodeManager();
+  Assert(eq[0].getNumChildren() >= 2);
+  Node concat = eq[0][0];
+  TypeNode stype = concat.getType();
+  Node emp = theory::strings::Word::mkEmptyWord(stype);
+  size_t nchildpre = 0;
+  ProofRewriteRule rule;
+  std::vector<Node> premises;
+  if (id == ProofRewriteRule::MACRO_STR_SPLIT_CTN)
+  {
+    Assert(concat.getKind() == Kind::STRING_CONCAT);
+    rule = ProofRewriteRule::STR_OVERLAP_SPLIT_CTN;
+    Assert(eq[1].getKind() == Kind::OR
+           && eq[1][0].getKind() == Kind::STRING_CONTAINS);
+    if (eq[1][0][0].getKind() == Kind::STRING_CONCAT)
+    {
+      nchildpre = eq[1][0][0].getNumChildren();
+    }
+    else if (eq[1][0][0] != emp)
+    {
+      nchildpre = 1;
+    }
+    // partition into three children
+    std::vector<Node> childpre(concat.begin(), concat.begin() + nchildpre);
+    Node cpre = theory::strings::utils::mkConcat(childpre, stype);
+    Node cmid = concat[nchildpre];
+    std::vector<Node> childpost(concat.begin() + nchildpre + 1, concat.end());
+    Node cpost = theory::strings::utils::mkConcat(childpost, stype);
+    Node cgroup = nm->mkNode(Kind::STRING_CONCAT, cpre, cmid, cpost);
+    if (concat != cgroup)
+    {
+      Node eqc = concat.eqNode(cgroup);
+      if (!cdp->addStep(eqc, ProofRule::ACI_NORM, {}, {eqc}))
+      {
+        Assert(false);
+        return false;
+      }
+      premises.push_back(eqc);
+    }
+  }
+  else
+  {
+    Assert(id == ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS);
+    theory::strings::ArithEntail ae(nullptr);
+    theory::strings::StringsEntail se(nullptr, ae);
+    theory::strings::SequencesRewriter srew(nm, ae, se, nullptr);
+    std::vector<Node> nb, nc1, ne;
+    // replay the strip endpoint operation
+    Kind k = eq[0].getKind();
+    Node res = srew.rewriteViaMacroStrStripEndpoints(eq[0], nb, nc1, ne);
+    if (res != eq[1])
+    {
+      Assert(false);
+      return false;
+    }
+    std::vector<Node> nc2;
+    theory::strings::utils::getConcat(eq[0][1], nc2);
+    std::vector<Node> newChildren[2];
+    for (size_t i = 0; i < 2; i++)
+    {
+      std::vector<Node>& vec = i == 0 ? nb : ne;
+      if (i == 0 && k == Kind::STRING_INDEXOF)
+      {
+        Assert(vec.empty());
+        continue;
+      }
+      else if (i == 1)
+      {
+        // placeholder for the middle term
+        newChildren[0].push_back(emp);
+        newChildren[1].push_back(emp);
+      }
+      if (vec.empty())
+      {
+        newChildren[0].push_back(emp);
+        newChildren[1].push_back(emp);
+        continue;
+      }
+      if (vec.size() != 1)
+      {
+        Trace("brc-macro") << "...fail due to multiple stripped components"
+                           << std::endl;
+        Assert(false);
+        return false;
+      }
+      newChildren[0].push_back(vec[0]);
+      // should be the case since we don't rewrite from both sides if
+      // the second term is a constant.
+      Assert(!nc2.empty());
+      size_t index2 = (i == 0 ? 0 : nc2.size() - 1);
+      if (i == 0)
+      {
+        newChildren[1].push_back(nc2[index2]);
+        nc2.erase(nc2.begin(), nc2.begin() + 1);
+      }
+      else
+      {
+        newChildren[1].push_back(nc2[index2]);
+        nc2.pop_back();
+      }
+    }
+    size_t remIndex = k == Kind::STRING_INDEXOF ? 0 : 1;
+    newChildren[0][remIndex] = theory::strings::utils::mkConcat(nc1, stype);
+    newChildren[1][remIndex] = theory::strings::utils::mkConcat(nc2, stype);
+    Trace("brc-macro") << "First child processed to : " << eq[0][0]
+                       << " == " << newChildren[0] << std::endl;
+    Trace("brc-macro") << "Second child processed to : " << eq[0][1]
+                       << " == " << newChildren[1] << std::endl;
+    // now, check if the children changed, if so add to premises
+    Node g1 = theory::strings::utils::mkConcat(newChildren[0], stype);
+    Node g2 = theory::strings::utils::mkConcat(newChildren[1], stype);
+    // the first may involve more than ACI_NORM, we use a subgoal
+    if (g1 != eq[0][0])
+    {
+      Node eqc = eq[0][0].eqNode(g1);
+      cdp->addTrustedStep(
+          eqc, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {});
+      premises.push_back(eqc);
+    }
+    // the second should just be ACI_NORM
+    if (g2 != eq[0][1])
+    {
+      // add the REFL step if we didnt change above
+      if (g1 == eq[0][0])
+      {
+        Node refl = eq[0][0].eqNode(eq[0][0]);
+        cdp->addStep(refl, ProofRule::REFL, {}, {eq[0][0]});
+        premises.push_back(refl);
+      }
+      Node eqc = eq[0][1].eqNode(g2);
+      if (!cdp->addStep(eqc, ProofRule::ACI_NORM, {}, {eqc}))
+      {
+        Assert(false);
+        Trace("brc-macro") << "...failed ACI_NORM" << std::endl;
+        return false;
+      }
+      premises.push_back(eqc);
+    }
+    switch (k)
+    {
+      case Kind::STRING_CONTAINS:
+        rule = ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN;
+        break;
+      case Kind::STRING_INDEXOF:
+        rule = ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF;
+        break;
+      case Kind::STRING_REPLACE:
+        rule = ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE;
+        break;
+      default: return false;
+    }
+  }
+  // cgroup is now the proper version of concat and we have proved (if
+  // necessary) that concat = cgroup.
+  Node input = eq[0];
+  // if we rewrote children above
+  std::vector<Node> transEq;
+  if (!premises.empty())
+  {
+    // prove input = inputRew by congruence given the premises
+    Node ceq = proveCong(cdp, input, premises);
+    transEq.push_back(ceq);
+    input = ceq[1];
+  }
+  Trace("brc-macro") << "Run " << rule << " on " << input << std::endl;
+  theory::Rewriter* rr = d_env.getRewriter();
+  Node ret = rr->rewriteViaRule(rule, input);
+  if (ret.isNull())
+  {
+    Trace("brc-macro") << "...failed rewrite" << std::endl;
+    return false;
+  }
+  // add the rewrite
+  Node equiv = input.eqNode(ret);
+  cdp->addTheoryRewriteStep(equiv, rule);
+  transEq.push_back(equiv);
+  if (ret != eq[1])
+  {
+    // should rewrite e.g. via ACI_NORM
+    Node eqpost = ret.eqNode(eq[1]);
+    Trace("brc-macro") << "- post-process subgoal " << eqpost << std::endl;
+    cdp->addTrustedStep(
+        eqpost, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {});
+    transEq.push_back(eqpost);
+  }
+  // apply transitivity if necessary
+  if (transEq.size() > 1)
+  {
+    cdp->addStep(eq, ProofRule::TRANS, transEq, {});
+  }
+  return true;
+}
+
 bool BasicRewriteRCons::ensureProofMacroQuantMergePrenex(CDProof* cdp,
                                                          const Node& eq)
 {

src/rewriter/basic_rewrite_rcons.h

@@ -191,6 +191,21 @@ 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_SPLIT_CTN or
+   * ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS.
+   *
+   * @param id The macro rule we are expanding.
+   * @param cdp The proof to add to.
+   * @param eq The rewrite proven by
+   * ProofRewriteRule::MACRO_STR_SPLIT_CTN or
+   * ProofRewriteRule::MACRO_STR_STRIP_ENDPOINTS.
+   * @return true if added a closed proof of eq to cdp.
+   */
+  bool ensureProofMacroOverlap(ProofRewriteRule id,
+                               CDProof* cdp,
+                               const Node& eq);
   /**
    * Elaborate a rewrite eq that was proven by
    * ProofRewriteRule::MACRO_QUANT_MERGE_PRENEX.

src/theory/bv/rewrites

@@ -192,14 +192,15 @@
 
 ; -- Simplify Bitblasting --
 
-; x < y + 1 <=> (not y < x) and y != 1...1
+; x < ys + 1 + zs <=> (not (ys + zs) < x) and (ys + zs) != 1...1
+; we use ys, zs as lists so that 1 may appear on the left or the right of the bvadd term.
 (define-cond-rule bv-ult-add-one
-  ((x ?BitVec) (y ?BitVec) (c1 ?BitVec) (w Int))
-  (and (= c1 (@bv 1 w)) (= w (@bvsize y)))
-  (bvult x (bvadd y c1))
+  ((x ?BitVec) (ys ?BitVec :list) (zs ?BitVec :list) (c1 ?BitVec) (w Int))
+  (and (= c1 (@bv 1 w)) (= w (@bvsize x)))
+  (bvult x (bvadd ys c1 zs))
   (and
-    (not (= y (bvnot (@bv 0 w))))
-    (not (bvult y x))))
+    (not (= (bvadd ys zs) (bvnot (@bv 0 w))))
+    (not (bvult (bvadd ys zs) x))))
 (define-cond-rule bv-concat-to-mult
   ((x ?BitVec) (i Int) (m Int) (n0 Int) (w Int))
   (and (= (+ 1 i m) (@bvsize x)) (= n0 0) (= w (@bvsize x)))