src/Tools/Argo/argo_heap.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Argo/argo_heap.ML	Thu Sep 29 20:54:44 2016 +0200
@@ -0,0 +1,186 @@
+(*  Title:      Tools/Argo/argo_heap.ML
+    Author:     Sascha Boehme
+
+A maximum-priority heap for literals with integer priorities and with inverse indices.
+The heap is intended to be used as VSIDS-like decision heuristics. This implementation
+is based on pairing heaps described in:
+
+  Chris Okasaki. Purely Functional Data Structures. Chapter 5.
+  Cambridge University Press, 1998.
+*)
+
+signature ARGO_HEAP =
+sig
+  type heap
+  val heap: heap
+  val insert: Argo_Lit.literal -> heap -> heap
+  val extract: heap -> (Argo_Lit.literal * heap) option
+  val increase: Argo_Lit.literal -> heap -> heap
+  val count: Argo_Lit.literal -> heap -> heap
+  val decay: heap -> heap
+  val rebuild: (Argo_Term.term -> bool) -> heap -> heap
+end
+
+structure Argo_Heap: ARGO_HEAP =
+struct
+
+(* heuristic activity constants *)
+
+val min_incr = 128
+fun decay_incr i = (i * 11) div 10
+val max_activity = Integer.pow 24 2
+val activity_rescale = Integer.pow 14 2
+
+
+(* data structures and basic operations *)
+
+datatype tree = E | T of Argo_Term.term * bool * tree list
+
+datatype parent = None | Root | Some of Argo_Term.term
+
+type heap = {
+  incr: int, (* the increment to apply in an increase operation *)
+  vals: ((int * int) * parent) Argo_Termtab.table, (* weights and parents of the stored terms *)
+  tree: tree} (* the pairing heap of literals; note: the tree caches literal polarities *)
+
+fun mk_heap incr vals tree: heap = {incr=incr, vals=vals, tree=tree}
+fun mk_heap' incr (tree, vals) = mk_heap incr vals tree
+
+val heap = mk_heap min_incr Argo_Termtab.empty E
+
+val empty_value = ((0, 0), None)
+fun value_of vals t = the_default empty_value (Argo_Termtab.lookup vals t)
+fun map_value t = Argo_Termtab.map_default (t, empty_value)
+
+
+(* weight operations *)
+
+(*
+  The weight of a term is a pair of activity and count. The activity describes how
+  often a term participated in conflicts. The count describes how often a term occurs
+  in clauses.
+*)
+
+val weight_ord = prod_ord int_ord int_ord
+
+fun weight_of vals t = fst (value_of vals t)
+
+fun less_than vals t1 t2 = weight_ord (weight_of vals t1, weight_of vals t2) = LESS
+
+fun rescale activity = activity div activity_rescale
+
+fun incr_activity incr t = map_value t (apfst (apfst (Integer.add incr)))
+fun incr_count t = map_value t (apfst (apsnd (Integer.add 1)))
+
+fun rescale_activities a incr vals =
+  if a <= max_activity then (incr, vals)
+  else (rescale incr, Argo_Termtab.map (fn _ => apfst (apfst rescale)) vals)
+
+
+(* reverse index operations *)
+
+(*
+  The reverse index is required to retrieve elements when increasing their priorities.
+*)
+
+fun contains vals t =
+  (case value_of vals t of
+    (_, None) => false
+  | _ => true)
+
+fun path_to vals t parents =
+  (case value_of vals t of
+    (_, Root) => parents
+  | (_, Some parent) => path_to vals parent (t :: parents)
+  | _ => raise Fail "bad heap")
+
+fun put_parent t parent = map_value t (apsnd (K parent))
+fun delete t = put_parent t None
+fun root t = put_parent t Root
+
+fun as_root (tree as T (t, _, _), vals) = (tree, root t vals)
+  | as_root x = x
+
+
+(* pairing heap operations *)
+
+fun merge E tree vals = (tree, vals)
+  | merge tree E vals = (tree, vals)
+  | merge (tree1 as T (t1, p1, trees1)) (tree2 as T (t2, p2, trees2)) vals =
+      if less_than vals t1 t2 then (T (t2, p2, tree1 :: trees2), put_parent t1 (Some t2) vals)
+      else (T (t1, p1, tree2 :: trees1), put_parent t2 (Some t1) vals)
+
+fun merge_pairs [] vals = (E, vals)
+  | merge_pairs [tree] vals = (tree, vals)
+  | merge_pairs (tree1 :: tree2 :: trees) vals =
+      vals |> merge tree1 tree2 ||>> merge_pairs trees |-> uncurry merge
+
+
+(* cutting subtrees specified by a path *)
+
+(*
+  The extractions are performed in such a way that the heap is changed in as few positions
+  as possible.
+*)
+
+fun with_index f u ((tree as T (t, _, _)) :: trees) =
+      if Argo_Term.eq_term (t, u) then f tree ||> (fn E => trees | tree => tree :: trees)
+      else with_index f u trees ||> cons tree
+  | with_index _ _ _ = raise Fail "bad heap"
+
+fun lift_index f u (T (t, p, trees)) = with_index f u trees ||> (fn trees => T (t, p, trees))
+  | lift_index _ _ E = raise Fail "bad heap"
+
+fun cut t [] tree = lift_index (fn tree => (tree, E)) t tree
+  | cut t (parent :: ts) tree = lift_index (cut t ts) parent tree
+
+
+(* filtering the heap *)
+
+val proper_trees = filter (fn E => false | T _ => true)
+
+fun filter_tree _ E vals = (E, vals)
+  | filter_tree pred (T (t, p, ts)) vals =
+      let val (ts, vals) = fold_map (filter_tree pred) ts vals |>> proper_trees
+      in if pred t then (T (t, p, ts), vals) else merge_pairs ts (delete t vals) end
+
+
+(* exported heap operations *)
+
+fun insert lit (h as {incr, vals, tree}: heap) = 
+  let val (t, p) = Argo_Lit.dest lit
+  in if contains vals t then h else mk_heap' incr (merge tree (T (t, p, [])) (root t vals)) end
+
+fun extract ({tree=E, ...}: heap) = NONE
+  | extract ({incr, vals, tree=T (t, p, ts)}: heap) =
+      SOME (Argo_Lit.literal t p, mk_heap' incr (as_root (merge_pairs ts (delete t vals))))
+
+fun with_term lit f = f (Argo_Lit.term_of lit)
+
+(*
+  If the changed weight violates the heap property, the corresponding tree
+  is extracted and merged with the root.
+*)
+
+fun fix t (w, Some parent) (incr, vals) tree =
+      if weight_ord (weight_of vals parent, w) = LESS then
+        let val (tree1, tree2) = cut t (path_to vals parent []) tree
+        in mk_heap' incr (merge tree1 tree2 (root t vals)) end
+      else mk_heap incr vals tree
+  | fix _ _ (incr, vals) tree = mk_heap incr vals tree
+
+fun increase lit ({incr, vals, tree}: heap) = with_term lit (fn t =>
+  let
+    val vals = incr_activity incr t vals
+    val value as ((a, _), _) = value_of vals t
+  in fix t value (rescale_activities a incr vals) tree end)
+
+fun count lit ({incr, vals, tree}: heap) = with_term lit (fn t =>
+  let val vals = incr_count t vals
+  in fix t (value_of vals t) (incr, vals) tree end)
+
+fun decay ({incr, vals, tree}: heap) = mk_heap (decay_incr incr) vals tree
+
+fun rebuild pred ({incr, vals, tree}: heap) = mk_heap' incr (filter_tree pred tree vals)
+
+end