type data = ClauseSet.elt and
type dataset = ClauseSet.t
= Make(FotermIndexable)(ClauseSet)
-
- let are_invertible maxvar varlist l r =
- let _,_,subst = U.relocate maxvar varlist FoSubst.id_subst in
- let l = FoSubst.apply_subst subst l in
- try (ignore(Unif.alpha_eq l r);true) with
- FoUnif.UnificationFailure _ -> false
let index_unit_clause maxvar t = function
| (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c ->
DT.index
(DT.index t l (Terms.Left2Right, c))
r (Terms.Right2Left, c)
+ | (_,Terms.Equation (l,r,_,Terms.Invertible),vl,_) as c ->
+ DT.index t l (Terms.Left2Right, c)
| (_,Terms.Equation (_,r,_,Terms.Eq),_,_) -> assert false
| (_,Terms.Predicate p,_,_) as c ->
DT.index t p (Terms.Nodir, c)
(* $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)
| XGT -> Terms.Gt
| XLT -> Terms.Lt
| XEQ -> Terms.Eq
+ | XINVERTIBLE -> Terms.Invertible
| _ -> assert false
;;
let eq_foterm = eq_foterm B.eq;;
+exception UnificationFailure of string Lazy.t;;
+
+
+(* DUPLICATE CODE FOR TESTS (see FoUnif) *)
+ let alpha_eq s t =
+ let rec equiv subst s t =
+ let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s
+ and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t
+
+ in
+ match s, t with
+ | s, t when eq_foterm s t -> subst
+ | Terms.Var i, Terms.Var j
+ when (not (List.exists (fun (_,k) -> k=t) subst)) ->
+ let subst = FoSubst.build_subst i t subst in
+ subst
+ | Terms.Node l1, Terms.Node l2 -> (
+ try
+ List.fold_left2
+ (fun subst' s t -> equiv subst' s t)
+ subst l1 l2
+ with Invalid_argument _ ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ )
+ | _, _ ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ in
+ equiv FoSubst.id_subst s t
+;;
+
+let relocate maxvar varlist subst =
+ List.fold_right
+ (fun i (maxvar, varlist, s) ->
+ maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s)
+ varlist (maxvar+1, [], subst)
+ ;;
+
+ let are_invertible l r =
+ let varlist = Terms.vars_of_term l in
+ let maxvar = List.fold_left max 0 varlist in
+ let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
+ let l = FoSubst.apply_subst subst l in
+ try (ignore(alpha_eq l r);true) with
+ UnificationFailure _ -> false
+
let compute_unit_clause_weight = compute_unit_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
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
;;
* 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
(bag,maxvar,[]) g_actives
in
let bag = Terms.replace_in_bag (current,false,iterno) bag in
+ (* prerr_endline (Pp.pp_bag bag); *)
bag, maxvar, actives,
add_passive_clauses passives new_clauses, g_actives,
add_passive_goals g_passives new_goals
| Terms.Gt -> "=>="
| Terms.Eq -> "==="
| Terms.Incomparable -> "=?="
+ | Terms.Invertible -> "=<->="
let pp_unit_clause ~formatter:f c =
let (id, l, vars, proof) = c in
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 substitution = (int * 'a foterm) list
-type comparison = Lt | Eq | Gt | Incomparable
+type comparison = Lt | Eq | Gt | Incomparable | Invertible
type rule = Superposition | Demodulation
projects / helm.git / commitdiff