Packages
fixpoint
0.15.4
0.22.2
0.22.1
0.21.5
0.21.4
0.21.3
0.21.2
0.21.1
0.21.0
0.20.6
0.20.5
0.20.4
0.20.3
0.20.2
0.20.1
0.19.5
0.19.4
0.19.3
0.19.2
0.19.1
0.18.2
0.18.1
0.17.6
0.17.5
0.17.4
0.17.3
0.17.2
0.17.1
0.16.5
0.16.4
0.16.3
0.16.2
0.16.1
0.16.0
0.15.6
0.15.5
0.15.4
0.15.3
0.15.2
0.15.1
0.15.0
0.14.9
0.14.8
0.14.7
0.14.6
0.14.5
0.14.4
0.14.3
0.14.2
0.14.1
0.13.5
0.13.4
0.13.2
0.13.1
0.12.9
0.12.8
0.12.7
0.12.6
0.12.5
0.12.4
0.12.2
0.12.1
0.11.8
0.11.7
0.11.6
0.11.5
0.11.4
0.11.3
0.11.2
0.11.1
0.10.7
0.10.6
0.10.5
0.10.4
0.10.3
0.10.2
0.10.1
0.9.12
0.9.11
0.9.10
0.9.9
0.9.8
0.9.7
0.9.6
0.9.5
0.9.4
0.9.3
0.9.2
0.9.1
0.9.0
0.8.52
0.8.51
0.8.50
0.8.49
0.8.48
0.8.46
0.8.44
0.8.43
0.8.42
0.8.41
0.8.40
0.8.39
0.8.38
0.8.37
0.8.36
0.8.35
0.8.34
0.8.33
0.8.32
0.8.31
0.8.30
0.8.29
0.8.28
0.8.27
0.8.26
0.8.25
0.8.24
0.8.23
0.8.22
0.8.21
0.8.20
0.8.19
0.8.18
0.8.17
0.8.16
0.8.15
0.8.14
0.8.13
0.8.12
0.8.11
0.8.10
0.8.9
0.8.8
0.8.7
0.8.6
0.8.5
0.8.4
0.8.3
0.8.2
0.8.1
0.8.0
0.7.10
0.7.9
0.7.8
0.7.7
0.7.6
0.7.5
0.7.4
0.7.3
0.7.2
0.7.1
0.7.0
0.6.5
0.6.4
0.6.3
0.6.2
0.6.1
0.6.0
0.5.12
0.5.11
0.5.10
0.5.9
0.5.8
0.5.7
0.5.6
0.5.5
0.5.4
0.5.3
0.5.2
0.5.1
0.5.0
0.4.3
0.4.2
0.4.1
0.4.0
0.3.6
0.3.5
0.3.4
0.3.3
0.3.2
0.3.1
0.3.0
0.2.3
0.2.2
0.2.1
0.1.3
0.1.2
0.1.1
0.1.0
Constraint Programming Solver
Current section
Files
Jump to
Current section
Files
lib/solver/constraints/propagators/reified.ex
defmodule CPSolver.Propagator.Reified do
use CPSolver.Propagator
alias CPSolver.BooleanVariable, as: BoolVar
alias CPSolver.Propagator
@moduledoc """
The propagator for reification constraints.
Full reification:
1. If b is fixed to 1, the propagator for the reification reduces to a propagator for C.
2. If b is fixed to 0, the propagator for the reification reduces to a propagator for opposite(C).
3. If a propagator for C would realize that the C would be entailed, the propagator for the reification fixes b to 1 and ceases to exist.
4. If a propagator for C would realize that the C would fail, the propagator for the reification fixes x b to 0 and ceases to exist.
Half-reification:
Rules 2 and 3 of full reification.
Inverse implication:
Rules 1 and 4 of full reification.
"""
def new(propagators, b_var, mode) when mode in [:full, :half, :inverse_half] do
new([propagators, b_var, mode])
end
@impl true
def variables([propagators, b_var, _mode]) do
Enum.reduce(
propagators,
[set_propagate_on(b_var, :fixed)],
fn p, acc -> acc ++ Propagator.variables(p) end
)
|> Enum.uniq()
end
@impl true
def filter(args, nil, changes) do
filter(args, initial_state(args), changes)
end
def filter(
[_propagators, b_var, mode] = _args,
%{active_propagators: active_propagators} = _state,
changes
) do
filter_impl(mode, b_var, active_propagators, changes)
end
@impl true
def bind(
%{args: [propagators, b_var, mode] = _args, state: state} = propagator,
source,
var_field
) do
bound_propagators = Enum.map(propagators, fn p -> Propagator.bind(p, source, var_field) end)
Map.put(propagator, :args, [
bound_propagators,
Propagator.bind_to_variable(b_var, source, var_field),
mode
])
|> Map.put(:state, %{active_propagators: bound_propagators, b_idx: state[:b_idx]})
end
defp actions() do
%{
:full => [
&propagate/2,
&propagate_negative/2,
&terminate_false/1,
&terminate_true/1
],
:half => [nil, &propagate_negative/2, nil, &terminate_true/1],
:inverse_half => [&propagate/2, nil, &terminate_false/1, nil]
}
end
## Callbacks for reified
defp propagate(propagators, incoming_changes) do
res =
Enum.reduce_while(propagators, [], fn p, active_propagators_acc ->
case Propagator.filter(p, changes: incoming_changes) do
:fail ->
throw(:fail)
%{active?: active?} ->
{:cont, (active? && [p | active_propagators_acc]) || active_propagators_acc}
:stable ->
{:cont, [p | active_propagators_acc]}
end
end)
cond do
res == :fail -> :fail
Enum.empty?(res) -> :passive
true -> {:state, %{active_propagators: res}}
end
end
defp propagate_negative(propagators, changes) do
propagators
|> opposite_propagators()
|> propagate(changes)
end
defp terminate_true(b_var) do
terminate_propagator(b_var, true)
end
defp terminate_false(b_var) do
terminate_propagator(b_var, false)
end
defp terminate_propagator(b_var, bool) do
(bool && fix(b_var, 1)) || fix(b_var, 0)
:passive
end
defp filter_impl(mode, b_var, propagators, changes) do
[propagate_action, propagate_negative_action, fix_to_false_action, fix_to_true_action] =
Map.get(actions(), mode)
cond do
BoolVar.true?(b_var) ->
propagate_action && propagate_action.(propagators, changes) && active_state(propagators)
BoolVar.false?(b_var) ->
propagate_negative_action && propagate_negative_action.(propagators, changes) &&
active_state(propagators)
true ->
## Control variable is not fixed
case check_propagators(propagators, changes) do
:fail ->
fix_to_false_action && fix_to_false_action.(b_var) && active_state(propagators)
:entailed ->
fix_to_true_action && fix_to_true_action.(b_var) && active_state(propagators)
active_propagators ->
active_state(active_propagators)
end
end
end
defp initial_state([propagators, _b_var, _mode] = args) do
%{active_propagators: propagators, b_idx: length(variables(args)) - 1}
end
defp check_propagators(propagators, _incoming_changes) do
propagators
|> Enum.reduce_while(
[],
fn p, active_propagators_acc ->
cond do
Propagator.failed?(p) ->
{:halt, :fail}
Propagator.entailed?(p) ->
{:cont, active_propagators_acc}
true ->
{:cont, [p | active_propagators_acc]}
end
end
)
|> case do
:fail ->
:fail
active_propagators ->
(Enum.empty?(active_propagators) && :entailed) || active_propagators
end
end
defp opposite_propagators(propagators) do
Enum.map(propagators, fn p -> opposite(p) end)
end
## Opposite propagators
alias CPSolver.Propagator.{Equal, NotEqual, Less, LessOrEqual, Absolute, AbsoluteNotEqual}
defp opposite(%{mod: Equal} = p) do
%{p | mod: NotEqual}
end
defp opposite(%{mod: NotEqual} = p) do
%{p | mod: Equal}
end
defp opposite(%{mod: LessOrEqual, args: [x, y, offset]} = p) do
%{p | mod: Less, args: [y, x, -offset]}
end
defp opposite(%{mod: Absolute} = p) do
%{p | mod: AbsoluteNotEqual}
end
defp active_state(propagators) do
{:state, %{active?: true, active_propagators: propagators}}
end
end