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.