DikeBenchmarker.solveradaptors package

Submodules

DikeBenchmarker.solveradaptors.abstractexecutable module

Abstract Executable.

Defines the AbstractExecutable class, which serves as a base for managing executables such as solvers, execution wrappers, or proof checkers. It provides methods for registering executables, reading them from a registry file, formatting command lines, and parsing results.

class DikeBenchmarker.solveradaptors.abstractexecutable.AbstractExecutable(serialized: dict = None)[source]

Bases: ABC

Interface for Executables such as Solvers or Execution Wrappers.

format_command(xid: str, binaries: list[str], *args, **kwargs) → str[source]

Return the command line to run the executable with parameters.

classmethod from_dict(data: dict) → AbstractExecutable[source]

Create an executable from a dictionary representation.

get_binaries(xid: str) → list[str][source]

Return the binary paths for a given executables ID.

get_checker(xid: str) → str[source]

Return the checker command for a given executable ID.

get_format_string(xid: str) → str[source]

Return the format string for a given executable ID.

get_ids() → list[str][source]

Return a list of available solver IDs.

abstractmethod parse_result(*args, **kwargs) → AbstractResult[source]

Parse result files; returns instance of an AbstractResult implementation.

read_registry(registry_path: str)[source]

Read a CSV registry file to populate executable configurations.

The CSV file format is: id;bin;fmt;checker

Parameters:

  • id (-) – Executable identifier (e.g., solver name, wrapper name)

  • bin (-) – Path(s) to binary executable(s), comma-separated. Relative paths are resolved relative to the registry file’s directory.

  • fmt (-) – Command format string with placeholders: - $BIN0, $BIN1, … for binary paths (in order) - Custom placeholders (e.g., $INST, $CERT) replaced by _format_extra()

  • checker (-) – Optional checker command ID for validating executable output

register(xid: str, sbin: list[str], sfmt: str, checker: str = None)[source]

Register an executable with its path and command format.

registry = {}
to_dict() → dict[source]

Convert the executable to a dictionary representation.

DikeBenchmarker.solveradaptors.checkeradaptor module

This module provides an adaptor for executing checkers of sat or unsat certificates.

class DikeBenchmarker.solveradaptors.checkeradaptor.CheckerAdaptor(serialized: dict = None)[source]

Bases: AbstractExecutable

A class for executing checkers of sat or unsat certificates.

DEFAULT_VARIANT = '32'
GRAT_MAXHEAP = {'256': '230G', '32': '31G', '64': '62G'}
HEAP_VARIANTS = ('256', '64', '32')
SCALABLE_BINARIES = ('cake_lpr', 'cake_pb_cnf')
format_command(xid, binaries, instance: str, certificate: str, trimmer_output: str, checker_output: str) → str[source]

Get the command line for a given checker ID, replacing placeholders.

get_binaries(xid: str) → list[str][source]

Return the binary paths for a checker id, resolving its heap-size variant.

parse_result(trimmer_file: str, checker_file: str) → CheckerResult[source]

Classify the trimmer + checker pipeline.

DikeBenchmarker.solveradaptors.executionwrapper module

Provides access to execution wrappers like runexec, runlim, or benchexec.

Resolves the paths to the wrapper binaries and constructs command-line arguments using the specified resource limits.

class DikeBenchmarker.solveradaptors.executionwrapper.ExecutionWrapper(mem=65536, cputime=3600, walltime=7200, serialized: dict = None)[source]

Bases: AbstractExecutable

A class to manage execution wrappers.

format_command(xid: str, binaries: list[str], wrapped_cmd: str, wrapper_output: str, wrapped_output: str, watcher_output: str) → str[source]

Return the command line to run the execution wrapper with parameters.

classmethod from_dict(data: dict) → ExecutionWrapper[source]

Create an execution wrapper from a dictionary representation.

parse_result(wrapper_file: str, watcher_file: str) → ResourceResult[source]

Parse wrapper record + watcher log into resource-based metrics.

set_resource_limits(cputimelimit: int = None, walltimelimit: int = None, memorylimit: int = None)[source]

Set resource limits if specified.

to_dict() → dict[source]

Convert the execution wrapper to a dictionary representation.

DikeBenchmarker.solveradaptors.solveradaptor module

SAT Solver Adaptor.

class DikeBenchmarker.solveradaptors.solveradaptor.SolverAdaptor(serialized: dict = None)[source]

Bases: AbstractExecutable

Maintain paths to solvers and make them accessible by their IDs.

format_command(xid: str, binaries: list[str], instance: str, certificate: str) → str[source]

Get the command line for a given solver ID, replacing placeholders.

parse_result(outfile: str) → SolverResult[source]

Classify the solver verdict.

Module contents