Support ProofRule::CONCAT_CPROP in ALF (cvc5#10697)

Also updates the internal inference, which had been short circuiting the evaluation of the spliced constants.

include/cvc5/cvc5_proof_rule.h

@@ -1531,9 +1531,9 @@ enum ENUM(ProofRule) : uint32_t
    * .. math::
    *
    *   \inferrule{(t_1\cdot w_1\cdot t_2) = (w_2 \cdot s),\,
-   *   \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = w_3\cdot r)}
+   *   \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = t_3\cdot r)}
    *
-   * where :math:`w_1,\,w_2,\,w_3` are words, :math:`w_3` is
+   * where :math:`w_1,\,w_2` are words, :math:`t_3` is
    * :math:`\mathit{pre}(w_2,p)`, :math:`p` is
    * :math:`\texttt{Word::overlap}(\mathit{suf}(w_2,1), w_1)`, and :math:`r` is
    * :math:`\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(w_3)))`.  Note that
@@ -1547,10 +1547,10 @@ enum ENUM(ProofRule) : uint32_t
    * .. math::
    *
    *   \inferrule{(t_1\cdot w_1\cdot t_2) = (s \cdot w_2),\,
-   *   \mathit{len}(t_2) \neq 0\mid \top}{(t_2 = r\cdot w_3)}
+   *   \mathit{len}(t_2) \neq 0\mid \top}{(t_2 = r\cdot t_3)}
    *
-   * where :math:`w_1,\,w_2,\,w_3` are words, :math:`w_3` is
-   * :math:`\mathit{suf}(w_2, \mathit{len}(w_2) - p)`, :math:`p` is
+   * where :math:`w_1,\,w_2` are words, :math:`t_3` is
+   * :math:`\mathit{substr}(w_2, \mathit{len}(w_2) - p, p)`, :math:`p` is
    * :math:`\texttt{Word::roverlap}(\mathit{pre}(w_2, \mathit{len}(w_2) - 1),
    * w_1)`, and :math:`r` is :math:`\mathit{skolem}(\mathit{pre}(t_2,
    * \mathit{len}(t_2) - \mathit{len}(w_3)))`.  Note that

proofs/alf/cvc5/programs/Nary.smt3

@@ -61,10 +61,11 @@
 ; nary.reverse cons nil xs
 ; Reverses the list `xs`.
 (program nary.reverse
-    ((L Type) (cons (-> L L L)) (nil L) (xs L :list))
-    ((-> L L L) L L) L
+    ((L Type) (cons (-> L L L)) (x L) (xs L :list))
+    (L) L
     (
-        ((nary.reverse cons nil xs) (nary.reverseRec cons nil xs nil))
+        ((nary.reverse (cons x xs)) (let ((nil (alf.nil cons x xs))) (nary.reverseRec cons nil (cons x xs) nil)))
+        ((nary.reverse x)           x)
     )
 )
 
@@ -86,10 +87,23 @@
     ((-> L L L) L L L) Bool
     (
         ((nary.is_prefix cons nil nil t)                       true)
+        ((nary.is_prefix cons nil t nil)                       false)
         ((nary.is_prefix cons nil (cons c1 xs1) (cons c2 xs2)) (alf.ite (alf.is_eq c1 c2) (nary.is_prefix cons nil xs1 xs2) false))
     )
 )
 
+; nary.is_compatible cons t s
+; Retuns `true` if t is a prefix of s, or s is a prefix of t.
+(program nary.is_compatible
+    ((L Type) (cons (-> L L L)) (nil L) (t L) (c1 L) (c2 L) (xs1 L :list) (xs2 L :list))
+    ((-> L L L) L L L) Bool
+    (
+        ((nary.is_compatible cons nil nil t)                       true)
+        ((nary.is_compatible cons nil t nil)                       true)
+        ((nary.is_compatible cons nil (cons c1 xs1) (cons c2 xs2)) (alf.ite (alf.is_eq c1 c2) (nary.is_compatible cons nil xs1 xs2) false))
+    )
+)
+
 ; nary.join
 (program nary.join
     ((L Type) (cons (-> L L L)) (nil L) (elim-nil L) (c L) (x L) (xs L :list) (y L) (ys L :list))

proofs/alf/cvc5/programs/Strings.smt3

@@ -138,11 +138,16 @@
   (str.substr s 0 n)
 )
 
-; Get the term corresponding to the suffix of term s of fixed length n.
+; Get the term corresponding to the suffix of term s starting from position n.
 (define skolem_suffix_rem ((U Type :implicit) (s (Seq U)) (n Int))
   (str.substr s n (- (str.len s) n))
 )
 
