Commit 15b29b45 authored by Simon Cruanes's avatar Simon Cruanes
Browse files

progress in hypothesis_selection, but errors -> need debug

parent b9ed5a46
......@@ -70,7 +70,7 @@ module NF = struct (* add memoization, one day ? *)
(** all quantifiers in prenex form *)
let prenex_fmla fmla =
Format.fprintf err "prenex_fmla :@ @[%a@]@." Pretty.print_fmla fmla;
Format.fprintf err "prenex_fmla : @[%a@]@." Pretty.print_fmla fmla;
fmla
(** creates a fresh formula representing a quantified formula *)
......@@ -81,8 +81,8 @@ module NF = struct (* add memoization, one day ? *)
(** transforms a formulae into its Normal Form as a list of clauses.
The first argument is a hastable from formulae to formulae.
A clause is a list of formulae *)
The first argument is a hastable from formulae to formulae.
A clause is a list of formulae *)
let rec transform fmlaTable fmla =
Format.fprintf err "transform : @[%a@]@." Pretty.print_fmla fmla;
match fmla.f_node with
......@@ -91,7 +91,7 @@ module NF = struct (* add memoization, one day ? *)
traverse fmlaTable fmla var f
| Fbinop (_,_,_) ->
let clauses = split fmla in
Format.fprintf err "split : %a@." Util.print_clause clauses;
Format.fprintf err "split : @[%a@]@." Util.print_clause clauses;
begin match clauses with
| [f] -> begin match f.f_node with
| Fbinop (For,f1,f2) ->
......@@ -102,7 +102,7 @@ module NF = struct (* add memoization, one day ? *)
end
| _ -> List.concat (List.map (transform fmlaTable) clauses)
end
| Fnot f -> handle_not fmlaTable f
| Fnot f -> handle_not fmlaTable fmla f
| Fapp (_,_) -> [[fmla]]
| Ftrue | Ffalse -> [[fmla]]
| Fif (_,_,_) -> failwith "if formulae not handled"
......@@ -112,7 +112,7 @@ module NF = struct (* add memoization, one day ? *)
| Fquant (_,f_bound) ->
let var,_,f = f_open_quant f_bound in
traverse fmlaTable old_fmla (var@vars) f
| _ -> (* TODO !! *)
| _ -> (* TODO !! remember link between new term and old quantified formula *)
if FmlaHashtbl.mem fmlaTable fmla then
[[FmlaHashtbl.find fmlaTable fmla]]
else
......@@ -135,7 +135,10 @@ module NF = struct (* add memoization, one day ? *)
else split (f_or (f_not f1) f2)
| Fbinop (Fand,f1,f2) -> [f1; f2]
| _ -> [f]
and handle_not fmlaTable f = match f.f_node with
and handle_not fmlaTable old_f f = match f.f_node with
| Fquant (Fforall,f_bound) ->
let vars,triggers,f1 = f_open_quant f_bound in
transform fmlaTable (f_exists vars triggers (f_not f1))
| Fnot f1 -> transform fmlaTable f1
| Fbinop (Fand,f1,f2) ->
transform fmlaTable (f_or (f_not f1) (f_not f2))
......@@ -145,7 +148,7 @@ module NF = struct (* add memoization, one day ? *)
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 *)
| _ -> [[old_f]] (* default case *)
end
......@@ -184,17 +187,26 @@ module GraphPredicate = struct
(** analyse a single clause *)
let analyse_clause symbTbl gp clause =
let negative,positive = List.partition is_negative clause in
let get_symbol x = find symbTbl (extract_symbol x) in
let negative,positive = List.partition is_negative clause in
let negative = List.map get_symbol negative in
let positive = List.map get_symbol positive in
let n = List.length clause in
let add left gp right =
let e = GP.E.create left n right in
GP.add_edge_e gp e in
List.fold_left (* add an edge from every negative to any positive *)
(fun gp left ->
List.fold_left (add left) gp positive) gp negative
try
let old = GP.find_edge gp left right in
if GP.E.label old <= n
then gp (* old edge is fine *)
else
let new_gp = GP.remove_edge_e gp old in
assert (not (GP.mem_edge new_gp left right));
GP.add_edge_e gp (GP.E.create left n right)
with Not_found ->
let e = GP.E.create left n right in
GP.add_edge_e gp e
in List.fold_left (* add an edge from every negative to any positive *)
(fun gp left ->
List.fold_left (add left) gp positive) gp negative
(** takes a prop, puts it in Normal Form and then builds a clause
from it *)
......@@ -225,32 +237,115 @@ end
(** module that makes the final selection *)
module Select = struct
let is_pertinent (_gc,_gp) _fmla = true (* TODO *)
let filter (gc,gp) decl =
match decl.d_node with
| Dtype _ | Dlogic _ | Dind _ -> [decl]
| Dprop (_,_,fmla) ->
Format.eprintf "filter : @[%a@]@." Pretty.print_fmla fmla;
let return_value = if is_pertinent (gc,gp) fmla then
[decl] else [] in
if return_value = [] then Format.eprintf "NO@.@." else Format.eprintf "YES@.@.";
return_value
let get_predicates fmla =
let id acc _ = acc in
let rec explore acc fmla = match fmla.f_node with
| Fapp (pred,_) -> pred::acc
| _ -> f_fold id explore acc fmla
in explore [] fmla
let get_clause_predicates acc clause =
let rec fmla_get_pred acc fmla = match fmla.f_node with
| Fnot f -> fmla_get_negative_pred acc f
| Fapp (pred,_) -> (pred, `Positive)::acc
| _ -> failwith "bad formula in get_predicates !"
and fmla_get_negative_pred acc fmla = match fmla.f_node with
| Fapp (pred,_) -> (pred, `Negative)::acc
| _ -> failwith "bad (negative) formula in get_predicates !"
in List.fold_left fmla_get_pred acc clause
(** get the predecessors of [positive] in the graph [gp], at distance <= [i]*)
let rec get_predecessors i gp acc positive =
if i <= 0
then acc
else
let acc = positive :: acc in
List.fold_left (follow_edge gp i) acc (GP.pred_e gp positive)
and follow_edge gp i acc edge =
get_predecessors (i - GP.E.label edge) gp acc (GP.E.src edge)
let rec get_successors _j _gp acc _negative = acc
(* TODO : be clear... *)
(** determines if a proposition is pertinent w.r.t the given goal formula,
from data stored in the two graphes [gc] and [gp] given.
[i] is the parameter of predicate graph ([gp]) based filtering.
[j] is the parameter for dynamic constants ([gc]) dependency filtering *)
let is_pertinent symTbl goal_clauses ?(i=2) ?(j=2) (_gc,gp) fmla =
let goal_predicates =
List.fold_left get_clause_predicates [] goal_clauses in
let predicates = get_predicates fmla in
let is_negative = function
| (_,`Positive) -> false
| (_,`Negative) -> true in
let negative,positive = List.partition is_negative goal_predicates in
let negative,positive = List.map fst negative, List.map fst positive in
let negative = List.map (SymbHashtbl.find symTbl) negative in
let positive = List.map (SymbHashtbl.find symTbl) positive in
let predicates = List.map (SymbHashtbl.find symTbl) predicates in
(* list of negative predecessors of any positive predicate of the goal,
at distance <= i *)
let predecessors = List.fold_left (get_predecessors i gp) [] positive in
let successors = List.fold_left (get_successors j gp) [] negative in
(* a predicates is accepted iff all its predicates are close enough in
successors or predecessors lists *)
List.for_all
(fun x -> List.mem x predecessors || List.mem x successors)
predicates
(** preprocesses the goal formula and the graph, and returns a function
that will accept or not axioms according to their relevance. *)
let filter symTbl goal_clauses (gc,gp) =
function decl -> (* TODO : clean up *)
match decl.d_node with
| Dtype _ | Dlogic _ | Dind _ -> [decl]
| Dprop (Paxiom,_,fmla) -> (* filter only axioms *)
Format.eprintf "filter : @[%a@]@." Pretty.print_fmla fmla;
let return_value =
try
if is_pertinent symTbl goal_clauses (gc,gp) fmla
then [decl] else []
with Not_found -> [decl] in (* TODO : remove ! *)
if return_value = [] then Format.eprintf "NO@.@."
else Format.eprintf "YES@.@.";
return_value
| Dprop(_,_,_) -> [decl]
end
(** if this is the goal, return it as Some goal after checking there is no other
goal. Else, return the option *)
let get_goal task_head option =
match task_head.task_decl with
| Decl {d_node = Dprop(Pgoal,_,goal_fmla)} ->
assert (option = None); (* only one goal ! *)
Some goal_fmla
| _ -> option
(** collects data on predicates and constants in task *)
let collect_info fmlaTable symbTbl =
Trans.fold (fun t (gc, gp) ->
GraphConstant.update gc t,
GraphPredicate.update fmlaTable symbTbl gp t)
(GC.empty, GP.empty)
Trans.fold
(fun t (gc, gp, goal_option) ->
GraphConstant.update gc t,
GraphPredicate.update fmlaTable symbTbl gp t,
get_goal t goal_option)
(GC.empty, GP.empty, None)
(** the transformation, made from applying collect_info and
then mapping Select.filter *)
let transformation fmlaTable symbTbl task =
let (gc,gp) = Trans.apply (collect_info fmlaTable symbTbl) task in
Trans.apply (Trans.decl (Select.filter (gc,gp)) None) task
(* first, collect data in 2 graphes *)
let (gc,gp,goal_option) =
Trans.apply (collect_info fmlaTable symbTbl) task in
(* get the goal *)
let goal_fmla = match goal_option with
| None -> failwith "no goal !"
| Some goal_fmla -> goal_fmla in
let goal_clauses = NF.transform fmlaTable goal_fmla in
(* filter one declaration at once *)
Trans.apply
(Trans.decl
(Select.filter symbTbl goal_clauses (gc,gp)) None) task
(** the transformation to be registered *)
let hypothesis_selection =
......@@ -258,12 +353,12 @@ let hypothesis_selection =
(fun () -> Trans.store
(transformation (FmlaHashtbl.create 17) (SymbHashtbl.create 17)))
let _ = Register.register_transform
let _ = Register.register_transform
"hypothesis_selection" hypothesis_selection
(*
Local Variables:
compile-command: "unset LANG; cd ../..; make"
compile-command: "unset LANG; cd ../..; make src/transform/hypothesis_selection.cmo"
End:
*)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment