Normalize rare lists for unary operations in rewrite engine

carcara/src/rare/mod.rs

@@ -1,17 +1,25 @@
-use indexmap::IndexMap;
+use indexmap::{IndexMap, IndexSet};
 
 use crate::{
-    ast::{rare_rules::RewriteTerm, Rc, Term, TermPool},
+    ast::{rare_rules::RewriteTerm, Operator, Rc, Term, TermPool},
     build_equation, pseudo_term,
 };
 
+#[derive(Debug, Default)]
+struct RewriteContext {
+    cache: IndexMap<Rc<Term>, Rc<Term>>,
+    in_progress: IndexSet<Rc<Term>>,
+}
+
 pub fn get_rules() -> Vec<(RewriteTerm, RewriteTerm)> {
     vec![
         build_equation!((RareList ..x..) ~> x),
+        build_equation!((And (RareList ..x..)) ~> (And x)),
+        build_equation!((Or (RareList ..x..)) ~> (Or x)),
+        build_equation!((And x) ~> x),
+        build_equation!((Or x) ~> x),
         build_equation!((Or true) ~> true),
-        build_equation!((Or) ~> true),
-        build_equation!((And) ~> false),
-        build_equation!((And false) ~> false),
+        build_equation!((And false) ~> false)
     ]
 }
 
