Skip to content
Snippets Groups Projects
Commit b8f983a4 authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Change name from veriT-schedgen to schedgen, mention PAAR publication.

This clarifies that the tool is solver independent.
veriT is now mentioned in the readme.
parent 7e18bdc1
No related branches found
No related tags found
No related merge requests found
# veriT-schedgen
# 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.
*schedgen* is a toolbox to easily generate and work with schedules for
SMT solvers and similar automated reasoning tools. It addresses
the core 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 strategies.
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.
The schedgen toolbox was originally developed to be used with the SMT solver
[veriT](https://www.verit-solver.org/), but is solver independent.
## Overview
The `schedgen` toolbox is a standard Python package. It has been tested with Python 3.10. To install the package it is enough to execute
......@@ -30,8 +33,10 @@ This will install the following tools that are part of the `schedgen` toolbox on
Each of those tools can generate an extensive documentation of the options it exposes via the standard `--help` option.
Some background information about the toolbox was [published](http://ceur-ws.org/Vol-3201/paper8.pdf) at the
PAAR workshop.
## A verit-schedgen Tutorial
## A schedgen Tutorial
This section shows how the `schedgen` toolbox can be used. We will build and explore an optimal schedule for some hand-crafted, artificialexample benchmark data. This data can be found in the file `contrib/example_data.csv`. The first strategy `base-strategy}`solves 20 benchmarks within one second. The five other strategies `extra01` to `extra05` solve up to five benchmarks exclusively such that `extra01` solves five benchmarks not solved by any other strategy, `extra02` solves four, and so on. There is one benchmark `unsolved.smt2` that is not solved by any strategy and a strategy `bad-strategy` that solves only one benchmark in 1.5 seconds. Hence, if the total timeout is six seconds we expect the optimal schedule to run the strategies in the order just presented for one second each. The solving times have been sampled from a normal distribution to ensure the resulting graphs look interesting.
......
......@@ -19,7 +19,7 @@ except FileNotFoundError:
long_description = short_description
setup(
name="veriT-schedgen",
name="schedgen",
version="0.1.0",
description=short_description,
long_description=long_description,
......@@ -27,7 +27,7 @@ setup(
author="Hans-Jörg Schurr",
author_email="hans-jorg.schurr@inria.fr",
python_requires=">=3.6.0",
url="https://gitlab.inria.fr/hschurr/verit-schedgen",
url="https://gitlab.uliege.be/verit/schedgen",
install_requires=["pandas", "pulp", "numpy", "jinja2"],
include_package_data=True,
packages=["schedgen"],
......
......@@ -4,7 +4,7 @@
*
* When the nix package manager is installed run
* > nix-shell
* to get a shell with the dependenies of veriT present. This was only tested
* to get a shell with the dependenies of schedgen present. This was only tested
* on NixOS, but should work on other platforms which are supported by the Nix
* packagemanger (such as MacOS X) too.
*/
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment