end
module NCicBlob(C : NCicContext) : Terms.Blob
-with type t = NCic.term and type input = NCic.term = struct
+with type t = NCic.term = struct
type t = NCic.term
let pp t =
NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
- type input = NCic.term
-
- let rec embed = function
- | NCic.Meta (i,_) -> Terms.Var i, [i]
- | NCic.Appl l ->
- let rec aux acc l = function
- |[] -> acc@l
- |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl
- in
- let res,vars = List.fold_left
- (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
- in (Terms.Node (List.rev res)), vars
- | t -> Terms.Leaf t, []
- ;;
-
- let embed t = fst (embed t) ;;
-
- let saturate t ty =
- let sty, _, args =
- NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context
- ty 0
- in
- let proof =
- if args = [] then Terms.Leaf t
- else Terms.Node (Terms.Leaf t :: List.map embed args)
- in
- let sty = embed sty in
- proof, sty
- ;;
-
let eqP =
let r =
OCic2NCic.reference_of_oxuri
end
module NCicBlob(C : NCicContext) : Terms.Blob
-with type t = NCic.term and type input = NCic.term
+with type t = NCic.term
(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
-let nparamod rdb metasenv subst context t table =
+let nparamod rdb metasenv subst context (g_t,g_ty) table =
let module C =
struct
let metasenv = metasenv
end
in
let module B : Orderings.Blob
- with type t = NCic.term and type input = NCic.term
+ with type t = NCic.term
= Orderings.NRKBO(NCicBlob.NCicBlob(C))
in
let module P = Paramod.Paramod(B) in
let module Pp = Pp.Pp(B) in
- let bag, maxvar = Terms.empty_bag, 0 in
- let (bag,maxvar), passives =
+
+ let rec embed = function
+ | NCic.Meta (i,_) -> Terms.Var i, [i]
+ | NCic.Appl l ->
+ let rec aux acc l = function
+ |[] -> acc@l
+ |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl
+ in
+ let res,vars = List.fold_left
+ (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
+ in (Terms.Node (List.rev res)), vars
+ | t -> Terms.Leaf t, []
+ in
+
+ let embed t = fst (embed t) in
+
+ let saturate ~is_goal t ty =
+ let sty, _, args =
+ NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context ty 0
+ in
+ let proof =
+ if args = [] then Terms.Leaf t
+ else Terms.Node (Terms.Leaf t :: List.map embed args)
+ in
+ let sty = embed sty in
+ proof, if is_goal then [sty],[] else [],[sty]
+ in
+ let goal = saturate ~is_goal:true g_t g_ty in
+ let hypotheses = List.map (fun (t,ty) -> saturate ~is_goal:false t ty) table in
+ (*let (bag,maxvar), passives =
HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table
in
let (bag,maxvar), goals =
HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
- in
+ in*)
match
- P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0)
- ~g_passives:goals ~passives (bag,maxvar)
+ P.paramod ~useage:true ~max_steps:max_int ~print_problem:true
+ goal hypotheses
with
| P.Error _ | P.GaveUp | P.Timeout _ -> []
| P.Unsatisfiable solutions ->
let get_literal id =
let (_, nlit, plit, vl, proof),_,_ = Terms.get_from_bag id bag in
let lit = match nlit,plit with
- | [],[Terms.Equation (l,r,ty,_),_] ->
+ | [Terms.Equation (l,r,ty,_),_],[]
+ | [],[Terms.Equation (l,r,ty,_),_] ->
Terms.Node [ Terms.Leaf eqP(); ty; l; r]
| _ -> assert false
in
end
module NRKBO (B : Terms.Blob) : Blob
-with type t = B.t and type input = B.input
+with type t = B.t
module KBO (B : Terms.Blob) : Blob
-with type t = B.t and type input = B.input
+with type t = B.t
-module LPO (B : Terms.Blob) : Blob
-with type t = B.t and type input = B.input
+module LPO (B : Terms.Blob) : Blob
+with type t = B.t
module type Paramod =
sig
type t
- type input
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 mk_passive : bag -> input * input -> bag * t Terms.clause
- val mk_goal : bag -> input * input -> bag * t Terms.clause
val paramod :
useage:bool ->
max_steps:int ->
+ print_problem:bool ->
?timeout:float ->
- bag ->
- g_passives:t Terms.clause list ->
- passives:t Terms.clause list -> szsontology
+ t Terms.foterm * (t Terms.foterm list * t Terms.foterm list) ->
+ (t Terms.foterm * (t Terms.foterm list * t Terms.foterm list)) list -> szsontology
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
else WeightPassiveSet.min_elt passives_w
;;
- let mk_clause bag maxvar (t,ty) =
- let (proof,ty) = B.saturate t ty in
- let c, maxvar = Utils.mk_clause maxvar [] [ty] proof in
- let bag, c = Terms.add_to_bag c bag in
- (bag, maxvar), c
- ;;
-
- let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
- let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
-
(* TODO : global age over facts and goals (without comparing weights) *)
let select ~use_age passives g_passives =
if is_passive_set_empty passives then begin
actives passives g_actives g_passives
;;
- let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+ let paramod ~useage ~max_steps ~print_problem ?timeout goal hypotheses =
let initial_timestamp = Unix.gettimeofday () in
+ let bag = Terms.empty_bag in
+ let maxvar = 0 in
+ let build_clause (bag,maxvar,l) (t,(nlit,plit)) =
+ let c,maxvar = Utils.mk_clause maxvar nlit plit t in
+ let bag,c = Terms.add_to_bag c bag in
+ (bag,maxvar,c::l)
+ in
+ let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in
+ let bag,maxvar,goals = build_clause (bag,maxvar,[]) goal in
+ let goal = match goals with | [g] -> g | _ -> assert false in
let passives =
- add_passive_clauses ~no_weight:true passive_empty_set passives
+ add_passive_clauses ~no_weight:true passive_empty_set hypotheses
in
let g_passives =
- add_passive_goals ~no_weight:true passive_empty_set g_passives
+ add_passive_goal ~no_weight:true passive_empty_set goal
in
let g_actives = [] in
let actives = [], IDX.DT.empty in
+ if print_problem then begin
+ prerr_endline "Facts:";
+ List.iter (fun x -> prerr_endline (" " ^ Pp.pp_clause x)) hypotheses;
+ prerr_endline "Goal:";
+ prerr_endline (" " ^ Pp.pp_clause goal);
+ end;
try
given_clause ~useage ~noinfer:false
bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
module type Paramod =
sig
type t
- type input
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 mk_passive : bag -> input * input -> bag * t Terms.clause
- val mk_goal : bag -> input * input -> bag * t Terms.clause
val paramod :
useage:bool ->
max_steps:int ->
+ print_problem:bool ->
?timeout:float ->
- bag ->
- g_passives:t Terms.clause list ->
- passives:t Terms.clause list -> szsontology
+ t Terms.foterm * (t Terms.foterm list * t Terms.foterm list) ->
+ (t Terms.foterm * (t Terms.foterm list * t Terms.foterm list)) list -> szsontology
end
module Paramod ( B : Orderings.Blob ) : Paramod
-with type t = B.t and type input = B.input
+with type t = B.t
struct
module SymbMap = Map.Make(B)
+ module Pp = Pp.Pp(B)
let rec occ_nbr t acc = function
| Terms.Leaf u when B.eq t u -> 1+acc
match l with
| [] -> acc
| (_,nlit,plit,_,_)::tl ->
- match nlit,plit with
- | [],[Terms.Equation (l,r,_,_),_] ->
- parse_symbols (aux (aux acc l) r) tl
- | _ -> assert false;
+ let acc = List.fold_left (fun acc t ->
+ match t with
+ | Terms.Equation (l,r,_,_),_ ->
+ (aux (aux acc l) r)
+ | _ -> assert false) acc (nlit@plit)
+ in
+ parse_symbols acc tl
;;
let goal_pos t goal =
else
dependencies op tl acc
| _ -> dependencies op tl acc)
- | _ -> assert false
+ | _ -> [] (* TODO : compute dependencies for clauses *)
;;
let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;
let demodulate_once ~jump_to_right bag (id, nlit, plit, vl, pr) table =
match nlit,plit with
+ |[literal,_], []
|[],[literal,_] ->
(match literal with
| Terms.Predicate t -> assert false
| _, [], [Terms.Equation (l,r,_,_),_], vl, proof when unify ->
(try ignore(Unif.unification (* vl *) [] l r); true
with FoUnif.UnificationFailure _ -> false)
- | _, [], [Terms.Equation (_,_,_,_),_], _, _ -> false
- | _ -> assert false
+ | _ -> false
;;
let build_new_clause bag maxvar filter rule t subst id id2 pos dir =
val compare : t -> t -> int
val eqP : t
val pp : t -> string
- type input
- val embed : input -> t foterm
- val saturate : input -> input -> t foterm * t foterm
+
end
* *)
val pp : t -> string
- type input
- val embed : input -> t foterm
- (* saturate [proof] [type] -> [proof] * [type] *)
- val saturate : input -> input -> t foterm * t foterm
-
end
projects / helm.git / commitdiff