The Standard Library

The Standard Library

Corset comes with a standard library, that provides functions commonly used in the writing of constraints.

Logical Functions

These functions implement boolean and loobean conditions on their operands.

Conversion Functions

(force-bool x) ⊨ Any{M} ↦ 𝔹

force casts x as a boolean value; it is up to the user to ensure that x is indeed guaranteed to be a boolean. It is recommended to accompany any calls to this function to a debug call to is-binary on x.

Cutoff Functions

These functions returns values whose interpretation is based on their zero-ness, without any assumptions on their value in the non-zero range.

(and x y) ⊨ (Any{M} Any{M}) ↦ M

returns a non-zero value if x and y are non-zero, zero otherwise

(or x y) ⊨ (Any{M} Any{M}) ↦ M

returns a non-zero value if at least one of x and y are non-zero, zero otherwise

(any x...) ⊨ (Any{M} ...) ↦ M

returns a non-zero value if any of its arguments are non-zero, zero otherwise

(all x...) ⊨ (Any{M} ...) ↦ M

returns a non-zero value if all of its arguments are non-zero, zero otherwise

Boolean Functions

These functions returns boolean values, which are equal to 1 when the function semantic is satisfied, and 0 otherwise.

(~and x y) ⊨ (Any{M} Any{M}) ↦ 𝔹

returns 1 if x and y are non-zero, 0 otherwise

(~or x y) ⊨ (Any{M} Any{M}) ↦ 𝔹

returns a non-zero value if at least one of x and y are non-zero, zero otherwise

Loobean Functions

These functions returns loobean values, which are equal to 0 when the function semantic is satisfied, and a non-zero value otherwise.

(eq! x y) ⊨ (Any{𝔹} Any{𝔹}) ↦ 𝕃

returns 0 if x and y are equals, and 1 otherwise

(eq! x y) ⊨ (Any{M} Any{M}) ↦ 𝕃

returns 0 if x and y are equals, and a non-zero value otherwise

(neq! x y) ⊨ (Any{M} Any{M}) ↦ 𝕃

returns 1 if x and y are equals, and 0 otherwise

(and! x y) ⊨ (Any{M} Any{M}) ↦ 𝕃

returns 0 if x and y are non-zero, and a non-zero value otherwise

(or! x y) ⊨ (Any{M} Any{M}) ↦ 𝕃

returns 0 if at least one of x and y are non-zero, and a non-zero value otherwise

(any! x...) ⊨ (Any{M} ...) ↦ 𝕃

returns 0 if any of its arguments are non-zero, a non-zero value otherwise otherwise

(all! x...) ⊨ (Any{M} ...) ↦ 𝕃

returns 0 if all of its arguments are zero, a non-zero value otherwise

Chronological Functions

Chronological functions peeks into the past or future values of columns or expressions, allowing the writing of constraints describing to the temporal evolution of the system rather than its instantaneous state.

Access Functions

Access functions fetch the value of a column at a different row than the currently evaluated one, and are the primitives used to build all more specialized chronological function.

(shift X n) ⊨ (Column{M} int) ↦ Column{M}

returns the value of the column X n steps in the past (if n is negative) or the future (if n is positive)

(prev X) ⊨ Column{M} ↦ Column{M}

return the value of X one step in the past

(next X) ⊨ Column{M} ↦ Column{M}

return the value of X one step in the future

Variation Functions

These functions define constraints to the variation of a column in the temporal dimension.

Definite Variations

These functions impose an exact numeric variation on the concerned column.

(did-inc! X offset) ⊨ (Column{M} integer) ↦ 𝕃

ensures that X increased by offset during the transition between the previous row and the current

(did-dec! X offset) ⊨ (Column{M} integer) ↦ 𝕃

ensures that X decreased by offset during the transition between the previous row and the current

(will-inc! X offset) ⊨ (Column{M} integer) ↦ 𝕃

ensures that X will increase by offset during the transition between the current row and the next one

(will-dec! X offset) ⊨ (Column{M} integer) ↦ 𝕃

ensures that X will decrease by offset during the transition between the current row and the next one

(In)Constancy

These functions constrain whether a given column has (resp. will) remained constant (resp. changed) between two consecutive rows.

(remained-constant! X) ⊨ (Column{M}) ↦ 𝕃

ensures that X has not changed its value between the previous row and the current one

(will-remain-constant! X) ⊨ (Column{M}) ↦ 𝕃

ensures that X will not change its value between the current row and the next one

(did-change! X) ⊨ (Column{M}) ↦ 𝕃

ensures that X has changed value between the current row and the previous one

(will-change! X) ⊨ (Column{M}) ↦ 𝕃

ensures that X will change its value between the current row and the next one

Value Latching

These functions impose a value to a given column at the previous (resp. next) row.

(was-eq! X n) ⊨ (Column{M} integer) ↦ 𝕃

ensure that X was equal to n at the previous row

(will-eq! X n) ⊨ (Column{M} integer) ↦ 𝕃

ensure that X will be equal to n at the next row