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)
}