API Reference Fixpoint v0.8.27


Solver API.

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

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.