1(* Title: Tools/Argo/argo_heap.ML 2 Author: Sascha Boehme 3 4A maximum-priority heap for literals with integer priorities and with inverse indices. 5The heap is intended to be used as VSIDS-like decision heuristics. This implementation 6is based on pairing heaps described in: 7 8 Chris Okasaki. Purely Functional Data Structures. Chapter 5. 9 Cambridge University Press, 1998. 10*) 11 12signature ARGO_HEAP = 13sig 14 type heap 15 val heap: heap 16 val insert: Argo_Lit.literal -> heap -> heap 17 val extract: heap -> (Argo_Lit.literal * heap) option 18 val increase: Argo_Lit.literal -> heap -> heap 19 val count: Argo_Lit.literal -> heap -> heap 20 val decay: heap -> heap 21 val rebuild: (Argo_Term.term -> bool) -> heap -> heap 22end 23 24structure Argo_Heap: ARGO_HEAP = 25struct 26 27(* heuristic activity constants *) 28 29val min_incr = 128 30fun decay_incr i = (i * 11) div 10 31val max_activity = Integer.pow 24 2 32val activity_rescale = Integer.pow 14 2 33 34 35(* data structures and basic operations *) 36 37datatype tree = E | T of Argo_Term.term * bool * tree list 38 39datatype parent = None | Root | Some of Argo_Term.term 40 41type heap = { 42 incr: int, (* the increment to apply in an increase operation *) 43 vals: ((int * int) * parent) Argo_Termtab.table, (* weights and parents of the stored terms *) 44 tree: tree} (* the pairing heap of literals; note: the tree caches literal polarities *) 45 46fun mk_heap incr vals tree: heap = {incr=incr, vals=vals, tree=tree} 47fun mk_heap' incr (tree, vals) = mk_heap incr vals tree 48 49val heap = mk_heap min_incr Argo_Termtab.empty E 50 51val empty_value = ((0, 0), None) 52fun value_of vals t = the_default empty_value (Argo_Termtab.lookup vals t) 53fun map_value t = Argo_Termtab.map_default (t, empty_value) 54 55 56(* weight operations *) 57 58(* 59 The weight of a term is a pair of activity and count. The activity describes how 60 often a term participated in conflicts. The count describes how often a term occurs 61 in clauses. 62*) 63 64val weight_ord = prod_ord int_ord int_ord 65 66fun weight_of vals t = fst (value_of vals t) 67 68fun less_than vals t1 t2 = is_less (weight_ord (weight_of vals t1, weight_of vals t2)) 69 70fun rescale activity = activity div activity_rescale 71 72fun incr_activity incr t = map_value t (apfst (apfst (Integer.add incr))) 73fun incr_count t = map_value t (apfst (apsnd (Integer.add 1))) 74 75fun rescale_activities a incr vals = 76 if a <= max_activity then (incr, vals) 77 else (rescale incr, Argo_Termtab.map (fn _ => apfst (apfst rescale)) vals) 78 79 80(* reverse index operations *) 81 82(* 83 The reverse index is required to retrieve elements when increasing their priorities. 84*) 85 86fun contains vals t = 87 (case value_of vals t of 88 (_, None) => false 89 | _ => true) 90 91fun path_to vals t parents = 92 (case value_of vals t of 93 (_, Root) => parents 94 | (_, Some parent) => path_to vals parent (t :: parents) 95 | _ => raise Fail "bad heap") 96 97fun put_parent t parent = map_value t (apsnd (K parent)) 98fun delete t = put_parent t None 99fun root t = put_parent t Root 100 101fun as_root (tree as T (t, _, _), vals) = (tree, root t vals) 102 | as_root x = x 103 104 105(* pairing heap operations *) 106 107fun merge E tree vals = (tree, vals) 108 | merge tree E vals = (tree, vals) 109 | merge (tree1 as T (t1, p1, trees1)) (tree2 as T (t2, p2, trees2)) vals = 110 if less_than vals t1 t2 then (T (t2, p2, tree1 :: trees2), put_parent t1 (Some t2) vals) 111 else (T (t1, p1, tree2 :: trees1), put_parent t2 (Some t1) vals) 112 113fun merge_pairs [] vals = (E, vals) 114 | merge_pairs [tree] vals = (tree, vals) 115 | merge_pairs (tree1 :: tree2 :: trees) vals = 116 vals |> merge tree1 tree2 ||>> merge_pairs trees |-> uncurry merge 117 118 119(* cutting subtrees specified by a path *) 120 121(* 122 The extractions are performed in such a way that the heap is changed in as few positions 123 as possible. 124*) 125 126fun with_index f u ((tree as T (t, _, _)) :: trees) = 127 if Argo_Term.eq_term (t, u) then f tree ||> (fn E => trees | tree => tree :: trees) 128 else with_index f u trees ||> cons tree 129 | with_index _ _ _ = raise Fail "bad heap" 130 131fun lift_index f u (T (t, p, trees)) = with_index f u trees ||> (fn trees => T (t, p, trees)) 132 | lift_index _ _ E = raise Fail "bad heap" 133 134fun cut t [] tree = lift_index (fn tree => (tree, E)) t tree 135 | cut t (parent :: ts) tree = lift_index (cut t ts) parent tree 136 137 138(* filtering the heap *) 139 140val proper_trees = filter (fn E => false | T _ => true) 141 142fun filter_tree _ E vals = (E, vals) 143 | filter_tree pred (T (t, p, ts)) vals = 144 let val (ts, vals) = fold_map (filter_tree pred) ts vals |>> proper_trees 145 in if pred t then (T (t, p, ts), vals) else merge_pairs ts (delete t vals) end 146 147 148(* exported heap operations *) 149 150fun insert lit (h as {incr, vals, tree}: heap) = 151 let val (t, p) = Argo_Lit.dest lit 152 in if contains vals t then h else mk_heap' incr (merge tree (T (t, p, [])) (root t vals)) end 153 154fun extract ({tree=E, ...}: heap) = NONE 155 | extract ({incr, vals, tree=T (t, p, ts)}: heap) = 156 SOME (Argo_Lit.literal t p, mk_heap' incr (as_root (merge_pairs ts (delete t vals)))) 157 158fun with_term lit f = f (Argo_Lit.term_of lit) 159 160(* 161 If the changed weight violates the heap property, the corresponding tree 162 is extracted and merged with the root. 163*) 164 165fun fix t (w, Some parent) (incr, vals) tree = 166 if is_less (weight_ord (weight_of vals parent, w)) then 167 let val (tree1, tree2) = cut t (path_to vals parent []) tree 168 in mk_heap' incr (merge tree1 tree2 (root t vals)) end 169 else mk_heap incr vals tree 170 | fix _ _ (incr, vals) tree = mk_heap incr vals tree 171 172fun increase lit ({incr, vals, tree}: heap) = with_term lit (fn t => 173 let 174 val vals = incr_activity incr t vals 175 val value as ((a, _), _) = value_of vals t 176 in fix t value (rescale_activities a incr vals) tree end) 177 178fun count lit ({incr, vals, tree}: heap) = with_term lit (fn t => 179 let val vals = incr_count t vals 180 in fix t (value_of vals t) (incr, vals) tree end) 181 182fun decay ({incr, vals, tree}: heap) = mk_heap (decay_incr incr) vals tree 183 184fun rebuild pred ({incr, vals, tree}: heap) = mk_heap' incr (filter_tree pred tree vals) 185 186end 187