Arithmetic constraints

The primitives every flattened model bottoms out in.

There is deliberately no int_le, int_plus, bool_and or bool_array_or here. Where a constraint is the same relation as another in a different argument shape, only the general form is kept: int_lin_le covers every integer inequality, bool_array_and covers the binary conjunction, bool_clause_reif covers disjunction, and rewriting into them costs nothing but a list literal. See About the registry for the rule in full.

The relations here also have a reified form _reif and an implied form _imp, taking the base arguments followed by a Boolean r. The operators do not: int_times computes a product rather than checking one, and a functional constraint names neither.

47 constraints

bool_array_and

bool_array_and(list of var bool: xs, var bool: r)

The result holds exactly when every element of the array does.

$$r \leftrightarrow \bigwedge_{i} \mathit{xs}_i$$

True when xs is empty. The binary conjunction is this constraint with a two-element list.

bool_array_xor

bool_array_xor(list of var bool: xs)

also declarable as bool_array_xor_reif and bool_array_xor_imp

An odd number of the array’s elements hold.

$$\bigoplus_{i} \mathit{xs}_i$$

bool_clause

bool_clause(list of var bool: pos, list of var bool: neg)

also declarable as bool_clause_reif and bool_clause_imp

At least one of the positive literals holds, or at least one of the negative literals fails.

$$\bigvee_{i} \mathit{pos}_i \;\vee\; \bigvee_{j} \neg \mathit{neg}_j$$

The CNF clause every SAT-style solver is built around. Either list may be empty, but not both. Implication is this constraint: a → b is ([b], [a]).

bool_lin_eq

bool_lin_eq(list of int: coeffs, list of var bool: xs, var int: total)

The weighted count of the Booleans that hold equals a given total.

$$\sum_{i} \mathit{coeffs}_i \cdot [\,\mathit{xs}_i\,] = \mathit{total}$$

[x] is 1 when x holds and 0 otherwise. Equality and negation between Booleans are both this constraint: a ↔ b is ([1,-1], [a,b], 0) and a ↔ ¬b is ([1,1], [a,b], 1).

bool_lin_le

bool_lin_le(list of int: coeffs, list of var bool: xs, int: bound)

also declarable as bool_lin_le_reif and bool_lin_le_imp

The weighted count of the Booleans that hold is at most a constant.

$$\sum_{i} \mathit{coeffs}_i \cdot [\,\mathit{xs}_i\,] \leq \mathit{bound}$$

bool_lin_ne

bool_lin_ne(list of int: coeffs, list of var bool: xs, var int: total)

also declarable as bool_lin_ne_reif and bool_lin_ne_imp

The weighted count of the Booleans that hold differs from a given total.

$$\sum_{i} \mathit{coeffs}_i \cdot [\, \mathit{xs}_i \,] \neq \mathit{total}$$

bool_to_int

bool_to_int(var bool: a, var int: b)

Maps a Boolean to 1 when it holds and 0 when it does not.

$$b = \begin{cases} 1 & \text{if } a \\ 0 & \text{otherwise} \end{cases}$$

float_abs

float_abs(var float: a, var float: b)

The second float is the absolute value of the first.

$$b = \lvert a \rvert$$

float_acos

float_acos(var float: a, var float: b)

The second float is the arccosine of the first.

$$b = \arccos a$$

float_acosh

float_acosh(var float: a, var float: b)

The second float is the inverse hyperbolic cosine of the first.

$$b = \operatorname{arcosh} a$$

float_asin

float_asin(var float: a, var float: b)

The second float is the arcsine of the first.

$$b = \arcsin a$$

float_asinh

float_asinh(var float: a, var float: b)

The second float is the inverse hyperbolic sine of the first.

$$b = \operatorname{arsinh} a$$

float_atan

float_atan(var float: a, var float: b)

The second float is the arctangent of the first.

$$b = \arctan a$$

float_atanh

float_atanh(var float: a, var float: b)

The second float is the inverse hyperbolic tangent of the first.

$$b = \operatorname{artanh} a$$

