For users repair statistics are provided via the exported predicate repair_stat/1.
:- export struct(repair(
tent, % tentative value
mon, % set element with suspension of monitor_tenable goal
ga_chg % suspensions to wake on global assignment changes
)).
The value of the mon attribute has a special structure which
allows constant time set membership testing and update (see below).
monitor_tenable is suspended on constrained, and uses not_unify
to check if the variable is tenable. If the variable has just become
untenable, it wakes the ga_chg suspension list.
:- local struct(repair_state(
conflict_vars,
conflict_hash_constraints,
conflict_constraints
)).
All information about conflict constraints and variables is held in
this local reference.
The attribute conflict_hash_constraints records, for each conflict
set, its conflict constraints. The conflict sets are held in a hash
table. The third attribute, conflict_constraints, is a global
(unnamed) conflict set, kept for legacy reasons.
:- local struct(monitor_conflict(constraint,annotation,conflict,prop,module)).
This internal structure maintains the information necessary to monitor
conflicts for a repair constraint.
The annotation is the information returned by the system when
listing conflicts.
The conflict is a (constant time set membership) structure which
both records whether the constraint is in conflict, and holds the suspension
which keeps this information up to date.
The prop attribute records whether the constraint should also
be propagated.
monitor_conflict is a demon suspended on the constrained and ga_chg lists of all variables in the constraint, it instantiates the variables to their tentative values (if they have one), and runs the constraint using not not to avoid any side-effects. If the check fails, the conflict is recorded, and if the propagation flag is set (to 0) the constraint is invoked.
Invariants allow tentative values to be propagated through a function
(functional constraint) from its inputs to its outputs.
In essence this is achieved by making a copy of the constraint, replacing
the input variables by their tentative values. This copy of the constraint
is then invoked, thereby instantiating its outputs. Finally the output
values from the copied constraint are used to update the tentative values
of the output variables of the original constraint.
For mathematical invariants (with the form Var tent_is Expr)
the expression is first linearized, creating a sum expression of the form
C1*V1+C2*V2+...+Cn*Vn together with none or more nonlinear
constraints of the form V=NonLin.
The sum expression allows the invariant to be computed in a way that
is independent of the number of terms n.
Specifically if the tentative value of one term changes, the difference
between its old and new value is computed, and the tentative value of the
whole sum is changed by that amount. This is done by a demon sum_update.
A separate invariant is created to handle each nonlinear subexpression
V=NonLin using tent_call.
All other (non-arithmetic) invariants are handled using tent_call,
which is implemented by making a copy of the constraint, as described above.
The constant time set of conflict variables, containing the mon
attributes of the repair variables, is in the conflict_vars attribute
of the repair_state.
The constant time set of conflict constraints, containing the conflict
argument of the monitor_conflict predicates, is in the conflict_hash_constraints
(or conflict_constraints) attribute of the repair_state.