fn process_string_fct()

in amzn-smt-string-transformer/src/transpiler_visitors.rs [114:163]

• 42 lines of code
• 8 McCabe index (conditional complexity)

    fn process_string_fct(&mut self, sfc: StringFct, t: &Term) -> Option<ISymbol> {
        let mut string_const_args = BTreeSet::<String>::new();
        // build up all the string constant args, and use this to check for non-string equality
        let mut non_string_arguments = false;
        if let Some(op) = t.op() {
            for arg in op.args() {
                if let Term::Constant(c) = arg {
                    if let Constant::String(s) = c.as_ref() {
                        string_const_args.insert(s.to_string());
                        continue;
                    }
                } else if let Term::Variable(v) = arg {
                    non_string_arguments |= !self.string_var_list.contains(v.sym());
                    continue;
                }
                non_string_arguments = true;
            }
        }
        if non_string_arguments && sfc == StringFct::StrEquality {
            // if it's equality, it might not be over strings
            // only proceed if all args are strings or some of our created string vars
            return None;
        }

        // add new_var to the list of new vars, storing this string function
        let len = self.const_map.len();
        let var_sym = match self.const_map.entry(t.clone()) {
            Entry::Occupied(o) => o.get().clone(),
            Entry::Vacant(v) => {
                let new_var_type = sfc.string_fct_return_type();
                let new_var_name = ISymbol::from(format!("new_var{}", len));
                self.decl_const_list
                    .push(Self::new_var_decl_const(new_var_name.clone(), new_var_type));
                self.string_var_defn_map
                    .insert(new_var_name.clone(), t.clone());
                self.assert_list
                    .push(new_assert_equal(new_var_name.clone(), t));
                self.string_var_list.insert(new_var_name.clone());
                v.insert(new_var_name.clone());
                new_var_name
            }
        };
        self.callgraph
            .add_call(var_sym.clone(), CallnodeData::new(sfc, string_const_args));
        // inspect the term parameters (if any), and map any string var params
        // to the current string var (add parent/child to the callgraph)
        self.inspect_parameters(var_sym.clone(), t, sfc);

        Some(var_sym)
    }