API Reference Fixpoint v0.8.30

Modules

Solver API.

Absolute value constraint. Costraints y to be |x|

Element constrains variables y and z such that: array[x] = y

Element2d constrains variables z, x and y such that: array2d[x][y] = z

Constraint store is a key-value store, where key is a variable id, and value is a implementation-dependent structure that allows to update and keep track of variables' domains.

The 'knapsack' problem is mathematically formulated in the following way. Given n items to choose from, each item i ∈ 0 ...n − 1 has a value v[i] and a weight w[i]. The knapsack has a limited capacity K. Let x[i] be a variable that is 1 if you choose to take item i and 0 if you leave item i behind. Then the knapsack problem is formalized as the following optimization problem

The classic "cryptarithmetic" (https://en.wikipedia.org/wiki/Verbal_arithmetic) problem. Solve the following (each letter is a separate digit)

The forward-checking propagator for AllDifferent constraint.

The propagator for 'circuit' constraint.

The constraint graph connects propagators and their variables. The edge between a propagator and a variable represents a notification the propagator receives upon variable's domain change.

The propagator for Element2D constraint.

The propagator for Sum constraint. Sum(y, x) constrains y to be a sum of variables in the list x.

Computation space. The concept is taken from Chapter 12, "Concepts, Techniques, and Models of Computer Programming" by Peter Van Roy and Seif Haridi.

View is a variable with attached mapper function. mapper is a bijection of the domain of original variable to the domain of the view