Metadata-Version: 2.1
Name: smartalloc
Version: 0.0.1
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
Description: # 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.
        
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
