fn fold_assert()

in amzn-smt-string-transformer/src/subformula_parser.rs [67:99]


    fn fold_assert(&mut self, term: Term) -> Result<Command, Self::Error> {
        let mut term_to_ret = term.clone();
        let mut useless_command = false;
        // this happens before iterating into the symbols
        if self.remap_string_vars {
            match term {
                Term::CoreOp(op) => {
                    if let CoreOp::Eq(args) = op.as_ref() {
                        if let [Term::Variable(v), f @ (Term::CoreOp(..) | Term::OtherOp(..) | Term::UF(..))] =
                            args.as_slice()
                        {
                            if v.sym_str().starts_with("new_var") {
                                self.string_fct_calls.insert(v.sym().clone(), f.clone());
                                useless_command = true;
                            }
                        }
                    }
                }
                Term::Variable(v) => {
                    if let Some(new_var_sym_term) = self.string_fct_calls.get(v.sym()) {
                        term_to_ret = new_var_sym_term.clone();
                    }
                }
                _ => {}
            }
        }
        let output = term_to_ret.fold_with(self)?;
        let output = Command::Assert { term: output };
        if useless_command {
            self.remap_useless_commands.insert(output.clone());
        }
        Ok(output)
    }