* B.t Terms.substitution
let print s = prerr_endline (Lazy.force s);;
- let debug _ = ();;
+ let debug _ = ();;
+ (* let debug = print;; *)
let enable = true;;
let rec list_first f = function
if filter subst then
let literal =
match t with
- | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP 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
| Terms.Equation (l,r,ty,_) ->
let bag,l,id1 =
visit bag [2]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id l
+ (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ]) id l
(ctx_demod table vl)
in
let bag,_,id2 =
visit bag [3]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 r
+ (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ]) id1 r
(ctx_demod table vl)
in
let cl,_,_ = Terms.get_from_bag id2 bag in
match lit with
| Terms.Predicate _ -> assert false
| Terms.Equation (l,r,ty,_) ->
- Terms.Node [Terms.Leaf B.eqP; ty; l ; r]
+ Terms.Node [Terms.Leaf (B.eqP()); ty; l ; r]
in
try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true
with FoUnif.UnificationFailure _ -> false
let reverse = (dir = Terms.Left2Right) = b in
let l, r, proof_rewrite_dir = if reverse then l,r,Terms.Left2Right
else r,l, Terms.Right2Left in
- (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl)
+ (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ], vl)
in
let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in
let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in
- let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in
+ let t = Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ] in
let locked_vars = if unify then [] else vl in
let rec aux = function
| [] -> None
match rewrite_eq ~unify l r ty vl table with
| None -> None
| Some (id2, dir, subst) ->
- let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in
+ let id_t = Terms.Node [ Terms.Leaf (B.eqP()); ty; r; r ] in
build_new_clause bag maxvar (fun _ -> true)
Terms.Superposition id_t subst id id2 [2] dir
;;
let newsubst = Subst.concat subst1 subst in
let id_t =
FoSubst.apply_subst newsubst
- (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r])
+ (Terms.Node[Terms.Leaf (B.eqP());ty;contextl r;contextr r])
in
(match
build_new_clause_reloc bag maxvar (fun _ -> true)
fold_build_new_clause bag maxvar id Terms.Superposition
(fun _ -> true)
(all_positions [3]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+ (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)
(all_positions [2]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+ (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ])
l (superposition table vl))
| Terms.Equation (l,r,ty,Terms.Incomparable) ->
let filtering avoid subst = (* Riazanov: p.33 condition (iv) *)
fold_build_new_clause bag maxvar id Terms.Superposition
(filtering Terms.Gt)
(all_positions [3]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+ (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ])
r (superposition table vl))
in
let bag, maxvar, l_terms =
fold_build_new_clause bag maxvar id Terms.Superposition
(filtering Terms.Lt)
(all_positions [2]
- (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+ (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ])
l (superposition table vl))
in
bag, maxvar, r_terms @ l_terms