+; Get the term corresponding to the suffix of term s of length n.
+(define $str_suffix_len ((U Type :implicit) (s (Seq U)) (n Int))
+  (str.substr s (- (str.len s) n) n)
+)
+
 ; The unified splitting term for t and s, which is the term that denotes the
 ; prefix (or suffix if rev is true) remainder of t (resp. s) in the case that
 ; t (resp. s) is the longer string.
@@ -170,21 +175,9 @@
 
 ;;-------------------- Utilities
 
-; Helper for reversing a concatenation term
-(program $str_rev_rec
-    ((T Type) (t (Seq T)) (ss (Seq T) :list) (acc (Seq T)))
-    ((Seq T) (Seq T) Type) (Seq T)
-    (
-        (($str_rev_rec (str.++ t ss) acc T) ($str_rev_rec ss ($str_cons t acc) T))
-        (($str_rev_rec t acc T)             (alf.requires t (mk_emptystr (Seq T)) acc))
-    )
-)
-
 ; Return reverse of t if rev = true, return t unchanged otherwise.
-(define $str_rev ((U Type :implicit) (rev Bool) (t (Seq U))) 
-  (alf.ite rev 
-    (let ((U ($char_type_of (alf.typeof t)))) ($str_rev_rec t (mk_emptystr (Seq U)) U)) 
-    t))
+(define $str_rev ((U Type :implicit) (rev Bool) (t U)) 
+  (alf.ite rev (nary.reverse t) t))
 
 ; Nary-intro, which ensures that the input t is a str.++ application.
 ; In particular, if it is not a str.++ and not the empty string, then we return
@@ -528,6 +521,28 @@
   )
 )
 
+; Helper for $str_overlap.
+(program $str_overlap_rec ((U Type) (s (Seq U)) (s1 (Seq U) :list) (t (Seq U)) (nil (Seq U)))
+  ((Seq U) (Seq U) (Seq U)) Int
+  (
+  (($str_overlap_rec nil (str.++ s s1) t) (alf.ite (nary.is_compatible str.++ nil (str.++ s s1) t)
+                                            0
+                                            (alf.add 1 ($str_overlap_rec nil s1 t))))
+  (($str_overlap_rec nil s t)             0)
+  )
+)
+
+; Returns the minimum number of characters that must be skipped in s before
+; string t can be compatible with it. For example:
+;   $str_overlap (str.++ "A" "B" "C" "") (str.++ "B" "C" "D" "") = 1
+;   $str_overlap (str.++ "A" "B" "C" "") (str.++ "B" "") = 1
+;   $str_overlap (str.++ "A" "B" "C" "") (str.++ "E" "") = 3
+;   $str_overlap (str.++ "A" "B" "C" "") (str.++ "A" "A" "") = 3
+;   $str_overlap (str.++ "A" "B" "C" "") (str.++ "A" "") = 0
+; Expects s and t to be in nary (flattened) form.
+(define $str_overlap ((U Type :implicit) (s (Seq U)) (t (Seq U)))
+  ($str_overlap_rec (mk_emptystr (alf.typeof s)) s t))
+
 ; Helper for $str_mk_re_loop_elim.
 ; When we call `$str_mk_re_loop_elim n d r rr`, we first decrement n until it
 ; is zero, while accumulating rr. When it is zero, then rr is r^n.

proofs/alf/cvc5/programs/Utils.smt3

@@ -53,6 +53,13 @@
 (define compare_var ((T Type :implicit) (U Type :implicit) (a T) (b U))
   (alf.is_neg (alf.add (alf.hash a) (alf.neg (alf.hash b)))))
 
+; Returns the tail of x, where x is expected to be a function application.
+(define $tail ((S Type :implicit) (x S))
+  (alf.match ((T Type) (U Type) (S Type) (f (-> T U S)) (x1 T) (x2 T :list))
+    x
+    (((f x1 x2) x2)))
+)
+
 ; Eliminate singleton list.
 ; If the input term is of the form (f x1 x2) where x2 is the nil terminator of
 ; f, then we return x1. Otherwise, we return the input term unchanged.

proofs/alf/cvc5/rules/Strings.smt3

@@ -118,6 +118,29 @@
                 )))))))))
 )
 
