/seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
H A D | QbfTrace.sml | 14 val trace = ref 2 value 16 val _ = Feedback.register_trace ("HolQbfLib", trace, 4)
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | pairSimps.sml | 29 trace = 2, 36 trace = 2, 43 trace = 2,
|
/seL4-l4v-10.1.1/HOL4/examples/ind_def/ |
H A D | algebraScript.sml | 3 (* DESCRIPTION : Maximal trace semantics and transition semantics of a *) 58 (* Definition of a maximal trace semantics for the process algebra. *) 66 val _ = type_abbrev("trace", ``:label list``); 69 (* Inductive definition of a trace relation MTRACE. This is defined so *) 70 (* that MTRACE P A means A is the maximal trace of the process P. The *) 91 (* Definition of a terminal process: one with [] as a maximal trace. *) 125 (* Inductive definition of a trace transition system *) 129 (* We now define a transition system that accumulates the trace of a *) 141 (* Strong form of rule induction for labelled (trace) transitions. *) 147 (* Theorem 1: Maximal trace semantic [all...] |
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Clause.sml | 159 val () = Print.trace pp "Clause.largestLiterals: cl" cl 161 val () = Print.trace ppResult "Clause.largestLiterals: result" result 232 val () = Print.trace Rewrite.pp "Clause.rewrite: rewr" rewr 233 val () = Print.trace Print.ppInt "Clause.rewrite: id" id 234 val () = Print.trace pp "Clause.rewrite: cl" cl 245 val () = Print.trace pp "Clause.rewrite: result" result 270 val () = Print.trace pp "Clause.factor: cl" cl 272 val () = Print.trace (Print.ppList pp) "Clause.factor: result" result 281 val () = Print.trace pp "Clause.resolve: cl1" cl1 282 val () = Print.trace Litera [all...] |
H A D | Resolution.sml | 46 val () = Print.trace Print.ppException "Resolution.new: exception" e 80 val () = Print.trace Active.pp "Resolution.iterate: active" active 81 val () = Print.trace Waiting.pp "Resolution.iterate: waiting" waiting 97 val () = Print.trace Clause.pp "Resolution.iterate: cl" cl
|
H A D | Waiting.sml | 158 val () = Print.trace Clause.pp "Waiting.clauseWeight: cl" cl 167 val () = trace ("Waiting.clauseWeight: dist = " ^ 169 val () = trace ("Waiting.clauseWeight: symbolsW = " ^ 171 val () = trace ("Waiting.clauseWeight: variablesW = " ^ 173 val () = trace ("Waiting.clauseWeight: literalsW = " ^ 175 val () = trace ("Waiting.clauseWeight: modelsW = " ^ 181 val () = trace ("Waiting.clauseWeight: weight = " ^ 227 val () = Print.trace pp "Waiting.add: waiting" waiting 228 val () = Print.trace (Print.ppList Clause.pp) "Waiting.add: cls" cls 234 val () = Print.trace p [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Clause.sml | 159 val () = Print.trace pp "Clause.largestLiterals: cl" cl 161 val () = Print.trace ppResult "Clause.largestLiterals: result" result 232 val () = Print.trace Rewrite.pp "Clause.rewrite: rewr" rewr 233 val () = Print.trace Print.ppInt "Clause.rewrite: id" id 234 val () = Print.trace pp "Clause.rewrite: cl" cl 245 val () = Print.trace pp "Clause.rewrite: result" result 270 val () = Print.trace pp "Clause.factor: cl" cl 272 val () = Print.trace (Print.ppList pp) "Clause.factor: result" result 281 val () = Print.trace pp "Clause.resolve: cl1" cl1 282 val () = Print.trace Litera [all...] |
H A D | Resolution.sml | 46 val () = Print.trace Print.ppException "Resolution.new: exception" e 80 val () = Print.trace Active.pp "Resolution.iterate: active" active 81 val () = Print.trace Waiting.pp "Resolution.iterate: waiting" waiting 97 val () = Print.trace Clause.pp "Resolution.iterate: cl" cl
|
H A D | Waiting.sml | 158 val () = Print.trace Clause.pp "Waiting.clauseWeight: cl" cl 167 val () = trace ("Waiting.clauseWeight: dist = " ^ 169 val () = trace ("Waiting.clauseWeight: symbolsW = " ^ 171 val () = trace ("Waiting.clauseWeight: variablesW = " ^ 173 val () = trace ("Waiting.clauseWeight: literalsW = " ^ 175 val () = trace ("Waiting.clauseWeight: modelsW = " ^ 181 val () = trace ("Waiting.clauseWeight: weight = " ^ 227 val () = Print.trace pp "Waiting.add: waiting" waiting 228 val () = Print.trace (Print.ppList Clause.pp) "Waiting.add: cls" cls 234 val () = Print.trace p [all...] |
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Exn.sml | 78 (* low-level trace *) 80 fun trace exn_message output e = function 82 (e, fn (trace, exn) => 84 val title = "Exception trace - " ^ exn_message exn; 85 val () = output (String.concatWith "\n" (title :: trace));
|
H A D | Exn.sig | 29 val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a value
|
H A D | Multithreading.sml | 16 val trace: int ref value 76 val trace = ref 0; value 79 if ! trace < level then () 97 if ! trace > 0 then
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | stats.py | 125 trace = list (knowledge.live_pairs_trace) 126 return (res, trace) 139 (_, trace) = trace_split_loop_pairs_window (prob, i) 140 big_traces.append ((i, trace)) 142 print 'Search pair decay in random examples (idx, window size, trace):' 143 for (i, (w, (_, trace))) in enumerate (ex_traces): 144 print ' %d: %d: %s' % (i, w, trace) 147 for (w, trace) in big_traces: 148 print ' %d: %s' % (w, trace) 151 for (w, (_, trace)) i [all...] |
H A D | solver.py | 179 from target_objects import structs, rodata, sections, trace, printout namespace 432 trace ('Env miss for %s in smt_expr' % expr.name) 433 trace ('Environment is %s' % env) 829 trace ('SMT conversation problem (attempt %d)' 831 trace ('I sent %s' % repr (e.prompt)) 832 trace ('I got %s' % repr (e.response)) 833 trace ('restarting solver') 836 trace ('Repeated SMT failure, giving up.') 932 trace ('WARNING: redef of var %r to name %s' % (val, name)) 1008 trace ('testin [all...] |
/seL4-l4v-10.1.1/HOL4/src/compute/src/ |
H A D | groundEval.sml | 106 fun trace(x, LZT(s,t)) = print (nspaces x ^ s ^ term_to_string t ^ "\n") function 107 | trace(x, MSG s) = print (nspaces x ^ s ^ "\n") 117 fun tracek n s (Conv _) = trace(n, MSG (s ^ " Conv(...)")) 118 | tracek n s (Trans(th, _)) = trace(n, LZT(s ^ " Trans: ", concl th)) 127 trace(i, LZT("std: SANITY OK, entering ", t)); 134 trace (i, LZT("L-Descending into ", l)); 140 (trace(i, LZT("Left finished with ", result_term leftresult)); 141 trace(i - 2, LZT("R-Descending into ", rtm)); 145 val _ = trace (i + 2, LZT ("Right finished with ", 148 Trans(th, _) => trace( [all...] |
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfoot_pp_print.sig | 5 (* trace "use holfoot_pp" for turning pretty printing on and off *);
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | SolverSpec.sml | 16 file (unless '!trace' = 4); emits messages according to '!trace' *) 29 val _ = if !Library.trace > 1 then 35 val _ = if !Library.trace > 1 then 42 if !Library.trace > 2 then 51 val _ = if !Library.trace > 0 then 71 val _ = if !Library.trace < 4 then 93 if !Library.trace > 2 then
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | simpfrag.sig | 7 trace: int,
|
H A D | simpfrag.sml | 8 trace: int,
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Trace.sig | 19 val trace : int * action -> unit value
|
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | RealArith.sml | 42 (* The trace system. *) 66 fun trace s = check (trace_pure (s ^ "\n")) function 418 val _ = trace "REAL_PROD_NORM_CONV" 453 val _ = trace "done REAL_PROD_NORM_CONV" 618 val _ = trace "linear_add" 630 val _ = trace "v1 =" 636 val _ = trace "v2 =" 666 val _ = trace "can't add_dest term2" 668 val _ = trace "v2 =" 690 val _ = trace "ca [all...] |
H A D | selftest.sml | 8 val t2s = trace ("Unicode", 0) term_to_string
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | simplifier.sml | 13 trace = 2,
|
/seL4-l4v-10.1.1/HOL4/src/emit/ |
H A D | selftest.sml | 22 val _ = trace ("Define.storage_message", 0) gh157 ()
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/ |
H A D | emit_eval.sig | 29 trace (* select updates to print *)
|