Metadata-Version: 2.1
Name: smartalloc
Version: 0.0.0
Summary: Resource allocation using an SMT solver.
Home-page: https://github.com/ignirtoq/smartalloc
Author: Jeffrey Bouas
Author-email: ignirtoq+smartalloc@gmail.com
License: MIT
Platform: UNKNOWN
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python
Classifier: Programming Language :: Python :: 2
Classifier: Programming Language :: Python :: 2.7
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.4
Classifier: Programming Language :: Python :: 3.5
Classifier: Programming Language :: Python :: 3.6
Classifier: Programming Language :: Python :: 3.7
Description-Content-Type: text/markdown
Requires-Dist: z3-solver

# smartalloc

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.

Allocation
----------
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.

The ``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.


