From a15dc157f7e63db12b9a7b59cf00aea108d7e073 Mon Sep 17 00:00:00 2001 From: denes Date: Wed, 17 Jun 2009 08:47:34 +0000 Subject: [PATCH] Added optionnal one pass simplification (instead of keep_simplified) Fix for varlists (we traverse the term to collect occuring variables) --- .../components/ng_paramodulation/paramod.ml | 39 ++++++++++------- .../ng_paramodulation/superposition.ml | 42 ++++++++++++++++--- .../ng_paramodulation/superposition.mli | 7 ++++ 3 files changed, 67 insertions(+), 21 deletions(-) diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 36adca454..8903ec02f 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -1,9 +1,9 @@ -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 @@ -39,19 +39,16 @@ let nparamod rdb metasenv subst context t table = 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 @@ -95,16 +92,26 @@ let nparamod rdb metasenv subst context t table = | 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 diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 2198ec8bd..e87a03f52 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -23,7 +23,7 @@ module Superposition (B : Terms.Blob) = 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 @@ -72,6 +72,14 @@ module Superposition (B : Terms.Blob) = 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 @@ -85,7 +93,7 @@ module Superposition (B : Terms.Blob) = | 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 @@ -128,7 +136,7 @@ module Superposition (B : Terms.Blob) = (* 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 @@ -191,20 +199,42 @@ module Superposition (B : Terms.Blob) = 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, @@ -216,8 +246,10 @@ module Superposition (B : Terms.Blob) = 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)) diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index d7efb1b42..6deb0a4eb 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -51,6 +51,13 @@ module Superposition (B : Terms.Blob) : B.t Terms.unit_clause -> B.t Terms.bag * B.t Terms.unit_clause + val one_pass_simplification: + B.t Terms.unit_clause -> + Index.Index(B).active_set -> + B.t Terms.bag -> + (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option + + val keep_simplified: B.t Terms.unit_clause -> Index.Index(B).active_set -> -- 2.39.2