From 6332719f74f68beb0501e03f8e8aa6a5e0a78aed Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 25 Nov 2009 13:01:10 +0000 Subject: [PATCH] Exported forward_inference_step --- .../ng_paramodulation/nCicParamod.ml | 22 ++++---- .../ng_paramodulation/nCicParamod.mli | 3 ++ .../components/ng_paramodulation/paramod.ml | 51 ++++++++++++++----- .../components/ng_paramodulation/paramod.mli | 7 +++ 4 files changed, 61 insertions(+), 22 deletions(-) diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 846a576c7..6096d88da 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -11,19 +11,23 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) + +module B(C : NCicBlob.NCicContext): Orderings.Blob + with type t = NCic.term and type input = NCic.term + = Orderings.LPO(NCicBlob.NCicBlob(C)) + +module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C)) + let nparamod rdb metasenv subst context t table = - let module C = - struct + let module C = + struct let metasenv = metasenv let subst = subst - let context = context - end - in - let module B : Orderings.Blob - with type t = NCic.term and type input = NCic.term - = Orderings.LPO(NCicBlob.NCicBlob(C)) + let context = context + end in - let module P = Paramod.Paramod(B) in + let module B = B(C) in + let module P = NCicParamod(C) in let module Pp = Pp.Pp(B) in let bag, maxvar = Terms.empty_bag, 0 in let (bag,maxvar), goals = diff --git a/helm/software/components/ng_paramodulation/nCicParamod.mli b/helm/software/components/ng_paramodulation/nCicParamod.mli index d24e5b57f..067235158 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.mli +++ b/helm/software/components/ng_paramodulation/nCicParamod.mli @@ -11,6 +11,9 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) +module NCicParamod(C : NCicBlob.NCicContext) : Paramod.Paramod +with type t = NCic.term and type input = NCic.term + val nparamod : #NRstatus.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 0dbd6260a..6f76e2ad4 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -20,14 +20,21 @@ module type Paramod = sig type t type input + type state 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 empty_state : state val mk_passive : bag -> input * input -> bag * t Terms.unit_clause val mk_goal : bag -> input * input -> bag * t Terms.unit_clause + val forward_infer_step : + state -> + t Terms.unit_clause -> + int -> + state val paramod : useage:bool -> max_steps:int -> @@ -38,15 +45,6 @@ module type Paramod = 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 - | Error of string - | Timeout of int * B.t Terms.bag - exception Stop of szsontology - type bag = B.t Terms.bag * int module Pp = Pp.Pp (B) module FU = FoUnif.Founif(B) module IDX = Index.Index(B) @@ -68,6 +66,32 @@ module Paramod (B : Orderings.Blob) = struct module WeightPassiveSet = Set.Make(WeightOrderedPassives) module AgePassiveSet = Set.Make(AgeOrderedPassives) + type t = B.t + type input = B.input + type state = + B.t Terms.bag + * int + * Index.Index(B).active_set + * (WeightPassiveSet.t * AgePassiveSet.t) + * B.t Terms.unit_clause list + * (WeightPassiveSet.t * AgePassiveSet.t) + type szsontology = + | Unsatisfiable of (B.t Terms.bag * int * int list) list + | GaveUp + | Error of string + | Timeout of int * B.t Terms.bag + exception Stop of szsontology + type bag = B.t Terms.bag * int + + let empty_state = + Terms.empty_bag, + 0, + ([],IDX.DT.empty), + (WeightPassiveSet.empty,AgePassiveSet.empty), + [], + (WeightPassiveSet.empty,AgePassiveSet.empty) +;; + 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 @@ -172,8 +196,8 @@ module Paramod (B : Orderings.Blob) = struct (add_passive_goals g_passives new_goals) ;; - let forward_infer_step bag maxvar actives passives g_actives - g_passives current iterno = + let forward_infer_step (bag,maxvar,actives,passives,g_actives,g_passives) + current iterno = (* forward step *) (* e = select P * @@ -321,8 +345,9 @@ module Paramod (B : Orderings.Blob) = struct in bag,maxvar,actives,passives,g_actives,g_passives else - forward_infer_step bag maxvar actives passives - g_actives g_passives current iterno + forward_infer_step + (bag,maxvar,actives,passives,g_actives,g_passives) + current iterno in diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index 9cffd9d28..b195e80c9 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -15,14 +15,21 @@ module type Paramod = sig type t type input + type state 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 empty_state : state val mk_passive : bag -> input * input -> bag * t Terms.unit_clause val mk_goal : bag -> input * input -> bag * t Terms.unit_clause + val forward_infer_step : + state -> + t Terms.unit_clause -> + int -> + state val paramod : useage:bool -> max_steps:int -> -- 2.39.2