From b7587a7dd68463086e8a6b7c14f10c1dc33f64ba Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 12 Jun 2009 12:33:45 +0000 Subject: [PATCH] Added a new keep_simplified function --- .../ng_paramodulation/superposition.ml | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 600e204c8..4142a35b6 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -191,6 +191,27 @@ module Superposition (B : Terms.Blob) = else Some (bag, clause) ;; + let rec keep_simplified (alist,atable) bag newc = + match newc with + | [] -> bag, (alist,atable) + | hd::tl -> + (match simplify atable bag hd with + | None -> keep_simplified (alist,atable) bag tl + | Some (bag, 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) c -> + let bag, c1 = demodulate bag c ctable in + if (c1 == c) then + bag, newa, c :: alist, IDX.index_unit_clause atable c + else + bag, c :: newa, alist, atable) + (bag,[],[],IDX.DT.empty) alist + in + keep_simplified (alist, atable) bag newa) + ;; + (* this is like simplify but raises Success *) let simplify_goal maxvar table bag clause = let bag, clause = demodulate bag clause table in -- 2.39.2