fn reconstruct_uninterpreted_funcs()

in amzn-smt-ir/src/ackerman.rs [62:135]

• 71 lines of code
• 4 McCabe index (conditional complexity)

    fn reconstruct_uninterpreted_funcs(
        uf_vars: HashMap<UF<Term<U>>, MappedApplication<U>>,
        arg_vars: HashMap<Term<U>, IVar<QualIdentifier>>,
        model: Model<U>,
    ) -> Model<U> {
        let substs: Vec<_> = (model.defns())
            .map(|defn| {
                debug_assert!(
                    defn.args.is_empty(),
                    "Ackermanization eliminates uninterpreted functions"
                );
                (defn.sym.clone(), defn.body.clone())
            })
            .collect();

        let mut uf_vars: HashMap<_, _> = uf_vars
            .into_iter()
            .map(|(t, data)| {
                (
                    data.corresponding_var.sym().clone(),
                    (data.arg_sorts, data.sort, t),
                )
            })
            .collect();
        let arg_vars: HashMap<_, _> = arg_vars.iter().map(|(t, v)| (v.sym(), t)).collect();
        let mut uf_piecewise_defns: HashMap<_, HashMap<_, _>> = HashMap::new();
        let mut defns = vec![];

        for defn in model.into_defns() {
            if let Some((arg_sorts, sort, uf)) = uf_vars.remove(&defn.sym) {
                let outputs = uf_piecewise_defns
                    .entry((uf.func, arg_sorts, sort))
                    .or_default();
                let args: Vec<_> = (Vec::from(uf.args).into_iter())
                    .map(|t| t.substitute(&substs))
                    .collect();
                let body = defn.body.substitute(&substs);
                outputs.insert(args, body);
            } else if !arg_vars.contains_key(&defn.sym) {
                defns.push(defn);
            }
        }

        let params = (0..)
            .map(|x| format!("x!{}", x))
            .map(|x| ISymbol::from(Symbol(x)));
        let uf_defns = uf_piecewise_defns
            .into_iter()
            .map(|((sym, arg_sorts, sort), outputs)| {
                let mut outputs = outputs.into_iter();
                let first = outputs.next().unwrap().1;
                let body = outputs.fold(first, |e, (args, out)| {
                    let args_match = CoreOp::And(
                        (params.clone().zip(args))
                            .map(|(param, arg)| {
                                Term::from(CoreOp::Eq(args![
                                    IVar::from(QualIdentifier::from(param)).into(),
                                    arg,
                                ]))
                            })
                            .collect(),
                    )
                    .into();
                    CoreOp::Ite(args_match, out, e).into()
                });
                DefineFun {
                    sym,
                    args: params.clone().zip(arg_sorts).collect(),
                    sort,
                    body: body.substitute(&substs),
                }
            });
        defns.into_iter().chain(uf_defns).collect()
    }