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

Return type:

None

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.

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

Return type:

None

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.

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

Return type:

None

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.

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.TaskEndBefore(task, value, kind='lax', optional=False)

Bases: TaskConstraint

task.end < value

Parameters:

  • value (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.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:

  • 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.TaskStartAfter(task, value, kind='lax', optional=False)

Bases: TaskConstraint

Parameters:

  • value (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.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

This constraint ensures that workers selected by two SelectWorker instances are distinct.

Parameters: - select_workers_1: The first set of selected workers. - select_workers_2: The second set of selected workers. - optional (bool, optional): Whether the constraint is optional (default is False).

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

This constraint enforces a specific number of time unitary periods between tasks for a single resource. The constraint can be applied within specified time intervals.

Parameters: - resource: The resource to which the constraint applies. - distance (int): The desired number of time unitary periods between tasks. - list_of_time_intervals (list, optional): A list of time intervals within which the constraint is restricted. - optional (bool, optional): Whether the constraint is optional (default is False). - mode (str, optional): The mode for enforcing the constraint - “exact” (default), “min”, or “max”.

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

This constraint sets the unavailability of a resource in terms of time intervals.

Parameters: - resource: The resource for which unavailability is defined. - list_of_time_intervals: A list of time intervals during which the resource is unavailable for any task.

For example, [(0, 2), (5, 8)] represents time intervals from 0 to 2 and from 5 to 8.

  • optional (bool, optional): Whether the constraint is optional (default is False).

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

This constraint ensures that workers selected by two SelectWorker instances are the same.

Parameters: - select_workers_1: The first set of selected workers. - select_workers_2: The second set of selected workers. - optional (bool, optional): Whether the constraint is optional (default is False).

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

A WorkLoad constraint restricts the number of tasks that can be executed on a resource during a certain time period. The resource can be a single Worker or a CumulativeWorker.

Parameters: - resource: The resource for which the workload constraint is defined. - dict_time_intervals_and_bound: A dictionary that maps interval tuples to integer bounds.

For example, {(1,20):6, (50,60):2} specifies that the resource can use no more than 6 slots in the interval (1,20), and no more than 2 slots in the interval (50,60).

  • kind (str, optional): Specifies whether the constraint is exact, a minimum, or a maximum (default is “max”).

  • optional (bool, optional): Whether the constraint is optional (default is False).

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(find_better_value=False)

check satisfiability. find_beter_value: the check_sat method is called from the incremental solver. Then we should not prompt that no solution can be found, but that no better solution can be found. Return * result as True (sat) or False (unsat, unknown). * the computation time.

Parameters:

find_better_value (Optional[bool]) –

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

get_parameters_description()

return the solver parameter names and values as a dict

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) –