struct
module IDX = Index.Index(B)
module Unif = FoUnif.Founif(B)
- module Subst = FoSubst (*.Subst(B)*)
+ module Subst = FoSubst
module Order = Orderings.Orderings(B)
module Utils = FoUtils.Utils(B)
module Pp = Pp.Pp(B)
| t -> Terms.Predicate t
in
let bag, uc =
- Utils.add_to_bag bag (0, literal, vars_of_term t, proof)
+ Terms.add_to_bag (0, literal, vars_of_term t, proof) bag
in
Some (bag, uc)
else
;;
let demodulate_once ~jump_to_right bag (id, literal, vl, pr) table =
- (* debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));*)
match literal with
| Terms.Predicate t -> assert false
| Terms.Equation (l,r,ty,_) ->
;;
let rec orphan_murder bag acc i =
- match Terms.M.find i bag with
+ match Terms.get_from_bag i bag with
| (_,_,_,Terms.Exact _),discarded -> (discarded,acc)
| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true -> (true,acc)
| (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false ->
let simplify table maxvar bag clause =
match simplify table maxvar bag clause with
- | bag, None -> let (id,_,_,_) = clause in
- Terms.M.add id (clause,true) bag, None
+ | bag, None ->
+ Terms.replace_in_bag (clause,true) bag, None
| bag, Some clause -> bag, Some clause
(*let (id,_,_,_) = clause in
if orphan_murder bag clause then
let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
(* We need to put fresh_current into the bag so that all *
* variables clauses refer to are known. *)
- let bag, fresh_current = Utils.add_to_bag bag fresh_current in
+ let bag, fresh_current = Terms.add_to_bag fresh_current bag in
(* We superpose current with active clauses *)
let bag, maxvar, additional_new_clauses =
superposition_with_table bag maxvar fresh_current atable