assign_value r distincts eq
selects the value to assign to r
in the model as a term t
, and returns Some (t, is_cs)
. is_cs
is described below.
If no appropriate value can be chosen here, return None
(only do this if either r
is already a value, or there is a mechanism somewhere else in the code, such as the case_split
function of a relation module, that ensures completeness of the generated model).
r
is the current class representative that a value should be chosen for. No assumptions should be made on the shape of r
, but do return None
if it is already a value.
distincts
is a list of term representatives that the returned value must be distinct from (choosing a value that is present in distincts
will cause the solver to loop infinitely).
eq
is a list of pairs (t, r)
of terms and their initial representative (i.e., r
is fst (X.make t)
for each pair) that encode the equivalence class of r
.
The returned bool serves a similar purpose as the is_cs
flag in Th_util.case_split
.
It should usually be true
, which indicates that the returned term is not forced.
Use false
only when the returned term contains aliens that should be assigned (e.g. records).
**When returning false
, you must ensure that the equality between the first argument and the return value always hold (i.e. is a *unit* fact). In particular, the equality *must not* depend on distincts
-- doing so would be unsound.**
In other words, if assign_value r distincts eq
returns Some (t, false)
, then there must be no context in which solve r (fst X.make t)
raises Unsolvable
. You have been warned!