-let debug s = ()
-(* prerr_endline s *)
+let debug s =
+ () (* prerr_endline s *)
;;
let nparamod rdb metasenv subst context t table =
- let nb_iter = ref 100 in
+ let nb_iter = ref 200 in
prerr_endline "========================================";
let module C = struct
let metasenv = metasenv
let rec given_clause bag maxvar actives
passives g_actives g_passives =
- decr nb_iter; if !nb_iter = 0 then raise (Failure "Timeout !");
+ decr nb_iter; if !nb_iter = 0 then
+ (*(prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
+ prerr_endline "Active table :";
+ (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
+ (fst actives));*)
+ raise (Failure "Timeout !");
+
- (* keep goals demodulated w.r.t. actives and check if solved *)
- (* we may move this at the end of infer_right *)
- let bag, g_actives =
- List.fold_left
- (fun (bag,acc) c ->
- let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
- bag, c::acc)
- (bag,[]) g_actives
- in
- (* superposition left, simplifications on goals *)
+ (* superposition left, simplifications on goals *)
debug "infer_left step...";
let bag, maxvar, g_actives, g_passives =
match select g_passives with
| Some (current, passives) ->
debug ("Selected fact : " ^ Pp.pp_unit_clause current);
match Sup.keep_simplified current actives bag with
+ (* match Sup.one_pass_simplification current actives bag with *)
| None -> aux_simplify passives
- | Some x -> x
+ | Some x -> x,passives
in
- let (current, bag, actives) = aux_simplify passives
+ let (current, bag, actives),passives = aux_simplify passives
in
debug ("Fact after simplification :"
^ Pp.pp_unit_clause current);
let bag, maxvar, actives, new_clauses =
Sup.infer_right bag maxvar current actives
in
+ debug "Demodulating goals with actives...";
+ (* keep goals demodulated w.r.t. actives and check if solved *)
+ let bag, g_actives =
+ List.fold_left
+ (fun (bag,acc) c ->
+ let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
+ bag, c::acc)
+ (bag,[]) g_actives
+ in
let ctable = IDX.index_unit_clause IDX.DT.empty current in
let bag, maxvar, new_goals =
List.fold_left
exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
let debug s =
- ()(* prerr_endline s *)
+ () (* prerr_endline s *)
;;
let rec list_first f = function
in
aux pos ctx t
;;
+
+ let vars_of_term t =
+ let rec aux acc = function
+ | Terms.Leaf _ -> acc
+ | Terms.Var i -> if (List.mem i acc) then acc else i::acc
+ | Terms.Node l -> List.fold_left aux acc l
+ in aux [] t
+ ;;
let build_clause bag filter rule t subst vl id id2 pos dir =
let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
| t -> Terms.Predicate t
in
let bag, uc =
- Utils.add_to_bag bag (0, literal, vl, proof)
+ Utils.add_to_bag bag (0, literal, vars_of_term t, proof)
in
Some (bag, uc)
else
(* XXX: possible optimization, if the literal has a "side" already
* in normal form we should not traverse it again *)
let demodulate_once bag (id, literal, vl, pr) table =
- debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));
+ (* debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));*)
let t =
match literal with
| Terms.Predicate t -> t
else Some (bag, clause)
;;
+ let one_pass_simplification new_clause (alist,atable) bag =
+ match simplify atable bag new_clause with
+ | None -> None (* new_clause has been discarded *)
+ | Some (bag, clause) ->
+ let ctable = IDX.index_unit_clause IDX.DT.empty clause in
+ let bag, alist, atable =
+ List.fold_left
+ (fun (bag, alist, atable as acc) c ->
+ match simplify ctable bag c with
+ |None -> acc (* an active clause as been discarded *)
+ |Some (bag, c1) ->
+ bag, c :: alist, IDX.index_unit_clause atable c)
+ (bag,[],IDX.DT.empty) alist
+ in
+ Some (clause, bag, (alist,atable))
+ ;;
+
let simplification_step ~new_cl cl (alist,atable) bag new_clause =
let atable1 =
if new_cl then atable else
IDX.index_unit_clause atable cl
in
+ (* Simplification of new_clause with : *
+ * - actives and cl if new_clause is not cl *
+ * - only actives otherwise *)
match simplify atable1 bag new_clause with
- | None -> (Some cl, None)
+ | None -> (Some cl, None) (* new_clause has been discarded *)
| Some (bag, clause) ->
+ (* Simplification of each active clause with clause *
+ * which is the simplified form of new_clause *)
let ctable = IDX.index_unit_clause IDX.DT.empty clause in
let bag, newa, alist, atable =
List.fold_left
(fun (bag, newa, alist, atable as acc) c ->
match simplify ctable bag c with
- |None -> acc
+ |None -> acc (* an active clause as been discarded *)
|Some (bag, c1) ->
if (c1 == c) then
bag, newa, c :: alist,
if new_cl then
(Some cl, Some (clause, (alist,atable), newa, bag))
else
+ (* if new_clause is not cl, we simplify cl with clause *)
match simplify ctable bag cl with
| None ->
+ (* cl has been discarded *)
(None, Some (clause, (alist,atable), newa, bag))
| Some (bag,cl1) ->
(Some cl1, Some (clause, (alist,atable), newa, bag))
projects / helm.git / commitdiff