veriT-schedgen

veriT-schedgen is a tool to easily generate schedules for SMT solvers and similar automated reasoning tools. It only addresses the easier part of the problem: to generate from a set of strategies a schedule which slices the available time into short runs with a specific strategy. The user has to come up with good option combinations.

The generator utilizes integer programming to find an optimal combination of slice length + strategy. The generated problems are not too difficult and can be solved on a laptop with open source integer programming tools.

Documentation

Unfortunately, the project currently lacks documentation.

On NixOS one can use the shell.nix file to bring the dependencies into context. On other systems Python3, Pandas, and PuLP is needed.

The main script is schedgen-optimize.py in the folder schedgen. Running this command with --help produces an overview of the available options. For some pointers on how to use everything, take a look at the contrib/run.sh script.