float_ceil

float_ceil(var float: a, var int: b)

The integer is the smallest one no less than the float.

$$b = \lceil a \rceil$$

float_cos

float_cos(var float: a, var float: b)

The second float is the cosine of the first, in radians.

$$b = \cos a$$

float_cosh

float_cosh(var float: a, var float: b)

The second float is the hyperbolic cosine of the first.

$$b = \cosh a$$

float_div

float_div(var float: a, var float: b, var float: c)

The third float is the quotient of the first two.

$$c = a / b$$

Undefined when b = 0.

float_exp

float_exp(var float: a, var float: b)

The second float is e raised to the power of the first.

$$b = e^{a}$$

float_floor

float_floor(var float: a, var int: b)

The integer is the largest one no greater than the float.

$$b = \lfloor a \rfloor$$

float_in

float_in(var float: x, float: lower_bound, float: upper_bound)

also declarable as float_in_reif and float_in_imp

The float lies within an inclusive interval.

$$\mathit{lower\_bound} \leq x \;\wedge\; x \leq \mathit{upper\_bound}$$

float_lin_eq

float_lin_eq(list of float: coeffs, list of var float: xs, float: total)

also declarable as float_lin_eq_reif and float_lin_eq_imp

The weighted sum of the variables equals a constant.

$$\sum_{i} \mathit{coeffs}_i \cdot \mathit{xs}_i = \mathit{total}$$

float_lin_le

float_lin_le(list of float: coeffs, list of var float: xs, float: bound)

also declarable as float_lin_le_reif and float_lin_le_imp

The weighted sum of the variables is at most a constant.

$$\sum_{i} \mathit{coeffs}_i \cdot \mathit{xs}_i \leq \mathit{bound}$$

float_lin_lt

float_lin_lt(list of float: coeffs, list of var float: xs, float: bound)

also declarable as float_lin_lt_reif and float_lin_lt_imp

The weighted sum of the variables is strictly less than a constant.

$$\sum_{i} \mathit{coeffs}_i \cdot \mathit{xs}_i < \mathit{bound}$$

Kept alongside float_lin_le, unlike the integer case: there is no next float to shift the bound by.

float_lin_ne

float_lin_ne(list of float: coeffs, list of var float: xs, float: total)

also declarable as float_lin_ne_reif and float_lin_ne_imp

The weighted sum of the variables differs from a constant.

$$\sum_{i} \mathit{coeffs}_i \cdot \mathit{xs}_i \neq \mathit{total}$$

float_ln

float_ln(var float: a, var float: b)

The second float is the natural logarithm of the first.

$$b = \ln a$$

Undefined for a at most 0.

float_log10

float_log10(var float: a, var float: b)

The second float is the base-10 logarithm of the first.

$$b = \log_{10} a$$

Undefined for a at most 0.

float_log2

float_log2(var float: a, var float: b)

The second float is the base-2 logarithm of the first.

$$b = \log_{2} a$$

Undefined for a at most 0.

float_piecewise_linear

float_piecewise_linear(var float: x, list of float: x_knot, list of float: y_knot, var float: y)

also declarable as float_piecewise_linear_reif and float_piecewise_linear_imp

The two floats are related by the piecewise-linear function through the given knots.

$$y = \mathit{y\_knot}_k + \left( x - \mathit{x\_knot}_k \right) \cdot \frac{\mathit{y\_knot}_{k+1} - \mathit{y\_knot}_k}{\mathit{x\_knot}_{k+1} - \mathit{x\_knot}_k} \quad \text{where } \mathit{x\_knot}_k \leq x \leq \mathit{x\_knot}_{k+1}$$

x_knot must be non-decreasing, and the two knot arrays must have equal length. x is constrained to the interval the knots span.

float_piecewise_linear_non_continuous

float_piecewise_linear_non_continuous(var float: x, list of float: x_start, list of float: x_end, list of float: y_start, list of float: y_end, var float: y)

also declarable as float_piecewise_linear_non_continuous_reif and float_piecewise_linear_non_continuous_imp

