API documentation

Problem

Problem definition and related classes.

class processscheduler.problem.SchedulingProblem(name, horizon=None, delta_time=None, start_time=None, end_time=None)

Bases: _NamedUIDObject

A scheduling problem

Parameters
  • name (str) – the problem name, a string type

  • horizon (Optional[int]) – an optional integer, the final instant of the timeline

  • delta_time (Optional[timedelta]) – an optional timedelta object

  • start_time (Optional[datetime]) – an optional datetime object

  • end_time (Optional[datetime]) – an optional datetime object

  • datetime_format – an optional string

add_indicator_number_tasks_assigned(resource)

compute the number of tasks as resource is assigned

Parameters

resource (Resource) –

add_indicator_resource_cost(list_of_resources)

compute the total cost of a set of resources

Parameters

list_of_resources (List[Resource]) –

Return type

Indicator

add_indicator_resource_utilization(resource)

Compute the total utilization of a single resource.

The percentage is rounded to an int value.

Parameters

resource (Resource) –

Return type

Indicator

add_objective_flowtime(weight=1)

the flowtime is the sum of all ends, minimize. Be carful that it is contradictory with makespan

Return type

Union[ArithRef, Indicator]

add_objective_flowtime_single_resource(resource, time_interval=None, weight=1)

Optimize flowtime for a single resource, for all the tasks scheduled in the time interval provided. Is ever no time interval is passed to the function, the flowtime is minimized for all the tasks scheduled in the workplan.

Return type

Union[ArithRef, Indicator]

add_objective_makespan(weight=1)

makespan objective

Return type

Union[ArithRef, Indicator]

add_objective_priorities(weight=1)

optimize the solution such that all task with a higher priority value are scheduled before other tasks

Return type

Union[ArithRef, Indicator]

add_objective_resource_cost(list_of_resources, weight=1)

minimise the cost of selected resources

Parameters

list_of_resources (List[Resource]) –

Return type

Union[ArithRef, Indicator]

add_objective_resource_utilization(resource, weight=1)

Maximize resource occupation.

Parameters

resource (Resource) –

Return type

Union[ArithRef, Indicator]

add_objective_start_earliest(weight=1)

minimize the greatest start time, i.e. tasks are schedules as early as possible

Return type

Union[ArithRef, Indicator]

add_objective_start_latest(weight=1)

maximize the minimum start time, i.e. all the tasks are scheduled as late as possible

Return type

Union[ArithRef, Indicator]

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

maximize_indicator(indicator)

Maximize indicator

Parameters

indicator (Indicator) –

Return type

MaximizeObjective

minimize_indicator(indicator)

Minimize indicator

Parameters

indicator (Indicator) –

Return type

MinimizeObjective

Tasks

Inheritance diagram of processscheduler.task

The module that defines the task related classes.

class processscheduler.task.FixedDurationTask(name, duration, work_amount=0, priority=1, optional=False)

Bases: Task

Task with constant duration.

Parameters
  • name (str) – the task name. It must be unique

  • duration (int) – the task duration as a number of periods

  • work_amount (Optional[int]) – represent the quantity of work this task must produce

  • priority (Optional[int]) – the task priority. The greater the priority, the sooner it will be scheduled

  • optional (Optional[bool]) – True if task schedule is optional, False otherwise (default)

add_required_resource(resource, dynamic=False)

Add a required resource to the current task.

Parameters

resource (Resource) – any of one of the Resource derivatives class (Worker, SelectWorkers etc.)

If dynamic flag (False by default) is set to True, then the resource is dynamic and can join the task any time between its start and end times.

Return type

None

add_required_resources(list_of_resources, dynamic=False)

Add a set of required resources to the current task.

This method calls the add_required_resource method for each resource of the list. As a consequence, be aware this is not an atomic transaction.

Parameters

list_of_resources (List[Resource]) – the list of resources to add.

Return type

None

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_assertions(list_of_z3_assertions)

Take a list of constraint to satisfy. Create two cases: if the task is scheduled, nothing is done; if the task is optional, move task to the past

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task.VariableDurationTask(name, min_duration=0, max_duration=None, allowed_durations=None, work_amount=0, priority=1, optional=False)

Bases: Task

The duration can take any value, computed by the solver.

Parameters
  • name (str) –

  • min_duration (Optional[int]) –

  • max_duration (Optional[int]) –

  • allowed_durations (Optional[List[int]]) –

  • work_amount (Optional[int]) –

  • priority (Optional[int]) –

  • optional (Optional[bool]) –

add_required_resource(resource, dynamic=False)

Add a required resource to the current task.

Parameters

