Fix to the verification optimization: only check conclusion variables.

lukstafi · Mar 3, 2015 · faa719b · faa719b
1 parent 0dfaa89
commit faa719b
Show file tree

Hide file tree

Showing 3 changed files with 371 additions and 349 deletions.
diff --git a/src/Abduction.ml b/src/Abduction.ml
@@ -892,10 +892,7 @@ let abd q ~bvs ~xbvs ?orig_ren ?b_of_v ~upward_of ~nonparam_vars
         neg_brs in
   let verif_brs = List.map2
       (fun (prem, concl_ty) (_, _, _, concl_num) ->
-         VarSet.union (fvs_sb prem.cnj_typ)
-           (VarSet.union (NumDefs.fvs_formula prem.cnj_num)
-              (VarSet.union (fvs_sb concl_ty)
-                 (NumDefs.fvs_formula concl_num))),
+         VarSet.union (fvs_sb concl_ty) (NumDefs.fvs_formula concl_num),
          prem, concl_ty, concl_num)
       brs_typ brs_num in
   let validate added_vs (vs, ans) =

diff --git a/src/NumS.ml b/src/NumS.ml
@@ -2374,10 +2374,10 @@ let subst_chi chi_sb pos_chi =
 let empty_renaming = Hashtbl.create 0
 let empty_b_of_v v = v
 
-let fvs_br (_, _, _, (d_eqn, d_ineqn),
+let fvs_br_concl (_, _, _, _,
             (c_eqn, c_ineqn, c_optis, c_suboptis)) =
   VarSet.union
-    (vars_of_map (vars_of_map fvs_w) [d_eqn; d_ineqn; c_eqn; c_ineqn])
+    (vars_of_map (vars_of_map fvs_w) [c_eqn; c_ineqn])
     (vars_of_map (vars_of_map fvs_2w) [c_optis; c_suboptis])
 
 let fvs_sep_w_formula (c_eqn, c_ineqn, c_optis, c_suboptis) =
@@ -2526,7 +2526,7 @@ let abd q ~bvs ~xbvs ?(orig_ren=empty_renaming) ?(b_of_v=empty_b_of_v)
          else
            let brs_n = List.length res in
            let brs_r = ref brs_n in
-           List.map (fun br -> br, (fvs_br br, brs_r, brs_n, br)) res)
+           List.map (fun br -> br, (fvs_br_concl br, brs_r, brs_n, br)) res)
       brs in
   let brs, validate_brs = List.split brs in
   (*[* Format.printf "NumS.abd: brs processing past merging@\n%!"; *]*)