fix: adds support for 2+ arguments in the str.++ operator

ufmg-smite · Jan 18, 2024 · bf53297 · bf53297
1 parent 935b1fd
commit bf53297
Showing 1 changed file with 25 additions and 11 deletions.
diff --git a/carcara/src/checker/rules/strings.rs b/carcara/src/checker/rules/strings.rs
@@ -6,26 +6,34 @@ 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(
             s.chars()
                 .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,
+            }
         }
     }
 }