; depends: nary_programs.plf theory_def.plf
-; Make empty string of the given string-like sort s.
-(program sc_mk_emptystr ((s sort)) term
- (match s
- ((Seq t) (seq.empty s))
+; This signature is used for both strings and sequences, where we often
+; write "string" in the documentation to refer to a string or sequence.
+
+; Make empty string of the given string-like sort u.
+(program sc_mk_emptystr ((u sort)) term
+ (match u
+ ((Seq t) (seq.empty u))
(String emptystr)))
+; Return true if s is the empty string or sequence.
+(program sc_string_is_empty ((s term)) flag
+ (match s
+ ((seq.empty s) tt)
+ (emptystr tt)
+ (default ff)))
+
; Get the term corresponding to the prefix of term s of fixed length n.
(program sc_skolem_prefix ((s term) (n term)) term
(str.substr s (int 0) n)
(program sc_string_head ((t term)) term (nary_head f_str.++ t))
(program sc_string_tail ((t term)) term (nary_tail f_str.++ t))
-; Concatenation str.++ applications t1 and t2.
-(program sc_string_concat ((t1 term) (t2 term)) term (nary_concat f_str.++ t1 t2 emptystr))
+; Concatenation str.++ applications t1 and t2. Note this side condition requires
+; taking the sort u of t1 for constructing the empty string.
+(program sc_string_concat ((t1 term) (t2 term) (u sort)) term (nary_concat f_str.++ t1 t2 (sc_mk_emptystr u)))
-; Decompose str.++ term t into a head and tail.
-(program sc_string_decompose ((t term)) termPair (nary_decompose f_str.++ t emptystr))
+; Decompose str.++ term t of sort u into a head and tail.
+(program sc_string_decompose ((t term) (u sort)) termPair (nary_decompose f_str.++ t (sc_mk_emptystr u)))
-; String is prefix, returns tt if s is a prefix of t
-(program sc_string_is_prefix ((s term) (t term)) flag (nary_is_prefix f_str.++ s t emptystr))
+; String is prefix, returns tt if t1 of sort u is a prefix of t2
+(program sc_string_is_prefix ((t1 term) (t2 term) (u sort)) flag (nary_is_prefix f_str.++ t1 t2 (sc_mk_emptystr u)))
-; Insert a string into str.++ term t.
-(program sc_string_insert ((elem term) (t term)) term (nary_insert f_str.++ elem t emptystr))
+; Insert a string into str.++ term t of sort u.
+(program sc_string_insert ((elem term) (t term) (u sort)) term (nary_insert f_str.++ elem t (sc_mk_emptystr u)))
; Return reverse of t if rev = tt, return t unchanged otherwise.
-(program sc_string_rev ((t term) (rev flag)) term (ifequal rev tt (nary_reverse f_str.++ t emptystr) t))
+(program sc_string_rev ((t term) (rev flag) (u sort)) term (ifequal rev tt (nary_reverse f_str.++ t (sc_mk_emptystr u)) t))
; Convert a str.++ application t into its element, if it is a singleton, return t unchanged otherwise.
-(program sc_string_nary_elim ((t term)) term (nary_elim f_str.++ t emptystr))
+(program sc_string_nary_elim ((t term) (u sort)) term (nary_elim f_str.++ t (sc_mk_emptystr u)))
; Convert t into a str.++ application, if it is not already in n-ary form.
-(program sc_string_nary_intro ((t term)) term (nary_intro f_str.++ t emptystr))
+(program sc_string_nary_intro ((t term) (u sort)) term (nary_intro f_str.++ t (sc_mk_emptystr u)))
; In the following, a "reduction predicate" refers to a formula that is used
; to axiomatize an extended string function in terms of (simpler) functions.
; Compute the reduction predicate for (str.substr x n m) of sort s.
-(program sc_string_reduction_substr ((x term) (n term) (m term) (s sort)) term
+(program sc_string_reduction_substr ((x term) (n term) (m term) (u sort)) term
(let k (sc_mk_skolem (str.substr x n m))
(let npm (a.+ n (a.+ m (int 0)))
(let k1 (sc_mk_skolem (sc_skolem_prefix x n))
(and (a.> m (int 0))
true)))
; if branch
- (and (= x (str.++ k1 (str.++ k (str.++ k2 (sc_mk_emptystr s)))))
+ (and (= x (str.++ k1 (str.++ k (str.++ k2 (sc_mk_emptystr u)))))
(and (= (str.len k1) n)
(and (or (= (str.len k2) (a.- (str.len x) npm))
(or (= (str.len k2) (int 0))
(and (a.<= (str.len k) m)
true))))
; else branch
- (= k (sc_mk_emptystr s))
+ (= k (sc_mk_emptystr u))
)))))
)
; Compute the reduction predicate for (str.indexof x y n) of sort s.
-(program sc_string_reduction_indexof ((x term) (y term) (n term) (s sort)) term
+(program sc_string_reduction_indexof ((x term) (y term) (n term) (u sort)) term
(let k (sc_mk_skolem (str.indexof x y n))
(let xn (str.substr x n (a.- (str.len x) n))
(let k1 (sc_mk_skolem (sc_skolem_first_ctn_pre xn y))
false)))
(= k (int (~ 1)))
(ite
- (= y (sc_mk_emptystr s))
+ (= y (sc_mk_emptystr u))
(= k n)
- (and (= xn (str.++ k1 (str.++ y (str.++ k2 (sc_mk_emptystr s)))))
+ (and (= xn (str.++ k1 (str.++ y (str.++ k2 (sc_mk_emptystr u)))))
(and (not (str.contains
(str.++ k1
(str.++ (str.substr y (int 0) (a.- (str.len y) (int 1)))
- (sc_mk_emptystr s))) y))
+ (sc_mk_emptystr u))) y))
(and (= k (a.+ n (a.+ (str.len k1) (int 0))))
true)))
)))))))
; Compute the reduction predicate for term t of sort s. Note that the operators
; listed in comments are missing from the signature currently.
-(program sc_string_reduction_pred ((t term) (s sort)) term
+(program sc_string_reduction_pred ((t term) (u sort)) term
(match t
((apply t1 t2)
(match t1
; str.contains
((apply t111 t112)
(match t111
- (f_str.substr (sc_string_reduction_substr t112 t12 t2 s))
- (f_str.indexof (sc_string_reduction_indexof t112 t12 t2 s))
+ (f_str.substr (sc_string_reduction_substr t112 t12 t2 u))
+ (f_str.indexof (sc_string_reduction_indexof t112 t12 t2 u))
; str.replace
; str.update
; str.from_int
; Returns the reduction predicate and purification equality for term t
; of sort s.
-(program sc_string_reduction ((t term) (s sort)) term
- (and (sc_string_reduction_pred t s) (and (= t (sc_mk_skolem t)) true))
+(program sc_string_reduction ((t term) (u sort)) term
+ (and (sc_string_reduction_pred t u) (and (= t (sc_mk_skolem t)) true))
)
; Compute the eager reduction predicate for (str.contains t r) where s
; is the sort of t and r.
; This is the formula:
; (ite (str.contains t r) (= t (str.++ sk1 r sk2)) (not (= t r)))
-(program sc_string_eager_reduction_contains ((t term) (r term) (s sort)) term
+(program sc_string_eager_reduction_contains ((t term) (r term) (u sort)) term
(let k1 (sc_mk_skolem (sc_skolem_first_ctn_pre t r))
(let k2 (sc_mk_skolem (sc_skolem_first_ctn_post t r))
(ite
(str.contains t r)
- (= t (str.++ k1 (str.++ r (str.++ k2 (sc_mk_emptystr s)))))
+ (= t (str.++ k1 (str.++ r (str.++ k2 (sc_mk_emptystr u)))))
(not (= t r)))
))
)
)
; Compute the eager reduction predicate of term t of sort s.
-(program sc_string_eager_reduction ((t term) (s sort)) term
+(program sc_string_eager_reduction ((t term) (u sort)) term
(match t
((apply t1 t2)
(match t1
(f_str.to_code (sc_string_eager_reduction_to_code t2))
((apply t11 t12)
(match t11
- (f_str.contains (sc_string_eager_reduction_contains t12 t2 s))
+ (f_str.contains (sc_string_eager_reduction_contains t12 t2 u))
((apply t111 t112)
(match t111
(f_str.indexof (sc_string_eager_reduction_indexof t112 t12 t2)))))))))
; (str.++ x (str.++ y ""))
; this returns:
; (and (= x "") (and (= y "") true))
-(program sc_non_empty_concats ((t term)) term
+(program sc_non_empty_concats ((t term) (u sort)) term
(match t
((apply t1 t2)
- (and (not (= (getarg f_str.++ t1) emptystr)) (sc_non_empty_concats t2)))
- (emptystr true)))
+ (and (not (= (getarg f_str.++ t1) (sc_mk_emptystr u))) (sc_non_empty_concats t2 u)))
+ (default (ifequal t (sc_mk_emptystr u) true (fail term)))))
; Get first character or empty string from term t.
; If t is of the form (str.++ (char n) ...), return (char n).
; If t is of the form emptystr, return emptystr.
; Otherwise, this side condition fails
-(program sc_string_first_char_or_empty ((t term)) term
+(program sc_string_first_char_or_empty ((t term) (u sort)) term
(match t
((apply t1 t2)
(let t12 (getarg f_str.++ t1)
(match t12
((char n) t12))))
- (emptystr t)))
+ (default (ifequal t (sc_mk_emptystr u) t (fail term)))))
; Flatten constants in str.++ application s. Notice that the rewritten form
; of strings in cvc5 are such that constants are grouped into constants of
; It does not insist that the nested concatenations are over characters only.
; This rule may fail if s is not a str.++ application corresponding to a term
; in cvc5 rewritten form.
-(program sc_string_flatten ((s term)) term
+(program sc_string_flatten ((s term) (u sort)) term
(match s
((apply s1 s2)
(let s12 (getarg f_str.++ s1)
; Must handle nested concatenation for word constant. We know there is no nested concatenation within s12, so we don't need to flatten it.
; Since s12 may not be a concat term, we must use n-ary intro to ensure it is in n-ary form
- (sc_string_concat (sc_string_nary_intro s12) (sc_string_flatten s2))))
- (emptystr s))
+ (sc_string_concat (sc_string_nary_intro s12 u) (sc_string_flatten s2 u) u)))
+ (default (ifequal s (sc_mk_emptystr u) s (fail term))))
)
; Helper for collecting adjacent constants. This side condition takes as input
; (str.++ "A" (str.++ "B" (str.++ x "")))
; We return:
; (pair (str.++ "A" (str.++ "B" "")) (str.++ x ""))
-(program sc_string_collect_acc ((s term)) termPair
+(program sc_string_collect_acc ((s term) (u sort)) termPair
(match s
((apply s1 s2)
(match (getarg f_str.++ s1)
((char n)
- (match (sc_string_collect_acc s2)
+ (match (sc_string_collect_acc s2 u)
((pair ssc1 ssc2) (pair (apply s1 ssc1) ssc2))))
- (default (pair emptystr s))))
- (emptystr (pair emptystr s)))
+ (default (pair (sc_mk_emptystr u) s))))
+ (default (ifequal s (sc_mk_emptystr u) (pair s s) (fail termPair))))
)
; Collect adjacent constants for the prefix of string s. For example:
; This side condition may fail if s is not a str.++ application.
; Notice that the collection of constants is done for all word constants in the
; term s recursively.
-(program sc_string_collect ((s term)) term
- (match (sc_string_collect_acc s)
+(program sc_string_collect ((s term) (u sort)) term
+ (match (sc_string_collect_acc s u)
((pair sc1 sc2)
- (match sc1
+ (ifequal sc1 (sc_mk_emptystr u)
; did not strip a constant prefix
- (emptystr
- (match s
- ((apply s1 s2) (apply s1 (sc_string_collect s2)))
- (emptystr s)))
+ (match s
+ ((apply s1 s2) (apply s1 (sc_string_collect s2 u)))
+ (default (ifequal s (sc_mk_emptystr u) s (fail term))))
; stripped a constant prefix, must eliminate singleton
- (default (str.++ (sc_string_nary_elim sc1) (sc_string_collect sc2))))))
+ (str.++ (sc_string_nary_elim sc1 u) (sc_string_collect sc2 u)))))
)
; Strip equal prefix of s and t. This returns the pair corresponding to s and
; This method will return:
; (pair (str.++ y (str.++ z "")) (str.++ w ""))
; This side condition may fail if s or t is not a str.++ application.
-(program sc_strip_prefix ((s term) (t term)) termPair
+(program sc_strip_prefix ((s term) (t term) (u sort)) termPair
(match s
((apply s1 s2)
(let s12 (getarg f_str.++ s1)
((apply t1 t2)
(let t12 (getarg f_str.++ t1)
(ifequal s12 t12
- (sc_strip_prefix s2 t2)
+ (sc_strip_prefix s2 t2 u)
(pair s t))))
- (emptystr (pair s t)))))
- (emptystr (pair s t)))
+ (default (ifequal t (sc_mk_emptystr u) (pair s t) (fail termPair))))))
+ (default (ifequal s (sc_mk_emptystr u) (pair s t) (fail termPair))))
)
; Converts a str.++ application into "flat form" so that we are ready to
; (1) convert s to n-ary form if it is not already a str.++ application,
; (2) flatten so that its constant prefix,
; (3) (optionally) reverse.
-(program sc_string_to_flat_form ((s term) (rev flag)) term
+(program sc_string_to_flat_form ((s term) (rev flag) (u sort)) term
; intro, flatten, reverse
- (sc_string_rev (sc_string_flatten (sc_string_nary_intro s)) rev))
+ (sc_string_rev (sc_string_flatten (sc_string_nary_intro s u) u) rev u))
; Converts a term in "flat form" to a term that is in a form that corresponds
; to one in cvc5 rewritten form. This is the dual method to
; (1) (optionally) reverse,
; (2) collect constants
; (3) eliminate n-ary form to its element if the term is a singleton list.
-(program sc_string_from_flat_form ((s term) (rev flag)) term
+(program sc_string_from_flat_form ((s term) (rev flag) (u sort)) term
; reverse, collect, elim
- (sc_string_nary_elim (sc_string_collect (sc_string_rev s rev))))
+ (sc_string_nary_elim (sc_string_collect (sc_string_rev s rev u) u) u))
; depends: strings_programs.plf
-(declare string_length_non_empty (! s term (! p (holds (not (= s emptystr))) (holds (not (= (str.len s) (int 0)))))))
+(declare string_length_non_empty (! s term
+ (! t term
+ (! p (holds (not (= s t)))
+ (! r (^ (sc_string_is_empty t) tt)
+ (holds (not (= (str.len s) (int 0)))))))))
; Computes the conclusion of the PfRule::CONCAT_EQ rule
-(program sc_concat_eq ((s term) (t term) (rev flag)) term
+(program sc_concat_eq ((s term) (t term) (rev flag) (u sort)) term
(match (sc_strip_prefix
- (sc_string_to_flat_form s rev)
- (sc_string_to_flat_form t rev))
+ (sc_string_to_flat_form s rev u)
+ (sc_string_to_flat_form t rev u) u)
((pair ss ts)
(=
- (sc_string_from_flat_form ss rev)
- (sc_string_from_flat_form ts rev)))))
+ (sc_string_from_flat_form ss rev u)
+ (sc_string_from_flat_form ts rev u)))))
(declare concat_eq (! s term
(! t term
(! res term
(! rev flag
+ (! u sort
(! p (holds (= s t))
- (! r (^ (sc_concat_eq s t rev) res)
- (holds res))))))))
+ (! r (^ (sc_concat_eq s t rev u) res)
+ (holds res)))))))))
; Helper method for PfRule::CONCAT_UNIFY. Returns ok if s or a prefix of its
; head is equal to s1, where the (suffix of the) head of the reverse of s is
; checked if rev is tt. Fails otherwise.
-(program sc_concat_head_or_self ((s term) (s1 term) (rev flag)) Ok
+(program sc_concat_head_or_self ((s term) (s1 term) (rev flag) (u sort)) Ok
(ifequal s s1
ok
- (let sh (sc_string_head (sc_string_rev s rev))
+ (let sh (sc_string_head (sc_string_rev s rev u))
(ifequal sh s1
ok
; otherwise we may be splitting a constant, we reverse the characters in sh
(ifequal (sc_string_is_prefix
- (sc_string_rev (sc_string_nary_intro s1) rev)
- (sc_string_rev sh rev))
+ (sc_string_rev (sc_string_nary_intro s1 u) rev u)
+ (sc_string_rev sh rev u) u)
tt ok (fail Ok)))))
)
; Computes whether the heads of the premise (= s t) match s1 and t1 for the
; PfRule::CONCAT_UNIFY rule
-(program sc_concat_unify ((s term) (t term) (s1 term) (t1 term) (rev flag)) Ok
- (ifequal (sc_concat_head_or_self s s1 rev) ok
- (ifequal (sc_concat_head_or_self t t1 rev) ok
+(program sc_concat_unify ((s term) (t term) (s1 term) (t1 term) (rev flag) (u sort)) Ok
+ (ifequal (sc_concat_head_or_self s s1 rev u) ok
+ (ifequal (sc_concat_head_or_self t t1 rev u) ok
ok
(fail Ok))
(fail Ok)))
(! s1 term
(! t1 term
(! rev flag
+ (! u sort
(! p (holds (= s t))
(! p1 (holds (= (str.len s1) (str.len t1)))
- (! r (^ (sc_concat_unify s t s1 t1 rev) ok)
- (holds (= s1 t1)))))))))))
+ (! r (^ (sc_concat_unify s t s1 t1 rev u) ok)
+ (holds (= s1 t1))))))))))))
; Computes the conclusion of the PfRule::CONCAT_CSPLIT rule
-(program sc_concat_csplit ((thead term) (t term) (s term) (rev flag)) term
- (match (sc_string_to_flat_form t rev)
+(program sc_concat_csplit ((thead term) (t term) (s term) (rev flag) (u sort)) term
+ (match (sc_string_to_flat_form t rev u)
((apply t1 t2)
(ifequal (getarg f_str.++ t1) thead
- (match (sc_string_to_flat_form s rev)
+ (match (sc_string_to_flat_form s rev u)
((apply s1 s2)
(let s12 (getarg f_str.++ s1)
(match s12
(! s term
(! res term
(! rev flag
+ (! u sort
(! p1 (holds (= t s))
(! p2 (holds (not (= (str.len t1) (int 0))))
- (! r (^ (sc_concat_csplit t1 t s rev) res)
- (holds res))))))))))
+ (! r (^ (sc_concat_csplit t1 t s rev u) res)
+ (holds res)))))))))))
; Checks whether the conditions on the premise (= s t) is satisfied for the
; PfRule::CONCAT_CONFLICT rule
-(program sc_concat_conflict ((s term) (t term) (rev flag)) Ok
+(program sc_concat_conflict ((s term) (t term) (rev flag) (u sort)) Ok
(match (sc_strip_prefix
- (sc_string_to_flat_form s rev)
- (sc_string_to_flat_form t rev))
+ (sc_string_to_flat_form s rev u)
+ (sc_string_to_flat_form t rev u) u)
((pair ss ts)
(ifequal
- (sc_string_first_char_or_empty ss)
- (sc_string_first_char_or_empty ts)
+ (sc_string_first_char_or_empty ss u)
+ (sc_string_first_char_or_empty ts u)
(fail Ok)
ok))))
(declare concat_conflict (! s term
(! t term
(! rev flag
+ (! u sort
(! p (holds (= s t))
- (! r (^ (sc_concat_conflict s t rev) ok)
- (holds false)))))))
+ (! r (^ (sc_concat_conflict s t rev u) ok)
+ (holds false))))))))
-(declare string_length_pos (! t term
- (holds (or (and (= (str.len t) (int 0)) (and (= t emptystr) true)) (or (a.> (str.len t) (int 0)) false)))))
+(program sc_string_length_pos ((t term) (u sort)) term
+ (or (and (= (str.len t) (int 0)) (and (= t (sc_mk_emptystr u)) true)) (or (a.> (str.len t) (int 0)) false))
+)
+
+(declare string_length_pos (! t term
+ (! u sort
+ (! s term
+ (! r (^ (sc_string_length_pos t u) s)
+ (holds s))))))
(declare re_inter (! x term (! s term (! t term (! p1 (holds (str.in_re x s)) (! p2 (holds (str.in_re x t))
(holds (str.in_re x (re.inter s (re.inter t (re.* re.allchar)))))))))))
((pair p1 p2)
(or (= t emptystr)
(or (str.in_re t r2)
- (or (and (sc_string_nary_elim (and (= t p1) p2)) (sc_non_empty_concats p1))
+ (or (and (sc_string_nary_elim (and (= t p1) p2) String) (sc_non_empty_concats p1 String))
false)))))))
((apply r11 r12)
(match r11
; case for concatenation
(f_re.++
(match (sc_re_unfold_pos_concat t r r 0)
- ((pair p1 p2) (sc_string_nary_elim (and (= t p1) p2)))))
+ ((pair p1 p2) (sc_string_nary_elim (and (= t p1) p2) String))))
))))))
(declare re_unfold_pos (! t term (! r term (! s term (! f (holds (str.in_re t r)) (! u (^ (sc_re_unfold_pos t r) s) (holds s)))))))
projects / cvc5.git / commitdiff