resource (Resource) – any of one of the Resource derivatives class (Worker, SelectWorkers etc.)

If dynamic flag (False by default) is set to True, then the resource is dynamic and can join the task any time between its start and end times.

Return type

None

add_required_resources(list_of_resources, dynamic=False)

Add a set of required resources to the current task.

This method calls the add_required_resource method for each resource of the list. As a consequence, be aware this is not an atomic transaction.

Parameters

list_of_resources (List[Resource]) – the list of resources to add.

Return type

None

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_assertions(list_of_z3_assertions)

Take a list of constraint to satisfy. Create two cases: if the task is scheduled, nothing is done; if the task is optional, move task to the past

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task.ZeroDurationTask(name, optional=False)

Bases: Task

Task with zero duration, an instant in the schedule.

The task end and start are constrained to be equal.

Parameters
  • name (str) – the task name. It must be unique

  • optional (Optional[bool]) –

add_required_resource(resource, dynamic=False)

Add a required resource to the current task.

Parameters

resource (Resource) – any of one of the Resource derivatives class (Worker, SelectWorkers etc.)

If dynamic flag (False by default) is set to True, then the resource is dynamic and can join the task any time between its start and end times.

Return type

None

add_required_resources(list_of_resources, dynamic=False)

Add a set of required resources to the current task.

This method calls the add_required_resource method for each resource of the list. As a consequence, be aware this is not an atomic transaction.

Parameters

list_of_resources (List[Resource]) – the list of resources to add.

Return type

None

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_assertions(list_of_z3_assertions)

Take a list of constraint to satisfy. Create two cases: if the task is scheduled, nothing is done; if the task is optional, move task to the past

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

Resources

Inheritance diagram of processscheduler.resource
class processscheduler.resource.CumulativeWorker(name, size, productivity=1, cost=None)

Bases: Resource

A cumulative worker can process multiple tasks in parallel.

Parameters
  • name (str) –

  • size (int) –

  • productivity (Optional[int]) –

  • cost (Optional[int]) –

add_busy_interval(task, interval)

add an interval in which the resource is busy

Parameters

interval (Tuple[ArithRef, ArithRef]) –

Return type

None

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_busy_intervals()

returns the list of all busy intervals

Return type

List[Tuple[ArithRef, ArithRef]]

get_select_workers()

Each time the cumulative resource is assigned to a task, a SelectWorker instance is assigned to the task.

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

class processscheduler.resource.Resource(name)

Bases: _NamedUIDObject

base class for the representation of a resource

Parameters

name (str) –

add_busy_interval(task, interval)

add an interval in which the resource is busy

Parameters

interval (Tuple[ArithRef, ArithRef]) –

Return type

None

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_busy_intervals()

returns the list of all busy intervals

Return type

List[Tuple[ArithRef, ArithRef]]

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

class processscheduler.resource.SelectWorkers(list_of_workers, nb_workers_to_select=1, kind='exact')

Bases: Resource

Class representing the selection of n workers chosen among a list of possible workers

Parameters
  • list_of_workers (List[Resource]) –

  • nb_workers_to_select (Optional[int]) –

  • kind (Optional[str]) –

add_busy_interval(task, interval)

add an interval in which the resource is busy

Parameters

interval (Tuple[ArithRef, ArithRef]) –

Return type

None

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_busy_intervals()

returns the list of all busy intervals

Return type

List[Tuple[ArithRef, ArithRef]]

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

class processscheduler.resource.Worker(name, productivity=1, cost=None)

Bases: Resource

A worker is an atomic resource that cannot be split into smaller parts. Typical workers are human beings, machines etc.

Parameters
  • name (str) –

  • productivity (Optional[int]) –

  • cost (Optional[int]) –

add_busy_interval(task, interval)

add an interval in which the resource is busy

Parameters

interval (Tuple[ArithRef, ArithRef]) –

Return type

None

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_busy_intervals()

returns the list of all busy intervals

Return type

List[Tuple[ArithRef, ArithRef]]

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

Constraints

Inheritance diagram of processscheduler.task_constraint, processscheduler.resource_constraint

Task constraints and related classes.

class processscheduler.task_constraint.ForceScheduleNOptionalTasks(list_of_optional_tasks, nb_tasks_to_schedule=1, kind='exact', optional=False)

Bases: TaskConstraint

Given a set of m different optional tasks, force the solver to schedule at at least/at most/exactly n tasks, with 0 < n <= m.

Parameters
  • nb_tasks_to_schedule (Optional[int]) –

  • kind (Optional[str]) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.OptionalTaskConditionSchedule(task, condition, optional=False)

Bases: TaskConstraint

