terms.cmi:
pp.cmi: terms.cmi
foSubst.cmi: terms.cmi
+orderings.cmi: terms.cmi
foUtils.cmi: terms.cmi
-foUnif.cmi: terms.cmi
index.cmi: terms.cmi
-orderings.cmi: terms.cmi
+foUnif.cmi: terms.cmi
superposition.cmi: terms.cmi index.cmi
nCicBlob.cmi: terms.cmi
cicBlob.cmi: terms.cmi
pp.cmx: terms.cmx pp.cmi
foSubst.cmo: terms.cmi foSubst.cmi
foSubst.cmx: terms.cmx foSubst.cmi
-foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
-foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
-foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi
-foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi
-index.cmo: terms.cmi foUtils.cmi index.cmi
-index.cmx: terms.cmx foUtils.cmx index.cmi
orderings.cmo: terms.cmi orderings.cmi
orderings.cmx: terms.cmx orderings.cmi
-superposition.cmo: terms.cmi index.cmi superposition.cmi
-superposition.cmx: terms.cmx index.cmx superposition.cmi
+foUtils.cmo: terms.cmi orderings.cmi index.cmi foSubst.cmi foUtils.cmi
+foUtils.cmx: terms.cmx orderings.cmx index.cmx foSubst.cmx foUtils.cmi
+index.cmo: terms.cmi foUtils.cmi index.cmi
+index.cmx: terms.cmx foUtils.cmx index.cmi
+foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi
+foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi
+superposition.cmo: terms.cmi orderings.cmi index.cmi foUtils.cmi foUnif.cmi \
+ foSubst.cmi superposition.cmi
+superposition.cmx: terms.cmx orderings.cmx index.cmx foUtils.cmx foUnif.cmx \
+ foSubst.cmx superposition.cmi
nCicBlob.cmo: terms.cmi nCicBlob.cmi
nCicBlob.cmx: terms.cmx nCicBlob.cmi
cicBlob.cmo: terms.cmi cicBlob.cmi
cicBlob.cmx: terms.cmx cicBlob.cmi
-paramod.cmo: terms.cmi superposition.cmi pp.cmi nCicBlob.cmi index.cmi \
+paramod.cmo: superposition.cmi pp.cmi nCicBlob.cmi index.cmi foUtils.cmi \
foUnif.cmi paramod.cmi
-paramod.cmx: terms.cmx superposition.cmx pp.cmx nCicBlob.cmx index.cmx \
+paramod.cmx: superposition.cmx pp.cmx nCicBlob.cmx index.cmx foUtils.cmx \
foUnif.cmx paramod.cmi
pp.cmi: terms.cmi
foSubst.cmi: terms.cmi
orderings.cmi: terms.cmi
-foUtils.cmi: terms.cmi
+foUtils.cmi: terms.cmi index.cmi
foUnif.cmi: terms.cmi
index.cmi: terms.cmi
superposition.cmi: terms.cmi index.cmi
foSubst.cmx: terms.cmx foSubst.cmi
orderings.cmo: terms.cmi orderings.cmi
orderings.cmx: terms.cmx orderings.cmi
-foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
-foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
+foUtils.cmo: terms.cmi orderings.cmi index.cmi foSubst.cmi foUtils.cmi
+foUtils.cmx: terms.cmx orderings.cmx index.cmx foSubst.cmx foUtils.cmi
foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi
foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi
index.cmo: terms.cmi foUtils.cmi index.cmi
nCicBlob.cmx: terms.cmx nCicBlob.cmi
cicBlob.cmo: terms.cmi cicBlob.cmi
cicBlob.cmx: terms.cmx cicBlob.cmi
-paramod.cmo: terms.cmi superposition.cmi pp.cmi nCicBlob.cmi index.cmi \
+paramod.cmo: superposition.cmi pp.cmi nCicBlob.cmi index.cmi foUtils.cmi \
foUnif.cmi paramod.cmi
-paramod.cmx: terms.cmx superposition.cmx pp.cmx nCicBlob.cmx index.cmx \
+paramod.cmx: superposition.cmx pp.cmx nCicBlob.cmx index.cmx foUtils.cmx \
foUnif.cmx paramod.cmi
INTERFACE_FILES = \
terms.mli pp.mli foSubst.mli \
- orderings.mli foUtils.mli foUnif.mli index.mli superposition.mli \
+ orderings.mli foUtils.mli index.mli foUnif.mli superposition.mli \
nCicBlob.mli cicBlob.mli paramod.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
let embed t = assert false;;
- let is_eq_predicate = assert false
- let saturate = assert false
+ let eqP = assert false;;
+
+ let saturate = assert false;;
end
in
let lit =
match ty with
- | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.is_eq_predicate eq ->
+ | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
let o = Order.compare_terms l r in
Terms.Equation (l, r, ty, o)
| t -> Terms.Predicate t
fresh_unit_clause maxvar (mk_id (), lit, varlist, proof)
;;
+ let add_to_bag =
+ let id = ref 0 in
+ fun bag (_,lit,vl,proof) ->
+ incr id;
+ let clause = (!id, lit, vl, proof) in
+ let bag = Terms.M.add !id clause bag in
+ bag, clause
+ ;;
+
+ let empty_bag = Terms.M.empty ;;
+
end
val eq_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> bool
val compare_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> int
+(*
val fresh_unit_clause :
int -> B.t Terms.unit_clause -> B.t Terms.unit_clause * int
+*)
+
+ (* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *)
+ val relocate : int -> int list -> int * int list * B.t Terms.substitution
+
+ (* also gives a fresh ID to the clause *)
+ val add_to_bag :
+ B.t Terms.bag -> B.t Terms.unit_clause ->
+ B.t Terms.bag * B.t Terms.unit_clause
+
+ val empty_bag : B.t Terms.bag
+
end
type dataset = ClauseSet.t
= Make(FotermIndexable)(ClauseSet)
+ let index_unit_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)
+ ;;
+
end
type input = B.t Terms.foterm and
type data = ClauseSet.elt and
type dataset = ClauseSet.t
+
+ val index_unit_clause :
+ DT.t -> B.t Terms.unit_clause -> DT.t
end
proof, sty
;;
- let is_eq_predicate t = assert false;;
+ let eqP =
+ let r =
+ OCic2NCic.reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
+ in
+ NCic.Const r
+ ;;
end
| Terms.Predicate t ->
let w, m = weight_of_term t in
weight_of_polynomial w m
- | Terms.Equation (_,x,_,Terms.Lt)
+ | Terms.Equation (_,x,_,Terms.Lt)
| Terms.Equation (x,_,_,Terms.Gt) ->
let w, m = weight_of_term x in
weight_of_polynomial w m
(* This order relation should be:
* - stable for instantiation
* - total on ground terms
+ *
*)
val compare_terms :
B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison
-let nparamod metasenv subst context t =
+let nparamod metasenv subst context t table =
let module C = struct
let metasenv = metasenv
let subst = subst
in
let module B = NCicBlob.NCicBlob(C) in
let module Pp = Pp.Pp (B) in
- let res = B.embed t in
let module FU = FoUnif.Founif(B) in
let module IDX = Index.Index(B) in
let module Sup = Superposition.Superposition(B) in
+ let module Utils = FoUtils.Utils(B) in
+(*
let test_unification _ = function
| Terms.Node [_; _; lhs; rhs] ->
prerr_endline "Unification test :";
prerr_endline (Pp.pp_foterm res);
prerr_endline "Substitution :";
prerr_endline (Pp.pp_substitution subst)
+*)
+ let mk_clause maxvar t =
+ let ty = B.embed t in
+ let proof = B.embed (NCic.Rel ~-1) in
+ Utils.mk_unit_clause maxvar ty proof
+ in
+ let clause, maxvar = mk_clause 0 t in
+ prerr_endline "Input clause :";
+ prerr_endline (Pp.pp_unit_clause clause);
+ let bag = Utils.empty_bag in
+ let active_clauses, maxvar =
+ List.fold_left
+ (fun (cl,maxvar) t ->
+ let c, m = mk_clause maxvar t in
+ c::cl, m)
+ ([],maxvar) table
+ in
+ let table =
+ List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
+ in
+ let bag, maxvar, newclauses =
+ Sup.superposition_right_with_table bag maxvar clause table
+ in
+ prerr_endline "Output clauses :";
+ List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
;;
-val nparamod : NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> unit
+val nparamod :
+ NCic.metasenv -> NCic.substitution -> NCic.context ->
+ NCic.term -> NCic.term list ->
+ unit
module Unif = FoUnif.Founif(B)
module Subst = FoSubst.Subst(B)
module Order = Orderings.Orderings(B)
+ module Utils = FoUtils.Utils(B)
- let all_positions t f =
+ let all_positions pos ctx t f =
let rec aux pos ctx = function
- | Terms.Leaf a as t -> f t pos ctx
- | Terms.Var i -> []
+ | Terms.Leaf _ as t -> f t pos ctx
+ | Terms.Var _ -> []
| Terms.Node l as t->
let acc, _, _ =
List.fold_left
in
acc
in
- aux [] (fun x -> x) t
+ aux pos ctx t
;;
let superposition_right table varlist subterm pos context =
match lit with
| Terms.Predicate _ -> assert false
| Terms.Equation (l,r,_,o) ->
+ assert(o <> Terms.Eq);
let side, newside = if dir=Terms.Left2Right then l,r else r,l in
try
let subst, varlist =
Unif.unification (varlist@vl) [] subterm side
in
- Some (context newside, subst, varlist, id, pos, dir)
+ if o = Terms.Incomparable 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
+ (* XXX: check Riazanov p. 33 (iii) *)
+ if o <> Terms.Lt && o <> Terms.Eq then
+ Some (context newside, subst, varlist, id, pos, dir)
+ else
+ None
+ else
+ Some (context newside, subst, varlist, id, pos, dir)
with FoUnif.UnificationFailure _ -> None)
(IDX.ClauseSet.elements cands)
;;
- let superposition_right_step bag (id,selected,vl,_) table =
+ let build_new_clause bag maxvar filter t subst vl id id2 pos dir =
+ let maxvar, vl, relocsubst = Utils.relocate maxvar vl in
+ let subst = Subst.concat relocsubst subst in
+ let proof = Terms.Step(Terms.SuperpositionRight,id,id2,dir,pos,subst) in
+ let t = Subst.apply_subst subst t in
+ if filter t then
+ let literal =
+ match t with
+ | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
+ let o = Order.compare_terms l r in
+ Terms.Equation (l, r, ty, o)
+ | t -> Terms.Predicate t
+ in
+ let bag, uc =
+ Utils.add_to_bag bag (0, literal, vl, proof)
+ in
+ Some (bag, maxvar, uc)
+ else
+ None
+ ;;
+
+ let fold_build_new_clause bag maxvar id filter res =
+ let maxvar, bag, new_clauses =
+ List.fold_left
+ (fun (maxvar, bag, acc) (t,subst,vl,id2,pos,dir) ->
+ match build_new_clause bag maxvar filter t subst vl id id2 pos dir
+ with Some (bag, maxvar, uc) -> maxvar, bag, uc::acc
+ | None -> maxvar, bag, acc)
+ (maxvar, bag, []) res
+ in
+ bag, maxvar, new_clauses
+ ;;
+
+ let superposition_right_with_table bag maxvar (id,selected,vl,_) table =
match selected with
| Terms.Predicate _ -> assert false
- | Terms.Equation (l,r,ty,Terms.Lt) ->
- let res = all_positions r (superposition_right table vl) in
- let _new_clauses =
- List.map
- (fun (r,subst,vl,id2,pos,dir) ->
- let proof =
- Terms.Step(Terms.SuperpositionRight,id,id2, dir, pos, subst)
- in
- let r = Subst.apply_subst subst r in
- let l = Subst.apply_subst subst l in
- let ty = Subst.apply_subst subst ty in
- let o = Order.compare_terms l r in
- (* can unif compute the right vl for both sides? *)
- (0, Terms.Equation (l,r,ty,o), vl, proof))
- res
- in
- (* fresh ID and metas and compute orientataion of new_clauses *)
- assert false
- | Terms.Equation (l,r,_,Terms.Gt) -> assert false
+ | Terms.Equation (l,r,ty,Terms.Lt) ->
+ fold_build_new_clause bag maxvar id (fun _ -> true)
+ (all_positions [3]
+ (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+ r (superposition_right table vl))
+ | Terms.Equation (l,r,ty,Terms.Gt) ->
+ fold_build_new_clause bag maxvar id (fun _ -> true)
+ (all_positions [2]
+ (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+ l (superposition_right table vl))
+ | Terms.Equation (l,r,ty,Terms.Incomparable) ->
+ fold_build_new_clause bag maxvar id
+ (function (* Riazanov: p.33 condition (iv) *)
+ | Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq ->
+ Order.compare_terms l r <> Terms.Eq
+ | _ -> assert false)
+ ((all_positions [3]
+ (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+ r (superposition_right table vl)) @
+ (all_positions [2]
+ (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+ l (superposition_right table vl)))
| _ -> assert false
;;
module Superposition (B : Terms.Blob) :
sig
- val superposition_right_step :
+ val superposition_right_with_table :
B.t Terms.bag ->
+ int -> (* maxvar *)
B.t Terms.unit_clause ->
Index.Index(B).DT.t ->
- B.t Terms.bag * B.t Terms.unit_clause list
+ B.t Terms.bag * int * B.t Terms.unit_clause list
end
type t
val eq : t -> t -> bool
val compare : t -> t -> int
- val is_eq_predicate : t -> bool
+ val eqP : t
val pp : t -> string
val embed : t -> t foterm
val saturate : t -> t -> t foterm * t foterm
type comparison = Lt | Eq | Gt | Incomparable
type rule = SuperpositionRight | SuperpositionLeft | Demodulation
+
+(* A Discrimination tree is a map: foterm |-> (dir, clause) *)
type direction = Left2Right | Right2Left | Nodir
+
type position = int list
type 'a proof =
module M : Map.S with type key = int
-type 'a bag = 'a unit_clause M.t
+type 'a bag = 'a unit_clause M.t
module type Blob =
sig
type t
val eq : t -> t -> bool
val compare : t -> t -> int
- val is_eq_predicate : t -> bool
+ val eqP : t
(* TODO: consider taking in input an imperative buffer for Format
* val pp : Format.formatter -> t -> unit
* *)
projects / helm.git / commitdiff