egraphs-good / egg

egg is a flexible, high-performance e-graph library
https://egraphs-good.github.io
MIT License
1.37k stars 137 forks source link

Syntax for passing multiple arguments to condition #272

Closed aditink closed 1 year ago

aditink commented 1 year ago

I am trying to write a conditional rule where the condition requires multiple arguments. The rule (for a smtlib-like language) is

            rewrite!("cell-collapse"; "(or (and ?a ?b) (?c ?d))" => "(and (or ?a ?c) ?b)"
                if cell_collapse_guard("?b", "?c", "?d")),

where cell_collapse_guard returns true if (?b and ?c) -> (?d).

 fn cell_collapse_guard(common: &'static str, cond: &'static str, predicate: &'static str) -> impl Fn(&mut EGraph<PropLang, ()>, Id, &Subst) -> bool {
            let var_common: Var = common.parse().unwrap();
            let var_cond: Var = cond.parse().unwrap();
            let var_predicate: Var = predicate.parse().unwrap();
            move |egraph, _, subst| {
                let common = subst[var_common];
                let cond = subst[var_cond];
                let predicate = subst[var_predicate];
                let extractor = Extractor::new(&egraph, AstSize);
                let common_fml = extractor.find_best(common).1.to_string();
                let cond_fml = extractor.find_best(cond).1.to_string();
                let predicate_fml = extractor.find_best(predicate).1.to_string();
                // Use z3 to return true if the first argument implies the second argument.
                z3utils::imply(format!("(and {} {})", common_fml, cond_fml), predicate_fml)
            }
        }

However, I get the error 'main' panicked at 'calledResult::unwrap()on anErrvalue: BadOp(UnexpectedVar("?c"))'. What is the correct way to pass multiple arguments to cell_collapse_guard? Sorry if I missed this in the documentation!

aditink commented 1 year ago

Nevermind, I realize now that the problem was in my rule, which was missing an and, and should have been

            rewrite!("cell-collapse"; "(or (and ?a ?b) (and ?c ?d))" => "(and (or ?a ?c) ?b)"
                if cell_collapse_guard("?b", "?c", "?d"))

Thanks!