| /seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
| H A D | graph_to_graph.py | 17 import conflict namespace
31 --x automated WCET estimating, firstly generate the loop heads, then automatically deduce the loop bounds, and finally use the automatically determined loopbounds to estimate teh WCET. A conflict file specifying additional preemption points
83 conflict.conflict(entry_point_function, tcfg_map_file_name, [], stripped_ilp, ilp_to_generate, dir_name, sol_to_generate, emit_conflicts=True, do_cplex=True, preempt_limit= preemption_limit,default_phantom_preempt=True)
|
| H A D | auto_infea.py | 13 import conflict namespace
68 print 'calling conflict.conflict'
71 conflict.cleanGlobalStates()
74 wcet = conflict.conflict(entry_point_function, tcfg_map, [manual_conflicts_file,auto_refutes_file],ilp_nofooter,ilp_file,dir_name, sol_file, emit_conflicts=True, do_cplex=True, silent_cplex=True, preempt_limit=preemption_limit)
77 print 'conflict.main returned'
|
| H A D | bench.py | 24 import conflict namespace
|
| H A D | conflict.py | 55 print 'conflict.py: global states cleaned'
387 fout.write('\ === conflict constraints from %s === \n\n' % conflict_file)
491 def conflict(entry_point_function, tcfg_map, conflict_files, old_ilp, new_ilp, dir_name, sol_file, emit_conflicts=False, do_cplex=False, interactive=False, silent_cplex=False, preempt_limit= None, default_phantom_preempt=False): function
498 print 'conflict.conflict: sol_file %s' % sol_file
518 print '''Usage: python conflict.py [tcfg map] [conflict file] [ilp file with footer stripped] [new ilp file] [target_dir] [flag] [preemption limit] [sol file to be generated]
519 conflict file 1 and/or 2 can be empty
522 generate a new conflict file
526 generate a new conflict fil
[all...] |
| /seL4-l4v-10.1.1/isabelle/src/Pure/Tools/ |
| H A D | check_keywords.scala | 20 private val conflict =
23 private val item = conflict ^^ (x => Some(x)) | other ^^ (_ => None)
50 "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos))
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/ |
| H A D | check_keywords.scala | 20 private val conflict =
23 private val item = conflict ^^ (x => Some(x)) | other ^^ (_ => None)
50 "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos))
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Solver.C | 48 | Allocate and add a new clause to the SAT solvers clause database. If a conflict is detected,
206 // Returns FALSE if immediate conflict.
235 | Analyze conflict and produce a reason clause ('out_learnt') and a backtracking level
261 // Generate conflict clause:
310 // Simplify conflict clause (a lot):
314 min_level |= 1 << (level[var(out_learnt[i])] & 31); // (maintain an abstraction of levels involved in conflict)
321 // Simplify conflict clause (a little):
344 // Finilize proof logging with conflict clause minimization steps:
408 | Specialized analysis procedure to express the final conflict in terms of assumptions.
409 | 'root_level' is allowed to point beyond end of trace (useful if called after conflict whil
[all...] |
| H A D | Solver.h | 174 bool expensive_ccmin; // Controls conflict clause minimization. TRUE by default.
196 vec<Lit> conflict; // If problem is unsatisfiable under assumptions, this vector represent the conflict clause expressed in the assumptions. member in class:Solver
197 ClauseId conflict_id; // (In proof logging mode only.) ID for the clause 'conflict' (for proof traverseral). NOTE! The empty clause is always the last clause derived, but for conflicts under assumption, this is not necessarly true.
|
| /seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
| H A D | verbose.sml | 75 print ": reduce/reduce conflict between rule ";
85 print ": shift/reduce conflict ";
|
| H A D | mklrtable.sml | 98 in say_error(rr,"reduce/reduce conflict");
99 say_error(sr,"shift/reduce conflict");
121 precedence, a shift/reduce conflict is reported.
132 A reduce/reduce conflict is reported. The lowest
169 conflict of term a, reduction by rule n, shift/reduce conficts exist
|
| H A D | yacc.sml | 694 is being used to resolve a shift/reduce conflict by checking if the
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | TermParse.sml | 33 ["Grammar introduces precedence conflict between tokens ",
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
| H A D | regAlloc.sml | 424 (* The first available memory slot that doesn't conflict with live "slots" *)
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/examples/ |
| H A D | amba_ahbScript.sml | 374 (* with >1 split-capable slave we would have to use HSPLITx to avoid conflict, but with only one we can access HSPLIT directly *)
|
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | boolScript.sml | 1311 * Note that there is a bound variable conflict if we use use t1
|
| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
| H A D | ltl_to_automaton_formulaScript.sml | 996 (*The extension does not conflict with old
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
| H A D | configure | 1918 which can conflict with char $2 (); below.
10248 # default) and relocated if they conflict, which is a slow very memory
14133 # default) and relocated if they conflict, which is a slow very memory
|
| /seL4-l4v-10.1.1/HOL4/polyml/ |
| H A D | configure | 1856 which can conflict with char $2 (); below.
10235 # default) and relocated if they conflict, which is a slow very memory
14569 # default) and relocated if they conflict, which is a slow very memory
|