|
(* 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 = is_less (weight_ord (weight_of vals t1, weight_of vals t2))
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 is_less (weight_ord (weight_of vals parent, w)) 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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
