small progress in hypothesis_selection

corrected bug in ocamlgraph presence checking in configure.in

configure.in

@@ -271,13 +271,8 @@ fi
 
 # hypothesis_selection
 
-AC_CHECK_FILE($OCAMLLIB/ocamlgraph/,enable_hypothesis_selection=yes)
+AC_CHECK_FILE($OCAMLLIB/ocamlgraph/,enable_hypothesis_selection=yes,enable_hypothesis_selection=no)
 
-if test "$enable_hypothesis_selection" = no; then
-  enable_hypothesis_selection=no
-else
-  enable_hypothesis_selection=yes
-fi
 
 #Viewer for ps and pdf
 dnl AC_CHECK_PROGS(PSVIEWER,gv evince)

src/transform/hypothesis_selection.ml

@@ -38,15 +38,68 @@ end
 
 module GP = Digraph.AbstractLabeled(struct type t = Term.lsymbol end)(Int_Dft)
 module GC = Graph.AbstractLabeled(struct type t = int end)(Int_Dft)			    
-
+module FmlaHashtbl = Hashtbl.Make(struct type t = Term.fmla
+					 let equal x y = x.f_tag = y.f_tag
+					 let hash x = x.f_tag
+				  end)
 
 module Util = struct
 end
 
 
 (** module used to reduce formulae to Normal Form *)
-module NF = struct (* add memoization ? *)
-
+module NF = struct (* add memoization, one day ? *)
+
+  (** creates a fresh formula representing a quantified formula *)
+  let create_fmla (vars:Term.vsymbol list) : Term.fmla =
+    let pred = create_psymbol (id_fresh "temoin")
+      (List.map (fun var -> var.vs_ty) vars) in
+    f_app pred (List.map t_var vars)
+
+
+  (** transforms a formulae into its Normal Form as a list of clauses.
+  The first argument is a hastable from formulae to formulae *)
+  let rec transform fmlaTable fmla = match fmla.f_node with
+    | Fquant (_,f_bound) ->
+	let var,_,f =  f_open_quant f_bound in
+	traverse fmlaTable fmla var f
+    | Fbinop (op,f1,f2) -> split_binop fmlaTable op f1 f2
+    | Fnot f -> handle_not fmlaTable f
+    | Fapp (_,_) -> [fmla]
+    | Ftrue | Ffalse -> [fmla]
+    | Fif (_,_,_) -> failwith "if formulae not handled"
+    | Flet (_,_) -> failwith "let formulae not handled"
+    | Fcase (_,_) -> failwith "case formulae not handled"
+  and traverse fmlaTable old_fmla vars fmla = match fmla.f_node with
+    | Fquant (_,f_bound) ->
+	let var,_,f =  f_open_quant f_bound in
+	traverse fmlaTable old_fmla (var@vars) f
+    | _ ->
+	let new_f = transform fmlaTable fmla in
+	FmlaHashtbl.add fmlaTable old_fmla (create_fmla vars);
+	assert false
+  and split_binop fmlaTable op f1 f2 = match (op,f1,f2) with
+    | Fimplies,{f_node = Fbinop (For, h1, h2)},f2 ->
+	split_binop fmlaTable op h1 f2 @ split_binop fmlaTable op h2 f2
+    | Fimplies,f1,f2 ->
+	List.concat
+	  (List.map (fun f -> split_binop fmlaTable op f1 f)
+	     (transform fmlaTable f2))
+    | Fand,f1,f2 ->
+	transform fmlaTable f1 @ transform fmlaTable f2
+    | _,_,_ ->
+	[f_binary op f1 f2]
+  and handle_not fmlaTable f = match f.f_node with
+    | Fnot f1 -> transform fmlaTable f1
+    | Fbinop (Fand,f1,f2) ->
+	transform fmlaTable (f_or (f_not f1) (f_not f2))
+    | Fbinop (For,f1,f2) ->
+	transform fmlaTable (f_and (f_not f1) (f_not f2))
+    | Fbinop (Fimplies,f1,f2) ->
+	transform fmlaTable (f_and f1 (f_not f2))
+    | Fbinop (Fiff,f1,f2) ->
+	transform fmlaTable (f_or (f_and f1 (f_not f2)) (f_and (f_not f1) f2))
+    | _ -> [f_not f] (* default case *)
 
 end
 
@@ -54,27 +107,30 @@ end
 (** module used to compute the graph of constants *)
 module GraphConstant = struct
 
-  let update gc task_head = assert false
+  let update gc task_head = gc (* TODO *)
 
 end
 
 (** module used to compute the directed graph of predicates *)
-module GraphPredicate : sig
-  val update : GP.t -> Task.task_hd -> GP.t
-end = struct
+module GraphPredicate = struct
+
+  (** analyse a single clause *)
+  let analyse_clause gp clause = assert false
 
-  let analyse_prop gp prop = assert false
+  let analyse_prop fmlaTable gp prop =
+    let clauses = NF.transform fmlaTable prop in
+    List.fold_left analyse_clause gp clauses
 
-  let add_symbol gp lsymbol = GP.add_vertex gp
-    (GP.V.create lsymbol)
+  let add_symbol gp lsymbol =
+    GP.add_vertex gp (GP.V.create lsymbol)
 
   (** takes a constant graph and a task_head, and add any interesting
   element to the graph it returns. *)
-  let update gp task_head =
+  let update fmlaTable gp task_head =
     match task_head.task_decl with
       | Decl {d_node = Dprop (_,_,prop_decl) } ->
 	  (* a proposition to analyse *)
-	  analyse_prop gp prop_decl
+	  analyse_prop fmlaTable gp prop_decl
       | Decl {d_node = Dlogic logic_decls } ->
 	  (* a symbol to add *)
 	  List.fold_left (fun gp logic_decl -> add_symbol gp (fst logic_decl))
@@ -90,21 +146,21 @@ module Select = struct
 end
 
 (** collects data on predicates and constants in task *)
-let collect_info =
+let collect_info fmlaTable =
   Trans.fold (fun t (gc, gp) ->
-    GraphConstant.update gc t, GraphPredicate.update gp t)
+    GraphConstant.update gc t, GraphPredicate.update fmlaTable gp t)
     (GC.empty, GP.empty)
 
 (** the transformation, made from applying collect_info and
 then mapping Select.filter *)
-let transformation task =
-  let (gc,gp) = Trans.apply collect_info task in
+let transformation fmlaTable task =
+  let (gc,gp) = Trans.apply (collect_info fmlaTable) task in
   Trans.apply (Trans.decl (Select.filter (gc,gp)) None) task
 
 (** the transformation to be registered *)
 let hypothesis_selection =
   Register.store
-    (fun () -> Trans.store transformation)
+    (fun () -> Trans.store (transformation (FmlaHashtbl.create 17)))
 
 let _ = Register.register_transform
   "hypothesis_selection" hypothesis_selection