SSL argo_heap.ML Sprache: SML

(*  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

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.