index.cmi: terms.cmi orderings.cmi
foUnif.cmi: terms.cmi orderings.cmi
superposition.cmi: terms.cmi orderings.cmi index.cmi
-stats.cmi: orderings.cmi
+stats.cmi: terms.cmi orderings.cmi
paramod.cmi: terms.cmi orderings.cmi
nCicBlob.cmi: terms.cmi
cicBlob.cmi: terms.cmi
orderings.cmx: terms.cmx pp.cmx orderings.cmi
foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
-index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi
-index.cmx: terms.cmx orderings.cmx foUtils.cmx index.cmi
+index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi foSubst.cmi \
+ index.cmi
+index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx foSubst.cmx \
+ index.cmi
foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi
foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
INTERFACE_FILES = \
terms.mli pp.mli foSubst.mli \
- orderings.mli foUtils.mli index.mli foUnif.mli superposition.mli \
+ orderings.mli foUtils.mli foUnif.mli index.mli superposition.mli \
stats.mli paramod.mli nCicBlob.mli cicBlob.mli nCicProof.mli \
nCicParamod.mli
subst
;;
+(* Sets of variables in s and t are assumed to be disjoint *)
let alpha_eq s t =
let rec equiv subst s t =
let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
let p = Subst.apply_subst subst p in
Terms.Predicate p
in
- let nlit = List.map apply_subst_on_lit nlit in
- let plit = List.map apply_subst_on_lit plit in
+ let nlit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) nlit in
+ let plit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) plit in
let proof =
match proof with
| Terms.Exact t -> Terms.Exact (Subst.apply_subst subst t)
match ty with
| Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
let o = Order.compare_terms l r in
- (vars,Terms.Equation (l, r, ty, o)::literals)
- | _ -> (vars,Terms.Predicate ty::literals)
+ (vars,(Terms.Equation (l, r, ty, o),false)::literals)
+ | _ -> (vars,(Terms.Predicate ty,false)::literals)
in
let varlist = Terms.vars_of_term proofterm in
let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in
module ClauseOT =
struct
- type t = Terms.direction * B.t Terms.clause
+ type t = Terms.direction * (* direction if it is an equality *)
+ bool * (* true if indexed literal is positive *)
+ int * (* position of literal in clause *)
+ B.t Terms.clause
- let compare (d1,uc1) (d2,uc2) =
- let c = Pervasives.compare d1 d2 in
+ let compare (d1,p1,pos1,uc1) (d2,p2,pos2,uc2) =
+ let c = Pervasives.compare (d1,p1,pos1) (d2,p2,pos2) in
if c <> 0 then c else U.compare_clause uc1 uc2
;;
end
module ClauseSet :
- Set.S with type elt = Terms.direction * B.t Terms.clause
+ Set.S with type elt = Terms.direction * (* direction if it is an equality *)
+ bool * (* true if indexed literal is positive *)
+ int * (* position of literal in clause *)
+ B.t Terms.clause
= Set.Make(ClauseOT)
open Discrimination_tree
type dataset = ClauseSet.t
= Make(FotermIndexable)(ClauseSet)
- let index_clause t = function
- | (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c ->
- DT.index t l (Terms.Left2Right, c)
- | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c ->
- DT.index t r (Terms.Right2Left, c)
- | (_,Terms.Equation (l,r,_,Terms.Incomparable),_,_) as c ->
- DT.index
- (DT.index t l (Terms.Left2Right, c))
- r (Terms.Right2Left, c)
- | (_,Terms.Equation (_,r,_,Terms.Eq),_,_) -> assert false
- | (_,Terms.Predicate p,_,_) as c ->
- DT.index t p (Terms.Nodir, c)
+ let index_literal t c is_pos pos = function
+ | Terms.Equation (l,_,_,Terms.Gt) ->
+ DT.index t l (Terms.Left2Right,is_pos,pos,c)
+ | Terms.Equation (_,r,_,Terms.Lt) ->
+ DT.index t r (Terms.Right2Left,is_pos,pos,c)
+ | Terms.Equation (l,r,_,Terms.Incomparable) ->
+ DT.index
+ (DT.index t l (Terms.Left2Right,is_pos,pos,c))
+ r (Terms.Right2Left,is_pos,pos,c)
+ | Terms.Equation (_,_,_,Terms.Eq) -> assert false
+ | Terms.Predicate p ->
+ DT.index t p (Terms.Nodir,is_pos,pos,c)
+ ;;
+
+ let index_clause t (_,nlit,plit,_,_ as c) =
+ let index_iter is_pos (t,pos) (lit,sel) =
+ if sel then index_literal t c is_pos pos lit,pos+1 else t,pos+1
+ in
+ let (res,_) = List.fold_left (index_iter false) (t,0) nlit in
+ fst (List.fold_left (index_iter true) (res,0) plit)
;;
type active_set = B.t Terms.clause list * DT.t
module Index (B : Orderings.Blob) :
sig
module ClauseSet : Set.S with
- type elt = Terms.direction * B.t Terms.clause
+ type elt =
+ Terms.direction * (* direction if it is an equality *)
+ bool * (* true if indexed literal is positive *)
+ int * (* position of literal in clause *)
+ B.t Terms.clause
module FotermIndexable : Discrimination_tree.Indexable with
type constant_name = B.t and
type dataset = ClauseSet.t
val index_clause :
- DT.t -> B.t Terms.clause -> DT.t
+ DT.t -> B.t Terms.clause -> DT.t
type active_set = B.t Terms.clause list * DT.t
HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
in
match
- P.paramod ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0)
+ P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0)
~g_passives:goals ~passives (bag,maxvar)
with
| P.Error _ | P.GaveUp | P.Timeout _ -> []
(* $Id$ *)
-type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
+type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE | XINVERTIBLE
module type Blob =
sig
let w, m = weight_of_term x in
weight_of_polynomial w m
| Terms.Equation (l,r,_,Terms.Eq)
- | Terms.Equation (l,r,_,Terms.Incomparable) ->
+ | Terms.Equation (l,r,_,Terms.Incomparable)
+ | Terms.Equation (l,r,_,Terms.Invertible) ->
let wl, ml = weight_of_term l in
let wr, mr = weight_of_term r in
weight_of_polynomial (wl+wr) (ml@mr)
;;
let compute_clause_weight (_,nl,pl,_,_) =
- List.fold_left (fun acc lit -> compute_literal_weight lit + acc) 0 (nl@pl)
+ List.fold_left (fun acc (lit,_) -> compute_literal_weight lit + acc) 0 (nl@pl)
let compute_goal_weight = compute_clause_weight;;
| XGT -> Terms.Gt
| XLT -> Terms.Lt
| XEQ -> Terms.Eq
+ | XINVERTIBLE -> Terms.Invertible
| _ -> assert false
;;
if aux_ordering B.compare t1 t2 = XLT then XLT else XINCOMPARABLE
| XGE ->
if aux_ordering B.compare t1 t2 = XGT then XGT else XINCOMPARABLE
- | XEQ -> aux_ordering B.compare t1 t2
+ | XEQ -> let res = aux_ordering B.compare t1 t2 in
+ if res = XINCOMPARABLE && are_invertible t1 t2 then XINVERTIBLE
+ else res
| res -> res
;;
let r = aux t1 t2 in
if r = XEQ then (
match t1, t2 with
+ | Terms.Var i, Terms.Var j when i=j -> XEQ
| Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
| _, _ -> XINCOMPARABLE
) else r
type bag = t Terms.bag * int
val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
- val paramod :
+ val paramod :
+ useage:bool ->
max_steps:int ->
?timeout:float ->
bag ->
* new'= demod A'' new *
* P' = P + new' *)
debug "Forward infer step...";
+ debug ("Number of actives : " ^ (string_of_int (List.length (fst actives))));
let bag, maxvar, actives, new_clauses =
Sup.infer_right bag maxvar current actives
in
debug
(Printf.sprintf "Number of passives : %d"
(passive_set_cardinal passives));
- given_clause ~noinfer
+ given_clause ~useage ~noinfer
bag maxvar iterno weight_picks max_steps timeout
actives passives g_actives g_passives
;;
- let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+ let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
let initial_timestamp = Unix.gettimeofday () in
let passives =
add_passive_clauses ~no_weight:true passive_empty_set passives
let g_actives = [] in
let actives = [], IDX.DT.empty in
try
- given_clause ~noinfer:false
+ given_clause ~useage ~noinfer:false
bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
with
| Sup.Success (bag, _, (i,_,_,_)) ->
val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
val paramod :
+ useage:bool ->
max_steps:int ->
?timeout:float ->
bag ->
| Terms.Gt -> "=>="
| Terms.Eq -> "==="
| Terms.Incomparable -> "=?="
+ | Terms.Invertible -> "=<->="
let pp_unit_clause ~formatter:f c =
let (id, l, vars, proof) = c in
(t,occ,ar,goal_occ_nbr t goal,goal_pos t goal)::acc) res []
;;
+ let rec leaf_count = function
+ | Terms.Node l -> List.fold_left (fun acc x -> acc + (leaf_count x)) 0 l
+ | Terms.Leaf _ -> 1
+ | _ -> 0
+ ;;
+
let rec dependencies op clauses acc =
match clauses with
| [] -> acc
else
dependencies op tl acc
else dependencies op tl acc
+ | ((Terms.Node (Terms.Leaf op1::t) as x),y)
+ | (y,(Terms.Node (Terms.Leaf op1::t) as x)) when leaf_count x > leaf_count y ->
+ let rec term_leaves = function
+ | Terms.Node l -> List.fold_left (fun acc x -> acc @ (term_leaves x)) [] l
+ | Terms.Leaf x -> [x]
+ | _ -> []
+ in
+ if List.mem op (List.filter (fun z -> not (B.eq op1 z)) (term_leaves x)) then
+ dependencies op tl (op1::acc)
+ else
+ dependencies op tl acc
| _ -> dependencies op tl acc
;;
- let dependencies op clauses = dependencies op clauses [];;
+ let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;
(* let max_weight_hyp = *)
let rec aux bag pos ctx id = function
| Terms.Leaf _ as t -> f bag t pos ctx id
| Terms.Var _ as t -> bag,t,id
- | Terms.Node l as t->
+ | Terms.Node (hd::l) as t->
let bag,t,id1 = f bag t pos ctx id in
if id = id1 then
let bag, l, _, id =
let bag,newt,id = aux bag newpos newctx id t in
if post = [] then bag, pre@[newt], [], id
else bag, pre @ [newt], List.tl post, id)
- (bag, [], List.tl l, id) l
+ (bag, [hd], List.tl l, id) l
in
bag, Terms.Node l, id
else bag,t,id1
+ | _ -> assert false
in
aux bag pos ctx id t
;;
(IDX.DT.retrieve_generalizations table) subterm
in
list_first
- (fun (dir, (id,lit,vl,_)) ->
+ (fun (dir, is_pos, pos, (id,nlit,plit,vl,_)) ->
match lit with
| Terms.Predicate _ -> assert false
| Terms.Equation (l,r,_,o) ->
prof_demod_s.HExtlib.profile
(Subst.apply_subst subst) newside
in
- if o = Terms.Incomparable then
+ if o = Terms.Incomparable || o = Terms.Invertible then
let o =
prof_demod_o.HExtlib.profile
(Order.compare_terms newside) side in
let subst =
Unif.unification (* (varlist@vl)*) [] subterm side
in
- if o = Terms.Incomparable then
+ if o = Terms.Incomparable || o = Terms.Invertible then
let side = Subst.apply_subst subst side in
let newside = Subst.apply_subst subst newside in
let o = Order.compare_terms side newside in
(all_positions [3]
(fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
r (superposition table vl))
+ | Terms.Equation (l,r,ty,Terms.Invertible)
| Terms.Equation (l,r,ty,Terms.Gt) ->
fold_build_new_clause bag maxvar id Terms.Superposition
(fun _ -> true)
fold_build_new_clause bag maxvar id Terms.Superposition
(filtering Terms.Lt)
(all_positions [2]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
- r (superposition table vl))
+ (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+ l (superposition table vl))
in
bag, maxvar, r_terms @ l_terms
| _ -> assert false
type 'a substitution = (int * 'a foterm) list
-type comparison = Lt | Eq | Gt | Incomparable
+type comparison = Lt | Eq | Gt | Incomparable | Invertible
type rule = Superposition | Demodulation
type direction = Left2Right | Right2Left | Nodir
type 'a clause =
int
- * 'a literal list (* left hand side of the arrow *)
- * 'a literal list (* right hand side of the arrow *)
+ * ('a literal * bool) list (* left hand side of the arrow,
+ with flag for selection *)
+ * ('a literal * bool) list (* right hand side of the arrow,
+ with flag for selection *)
* varlist
* 'a proof
type 'a substitution = (int * 'a foterm) list
-type comparison = Lt | Eq | Gt | Incomparable
+type comparison = Lt | Eq | Gt | Incomparable | Invertible
type rule = Superposition | Demodulation
type 'a clause =
int
- * 'a literal list (* left hand side of the arrow *)
- * 'a literal list (* right hand side of the arrow *)
+ * ('a literal * bool) list (* left hand side of the arrow,
+ with flag for selection *)
+ * ('a literal * bool) list (* right hand side of the arrow,
+ with flag for selection *)
* varlist
* 'a proof
projects / helm.git / commitdiff