The two floats are related by a piecewise-linear function whose pieces need not meet.

$$x \in [\, \mathit{x\_start}_i,\, \mathit{x\_end}_i \,] \;\wedge\; y = \mathit{y\_start}_i + \left( x - \mathit{x\_start}_i \right) \cdot \frac{\mathit{y\_end}_i - \mathit{y\_start}_i}{\mathit{x\_end}_i - \mathit{x\_start}_i} \quad \text{for some } i$$

The four arrays must have equal length, and x must lie in one of the intervals.

float_pow

float_pow(var float: a, var float: b, var float: c)

The third float is the first raised to the power of the second.

$$c = a^{b}$$

float_round

float_round(var float: a, var int: b)

The integer is the float rounded to nearest, halves away from zero.

$$b = \operatorname{round}(a)$$

float_sin

float_sin(var float: a, var float: b)

The second float is the sine of the first, in radians.

$$b = \sin a$$

float_sinh

float_sinh(var float: a, var float: b)

The second float is the hyperbolic sine of the first.

$$b = \sinh a$$

float_sqrt

float_sqrt(var float: a, var float: b)

The second float is the non-negative square root of the first.

$$b = \sqrt{a} \;\wedge\; b \geq 0$$

Undefined when a is negative.

float_tan

float_tan(var float: a, var float: b)

The second float is the tangent of the first, in radians.

$$b = \tan a$$

float_tanh

float_tanh(var float: a, var float: b)

The second float is the hyperbolic tangent of the first.

$$b = \tanh a$$

float_times

float_times(var float: a, var float: b, var float: c)

The third float is the product of the first two.

$$c = a \cdot b$$

int_abs

int_abs(var int: a, var int: b)

The second integer is the absolute value of the first.

$$b = \lvert a \rvert$$

int_div

int_div(var int: a, var int: b, var int: c)

Integer division truncating towards zero.

$$c = \operatorname{trunc}(a / b)$$

Undefined when b = 0; a solver may fail the constraint or reject the model.

int_lin_eq

int_lin_eq(list of int: coeffs, list of var int: xs, int: total)

also declarable as int_lin_eq_reif and int_lin_eq_imp

The weighted sum of the variables equals a constant.

$$\sum_{i} \mathit{coeffs}_i \cdot \mathit{xs}_i = \mathit{total}$$

coeffs and xs must have equal length. Equality between two variables, and addition, are both this constraint: a = b is ([1,-1], [a,b], 0) and a + b = c is ([1,1,-1], [a,b,c], 0).

int_lin_le

int_lin_le(list of int: coeffs, list of var int: xs, int: bound)

also declarable as int_lin_le_reif and int_lin_le_imp

The weighted sum of the variables is at most a constant.

$$\sum_{i} \mathit{coeffs}_i \cdot \mathit{xs}_i \leq \mathit{bound}$$

Strict inequality is the same constraint with a tighter bound: a < b is ([1,-1], [a,b], -1).

int_lin_ne

int_lin_ne(list of int: coeffs, list of var int: xs, int: total)

also declarable as int_lin_ne_reif and int_lin_ne_imp

The weighted sum of the variables differs from a constant.

$$\sum_{i} \mathit{coeffs}_i \cdot \mathit{xs}_i \neq \mathit{total}$$

int_mod

int_mod(var int: a, var int: b, var int: c)

The remainder of integer division, taking the sign of the dividend.

$$c = a - b \cdot \operatorname{trunc}(a / b)$$

Undefined when b = 0. The sign follows a, so -7 mod 2 = -1.

int_pow

int_pow(var int: a, var int: b, var int: c)

The third integer is the first raised to the power of the second.

$$c = a^{b}$$

Undefined when b is negative and a is neither 1 nor -1.

int_times

int_times(var int: a, var int: b, var int: c)

The third integer is the product of the first two.

$$c = a \cdot b$$

int_to_float

int_to_float(var int: a, var float: b)

Converts an integer to the float of the same value.

$$b = a$$