Resource allocation using an SMT solver.
A collection of utility functions for using Microsoft's Z3 theorem prover to find the maximal allocation of limited resources given a prioritized list of discrete tasks to be executed.
Resources and Tasks
smartalloc is designed to be as thin of a wrapper around the Z3 library as
possible, so it does not define classes called "Resource" or "Task."
Instead, Z3 primitives, such as Int or Real, are considered the resources, and tasks that they are allocated for are represented by (collections of) Z3 constraints.
The main workhorse of
smartalloc is the
allocate() function. It takes
two arguments: the intrinsic constraints on the resources, and a list of the
constraints required for each task.
Intrinsic resource constraints are applied immediately, and if the system already has no solution then an exception will be raised. After this, the constraints for each task are added to the system. If the system is still satisfiable then the task is considered "worked" and the next task will be added. If the system is not satisfiable, that task will be removed from the system before moving to the next. All tasks provided will be attempted to be added to the system; the ordering of the tasks determines which tasks get to claim their necessary resources first.
allocate() function returns a tuple of two items. The first is the
allocation description object (in the form of a Z3 model). The value of a
resource variable can be retrieved from it by using it like a dictionary with
the resource variable as the key. The second is a list of the indices of the
tasks from the input are "worked" in the allocation result.
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Hashes for smartalloc-0.0.1-py2.py3-none-any.whl