@@ -81,8 +89,9 @@ fn reconstruct_meta_terms<'a>(
             let mut args = vec![];
             for param in params {
                 let k = reconstruct_meta_terms(pool, param, traces);
-                if let Trace::Term(term) = k {
-                    args.push(term.clone());
+                match k {
+                    Trace::Term(term) => args.push(term.clone()),
+                    Trace::ManyTerm(terms) => args.extend(terms.iter().cloned()),
                 }
             }
             Trace::Term(pool.add(Term::Op(*op, args)))
@@ -113,114 +122,153 @@ fn check_rewrites(
     None
 }
 
-pub fn rewrite_meta_terms(
+fn rewrite_arg_for_parent(
+    pool: &mut dyn TermPool,
+    arg: &Rc<Term>,
+    rules: &[(RewriteTerm, RewriteTerm)],
+    ctx: &mut RewriteContext,
+) -> Vec<Rc<Term>> {
+    if let Some(trace) = check_rewrites(pool, arg, rules) {
+        match trace {
+            Trace::Term(t) => {
+                if t == *arg {
+                    vec![t]
+                } else {
+                    vec![rewrite_meta_terms_inner(pool, t, rules, ctx)]
+                }
+            }
+            Trace::ManyTerm(subs) => match arg.as_ref() {
+                Term::Op(Operator::RareList, _) => subs,
+                _ => vec![arg.clone()],
+            },
+        }
+    } else {
+        vec![rewrite_meta_terms_inner(pool, arg.clone(), rules, ctx)]
+    }
+}
+
+fn rewrite_arguments(
+    pool: &mut dyn TermPool,
+    args: &[Rc<Term>],
+    rules: &[(RewriteTerm, RewriteTerm)],
+    ctx: &mut RewriteContext,
+) -> Vec<Rc<Term>> {
+    let mut flattened = Vec::new();
+    for arg in args {
+        flattened.extend(rewrite_arg_for_parent(pool, arg, rules, ctx));
+    }
+
+    let mut normalized = Vec::with_capacity(flattened.len());
+    for arg in flattened {
+        let rewritten = rewrite_meta_terms_inner(pool, arg.clone(), rules, ctx);
+        if rewritten == arg {
+            normalized.push(arg);
+        } else {
+            normalized.push(rewritten);
+        }
+    }
+    normalized
+}
+
+fn rewrite_meta_terms_inner(
     pool: &mut dyn TermPool,
     term: Rc<Term>,
     rules: &[(RewriteTerm, RewriteTerm)],
+    ctx: &mut RewriteContext,
 ) -> Rc<Term> {
-    match term.as_ref() {
+    if let Some(cached) = ctx.cache.get(&term) {
+        return cached.clone();
+    }
+    if !ctx.in_progress.insert(term.clone()) {
+        return term;
+    }
+
+    let result = match term.as_ref() {
         Term::Var(_, _) => term.clone(),
         Term::Const(_) => term.clone(),
         Term::Sort(_) => term.clone(),
 
         Term::App(f, args) => {
-            let f_prime = rewrite_meta_terms(pool, f.clone(), rules);
-            let new_args = args
-                .iter()
-                .flat_map(|arg| {
-                    if let Some(trace) = check_rewrites(pool, arg, rules) {
-                        match trace {
-                            Trace::Term(t) => vec![t],
-                            Trace::ManyTerm(subs) => subs,
-                        }
-                    } else {
-                        vec![rewrite_meta_terms(pool, arg.clone(), rules)]
-                    }
-                })
-                .collect::<Vec<_>>();
+            let f_prime = rewrite_meta_terms_inner(pool, f.clone(), rules, ctx);
+            let new_args = rewrite_arguments(pool, args, rules, ctx);
             let new_term = pool.add(Term::App(f_prime, new_args));
             if new_term != term {
-                return rewrite_meta_terms(pool, new_term, rules);
+                rewrite_meta_terms_inner(pool, new_term, rules, ctx)
+            } else {
+                new_term
             }
-
-            new_term
         }
 
         Term::Op(op, args) => {
             if let Some(trace) = check_rewrites(pool, &term, rules) {
                 match trace {
-                    Trace::Term(t) => t,
+                    Trace::Term(t) => {
+                        if t == term {
+                            t
+                        } else {
+                            rewrite_meta_terms_inner(pool, t, rules, ctx)
+                        }
+                    }
                     Trace::ManyTerm(_) => {
-                        let new_args = args
-                            .iter()
-                            .flat_map(|arg| {
-                                if let Some(trace) = check_rewrites(pool, arg, rules) {
-                                    match trace {
-                                        Trace::Term(t) => vec![t],
-                                        Trace::ManyTerm(subs) => subs,
-                                    }
-                                } else {
-                                    vec![rewrite_meta_terms(pool, arg.clone(), rules)]
-                                }
-                            })
-                            .collect::<Vec<_>>();
+                        let new_args = rewrite_arguments(pool, args, rules, ctx);
                         let new_term: Rc<Term> = pool.add(Term::Op(*op, new_args));
                         if new_term != term {
-                            return rewrite_meta_terms(pool, new_term, rules);
+                            rewrite_meta_terms_inner(pool, new_term, rules, ctx)
+                        } else {
+                            new_term
                         }
-
-                        new_term
                     }
                 }
             } else {
-                let new_args = args
-                    .iter()
-                    .flat_map(|arg| {
-                        if let Some(trace) = check_rewrites(pool, arg, rules) {
-                            match trace {
-                                Trace::Term(t) => vec![t],
-                                Trace::ManyTerm(subs) => subs,
-                            }
-                        } else {
-                            vec![rewrite_meta_terms(pool, arg.clone(), rules)]
-                        }
-                    })
-                    .collect::<Vec<_>>();
+                let new_args = rewrite_arguments(pool, args, rules, ctx);
                 let new_term = pool.add(Term::Op(*op, new_args));
                 if check_rewrites(pool, &new_term, rules).is_some() {
-                    return rewrite_meta_terms(pool, new_term, rules);
+                    rewrite_meta_terms_inner(pool, new_term, rules, ctx)
+                } else {
+                    new_term
                 }
-
-                new_term
             }
         }
 
         Term::Binder(binder, bindings, body) => {
-            let new_body = rewrite_meta_terms(pool, body.clone(), rules);
+            let new_body = rewrite_meta_terms_inner(pool, body.clone(), rules, ctx);
             pool.add(Term::Binder(*binder, bindings.clone(), new_body))
         }
 
         Term::Let(bindings, body) => {
-            let new_body = rewrite_meta_terms(pool, body.clone(), rules);
+            let new_body = rewrite_meta_terms_inner(pool, body.clone(), rules, ctx);
             pool.add(Term::Let(bindings.clone(), new_body))
         }
 
         Term::ParamOp { op, op_args, args } => {
             let new_op_args = op_args
                 .iter()
-                .map(|op_arg| rewrite_meta_terms(pool, op_arg.clone(), rules))
+                .map(|op_arg| rewrite_meta_terms_inner(pool, op_arg.clone(), rules, ctx))
                 .collect::<Vec<_>>();
             let new_args = args
                 .iter()
-                .map(|arg| rewrite_meta_terms(pool, arg.clone(), rules))
+                .map(|arg| rewrite_meta_terms_inner(pool, arg.clone(), rules, ctx))
                 .collect::<Vec<_>>();
             pool.add(Term::ParamOp {
                 op: *op,
                 op_args: new_op_args,
                 args: new_args,
             })
         }
-    }
+    };
+
+    ctx.in_progress.shift_remove(&term);
+    ctx.cache.insert(term, result.clone());
+    result
+}
+
+pub fn rewrite_meta_terms(
+    pool: &mut dyn TermPool,
+    term: Rc<Term>,
+    rules: &[(RewriteTerm, RewriteTerm)],
+) -> Rc<Term> {
+    let mut ctx = RewriteContext::default();
+    rewrite_meta_terms_inner(pool, term, rules, &mut ctx)
 }
 
 #[cfg(test)]

carcara/tests/rules/rare.rs

@@ -46,6 +46,30 @@ const RARE_RULES: &str = r#"
     :conclusion (= (=> x y) (or (not x) y)))
 "#;
 
+const SMALL_RARE_RULES: &str = r#"
+(declare-rare-rule bool-and-de-morgan ((x1 Bool) (y1 Bool))
+  :args (x1 y1)
+  :conclusion (= (not (and x1 y1)) (or (not x1) (not y1)))
+)
+"#;
+
+const DD_CHECK_CC_BVXOR_XSIMP_SMT2: &str = r#"
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const _x (_ BitVec 1))
+(declare-const s (_ BitVec 64))
+(declare-const t (_ BitVec 64))
+(assert (distinct (= (bvxor s t) (bvand (bvxor s t) ((_ zero_extend 63) _x))) (exists ((x (_ BitVec 64))) (and (= t (bvxor x s)) (= x (bvand x ((_ zero_extend 63) _x)))))))
+(check-sat)
+"#;
+
+const DD_CHECK_CC_BVXOR_XSIMP_ALETHE: &str = r#"
+(anchor :step t38 :args ((x (_ BitVec 64)) (:= (x (_ BitVec 64)) x)))
+(step t38.t0 (cl (= (not (and (= t (bvxor s x)) (= x (concat (_ bv0 63) (bvand _x ((_ extract 0 0) x)))))) (or (not (= t (bvxor s x))) (not (= x (concat (_ bv0 63) (bvand _x ((_ extract 0 0) x)))))))) :rule rare_rewrite :args ("bool-and-de-morgan" (= t (bvxor s x)) (= x (concat (_ bv0 63) (bvand _x ((_ extract 0 0) x))))))
+(step t38 (cl (= (forall ((x (_ BitVec 64))) (not (and (= t (bvxor s x)) (= x (concat (_ bv0 63) (bvand _x ((_ extract 0 0) x))))))) (forall ((x (_ BitVec 64))) (or (not (= t (bvxor s x))) (not (= x (concat (_ bv0 63) (bvand _x ((_ extract 0 0) x))))))))) :rule bind)
+(step t73 (cl) :rule hole)
+"#;
+
 fn run_rare_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) {
     for (i, (proof, expected)) in cases.iter().enumerate() {
         let (mut problem, mut proof, rare_rules, mut pool) = parser::parse_instance(
@@ -111,6 +135,40 @@ fn run_rare_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) {
     }
 }
 
+fn run_rare_file_test(
+    test_name: &str,
+    problem: &str,
+    proof: &str,
+    rare_rules: &str,
+    expected_holey: bool,
+) {
+    let (problem, proof, rare_rules, mut pool) = parser::parse_instance(
+        Cursor::new(problem),
+        Cursor::new(proof),
+        Some(Cursor::new(rare_rules)),
+        parser::Config {
+            apply_function_defs: true,
+            expand_lets: true,
+            allow_int_real_subtyping: true,
+            parse_hole_args: true,
+            ..Default::default()
+        },
+    )
+    .unwrap_or_else(|e| panic!("parser error during test \"{}\": {}", test_name, e));
+
+    let mut checker = checker::ProofChecker::new(&mut pool, &rare_rules, checker::Config::new());
+    let check_result = checker.check(&problem, &proof);
+
+    match check_result {
+        Ok(is_holey) => assert_eq!(
+            is_holey, expected_holey,
+            "test '{}' expected holey={} but got holey={}",
+            test_name, expected_holey, is_holey
+        ),
+        Err(e) => panic!("checker error during test \"{}\": {}", test_name, e),
+    }
+}
+
 macro_rules! rare_test_cases {
     (
         definitions = $defs:expr,
@@ -168,3 +226,14 @@ fn rare_rewrite() {
         }
     }
 }
+
+#[test]
+fn encoded_rare_examples() {
+    run_rare_file_test(
+        "dd_check_cc_bvxor_xsimp",
+        DD_CHECK_CC_BVXOR_XSIMP_SMT2,
+        DD_CHECK_CC_BVXOR_XSIMP_ALETHE,
+        SMALL_RARE_RULES,
+        true,
+    );
+}

rare-tests/rare/dd_check_cc_bvxor_xsimp.smt2

@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const _x (_ BitVec 1))
+(declare-const s (_ BitVec 64))
+(declare-const t (_ BitVec 64))
+(assert (distinct (= (bvxor s t) (bvand (bvxor s t) ((_ zero_extend 63) _x))) (exists ((x (_ BitVec 64))) (and (= t (bvxor x s)) (= x (bvand x ((_ zero_extend 63) _x)))))))
+(check-sat)

