Tutorial Understanding ProB's Constraint Solver

We assume that you grasped the way that ProB setups up the initial states of a B machine as outlined in Tutorial Setup Phases, and have understood why animation is difficult as outlined in Tutorial Understanding the Complexity of B Animation.

First, it is important to understand that as of version 1.3, ProB uses two representations for sets and relations:

a classical list representation
a representation using AVL-trees.

The second representation allows ProB to deal with larger sets and relations (starting at around 100,000 elements performance will start to slow down). However, this representation can only be used if the constraint solver knows exactly all elements of a set or relation. The list representation will be used if only part of the set or relation is known.

To give an idea about the performance related to the new AVL-based representation, take the substitution

numbers := numbers - ran(%n.(n:cur..limit/cur|cur*n))

For limit=10,000 this takes 0.2 seconds (on a 2008 laptop); with the list representation this operation ran out of memory after 2 minutes in ProB 1.2.x.
For limit=100,000 this takes 2.1 seconds.
For limit=1,000,000 this takes about 21.9 seconds.

For example, if the PROPERTIES contains the following predicates

x = {1,2}
y = {1|-2, 3|->4, 4|->5}
a = 1 & b=2 & d = {a|-b}

then all values will be fully known and the new AVL-based representation will be used. However, for example for

card(x) = 2 & dom(x) = {1,2}

we would only have partial information about x (which the constraint solver will encode using the list [1|->_, 2|->_] where the underscore marks as of yet unknown bits.

Basically, the ProB constraint solver works as follows:

while interpreting the predicates, it will first try to "execute" predicates (or sub-predicates) which result in information which can be stored in AVL-form
after having interpreted the whole predicate, it will then perform deterministic propagation
only after all deterministic propagation has been performed, will the constraint solver start enumerating possibilities. For this it maintains a priority queue of enumerations and choice points.

The priority is a rough estimate of the number of possible solutions; predicates with the lowest estimate will be "executed" first.

The following picture provides a very rough picture of this process: