| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Heap.sml | 6 structure Heap :> Heap = structure
13 datatype 'a heap = Heap of ('a * 'a -> order) * int * 'a node;
33 fun new cmp = Heap (cmp,0,E);
35 fun add (Heap (f,n,a)) x = Heap (f, n + 1, merge f (T (1,x,E,E), a));
37 fun size (Heap (_, n, _)) = n;
41 fun top (Heap (_,_,E)) = raise Empty
42 | top (Heap (_, _, T (_,x,_,_))) = x;
44 fun remove (Heap (
[all...] |
| H A D | Heap.sig | 6 signature Heap = signature
|
| H A D | Waiting.sml | 35 clauses : (weight * (distance * Clause.clause)) Heap.heap,
55 fun size (Waiting {clauses,...}) = Heap.size clauses;
66 List.map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses))
212 Heap.add acc (weight,(dist,cl))
246 val clauses = Heap.new cmp
277 if Heap.null clauses then NONE
280 val ((_,dcl),clauses) = Heap.remove clauses
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Heap.sml | 6 structure Heap :> Heap = structure
13 datatype 'a heap = Heap of ('a * 'a -> order) * int * 'a node;
33 fun new cmp = Heap (cmp,0,E);
35 fun add (Heap (f,n,a)) x = Heap (f, n + 1, merge f (T (1,x,E,E), a));
37 fun size (Heap (_, n, _)) = n;
41 fun top (Heap (_,_,E)) = raise Empty
42 | top (Heap (_, _, T (_,x,_,_))) = x;
44 fun remove (Heap (
[all...] |
| H A D | Heap.sig | 6 signature Heap = signature
|
| H A D | Waiting.sml | 35 clauses : (weight * (distance * Clause.clause)) Heap.heap,
55 fun size (Waiting {clauses,...}) = Heap.size clauses;
66 List.map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses))
212 Heap.add acc (weight,(dist,cl))
246 val clauses = Heap.new cmp
277 if Heap.null clauses then NONE
280 val ((_,dcl),clauses) = Heap.remove clauses
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Heap.h | 0 /******************************************************************************************[Heap.h]
32 class Heap { class
67 Heap(C c) : comp(c) { heap.push(-1); }
|
| H A D | VarOrder.h | 24 #include "Heap.h"
39 Heap<VarOrder_lt> heap;
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/ |
| H A D | Makefile | 59 src/Heap.sig src/Heap.sml \
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/ |
| H A D | Makefile | 59 src/Heap.sig src/Heap.sml \
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | x86assembly_masm32.S | 88 ; 5. Return from "trap" i.e. Heap/Stack overflow. Stack-overflow can result in an exception
|
| H A D | x86assembly_masm64.S | 117 ; 5. Return from "trap" i.e. Heap/Stack overflow. Stack-overflow can result in an exception
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/Admin/ |
| H A D | build_log.scala | 516 val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
590 case Heap(name, Value.Long(size)) =>
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/ |
| H A D | build_log.scala | 516 val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
590 case Heap(name, Value.Long(size)) =>
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
| H A D | HSLScript.sml | 285 (* Heap and Stack Level (HSL) *)
|