rare-tests/rare/dd_check_cc_bvxor_xsimp.smt2.alethe

@@ -0,0 +1,4 @@
+(anchor :step t38 :args ((x (_ BitVec 64)) (:= (x (_ BitVec 64)) x)))
+(step t38.t0 (cl (= (not (and (= t (bvxor s x)) (= x (concat (_ bv0 63) (bvand _x ((_ extract 0 0) x)))))) (or (not (= t (bvxor s x))) (not (= x (concat (_ bv0 63) (bvand _x ((_ extract 0 0) x)))))))) :rule rare_rewrite :args ("bool-and-de-morgan" (= t (bvxor s x)) (= x (concat (_ bv0 63) (bvand _x ((_ extract 0 0) x))))))
+(step t38 (cl (= (forall ((x (_ BitVec 64))) (not (and (= t (bvxor s x)) (= x (concat (_ bv0 63) (bvand _x ((_ extract 0 0) x))))))) (forall ((x (_ BitVec 64))) (or (not (= t (bvxor s x))) (not (= x (concat (_ bv0 63) (bvand _x ((_ extract 0 0) x))))))))) :rule bind)
+(step t73 (cl) :rule hole)

rare-tests/rare/small.rare

@@ -0,0 +1,4 @@
+(declare-rare-rule bool-and-de-morgan ((x1 Bool) (y1 Bool))
+  :args (x1 y1)
+  :conclusion (= (not (and x1 y1)) (or (not x1) (not y1)))
+)