let compute_unit_clause_weight = compute_unit_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
- let rec lpo s t =
+ (*CSC: beware! Imperative cache! *)
+ let cache = Hashtbl.create 101
+
+ let rec lpo_le s t =
+ eq_foterm s t || lpo_lt s t
+
+ and lpo_lt s t =
+ try Hashtbl.find cache (s,t)
+ with
+ Not_found -> let res =
match s,t with
- | s, t when eq_foterm s t ->
- XEQ
- | Terms.Var _, Terms.Var _ ->
- XINCOMPARABLE
- | _, Terms.Var i ->
- if (List.mem i (Terms.vars_of_term s)) then XGT
- else XINCOMPARABLE
+ | _, Terms.Var _ -> false
| Terms.Var i,_ ->
- if (List.mem i (Terms.vars_of_term t)) then XLT
- else XINCOMPARABLE
+ if (List.mem i (Terms.vars_of_term t)) then true
+ else false
+ | Terms.Leaf a, Terms.Leaf b -> B.compare a b < 0
+ | Terms.Leaf _, Terms.Node _ -> true (* we assume unary constants
+ are smaller than constants with higher arity *)
+ | Terms.Node _, Terms.Leaf _ -> false
+ | Terms.Node [],_
+ | _,Terms.Node [] -> assert false
| Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
- let rec ge_subterm t ol = function
- | [] -> (false, ol)
- | x::tl ->
- let res = lpo x t in
- match res with
- | XGT | XEQ -> (true,res::ol)
- | o -> ge_subterm t (o::ol) tl
- in
- let (res, l_ol) = ge_subterm t [] tl1 in
- if res then XGT
- else let (res, r_ol) = ge_subterm s [] tl2 in
- if res then XLT
- else begin
- let rec check_subterms t = function
- | _,[] -> true
- | o::ol,_::tl ->
- if o = XLT then check_subterms t (ol,tl)
- else false
- | [], x::tl ->
- if lpo x t = XLT then check_subterms t ([],tl)
- else false
- in
- match aux_ordering B.compare hd1 hd2 with
- | XGT -> if check_subterms s (r_ol,tl2) then XGT
- else XINCOMPARABLE
- | XLT -> if check_subterms t (l_ol,tl1) then XLT
- else XINCOMPARABLE
- | XEQ ->
- (try
- let lex = List.fold_left2
- (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
- XEQ tl1 tl2
- in
- (match lex with
- | XGT ->
- if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
- else XINCOMPARABLE
- | XLT ->
- if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
- else XINCOMPARABLE
- | o -> o)
- with Invalid_argument _ -> (* assert false *)
- XINCOMPARABLE)
- | XINCOMPARABLE -> XINCOMPARABLE
- | _ -> assert false
- end
- | _,_ -> aux_ordering B.compare s t
-
+ if List.exists (lpo_le s) tl2 then true
+ else
+ begin
+ match aux_ordering B.compare hd1 hd2 with
+ | XINCOMPARABLE
+ | XGT -> false
+ | XLT -> List.for_all (fun x -> lpo_lt x t) tl1
+ | XEQ ->
+ let rec compare_args l1 l2 =
+ match l1,l2 with
+ | [],_
+ | _,[] -> false
+ | a1::tl1,a2::tl2 ->
+ if eq_foterm a1 a2 then compare_args tl1 tl2
+ else if lpo_lt a1 a2 then List.for_all (fun x -> lpo_lt x t) tl1
+ else false
+ in
+ compare_args tl1 tl2
+ | _ -> assert false
+ end
+ in
+ Hashtbl.add cache (s,t) res; res
+ ;;
+
+ let lpo s t =
+ let res =
+ if eq_foterm s t then XEQ
+ else if lpo_lt s t then XLT
+ else if lpo_lt t s then XGT
+ else XINCOMPARABLE
+ in
+ Hashtbl.clear cache; res
;;
+
let compare_terms = compare_terms lpo;;