Commit 9778f3e8 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

fix hypothesis_selection

parent 9345a9b6
...@@ -267,8 +267,9 @@ module GraphConstant = struct ...@@ -267,8 +267,9 @@ module GraphConstant = struct
List.fold_left (analyse_clause fTbl tTbl) gc clauses List.fold_left (analyse_clause fTbl tTbl) gc clauses
(** processes a single task_head. *) (** processes a single task_head. *)
let update fmlaTable fTbl tTbl gc task_head = match task_head.task_decl with let update fmlaTable fTbl tTbl gc task_head =
| Decl {d_node = Dprop(_,_,prop_decl)} -> match task_head.task_decl.Theory.td_node with
| Theory.Decl {d_node = Dprop(_,_,prop_decl)} ->
analyse_prop fmlaTable fTbl tTbl gc prop_decl analyse_prop fmlaTable fTbl tTbl gc prop_decl
| _ -> gc | _ -> gc
end end
...@@ -334,11 +335,11 @@ module GraphPredicate = struct ...@@ -334,11 +335,11 @@ module GraphPredicate = struct
(** takes a constant graph and a task_head, and add any interesting (** takes a constant graph and a task_head, and add any interesting
element to the graph it returns. *) element to the graph it returns. *)
let update fmlaTable symbTbl gp task_head = let update fmlaTable symbTbl gp task_head =
match task_head.task_decl with match task_head.task_decl.Theory.td_node with
| Decl {d_node = Dprop (_,_,prop_decl) } -> | Theory.Decl {d_node = Dprop (_,_,prop_decl) } ->
(* a proposition to analyse *) (* a proposition to analyse *)
analyse_prop fmlaTable symbTbl gp prop_decl analyse_prop fmlaTable symbTbl gp prop_decl
| Decl {d_node = Dlogic logic_decls } -> | Theory.Decl {d_node = Dlogic logic_decls } ->
(* a symbol to add *) (* a symbol to add *)
List.fold_left List.fold_left
(fun gp logic_decl -> add_symbol symbTbl gp (fst logic_decl)) (fun gp logic_decl -> add_symbol symbTbl gp (fst logic_decl))
...@@ -523,8 +524,8 @@ end ...@@ -523,8 +524,8 @@ end
(** if this is the goal, return it as Some goal after checking there is no other (** if this is the goal, return it as Some goal after checking there is no other
goal. Else, return the option *) goal. Else, return the option *)
let get_goal task_head option = let get_goal task_head option =
match task_head.task_decl with match task_head.task_decl.Theory.td_node with
| Decl {d_node = Dprop(Pgoal,_,goal_fmla)} -> | Theory.Decl {d_node = Dprop(Pgoal,_,goal_fmla)} ->
assert (option = None); (* only one goal ! *) assert (option = None); (* only one goal ! *)
Some goal_fmla Some goal_fmla
| _ -> option | _ -> option
......
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