From bf53297376f6de23a594f97006d93108e4b712a5 Mon Sep 17 00:00:00 2001
From: Vinicius Gomes <vinicius.svgomes@gmail.com>
Date: Thu, 18 Jan 2024 20:52:00 -0300
Subject: [PATCH] fix: adds support for 2+ arguments in the str.++ operator

---
 carcara/src/checker/rules/strings.rs | 36 +++++++++++++++++++---------
 1 file changed, 25 insertions(+), 11 deletions(-)

diff --git a/carcara/src/checker/rules/strings.rs b/carcara/src/checker/rules/strings.rs
index 5dd7f6c4..dc91c560 100644
--- a/carcara/src/checker/rules/strings.rs
+++ b/carcara/src/checker/rules/strings.rs
@@ -6,7 +6,7 @@ use super::{
 };
 use crate::ast::*;
 
-fn flatten(mut term: Rc<Term>, pool: &mut dyn TermPool) -> Vec<Rc<Term>> {
+fn flatten(term: Rc<Term>, pool: &mut dyn TermPool) -> Vec<Rc<Term>> {
     let mut flattened = Vec::new();
     if let Term::Const(Constant::String(s)) = term.as_ref() {
         flattened.extend(
@@ -14,18 +14,26 @@ fn flatten(mut term: Rc<Term>, pool: &mut dyn TermPool) -> Vec<Rc<Term>> {
                 .map(|c| pool.add(Term::Const(Constant::String(c.to_string())))),
         );
     } else {
-        while let Some((head, tail)) = match_term!((strconcat head tail) = term) {
-            if let Term::Const(Constant::String(s)) = head.as_ref() {
-                flattened.extend(
-                    s.chars()
-                        .map(|c| pool.add(Term::Const(Constant::String(c.to_string())))),
-                );
-            } else {
-                flattened.push(head.clone());
+        if let Some(args) = match_term!((strconcat ...) = term) {
+            for arg in args {
+                match arg.as_ref() {
+                    Term::Const(Constant::String(s)) => {
+                        flattened.extend(
+                            s.chars()
+                                .map(|c| pool.add(Term::Const(Constant::String(c.to_string())))),
+                        );
+                    }
+                    Term::Op(Operator::StrConcat, _) => {
+                        flattened.extend(flatten(arg.clone(), pool));
+                    }
+                    _ => {
+                        flattened.push(arg.clone());
+                    }
+                };
             }
-            term = tail.clone();
+        } else {
+            flattened.push(term.clone());
         }
-        flattened.push(term.clone());
     }
     flattened
 }
@@ -114,6 +122,12 @@ mod tests {
                 r#"(assume h1 (= (str.++ a (str.from_int (str.len b))) (str.++ "0" (str.++ "A" c))))
                    (step t1 (cl (= (str.++ a (str.from_int (str.len b))) (str.++ "0" (str.++ "A" c)))) :rule concat_eq :premises (h1) :args (false))"#: true,
             }
+            "Concatenation with more than 2 arguments" {
+                r#"(assume h1 (= "xyzw" (str.++ "xy" "z" a)))
+                   (step t1 (cl (= "w" a)) :rule concat_eq :premises (h1) :args (false))"#: true,
+                r#"(assume h1 (= "xyzw" (str.++ "x" (str.++ "y" "z") a)))
+                   (step t1 (cl (= "w" a)) :rule concat_eq :premises (h1) :args (false))"#: true,
+            }
         }
     }
 }