((*prerr_endline ("Filtering: " ^
Pp.pp_foterm side ^ " =(< || =)" ^
Pp.pp_foterm newside ^ " coming from " ^
((*prerr_endline ("Filtering: " ^
Pp.pp_foterm side ^ " =(< || =)" ^
Pp.pp_foterm newside ^ " coming from " ^
else
Some (newside, subst, id, dir)
else
Some (newside, subst, id, dir)
;;
let rec demodulate bag (id, literal, vl, pr) table =
;;
let rec demodulate bag (id, literal, vl, pr) table =
match literal with
| Terms.Predicate t -> assert false
| Terms.Equation (l,r,ty,_) ->
match literal with
| Terms.Predicate t -> assert false
| Terms.Equation (l,r,ty,_) ->
debug (lazy "First superpositions");
(* We add current to active clauses so that it can be *
* superposed with itself *)
debug (lazy "First superpositions");
(* We add current to active clauses so that it can be *
* superposed with itself *)