(* $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)
;;
let compute_clause_weight (_,nl,pl,_,_) =
- List.fold_left (fun acc lit -> compute_literal_weight lit + acc) 0 (nl@pl)
+ List.fold_left (fun acc (lit,_) -> compute_literal_weight lit + acc) 0 (nl@pl)
let compute_goal_weight = compute_clause_weight;;
| XGT -> Terms.Gt
| XLT -> Terms.Lt
| XEQ -> Terms.Eq
+ | XINVERTIBLE -> Terms.Invertible
| _ -> assert false
;;
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
;;
let r = aux t1 t2 in
if r = XEQ then (
match t1, t2 with
+ | Terms.Var i, Terms.Var j when i=j -> XEQ
| Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
| _, _ -> XINCOMPARABLE
) else r