(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
-let debug s = prerr_endline (Lazy.force s) ;;
-(* let debug _ = ();; *)
+let print s = prerr_endline (Lazy.force s) ;;
+let noprint s = ();;
+let debug = noprint;;
let monster = 100;;
type t
type input
type szsontology =
- | Unsatisfiable of (t Terms.bag * int * int list) list
+ | Unsatisfiable of
+ (t Terms.bag * int * t Terms.substitution * int list) list
| GaveUp
| Error of string
| Timeout of int * t Terms.bag
bag ->
g_passives:t Terms.unit_clause list ->
passives:t Terms.unit_clause list -> szsontology
+ val demod :
+ state -> input* input -> szsontology
val fast_eq_check :
state -> input* input -> szsontology
+ val nparamod :
+ useage:bool ->
+ max_steps:int ->
+ ?timeout:float ->
+ state -> input* input -> szsontology
end
module Paramod (B : Orderings.Blob) = struct
type input = B.input
type bag = B.t Terms.bag * int
type szsontology =
- | Unsatisfiable of (B.t Terms.bag * int * int list) list
+ | Unsatisfiable of
+ (B.t Terms.bag * int * B.t Terms.substitution * int list) list
| GaveUp
| Error of string
| Timeout of int * B.t Terms.bag
else WeightPassiveSet.min_elt passives_w
;;
+ let mk_unit_clause bag maxvar (t,ty) =
+ let c, maxvar = Utils.mk_unit_clause maxvar (B.embed ty) (B.embed t) in
+ let bag, c = Terms.add_to_bag c bag in
+ (bag, maxvar), c
+ ;;
+
let mk_clause bag maxvar (t,ty) =
let (proof,ty) = B.saturate t ty in
let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
;;
let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
+
let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
+
let initialize_goal (bag,maxvar,actives,passives,_,_) t =
- let (bag,maxvar), g = mk_goal (bag,maxvar) t in
+ let (bag,maxvar), g = mk_unit_clause bag maxvar t in
let g_passives = g_passive_empty_set in
- let g_passives = add_passive_goal g_passives g in
+ (* if the goal is not an equation we returns an empty
+ passive set *)
+ let g_passives =
+ if Terms.is_eq_clause g then add_passive_goal g_passives g
+ else g_passives
+ in
(bag,maxvar,actives,passives,[],g_passives)
in
debug (lazy "Performed infer_left step");
let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
- bag, maxvar, actives, passives, g_current::g_actives,
+ bag, maxvar, actives, passives, g_current::g_actives,
(add_passive_goals g_passives new_goals)
;;
+ let pp_clauses actives passives =
+ let actives_l, _ = actives in
+ let passive_t,_,_ = passives in
+ let wset = IDX.elems passive_t in
+ ("Actives :" ^ (String.concat ";\n"
+ (List.map Pp.pp_unit_clause actives_l)))
+ ^
+ ("Passives:" ^(String.concat ";\n"
+ (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
+ (IDX.ClauseSet.elements wset))))
+ ;;
+
let forward_infer_step
((bag,maxvar,actives,passives,g_actives,g_passives) as s)
current iterno =
* P' = P + new' *)
debug (lazy "Forward infer step...");
debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
- let id,_,_,_ = current in
- let _ = Terms.get_from_bag id bag in
-
+ noprint (lazy (pp_clauses actives passives));
match Sup.keep_simplified current actives bag maxvar
with
| _,None -> s
| bag,Some (current,actives) ->
- debug (lazy "simplified...");
+ debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current)));
let bag, maxvar, actives, new_clauses =
Sup.infer_right bag maxvar current actives
in
+ debug
+ (lazy
+ ("New clauses :" ^ (String.concat ";\n"
+ (List.map Pp.pp_unit_clause new_clauses))));
debug (lazy "Demodulating goals with actives...");
(* keep goals demodulated w.r.t. actives and check if solved *)
let bag, g_actives =
(passive_set_cardinal passives)))
;;
-
+
(* we just check if any of the active goals is subsumed by a
passive clause, or if any of the passive goal is subsumed
by an active or passive clause *)
let last_chance (bag,maxvar,actives,passives,g_actives,g_passives) =
debug (lazy("Last chance " ^ string_of_float
(Unix.gettimeofday())));
- let active_t = snd actives in
- let passive_t,_,_ = passives in
+ let actives_l, active_t = actives in
+ let passive_t,wset,_ = passives in
+ let _ = noprint
+ (lazy
+ ("Actives :" ^ (String.concat ";\n"
+ (List.map Pp.pp_unit_clause actives_l)))) in
+ let wset = IDX.elems passive_t in
+ let _ = noprint
+ (lazy
+ ("Passives:" ^(String.concat ";\n"
+ (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
+ (IDX.ClauseSet.elements wset))))) in
let g_passives =
WeightPassiveSet.fold
(fun (_,x) acc ->
if List.exists (Sup.are_alpha_eq x) g_actives then acc
else x::acc)
(fst g_passives) []
- in
+ in
ignore
(List.iter
(fun x ->
ignore
- (Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
+ (debug (lazy("ckecking goal vs a: " ^ Pp.pp_unit_clause x));
+ Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
g_passives);
ignore
(List.iter
(fun x ->
ignore
- (Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
+ (debug (lazy("ckecking goal vs p: " ^ Pp.pp_unit_clause x));
+ Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
(g_actives@g_passives));
raise (Stop (Timeout (maxvar,bag)))
actives passives g_actives g_passives
;;
+ let check_and_infer ~no_demod iterno status current =
+ let bag,maxvar,actives,passives,g_actives,g_passives = status in
+ match
+ Sup.simplify_goal
+ ~no_demod maxvar (snd actives) bag g_actives current
+ with
+ | None -> debug (lazy "None"); status
+ | Some (bag,g_current) ->
+ let _ =
+ debug (lazy("Infer on goal : "
+ ^ Pp.pp_unit_clause g_current))
+ in
+ backward_infer_step bag maxvar actives passives
+ g_actives g_passives g_current iterno
+
(* similar to given_clause, but it merely works on goals,
in parallel, at each iteration *)
let rec goal_narrowing iterno max_steps timeout status
let _ =
debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current))
in
- match
- Sup.simplify_goal
- ~no_demod:false maxvar (snd actives) bag g_actives current
- with
- | None -> acc
- | Some (bag,g_current) ->
- let _ =
- debug (lazy("Demodulated goal : "
- ^ Pp.pp_unit_clause g_current))
- in
- backward_infer_step bag maxvar actives passives
- g_actives g_passives g_current iterno)
- status passive_goals
+ (* we work both on the original goal and the demodulated one*)
+ let acc = check_and_infer ~no_demod:false iterno acc current
+ in check_and_infer ~no_demod:true iterno acc current)
+ status passive_goals
in
goal_narrowing iterno max_steps timeout newstatus
- let compute_result bag i =
+ let compute_result bag i subst =
let l =
let rec traverse ongoal (accg,acce) i =
match Terms.get_from_bag i bag with
let gsteps,esteps = traverse true ([],[]) i in
(List.rev esteps)@gsteps
in
- prerr_endline ("steps: " ^ (string_of_int (List.length l)));
+ debug (lazy ("steps: " ^ (string_of_int (List.length l))));
let max_w =
List.fold_left
(fun acc i ->
let (cl,_,_) = Terms.get_from_bag i bag in
max acc (Order.compute_unit_clause_weight cl)) 0 l in
- prerr_endline "Statistics :";
- prerr_endline ("Max weight : " ^ (string_of_int max_w));
+ debug (lazy ("Max weight : " ^ (string_of_int max_w)));
(* List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) =
Terms.get_from_bag id bag in
if d then
(Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
id it (Order.compute_unit_clause_weight cl)
(Pp.pp_proof_step proof))) l;*)
- prerr_endline "Proof:";
- List.iter
- (fun x ->
- let cl,_,_ = Terms.get_from_bag x bag in
- prerr_endline (Pp.pp_unit_clause cl)) l;
- Unsatisfiable [ bag, i, l ]
+ debug (lazy ("Proof:" ^
+ (String.concat "\n"
+ (List.map
+ (fun x ->
+ let cl,_,_ = Terms.get_from_bag x bag in
+ Pp.pp_unit_clause cl) l))));
+ Unsatisfiable [ bag, i, subst, l ]
let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
let _initial_timestamp = Unix.gettimeofday () in
given_clause ~useage ~noinfer:false
bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
with
- | Sup.Success (bag, _, (i,_,_,_)) ->
- compute_result bag i
- | Stop (Unsatisfiable _) -> Error "stop bug solution found!"
+ | Sup.Success (bag, _, (i,_,_,_),subst) ->
+ compute_result bag i subst
+ | Stop (Unsatisfiable _) -> Error "solution found!"
| Stop o -> o
;;
+let demod s goal =
+ let bag,maxvar,actives,passives,g_actives,g_passives = s in
+ let (bag,maxvar), g = mk_goal (bag,maxvar) goal in
+ let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
+ if g1 = g then GaveUp else compute_result bag i []
+(*
+ if Terms.is_eq_clause g then
+
+ else GaveUp *)
+
let fast_eq_check s goal =
- let s = initialize_goal s goal in
+ let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
+ if is_passive_g_set_empty g_passives then Error "not an equation"
+ else
try
goal_narrowing 0 2 None s
with
- | Sup.Success (bag, _, (i,_,_,_)) ->
- compute_result bag i
- | Stop (Unsatisfiable _) -> Error "stop bug solution found!"
+ | Sup.Success (bag, _, (i,_,_,_),subst) ->
+ compute_result bag i subst
+ | Stop (Unsatisfiable _) -> Error "solution found!"
+ | Stop o -> o
+ ;;
+
+let nparamod ~useage ~max_steps ?timeout s goal =
+ let bag,maxvar,actives,passives,g_actives,g_passives
+ = initialize_goal s goal in
+ if is_passive_g_set_empty g_passives then Error "not an equation"
+ else
+ try given_clause ~useage ~noinfer:false
+ bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
+ with
+ | Sup.Success (bag, _, (i,_,_,_),subst) ->
+ compute_result bag i subst
+ | Stop (Unsatisfiable _) -> Error "solution found!"
| Stop o -> o
;;