From 07d48fa7d8aebdeae5dcfae855a9a48d805a231c Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 28 Feb 2019 06:45:39 -0800 Subject: [PATCH] [sledge] Make simplification subexp check more precise Summary: Exp simplification must not generate fresh subexpressions in its output that do not appear in its input, lest congruence closure gets confused. Previously this check only considered immediate subexpressions, which is overly restrictive. Reviewed By: ngorogiannis Differential Revision: D14251653 fbshipit-source-id: f8d5d9756 --- sledge/src/llair/exp.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index f13d518e7..3d8f9796d 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -618,6 +618,8 @@ let fold_exps e ~init ~f = in fix fold_exps_ (fun _ z -> z) e init +let iter_exps e ~f = fold_exps e ~init:() ~f:(fun () e -> f e) + let fold_vars e ~init ~f = fold_exps e ~init ~f:(fun z -> function | Var _ as v -> f z (v :> Var.t) | _ -> z ) @@ -1047,6 +1049,12 @@ let fold e ~init:s ~f = let for_all e ~f = fold ~f:(fun a so_far -> so_far && f a) ~init:true e let exists e ~f = fold ~f:(fun a found -> found || f a) ~init:false e +let is_subexp ~sub ~sup = + With_return.with_return + @@ fun {return} -> + iter_exps sup ~f:(fun e -> if equal sub e then return true) ; + false + let app1 ?(partial = false) op arg = ( match (op, arg) with | App {op= Eq; arg= x}, y -> simp_eq x y @@ -1081,9 +1089,10 @@ let app1 ?(partial = false) op arg = | App {op= Eq | Dq} -> () | _ -> iter e ~f:(function + | App {op= Eq | Dq} -> () | App _ as a -> assert ( - equal a op || equal a arg + is_subexp ~sub:a ~sup:op || is_subexp ~sub:a ~sup:arg || Trace.fail "simplifying %a %a@ yields %a@ with new subexp %a" pp op pp arg pp e pp a )