使用SMT解算器进行资源分配。
smartalloc的Python项目详细描述
智能分配
使用微软z3定理证明器的实用函数集合 找到优先分配的有限资源的最大分配 要执行的离散任务。
资源和任务
smartalloc被设计成与z3库周围的包装一样薄
可能，因此它不定义称为“resource”或“task”的类。
相反，z3原语（如int或real）被视为资源，并且 分配给它们的任务由（z3的集合）表示 约束条件。
分配
smartalloc的主要工作是allocate()函数。它需要
两个参数：资源的内在约束，以及
每个任务所需的约束。
立即应用内部资源约束，如果系统 已经没有解决方案，则将引发异常。在这之后， 每个任务的约束都会添加到系统中。如果系统仍然 可满足，则该任务被视为“已完成”，下一个任务将是 补充。如果系统不可满足，则该任务将从 移动到下一个之前的系统。提供的所有任务将尝试 添加到系统中；任务的顺序决定到哪个任务 先申请必要的资源。
allocate()函数返回两个项的元组。第一个是
分配描述对象（以Z3模型的形式）。价值
资源变量可以像字典一样使用它来检索
资源变量作为键。第二个是
来自输入的任务在分配结果中“工作”。
欢迎加入QQ群-->： 979659372
