Searched refs:trace (Results 1 - 25 of 260) sorted by relevance

1234567891011

/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A DQbfTrace.sml14 val trace = ref 2 value
16 val _ = Feedback.register_trace ("HolQbfLib", trace, 4)
/seL4-l4v-10.1.1/HOL4/src/coretypes/
H A DpairSimps.sml29 trace = 2,
36 trace = 2,
43 trace = 2,
/seL4-l4v-10.1.1/HOL4/examples/ind_def/
H A DalgebraScript.sml3 (* 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 DClause.sml159 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 DResolution.sml46 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 DWaiting.sml158 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 DClause.sml159 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 DResolution.sml46 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 DWaiting.sml158 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 DExn.sml78 (* 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 DExn.sig29 val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a value
H A DMultithreading.sml16 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 Dstats.py125 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 Dsolver.py179 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 DgroundEval.sml106 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 Dholfoot_pp_print.sig5 (* trace "use holfoot_pp" for turning pretty printing on and off *);
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DSolverSpec.sml16 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 Dsimpfrag.sig7 trace: int,
H A Dsimpfrag.sml8 trace: int,
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DTrace.sig19 val trace : int * action -> unit value
/seL4-l4v-10.1.1/HOL4/src/real/
H A DRealArith.sml42 (* 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 Dselftest.sml8 val t2s = trace ("Unicode", 0) term_to_string
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A Dsimplifier.sml13 trace = 2,
/seL4-l4v-10.1.1/HOL4/src/emit/
H A Dselftest.sml22 val _ = trace ("Define.storage_message", 0) gh157 ()
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/
H A Demit_eval.sig29 trace (* select updates to print *)

Completed in 148 milliseconds

1234567891011