CHC: add function to prioritize invariants

Author: sipma

CodeHawk/CHC/cchpre/cCHInvariantFact.ml

@@ -744,3 +744,14 @@ let get_invariant_messages
           let inv = invio#get_invariant invindex in
           let p = LBLOCK [STR "["; INT k; STR "] "; inv#value_to_pretty] in
           p::acci) acc ilist) [] l
+
+
+let prioritize_invariants (f: invariant_int -> bool) (invs: invariant_int list) =
+  List.stable_sort
+    (fun inv1 inv2 ->
+      if f inv1 && f inv2 then
+        0
+      else if f inv1 then
+        -1
+      else
+        1) invs

CodeHawk/CHC/cchpre/cCHInvariantFact.mli

@@ -72,3 +72,15 @@ val mk_invariant_io:
 
 val get_invariant_messages:
   invariant_io_int -> (int * int list) list -> pretty_t list
+
+
+(** [prioritize_invariants f invs] returns the invariants in [invs]
+    sorted such that the invariants for which [(f inv)] is true are
+    listed before other invariants.
+
+    This is useful in the application of invariants in the checkers,
+    where multiple invariants apply to discharge a proof obligation,
+    but some invariants may be preferred over others.
+ *)
+val prioritize_invariants:
+  (invariant_int -> bool) -> invariant_int list -> invariant_int list