Searched refs:stats (Results 1 - 20 of 20) sorted by relevance

/seL4-l4v-master/HOL4/examples/AI_tasks/TPTP/
H A Dall_stats.sh1 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 DMakefile14 python stats.py -R $(REPEATS) --root ../../.. --output $@ $<
17 python stats.py -R $(REPEATS) --root ../../.. --output $@ $<
/seL4-l4v-master/HOL4/polyml/PolyPerf/
H A DPolyPerf.cpp204 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 DMain.C71 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 DSolver.C136 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 DSolver.h169 SolverStats stats; member in class:Solver
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Dmonitor_dockable.scala32 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 Dmonitor_dockable.scala32 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 Dstatistics.h132 Handle returnStatistics(TaskData *taskData, const unsigned char *stats, size_t size);
H A Dstatistics.cpp184 // 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 DSatSolvers.sml95 p (outfile ^".stats")]),
H A DminisatProve.sml96 in_name^"."^solver_name^".stats"
/seL4-l4v-master/graph-refine/
H A Dgraph-refine.py325 import stats namespace
326 prev_proofs = stats.scan_proofs (open (fname))
/seL4-l4v-master/HOL4/examples/muddy/
H A Dbdd.sig136 val stats : unit -> {produced : int, value
345 [stats()] gives various statstistical information from the
H A Dbdd.sml107 fun stats unit = function
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A Dfile_readerLib.sml230 (* print stats *)
/seL4-l4v-master/HOL4/Manual/Description/
H A DHolBdd.tex333 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 DHolBdd.tex333 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 Dlisp_opsScript.sml1427 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 Dlisp_symbolsScript.sml3587 (* call stats function 1 *)
3627 (* call stats function 2 *)

Completed in 265 milliseconds