/seL4-l4v-master/HOL4/examples/AI_tasks/TPTP/ |
H A D | all_stats.sh | 1 sh stats.sh combin_test/eprover 2 sh stats.sh combin_test/eprover_schedule 3 sh stats.sh combin_test/vampire 4 sh stats.sh combin_test/vampire_casc 5 sh stats.sh combin_train/eprover 6 sh stats.sh combin_train/eprover_schedule 7 sh stats.sh combin_train/vampire 8 sh stats.sh combin_train/vampire_casc
|
/seL4-l4v-master/l4v/tools/autocorres/tools/stats/ |
H A D | Makefile | 14 python stats.py -R $(REPEATS) --root ../../.. --output $@ $< 17 python stats.py -R $(REPEATS) --root ../../.. --output $@ $<
|
/seL4-l4v-master/HOL4/polyml/PolyPerf/ |
H A D | PolyPerf.cpp | 204 ASN1Parse (statistics *s, unsigned char *p): stats(s), ptr(p) {} 213 statistics *stats; member in class:ASN1Parse 340 stats->psCounters[PSC_THREADS] = cValue; break; 342 stats->psCounters[PSC_THREADS_IN_ML] = cValue; break; 344 stats->psCounters[PSC_THREADS_WAIT_IO] = cValue; break; 346 stats->psCounters[PSC_THREADS_WAIT_MUTEX] = cValue; break; 348 stats->psCounters[PSC_THREADS_WAIT_CONDVAR] = cValue; break; 350 stats->psCounters[PSC_THREADS_WAIT_SIGNAL] = cValue; break; 352 stats->psCounters[PSC_GC_FULLGC] = cValue; break; 354 stats [all...] |
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Main.C | 71 void printStats(SolverStats& stats, double& cpu_time, int64& mem_used) argument 75 reportf("restarts : %"I64_fmt"\n", stats.starts); 76 reportf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", stats.conflicts , stats.conflicts /cpu_time); 77 reportf("decisions : %-12"I64_fmt" (%.0f /sec)\n", stats.decisions , stats.decisions /cpu_time); 78 reportf("propagations : %-12"I64_fmt" (%.0f /sec)\n", stats.propagations, stats.propagations/cpu_time); 79 reportf("conflict literals : %-12"I64_fmt" (%4.2f %% deleted)\n", stats.tot_literals, (stats [all...] |
H A D | Solver.C | 136 stats.learnts_literals += c->size(); 143 stats.clauses_literals += c->size(); 157 if (c->learnt()) stats.learnts_literals -= c->size(); 158 else stats.clauses_literals -= c->size(); 364 stats.max_literals += out_learnt.size(); 366 stats.tot_literals += out_learnt.size(); 505 stats.propagations++; 646 simpDB_props = stats.clauses_literals + stats.learnts_literals; // (shouldn't depend on 'stats' reall [all...] |
H A D | Solver.h | 169 SolverStats stats; member in class:Solver
|
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | monitor_dockable.scala | 32 private def add_statistics(stats: Properties.T) 34 statistics = statistics.enqueue(stats) 111 case stats: Session.Statistics => 112 add_statistics(stats.props)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | monitor_dockable.scala | 32 private def add_statistics(stats: Properties.T) 34 statistics = statistics.enqueue(stats) 111 case stats: Session.Statistics => 112 add_statistics(stats.props)
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | statistics.h | 132 Handle returnStatistics(TaskData *taskData, const unsigned char *stats, size_t size);
|
H A D | statistics.cpp | 184 // If this fails just create local stats. 709 Handle Statistics::returnStatistics(TaskData *taskData, const unsigned char *stats, size_t size) 712 return taskData->saveVec.push(C_string_to_Poly(taskData, (const char*)stats, size));
|
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | SatSolvers.sml | 95 p (outfile ^".stats")]),
|
H A D | minisatProve.sml | 96 in_name^"."^solver_name^".stats"
|
/seL4-l4v-master/graph-refine/ |
H A D | graph-refine.py | 325 import stats namespace 326 prev_proofs = stats.scan_proofs (open (fname))
|
/seL4-l4v-master/HOL4/examples/muddy/ |
H A D | bdd.sig | 136 val stats : unit -> {produced : int, value 345 [stats()] gives various statstistical information from the
|
H A D | bdd.sml | 107 fun stats unit = function
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | file_readerLib.sml | 230 (* print stats *)
|
/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | HolBdd.tex | 333 using the function \t{stats} 336 stats : unit -> {produced : int, 344 \end{verbatim}\index{HolBddLib!ML bindings!{stats}@\ml{stats}} 347 evaluating \t{stats()} are
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | HolBdd.tex | 333 using the function \t{stats} 336 stats : unit -> {produced : int, 344 \end{verbatim}\index{HolBddLib!ML bindings!{stats}@\ml{stats}} 347 evaluating \t{stats()} are
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_opsScript.sml | 1427 val stats = [(``1``, mc_print_stats1_spec, mc_print_stats1_thm, "1"), value 1443 val X64_LISP_PRINT_STATS_BEGIN = X64_LISP_PRINT_STATS (el 1 stats); 1444 val X64_LISP_PRINT_STATS_END = X64_LISP_PRINT_STATS (el 2 stats);
|
H A D | lisp_symbolsScript.sml | 3587 (* call stats function 1 *) 3627 (* call stats function 2 *)
|