more agressive simplifications in Eliminate_algebraic

src/core/pattern.ml

@@ -145,7 +145,7 @@ end
 module CompileTerm  = Compile (struct
   type action = term
   type branch = term_branch
-  let mk_let v s t  = t_let_close v s t
+  let mk_let v s t  = t_let_close_simp v s t
   let mk_branch p t = t_close_branch p t
   let mk_case t bl  = t_case t bl
 end)
@@ -153,7 +153,7 @@ end)
 module CompileFmla  = Compile (struct
   type action = fmla
   type branch = fmla_branch
-  let mk_let v t f  = f_let_close v t f
+  let mk_let v t f  = f_let_close_simp v t f
   let mk_branch p f = f_close_branch p f
   let mk_case t bl  = f_case t bl
 end)

src/core/term.ml

@@ -1855,20 +1855,34 @@ let f_if_simp f1 f2 f3 = match f1.f_node, f2.f_node, f3.f_node with
   | _, _, Ffalse -> f_and_simp f1 f2
   | _, _, _      -> if f_equal f2 f3 then f2 else f_if f1 f2 f3
 
-let f_let_simp t ((_,_,f) as bf) = match f.f_node with
-  | Ftrue | Ffalse -> f | _ -> f_let t bf
-
-let f_let_close_simp v t f = match f.f_node with
-  | Ftrue | Ffalse -> f | _ -> f_let_close v t f
-
-let f_quant_simp q ((_,_,_,f) as qf) = match f.f_node with
-  | Ftrue | Ffalse -> f | _ -> f_quant q qf
+let t_let_simp e ((v,_,t) as bt) = match e.t_node with
+  | _ when not (Svs.mem v t.t_vars) -> t
+  | Tvar _ -> t_subst_single v e t
+  | _ -> t_let e bt
+
+let f_let_simp e ((v,_,f) as bf) = match e.t_node with
+  | _ when not (Svs.mem v f.f_vars) -> f
+  | Tvar _ -> f_subst_single v e f
+  | _ -> f_let e bf
+
+let t_let_close_simp v e t = t_let_simp e (t_close_bound v t)
+let f_let_close_simp v e f = f_let_simp e (f_close_bound v f)
+
+let f_quant_simp q ((vl,_,tl,f) as qf) =
+  if List.for_all (fun v -> Svs.mem v f.f_vars) vl then
+    f_quant q qf
+  else
+    let vl = List.filter (fun v -> Svs.mem v f.f_vars) vl in
+    let e_vars = e_apply (fun t -> t.t_vars) (fun f -> f.f_vars) in
+    let tl = List.filter
+      (List.for_all (fun e -> Svs.subset (e_vars e) f.f_vars)) tl
+    in
+    f_quant_close q vl tl f
 
 let f_forall_simp = f_quant_simp Fforall
 let f_exists_simp = f_quant_simp Fexists
 
-let f_quant_close_simp q vl tl f = match f.f_node with
-  | Ftrue | Ffalse -> f | _ -> f_quant_close q vl tl f
+let f_quant_close_simp q vl tl f = f_quant_simp q (f_close_quant vl tl f)
 
 let f_forall_close_simp = f_quant_close_simp Fforall
 let f_exists_close_simp = f_quant_close_simp Fexists

src/core/term.mli

@@ -304,8 +304,10 @@ val f_iff_simp : fmla -> fmla -> fmla
 val f_not_simp : fmla -> fmla
 val t_if_simp : fmla -> term -> term -> term
 val f_if_simp : fmla -> fmla -> fmla -> fmla
+val t_let_simp : term -> term_bound -> term
 val f_let_simp : term -> fmla_bound -> fmla
 
+val t_let_close_simp : vsymbol -> term -> term -> term
 val f_let_close_simp : vsymbol -> term -> fmla -> fmla
 val f_quant_close_simp : quant -> vsymbol list -> trigger list -> fmla -> fmla
 val f_forall_close_simp : vsymbol list -> trigger list -> fmla -> fmla

src/transform/eliminate_algebraic.ml

@@ -79,7 +79,7 @@ let rec rewriteT kn state t = match t.t_node with
         match p with
         | { pat_node = Papp (cs,pl) } ->
             let add_var e p pj = match p.pat_node with
-              | Pvar v -> t_let_close v (t_app pj [t1] v.vs_ty) e
+              | Pvar v -> t_let_close_simp v (t_app pj [t1] v.vs_ty) e
               | _ -> Printer.unsupportedTerm t uncompiled
             in
             let pjl = Mls.find cs state.pj_map in
@@ -130,7 +130,7 @@ and rewriteF kn state av sign f = match f.f_node with
         let hd = t_app cs (List.map t_var vl) t1.t_ty in
         match t1.t_node with
         | Tvar v when Svs.mem v av ->
-            let hd = f_let_close v hd e in if sign
+            let hd = f_let_close_simp v hd e in if sign
             then f_forall_close_simp vl [] hd
             else f_exists_close_simp vl [] hd
         | _ ->
@@ -150,7 +150,7 @@ and rewriteF kn state av sign f = match f.f_node with
                       (rewriteF kn state Svs.empty sign) tr in
       let av = List.fold_left (fun s v -> Svs.add v s) av vl in
       let f1 = rewriteF kn state av sign f1 in
-      f_quant q (close vl tr f1)
+      f_quant_simp q (close vl tr f1)
   | Fbinop (o, _, _) when (o = Fand && sign) || (o = For && not sign) ->
       f_map_sign (rewriteT kn state) (rewriteF kn state av) sign f
   | Flet (t1, _) ->