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(outfile: str)[source]

Extract the result from the solver file.

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.

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.

parse_result(outfile: str)[source]

Extract the result from the checker file.

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) → 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(outfile: str)[source]

Parse the runsolver log output to extract runtime statistics.

Parameters: - tool_output: Path to the runsolver log output file.

Returns: - dictionary with keys ‘walltime’, ‘cputime’, ‘memory’, ‘timeout’, ‘memout’, and ‘exitstatus’.

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)[source]

Extract the result from the solver file.

Module contents