From 53e7bc8d02c57b02d4dbd793f2f3ccddae77e638 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 3 Mar 2022 09:59:04 -0600 Subject: [PATCH] Generalize LFSC string signature to sequences (#8220) --- proofs/lfsc/signatures/strings_programs.plf | 128 +++++++++++--------- proofs/lfsc/signatures/strings_rules.plf | 81 ++++++++----- src/proof/lfsc/lfsc_printer.cpp | 23 ++-- 3 files changed, 132 insertions(+), 100 deletions(-) diff --git a/proofs/lfsc/signatures/strings_programs.plf b/proofs/lfsc/signatures/strings_programs.plf index 8614f9536..384343052 100644 --- a/proofs/lfsc/signatures/strings_programs.plf +++ b/proofs/lfsc/signatures/strings_programs.plf @@ -1,11 +1,21 @@ ; 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) @@ -30,32 +40,33 @@ (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)) @@ -67,7 +78,7 @@ (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)) @@ -75,12 +86,12 @@ (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)) @@ -92,20 +103,20 @@ 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 @@ -114,8 +125,8 @@ ; 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 @@ -132,20 +143,20 @@ ; 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))) )) ) @@ -175,14 +186,14 @@ ) ; 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))))))))) @@ -216,23 +227,23 @@ ; (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 @@ -257,14 +268,14 @@ ; 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 @@ -275,15 +286,15 @@ ; (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: @@ -293,17 +304,16 @@ ; 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 @@ -313,7 +323,7 @@ ; 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) @@ -321,10 +331,10 @@ ((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 @@ -332,9 +342,9 @@ ; (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 @@ -342,6 +352,6 @@ ; (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)) diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf index 5d4f5ad3d..4e2762321 100644 --- a/proofs/lfsc/signatures/strings_rules.plf +++ b/proofs/lfsc/signatures/strings_rules.plf @@ -1,46 +1,51 @@ ; 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))) @@ -50,17 +55,18 @@ (! 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 @@ -78,33 +84,42 @@ (! 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))))))))))) @@ -127,14 +142,14 @@ ((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))))))) diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp index 8c659dc0c..3018d3b6b 100644 --- a/src/proof/lfsc/lfsc_printer.cpp +++ b/src/proof/lfsc/lfsc_printer.cpp @@ -576,22 +576,29 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn, Assert(res[1].getKind() == CONST_RATIONAL); pf << h << h << d_tproc.convert(res[1]) << cs[0]; } - break; // strings - case PfRule::STRING_LENGTH_POS: pf << as[0]; break; - case PfRule::STRING_LENGTH_NON_EMPTY: pf << h << cs[0]; break; + break;case PfRule::STRING_LENGTH_POS: + pf << as[0] << d_tproc.convertType(as[0].getType()) << h; + break; + case PfRule::STRING_LENGTH_NON_EMPTY: pf << h << h << cs[0]; break; case PfRule::RE_INTER: pf << h << h << h << cs[0] << cs[1]; break; case PfRule::CONCAT_EQ: - pf << h << h << h << args[0].getConst() << cs[0]; + pf << h << h << h << args[0].getConst() + << d_tproc.convertType(children[0]->getResult()[0].getType()) << cs[0]; break; case PfRule::CONCAT_UNIFY: - pf << h << h << h << h << args[0].getConst() << cs[0] << cs[1]; + pf << h << h << h << h << args[0].getConst() + << d_tproc.convertType(children[0]->getResult()[0].getType()) << cs[0] + << cs[1]; break; case PfRule::CONCAT_CSPLIT: - pf << h << h << h << h << args[0].getConst() << cs[0] << cs[1]; + pf << h << h << h << h << args[0].getConst() + << d_tproc.convertType(children[0]->getResult()[0].getType()) << cs[0] + << cs[1]; break; case PfRule::CONCAT_CONFLICT: - pf << h << h << args[0].getConst() << cs[0]; + pf << h << h << args[0].getConst() + << d_tproc.convertType(children[0]->getResult()[0].getType()) << cs[0]; break; case PfRule::RE_UNFOLD_POS: if (children[0]->getResult()[1].getKind() != REGEXP_CONCAT) @@ -619,7 +626,7 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn, Kind k = as[0].getKind(); if (k == STRING_SUBSTR || k == STRING_INDEXOF) { - pf << h << as[0] << as[0][0].getType(); + pf << h << as[0] << d_tproc.convertType(as[0][0].getType()); } else { -- 2.30.2