module type Paramod =
sig
type t
- type input
type szsontology =
| Unsatisfiable of (t Terms.bag * int * int list) list
| GaveUp
| Error of string
| Timeout of int * t Terms.bag
- type bag = t Terms.bag * int
- val mk_passive : bag -> input * input -> bag * t Terms.clause
- val mk_goal : bag -> input * input -> bag * t Terms.clause
val paramod :
useage:bool ->
max_steps:int ->
+ print_problem:bool ->
?timeout:float ->
- bag ->
- g_passives:t Terms.clause list ->
- passives:t Terms.clause list -> szsontology
+ t Terms.foterm * (t Terms.foterm list * t Terms.foterm list) ->
+ (t Terms.foterm * (t Terms.foterm list * t Terms.foterm list)) list -> szsontology
end
module Paramod (B : Orderings.Blob) = struct
type t = B.t
- type input = B.input
type szsontology =
| Unsatisfiable of (B.t Terms.bag * int * int list) list
| GaveUp
exception Stop of szsontology
type bag = B.t Terms.bag * int
module Pp = Pp.Pp (B)
- module FU = FoUnif.Founif(B)
+ module FU = FoUnif.FoUnif(B)
module IDX = Index.Index(B)
module Sup = Superposition.Superposition(B)
module Utils = FoUtils.Utils(B)
module Order = B
+ module Clauses = Clauses.Clauses(B)
module WeightOrderedPassives =
struct
type t = B.t Terms.passive_clause
- let compare = Utils.compare_passive_clauses_weight
+ let compare = Clauses.compare_passive_clauses_weight
end
module AgeOrderedPassives =
struct
type t = B.t Terms.passive_clause
- let compare = Utils.compare_passive_clauses_age
+ let compare = Clauses.compare_passive_clauses_age
end
module WeightPassiveSet = Set.Make(WeightOrderedPassives)
module AgePassiveSet = Set.Make(AgeOrderedPassives)
- let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl =
- let cl = if no_weight then (0,cl)
- else Utils.mk_passive_clause cl in
- WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
+ let add_passive_clause ?(bonus_weight=0) (passives_w,passives_a) cl =
+ let (w,cl) = Clauses.mk_passive_clause cl in
+ (* let cl = (w+bonus_weight,cl) in *)
+ let cl = if bonus_weight = 0 then (w,cl) else (0,cl) in
+ WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
;;
- let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g =
- let g = if no_weight then (0,g)
- else Utils.mk_passive_goal g in
- WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
+ let add_passive_goal ?(bonus_weight=0) (passives_w,passives_a) g =
+ let (w,g) = Clauses.mk_passive_goal g in
+ (* let g = (w+bonus_weight,g) in *)
+ let g = if bonus_weight = 0 then (w,g) else (0,g) in
+ WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
;;
let remove_passive_clause (passives_w,passives_a) cl =
passives_w,passives_a
;;
- let add_passive_clauses ?(no_weight=false)
+ let add_passive_clauses ?(bonus_weight=0)
(passives_w,passives_a) new_clauses =
let new_clauses_w,new_clauses_a =
- List.fold_left (add_passive_clause ~no_weight)
+ List.fold_left (add_passive_clause ~bonus_weight)
(WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
in
(WeightPassiveSet.union new_clauses_w passives_w,
AgePassiveSet.union new_clauses_a passives_a)
;;
- let add_passive_goals ?(no_weight=false)
+ let add_passive_goals ?(bonus_weight=0)
(passives_w,passives_a) new_clauses =
let new_clauses_w,new_clauses_a =
- List.fold_left (add_passive_goal ~no_weight)
+ List.fold_left (add_passive_goal ~bonus_weight)
(WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
in
(WeightPassiveSet.union new_clauses_w passives_w,
else WeightPassiveSet.min_elt passives_w
;;
- let mk_clause bag maxvar (t,ty) =
- let (proof,ty) = B.saturate t ty in
- let c, maxvar = Utils.mk_clause maxvar [] [ty] proof in
- let bag, c = Terms.add_to_bag c bag in
- (bag, maxvar), c
- ;;
-
- let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
- let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
-
(* TODO : global age over facts and goals (without comparing weights) *)
let select ~use_age passives g_passives =
if is_passive_set_empty passives then begin
actives passives g_actives g_passives
;;
- let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+ let paramod ~useage ~max_steps ~print_problem ?timeout goal hypotheses =
let initial_timestamp = Unix.gettimeofday () in
+ let bag = Terms.empty_bag in
+ let maxvar = 0 in
+ let build_clause (bag,maxvar,l) (t,(nlit,plit)) =
+ let c,maxvar = Clauses.mk_clause maxvar nlit plit t in
+ let bag,c = Terms.add_to_bag c bag in
+ (bag,maxvar,c::l)
+ in
+ let bag,maxvar,goals = build_clause (bag,maxvar,[]) goal in
+ let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in
+ let goal = match goals with | [g] -> g | _ -> assert false in
let passives =
- add_passive_clauses ~no_weight:true passive_empty_set passives
+ add_passive_clauses ~bonus_weight:(-1000) passive_empty_set hypotheses
in
let g_passives =
- add_passive_goals ~no_weight:true passive_empty_set g_passives
+ add_passive_goal ~bonus_weight:(-1000) passive_empty_set goal
in
let g_actives = [] in
let actives = [], IDX.DT.empty in
+ if print_problem then begin
+ prerr_endline "Facts:";
+ List.iter (fun x -> prerr_endline (" " ^ Pp.pp_clause x)) hypotheses;
+ prerr_endline "Goal:";
+ prerr_endline (" " ^ Pp.pp_clause goal);
+ end;
try
given_clause ~useage ~noinfer:false
bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives