diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index 0651c6a4fef..d90610f1541 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/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 diff --git a/proofs/alf/cvc5/programs/Nary.smt3 b/proofs/alf/cvc5/programs/Nary.smt3 index 71004312a1b..c0317132f57 100644 --- a/proofs/alf/cvc5/programs/Nary.smt3 +++ b/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)) diff --git a/proofs/alf/cvc5/programs/Strings.smt3 b/proofs/alf/cvc5/programs/Strings.smt3 index 61f645d4550..da66ef6e8b8 100644 --- a/proofs/alf/cvc5/programs/Strings.smt3 +++ b/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. diff --git a/proofs/alf/cvc5/programs/Utils.smt3 b/proofs/alf/cvc5/programs/Utils.smt3 index 4fdfdcf3fb7..0964d799d97 100644 --- a/proofs/alf/cvc5/programs/Utils.smt3 +++ b/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. diff --git a/proofs/alf/cvc5/rules/Strings.smt3 b/proofs/alf/cvc5/rules/Strings.smt3 index 443df64600a..24a0987c2b3 100644 --- a/proofs/alf/cvc5/rules/Strings.smt3 +++ b/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)) diff --git a/proofs/alf/cvc5/theories/Sets.smt3 b/proofs/alf/cvc5/theories/Sets.smt3 index 8981bc2f045..67262bc9ad6 100644 --- a/proofs/alf/cvc5/theories/Sets.smt3 +++ b/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)))) diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index d60dec1cb32..a0c52737900 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/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: diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 7e4930d475b..60af33d8379 100644 --- a/src/theory/strings/core_solver.cpp +++ b/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, diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index aaad7b308c7..dc3d758aae3 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/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) { diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h index afb9a6c9b02..293e662ecbf 100644 --- a/src/theory/strings/theory_strings_utils.h +++ b/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.