DikeBenchmarker package

Subpackages

Submodules

DikeBenchmarker.benchmarkatoms module

Basic benchmarking job and result representation

class DikeBenchmarker.benchmarkatoms.AbstractResult(state: Enum, detail: str | None = None)[source]

Bases: object

Mixin providing baseline functionality for result atoms.

detail: str | None = None
property get_detail: str | None

Return the detail message of the result atom.

property has_detail: bool

Return True if the result atom has a detail message.

property has_error: bool

Return True if the result atom encountered an error (state is ERROR).

property has_result: bool

Return True if the result atom has a valid, non-error result.

property is_empty: bool

Return True if the result atom has no data (state is NONE).

state: Enum
class DikeBenchmarker.benchmarkatoms.CheckerResult(state: State = State.NONE, detail: str | None = None)[source]

Bases: AbstractResult

Verdict reported by a proof/model checker.

class State(value)[source]

Bases: str, Enum

Possible verdicts a checker can report.

ERROR = 'error'
NONE = 'none'
UNKNOWN = 'unknown'
UNVERIFIED = 'unverified'
VERIFIED = 'verified'
state: State = 'none'
class DikeBenchmarker.benchmarkatoms.ExecutionResult(state: State = State.NONE, detail: str | None = None)[source]

Bases: AbstractResult

Execution outcome of one wrapped job.

class State(value)[source]

Bases: str, Enum

Possible execution verdicts a wrapper can report.

ERROR = 'error'
NONE = 'none'
SUCCESS = 'success'
state: State = 'none'
class DikeBenchmarker.benchmarkatoms.Job(job_producer: AbstractBenchmarker, benchmark_id: str, solver_id: str, checker_id: str, logroot: str, retries: int = 3)[source]

Bases: object

Benchmarking Job that behaves like a future.

Identity: benchmark_id, solver_id, created_at (ctor time).

Lifecycle:

CREATED (initial)

–[put into JobLog]–> SUBMITTED –[start working on]–> RUNNING –[finish working on]–> FINISHED | FAILED

CREATED/SUBMITTED -> CANCELLED

benchmark_id: str
cancel_local() → bool[source]

Mark the job as cancelled.

Called by the benchmarker to prevent the job from being submitted to the external system.

checker_id: str
clone_retry(decrement: int = 1) → Job[source]

Create a clone of this job with identical benchmark_id, solver_id, checker_id, and logroot.

The cloned job will have a new created_at timestamp and will be in the CREATED state.

created_at: datetime
finished_at: datetime | None
get_log_prefix() → str[source]

Get the logfile prefix for this job.

job_producer: AbstractBenchmarker
logroot: str
mark_running() → None[source]

Mark the job as running.

Called by the infrastructure adaptor once the job started to run.

mark_submitted() → None[source]

Mark the job as submitted.

Called by the infrastructure adaptor upon receiving the job.

result: 'Result' | None
set_failed() → None[source]

Mark the job as failed.

Called by the infrastructure adaptor when the job has completed unsuccessfully.

set_finished() → None[source]

Mark the job as finished.

Called by the infrastructure adaptor when the job has completed successfully.

solver_id: str
started_at: datetime | None
state: JobState
submitted_at: datetime | None
class DikeBenchmarker.benchmarkatoms.JobState(value)[source]

Bases: Enum

Possible states of a Job.

CANCELLED = 6
CREATED = 1
FAILED = 5
FINISHED = 4
RUNNING = 3
SUBMITTED = 2
exception DikeBenchmarker.benchmarkatoms.JobStateError[source]

Bases: Exception

Raised when an invalid state transition is attempted on a Job.

class DikeBenchmarker.benchmarkatoms.ResourceResult(state: State = State.NONE, detail: str | None = None, cputime: float | None = None, walltime: float | None = None, memory: float | None = None)[source]

Bases: AbstractResult

Resource usage and limit outcome of one wrapped execution.

class State(value)[source]

Bases: str, Enum

Possible resource-limit verdicts a wrapper can report.

ERROR = 'error'
MEMOUT = 'memout'
NONE = 'none'
SUCCESS = 'success'
TIMEOUT = 'timeout'
cputime: float | None = None
memory: float | None = None
state: State = 'none'
walltime: float | None = None
class DikeBenchmarker.benchmarkatoms.Result(job: Job)[source]

Bases: object

Aggregate benchmarking result composed of independent per-dimension atoms.

property detail: str | None

Join every atom’s detail message, namespaced by atom name.

get_job() → Job[source]

Return the job object associated with this result.

property has_error: bool

Return True if any atom reports an error.

property has_result: bool

Return True if any atom produced a valid, non-error result.

property is_empty: bool

Return True only if every atom is still empty (nothing has produced data yet).

to_eval_record() → dict[source]

Flatten every attached atom’s fields into a namespaced dict.

class DikeBenchmarker.benchmarkatoms.SolverResult(state: State = State.NONE, detail: str | None = None)[source]

Bases: AbstractResult

Satisfiability verdict reported by a solver.

class State(value)[source]

Bases: str, Enum

Possible satisfiability verdicts a solver can report.

ERROR = 'error'
NONE = 'none'
SAT = 'sat'
UNKNOWN = 'unknown'
UNSAT = 'unsat'
state: State = 'none'

Module contents