+; ProofRule::CONCAT_CPROP
+(declare-rule concat_cprop ((U Type) (t (Seq U)) (tc (Seq U)) (s (Seq U)) (rev Bool))
+  :premises ((= t s) (not (= (str.len tc) 0)))
+  :args (rev)
+  :conclusion
+    (alf.match ((t1 (Seq U)) (t2 (Seq U)) (t3 (Seq U) :list))
+      ($str_rev rev t)
+      (((str.++ t1 t2 t3)
+        (alf.requires t1 tc
+          (alf.match ((s1 (Seq U)) (s2 (Seq U) :list))
+            ($str_rev rev ($str_nary_intro s))  ; must do nary intro when s is just a constant
+            (((str.++ s1 s2)
+                (let ((sc (string_to_flat_form s1 rev)))
+                (let ((v (alf.add 1 ($str_overlap ($tail sc) (string_to_flat_form t2 rev)))))
+                  (= tc
+                    (alf.ite rev
+                      (let ((oc ($str_suffix_len s1 v)))
+                      (str.++ (skolem (skolem_prefix tc (- (str.len tc) (str.len oc)))) oc))
+                      (let ((oc (skolem_prefix s1 v)))
+                      (str.++ oc (skolem (skolem_suffix_rem tc (str.len oc)))))))
+                )))))))))
+)
+
 ; ProofRule::CONCAT_CONFLICT, for strings only
 (declare-rule concat_conflict ((s String) (t String) (rev Bool))
   :premises ((= s t))

proofs/alf/cvc5/theories/Sets.smt3

@@ -35,7 +35,7 @@
 
 ; Relation operators.
 (declare-const rel.tclosure (-> (! Type :var T :implicit) (Set (Tuple T T)) (Set (Tuple T T))))
-(declare-const rel.transpose (-> (! Type :var T :implicit) (Set T) (Set (nary.reverse Tuple UnitTuple T))))
+(declare-const rel.transpose (-> (! Type :var T :implicit) (Set T) (Set (nary.reverse T))))
 (declare-const rel.product (-> (! Type :var T :implicit) (! Type :var U :implicit) (Set T) (Set U) (Set (alf.concat Tuple T U))))
 (declare-const rel.join (-> (! Type :var T :implicit) (! Type :var U :implicit) (Set T) (Set U) (Set (nary.join Tuple UnitTuple T U))))
 (declare-const rel.group (-> (! Type :var T :implicit) @List (Set T) (Set (Set T))))

src/proof/alf/alf_printer.cpp

@@ -129,6 +129,7 @@ bool AlfPrinter::isHandled(const ProofNode* pfn) const
     case ProofRule::CONCAT_EQ:
     case ProofRule::CONCAT_UNIFY:
     case ProofRule::CONCAT_CSPLIT:
+    case ProofRule::CONCAT_CPROP:
     case ProofRule::CONCAT_CONFLICT:
     case ProofRule::CONCAT_SPLIT:
     case ProofRule::CONCAT_LPROP:

src/theory/strings/core_solver.cpp

@@ -792,10 +792,9 @@ Node CoreSolver::getConclusion(Node x,
     Assert(d.isConst());
     Node c = y;
     Assert(c.isConst());
-    size_t cLen = Word::getLength(c);
     size_t p = getSufficientNonEmptyOverlap(c, d, isRev);
-    Node preC =
-        p == cLen ? c : (isRev ? Word::suffix(c, p) : Word::prefix(c, p));
+    Node rp = nm->mkConstInt(p);
+    Node preC = (isRev ? utils::mkSuffixOfLen(c, rp) : utils::mkPrefix(c, rp));
     Node sk = skc->mkSkolemCached(
         z,
         preC,

src/theory/strings/theory_strings_utils.cpp

@@ -157,6 +157,12 @@ Node mkSuffix(Node t, Node n)
       n,
       nm->mkNode(Kind::SUB, nm->mkNode(Kind::STRING_LENGTH, t), n));
 }
+Node mkSuffixOfLen(Node t, Node n)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node lent = nm->mkNode(Kind::STRING_LENGTH, t);
+  return nm->mkNode(Kind::STRING_SUBSTR, t, nm->mkNode(Kind::SUB, lent, n), n);
+}
 
 Node mkUnit(TypeNode tn, Node n)
 {

src/theory/strings/theory_strings_utils.h

@@ -70,6 +70,11 @@ Node mkPrefix(Node t, Node n);
  */
 Node mkSuffix(Node t, Node n);
 
+/**
+ * Returns (suf t n), which is (str.substr t (- (str.len t) n) n).
+ */
+Node mkSuffixOfLen(Node t, Node n);
+
 /**
  * Make a unit, returns either (str.unit n) or (seq.unit n) depending
  * on if tn is a string or a sequence.