An optional task that is scheduled only if a condition is fulfilled.

Parameters
  • condition (BoolRef) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.OptionalTasksDependency(task_1, task_2, optional=False)

Bases: TaskConstraint

task_2 is scheduled if and only if task_1 is scheduled

Parameters

optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.OrderedTaskGroup(list_of_tasks, time_interval=None, kind='lax', time_interval_length=0, optional=False)

Bases: TaskConstraint

A set of tasks that can be scheduled in a specified order, with time bounds.

Parameters
  • kind (Optional[str]) –

  • time_interval_length (Optional[int]) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.ScheduleNTasksInTimeIntervals(list_of_tasks, nb_tasks_to_schedule, list_of_time_intervals, kind='exact', optional=False)

Bases: TaskConstraint

Given a set of m different tasks, and a list of time intervals, schedule N tasks among m in this time interval

Parameters
  • kind (Optional[str]) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TaskEndAt(task, value, optional=False)

Bases: TaskConstraint

On task must complete at the desired time

Parameters
  • value (int) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TaskEndBeforeLax(task, value, optional=False)

Bases: TaskConstraint

task.end <= value

Parameters
  • value (int) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TaskEndBeforeStrict(task, value, optional=False)

Bases: TaskConstraint

task.end < value

Parameters
  • value (int) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TaskLoadBuffer(task, buffer, quantity, optional=False)

Bases: TaskConstraint

A task that loads a buffer

Parameters

optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TaskPrecedence(task_before, task_after, offset=0, kind='lax', optional=False)

Bases: TaskConstraint

Task precedence relation

Parameters

optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TaskStartAfterLax(task, value, optional=False)

Bases: TaskConstraint

task.start >= value

Parameters
  • value (int) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TaskStartAfterStrict(task, value, optional=False)

Bases: TaskConstraint

task.start > value

Parameters
  • value (int) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TaskStartAt(task, value, optional=False)

Bases: TaskConstraint

One task must start at the desired time

Parameters
  • value (int) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TaskUnloadBuffer(task, buffer, quantity, optional=False)

Bases: TaskConstraint

A tasks that unloads a buffer

Parameters

optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TasksContiguous(list_of_tasks, optional=False)

Bases: TaskConstraint

A list of tasks are scheduled contiguously.

Parameters

optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TasksDontOverlap(task_1, task_2, optional=False)

Bases: TaskConstraint

Two tasks must not overlap, i.e. one needs to be completed before the other can be processed

Parameters

optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TasksEndSynced(task_1, task_2, optional=False)

Bases: TaskConstraint

Two tasks that must complete at the same time

Parameters

optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.TasksStartSynced(task_1, task_2, optional=False)

Bases: TaskConstraint

Two tasks that must start at the same time

Parameters

optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.task_constraint.UnorderedTaskGroup(list_of_tasks, time_interval=None, time_interval_length=0, optional=False)

Bases: TaskConstraint

A set of tasks that can be scheduled in any order, with time bounds.

Parameters
  • time_interval_length (Optional[int]) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

Resource constraints and related classes.

class processscheduler.resource_constraint.DistinctWorkers(select_workers_1, select_workers_2, optional=False)

Bases: ResourceConstraint

Selected workers by both AlternateWorkers are constrained to be the same

Parameters

optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.resource_constraint.ResourceTasksDistance(resource, distance, list_of_time_intervals=None, optional=False, mode='exact')

Bases: ResourceConstraint

Force a minimal/exact/maximal number time unitary periods between tasks for a single resource. This distance constraint is restricted to a certain number of time intervals

