add dont show refinement option

hopv · Apr 30, 2021 · fbe9259 · fbe9259
1 parent 08ab27c
commit fbe9259
Show file tree

Hide file tree

Showing 3 changed files with 46 additions and 3 deletions.
diff --git a/lib/options/hflmc2_options.ml b/lib/options/hflmc2_options.ml
@@ -87,6 +87,8 @@ type params =
   ; show_refinement: bool [@default false] [@docs "Typing"] [@docv "show refinement"]
   (** Show refinement types. This sometimes fails because of parsing the solution from CHC solver... *)
 
+  ; dont_show_refinement : bool [@default false] [@docs "Typing"] [@docv "don't show refinement"]
+
   ; mode_burn_et_al: bool [@default false] [@docs "Typing"] [@docv "Use the subtyping rule of burn et al"]
   (** Use Subtying rule in burn et al *)
 
@@ -105,7 +107,7 @@ let set_up_params params =
   set_ref Abstraction.modify_pred_by_guard (not params.abst_no_modify_pred_by_guard);
   set_ref Refine.use_legacy                params.refine_legacy;
   set_ref Typing.solver                    params.solver;
-  set_ref Typing.show_refinement           params.show_refinement;
+  set_ref Typing.show_refinement           (params.show_refinement && not params.dont_show_refinement);
   set_ref Typing.mode_burn_et_al           params.mode_burn_et_al;
   set_ref Typing.no_disprove               params.no_disprove;
   params.input

diff --git a/lib/typing/disprove.ml b/lib/typing/disprove.ml
@@ -14,9 +14,37 @@ exception Infeasible
 let rid_of_arithid id = 
   Id.({name=id.name; id=id.id; ty=Rtype.RInt(RId(id))})
 
+let show_fixpoint = function
+  | Fixpoint.Greatest -> "v"
+  | Fixpoint.Least -> "u"
+
+let print_rhflz_hes hes =
+  List.iter
+    (fun {Rhflz.body; var; fix} ->
+      print_string @@ Id.to_string var;
+      print_string " =";
+      print_string @@ show_fixpoint fix;
+      print_string " ";
+      Rhflz.print_formula body;
+      print_string "\n"
+    )
+    hes
+
+let print_count_map (map : (Rtype.t Id.t * int list) list list) =
+  List.map (fun id_args ->
+    match id_args with
+    | [] -> ""
+    | (id, _)::_ ->
+      Id.to_string id ^ " -> " ^
+        (List.map (fun (_, args) -> "(" ^ (List.map string_of_int args |> String.concat ",") ^ ")") id_args |> String.concat "\n")
+  ) map
+  |> String.concat "\n"
+
 let disprove unsat_proof hes env top = 
   (* no recursive hes *)
-  let hes = Expand.expand unsat_proof hes in
+  let hes, args_map = Expand.expand unsat_proof hes in
+  print_rhflz_hes hes;
+  print_endline @@ print_count_map args_map;
   let fml = (Rhflz.lookup_rule top hes).body in
   let eval fml = 
     (* evaluator *)

diff --git a/lib/typing/expand.ml b/lib/typing/expand.ml
@@ -12,6 +12,13 @@ let gen_map nodes =
   ) M.empty nodes
 
 
+let gen_args_map nodes = 
+  List.fold_left (fun m x -> 
+    match M.find_opt x.name m with
+    | Some(l) -> M.add x.name ((x, x.args)::l) m
+    | None -> M.add x.name [x, x.args] m
+  ) M.empty nodes
+
 let expand unsat_proof hes =
   let map = gen_map unsat_proof in
   let expand_forall rule = 
@@ -92,5 +99,11 @@ let expand unsat_proof hes =
       let rules' = subst_rules fml rule.var rules in
       expand_rule xs rules'
   in
-  expand_rule hes hes
+  let args_map =
+    let map = gen_args_map unsat_proof in
+    List.map (fun rule ->
+      let id, _ = Rtype.get_top rule.var.ty in
+      match M.find_opt id map with Some(l) -> List.map (fun (_, args) -> (rule.var, args)) l | None -> []
+    ) hes in
+  expand_rule hes hes, args_map