The current cache is based on imperative lists.
Can it be improved with smarter data structures (e.g. HashTables?)
let compute_unit_clause_weight = compute_unit_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
let compute_unit_clause_weight = compute_unit_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
+ (*CSC: beware! Imperative cache! *)
+ let cache = ref [];;
+
let rec lpo_le s t =
eq_foterm s t || lpo_lt s t
and lpo_lt s t =
let rec lpo_le s t =
eq_foterm s t || lpo_lt s t
and lpo_lt s t =
+ try List.assoc (s,t) !cache
+ with
+ Not_found -> let res =
match s,t with
| _, Terms.Var _ -> false
| Terms.Var i,_ ->
match s,t with
| _, Terms.Var _ -> false
| Terms.Var i,_ ->
compare_args tl1 tl2
| _ -> assert false
end
compare_args tl1 tl2
| _ -> assert false
end
+ in
+ cache := ((s,t),res)::!cache; 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
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