Parameters
  • distance (int) –

  • list_of_time_intervals (Optional[list]) –

  • optional (Optional[bool]) –

  • mode (Optional[str]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.resource_constraint.ResourceUnavailable(resource, list_of_time_intervals, optional=False)

Bases: ResourceConstraint

set unavailablity or a resource, in terms of busy intervals

Parameters

optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.resource_constraint.SameWorkers(select_workers_1, select_workers_2, optional=False)

Bases: ResourceConstraint

Selected workers by both AlternateWorkers are constrained to be the same

Parameters

optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

class processscheduler.resource_constraint.WorkLoad(resource, dict_time_intervals_and_bound, kind='max', optional=False)

Bases: ResourceConstraint

set a mini/maxi/exact number of slots a resource can be scheduled.

Parameters
  • kind (Optional[str]) –

  • optional (Optional[bool]) –

append_z3_assertion(z3_assertion)

Add a z3 assertion to the list of assertions to be satisfied.

Parameters

z3_assertion (BoolRef) – the z3 assertion

Return type

bool

get_z3_assertions()

Return the assertions list

Return type

List[BoolRef]

set_created_from_assertion()

Set the flag created_from_assertion True. This flag must be set to True if, for example, a constraint is defined from the expression: ps.not_(ps.TaskStartAt(task_1, 0)) thus, the Task task_1 assertions must not be add to the z3 solver.

Return type

None

set_z3_assertions(list_of_z3_assertions)

Each constraint comes with a set of z3 assertions to satisfy.

Parameters

list_of_z3_assertions (List[BoolRef]) –

Return type

None

Solver

Solver definition and related classes/functions.

class processscheduler.solver.SchedulingSolver(problem, debug=False, max_time=10, parallel=False, random_values=False, logics=None, verbosity=0, optimizer='incremental', optimize_priority='pareto')

Bases: object

A solver class

Parameters
  • debug (Optional[bool]) –

  • max_time (Optional[int]) –

  • parallel (Optional[bool]) –

  • random_values (Optional[bool]) –

  • logics (Optional[str]) –

  • verbosity (Optional[int]) –

  • optimizer (Optional[str]) –

  • optimize_priority (Optional[str]) –

build_solution(z3_sol)

create and return a SchedulingSolution instance

check_sat()

check satisfiability. Returns resulta as True (sat) or False (unsat, unknown). The computation time.

create_objective()

create optimization objectives

Return type

bool

export_to_smt2(smt_filename)

export the model to a smt file to be processed by another SMT solver

Parameters

smt_filename (str) –

find_another_solution(variable)

let the solver find another solution for the variable

Parameters

variable (ArithRef) –

Return type

bool

print_assertions()

A utility method to display solver assertions

print_solution()

A utility method that displays all internal variables for the current solution

print_statistics()

A utility method that displays solver statistics

solve()

call the solver and returns the solution, if ever

Return type

Union[bool, SchedulingSolution]

solve_optimize_incremental(variable, max_recursion_depth=None, kind='min')

target a min or max for a variable, without the Optimize solver. The loop continues ever and ever until the next value is more than 90%

Parameters
  • variable (ArithRef) –

  • max_recursion_depth (Optional[int]) –

  • kind (Optional[str]) –

Return type

int

Solution

Solution definition and Gantt export.

class processscheduler.solution.BufferSolution(name)

Bases: object

Class to represent the solution for a Buffer.

Parameters

name (str) –

class processscheduler.solution.ResourceSolution(name)

Bases: object

Class to represent the solution for the resource assignments.

Parameters

name (str) –

class processscheduler.solution.SchedulingSolution(problem)

Bases: object

A class that represent the solution of a scheduling problem. Can be rendered to a matplotlib Gantt chart, or exported to json

add_indicator_solution(indicator_name, indicator_value)

Add indicator solution.

Parameters
  • indicator_name (str) –

  • indicator_value (int) –

Return type

None

add_resource_solution(resource_solution)

Add resource solution.

Parameters

resource_solution (ResourceSolution) –

Return type

None

add_task_solution(task_solution)

Add task solution.

Parameters

task_solution (TaskSolution) –

Return type

None

get_all_tasks_but_unavailable()

Return all tasks except those of the type UnavailabilityTask used to represent a ResourceUnavailable constraint.

get_scheduled_tasks()

Return scheduled tasks.

render_gantt_matplotlib(fig_size=(9, 6), show_plot=True, show_indicators=True, render_mode='Resource', fig_filename=None)

generate a gantt diagram using matplotlib. Inspired by https://www.geeksforgeeks.org/python-basic-gantt-chart-using-matplotlib/

Parameters
  • fig_size (Optional[Tuple[int, int]]) –

  • show_plot (Optional[bool]) –

  • show_indicators (Optional[bool]) –

  • render_mode (Optional[str]) –

  • fig_filename (Optional[str]) –

Return type

None

render_gantt_plotly(fig_size=None, show_plot=True, show_indicators=True, render_mode='Resource', sort=None, fig_filename=None, html_filename=None)

Use plotly.create_gantt method, see https://plotly.github.io/plotly.py-docs/generated/plotly.figure_factory.create_gantt.html

Parameters
  • fig_size (Optional[Tuple[int, int]]) –

  • show_plot (Optional[bool]) –

  • show_indicators (Optional[bool]) –

  • render_mode (Optional[str]) –

  • sort (Optional[str]) –

  • fig_filename (Optional[str]) –

  • html_filename (Optional[str]) –

Return type

None

to_json_string()

Export the solution to a json string.

Return type

str

class processscheduler.solution.TaskSolution(name)

Bases: object

Class to represent the solution for a scheduled Task.

Parameters

name (str) –