Searched refs:search (Results 1 - 25 of 150) sorted by relevance

123456

/seL4-l4v-10.1.1/graph-refine/graph-to-graph/
H A Delf_parser.py52 header = re.search('kernel\.elf:\s*file\s*format\s*elf32-littlearm',line)
53 header2 = re.search('Disassembly of section \..*:',line)
57 ndks = re.search('.*ndks_boot.*',line)
63 r = re.search('(?P<f_addr>.*) <(?P<f_name>.*)>:$',line)
80 literal = re.search('(?P<addr>.*):\s*[a-f0-9]+\s*(?P<size>(\.word)|(\.short)|(\.byte))\s*(?P<value>0x[a-f0-9]+)$',line)
92 match = re.search('(?P<line_addr>.*):.*',line)
107 match = re.search(r'[a-f0-9]+:\s*[a-f0-9]+\s+(b|bx)\s+.*',inst)
H A Dcplex.py70 if re.search(unbounded,line) or re.search(infeasible, line):
74 match = re.search(objective_regex,line)
87 if re.search(r'^End',line):
H A Delf_file.py59 match = re.search('(.*)(_clone).*',f)
112 match = re.search(r'^.*:\s+(?P<raw>[a-f0-9]+)\s*(?P<text>.*)$',inst)
H A Dbench.py131 if s.startswith('Loop') or re.search(r'\s*\(=',s) or re.search(r'\s*\(',s):
H A Dconflict.py362 match = re.search(r'\s*\[(?P<infeas>.*)\]\s*:\s*(?P<kind>.*$)', line)
402 match = re.search(r'.*:\s*(?P<kind>.*$)', line)
410 match = re.search(r'\[(?P<addr>.*)\]:(?P<kind>.*$)', line)
413 match = re.search(r'\s*\[(?P<addr>.*)\]\s*:\s*\[(?P<times>.*)\]\s*:\s*(?P<kind>.*$)', line)
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/
H A DquantHeuristicsLibSimple.sig35 - ty : search a guess for either universal or existential quantification
36 - v : variable to search an instance for
37 - tm : a term to search an instantiation in
49 Having an additional callback argument to search guesses for subterms is also useful.
50 combine_sgsfwcs then allows combining a list of such search functions with callback
51 into a single search function.
60 (* search functions for common operations *)
86 (* Generalised conversions that allow specifying which search functions to use *)
/seL4-l4v-10.1.1/HOL4/src/meson/src/
H A DmesonLib.sig2 (* Version of the MESON procedure a la PTTP. Various search options. *)
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibMetis.sig11 1: Status information during proof search
14 4: High-level proof search information
15 5: Log of every inference during proof search
H A DmlibMetis.sml28 1: Status information during proof search
31 4: High-level proof search information
32 5: Log of every inference during proof search
/seL4-l4v-10.1.1/graph-refine/
H A Dstats.py9 import search namespace
63 nec = search.get_necessary_split_opts (p, loop_head,
92 va = search.get_loop_var_analysis_at (p, loop_head)
119 i_j_opts = search.mk_i_j_opts (unfold_limit = window_size)
121 knowledge = search.setup_split_search (rep, loop_head, restrs, hyps,
124 res = search.split_search (loop_head, knowledge)
137 if not search.mk_i_j_opts (unfold_limit = i):
H A Ddebug.py16 import search namespace
118 if search.eval_model_expr (m, rep.solv,
154 r = search.eval_model (m, x)
343 v = search.eval_model (m, sx)
367 v = search.eval_model_expr (m, solv, expr)
503 offs = search.eval_model_expr (m, rep.solv, offs)
508 data = [(addr, search.eval_model_expr (m, rep.solv,
550 ev = search.eval_model (m, s_x)
689 proof = search.last_proof[0]
700 proof = search
[all...]
H A Dloop_bounds.py1 import check,search,problem,syntax,solver,logic,rep_graph,re namespace
8 from search import eval_model_expr
30 """performs a binary search between minimum and maximum, but does not start
71 #naive binary search to find loop bounds
105 #do a downward binary search to find the concrete loop bound
185 standard = set (search.mk_seq_eqs (p, split, 1, with_rodata = False))
189 cands = search.mk_seq_eqs (p, split, 1, with_rodata = False)
223 standard = set (search.mk_seq_eqs (p, split, 1, with_rodata = False))
258 vas = search.get_loop_var_analysis_at(p, split)
486 if len (search
[all...]
H A Dgraph-refine.py18 import search namespace
71 proof = search.build_proof (p)
94 except search.NoSplit:
97 printout ('Solver timeout/failure in proof search.')
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttSearch.sig25 val search : value
H A DtttSetup.sig37 (* search *)
/seL4-l4v-10.1.1/l4v/tools/autocorres/tools/stats/
H A Dsummary.py20 m = re.search(r, str)
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DSubsume.sml186 fun search [] = NONE function
187 | search ((sub,[]) :: others) =
191 if pred x then SOME x else search others
193 | search ((_, [] :: _) :: others) = search others
194 | search ((sub, (sub' :: subs) :: subsl) :: others) =
199 NONE => search others
200 | SOME sub => search ((sub,subsl) :: others)
205 | SOME sub_subsl => search [sub_subsl]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DSubsume.sml186 fun search [] = NONE function
187 | search ((sub,[]) :: others) =
191 if pred x then SOME x else search others
193 | search ((_, [] :: _) :: others) = search others
194 | search ((sub, (sub' :: subs) :: subsl) :: others) =
199 NONE => search others
200 | SOME sub => search ((sub,subsl) :: others)
205 | SOME sub_subsl => search [sub_subsl]
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/
H A DHelp.sig36 /str cyclically search for string str in help file (case-insensitive)
37 n search for next occurrence of str
51 records, each of which maps a search term to the specified file
H A DHelp.sml28 The browser's search facility cyclically searches (case-insensitive)
41 (* Additional directories to search for help files *)
79 (* Mapping particular search terms to non-.sig files: *)
151 fun search chars = function
156 NONE => (print "**** No previous search string\n";
170 | SOME (#"/" :: s) => search s
289 (* Main help function: search for a string in the signature index database: *)
/seL4-l4v-10.1.1/HOL4/src/1/
H A Dmatch_goal.sml144 fun search [] d = try_tactic d function
145 | search (m::ms) d = stream_flat (stream_map (search ms) (m d))
151 (case search matches (empty_named_thms,empty_named_tms) () of
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DHM_DepGraph.sml147 fun search i = function
151 if #status nI <> Pending then search (i + 1)
153 else search (i + 1)
155 search 0
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DHolKernel.sml262 * the search failed because the sought-for subterm is not there, or because *
287 fun search bvs actions = function
290 | POP :: alist => search (tl bvs) alist
296 COMB (t1, t2) => search bvs (SEARCH t1 :: SEARCH t2 :: alist)
297 | LAMB (bv, t) => search (bv :: bvs) (SEARCH t :: POP :: alist)
298 | _ => search bvs alist
300 search [] [SEARCH t]
304 fun search bvs actions acc = function
307 | POP :: alist => search (tl bvs) alist acc
314 COMB(t1, t2) => search bv
[all...]
/seL4-l4v-10.1.1/HOL4/src/num/arith/Manual/
H A Ddescription.tex81 help\index{help!updating search path} search path. The help search path is
83 library. After updating the help search path, the \ml{reduce}
95 Updating help search path
97 Extending help search path.
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/
H A Dcombin.tex140 Meson search level: ...
304 Meson search level: .........
328 Meson search level: ..........
503 Meson search level: .....
525 Meson search level: ............
549 Meson search level: .......
631 Meson search level: ...
653 Meson search level: ............
682 Meson search level: .......
835 Meson search leve
[all...]

Completed in 122 milliseconds

123456