Check whether a tuple of variables cannot be constrained any further, in Mozart/Oz

Question

Greetings,

The idea can be best given with an example:

Suppose we have a vector vec(a:{FD.int 1#100} b:{FD.int 1#100} c:{FD.int 1#100}). I want to be able to add constraints to this vector, until the point that every additional constraint I add to it does not add any more information, e.g. does not constraint vec.a, vec.b and vec.c any further.

Is it possible to do it in Mozart/Oz?

I'd like to think it that way.

In a loop:

1. Access the constraint store,
2. Check whether it is changed
3. Terminate if there is no change.

Answer 1

You can check the state of a finite domain variable with the functions in the FD.reflect module. The FD.reflect.dom function seems especially useful in this context.

To get the current domain of every field in a record, you can map this function over records:

declare

fun {GetDomains Vec}
   {Record.map Vec FD.reflect.dom}
end

The initial result in your example would be:

vec(a:[1#100] b:[1#100] c:[1#100])

Now you can compare the result of this function before and after adding constraints, to see if anything happens.

Two limitations:

1. This will only work with constraints which actually change the domain of at least one variable. Some constraints change the constraint store but do not change any domains, for example an equality constraint with an unbound variable.
2. Using reflection like this does not work well with concurrency, i.e. if constraints are added from multiple threads, this will introduce race conditions.

If you need an example on how to use the GetDomains function in a loop, let me know...

EDIT: With a hint from an old mailing list message, I came up with this general solution which should work with all types of constraints. It works by speculatively executing a constraint in a subordinate computation space.

declare

Vec = vec(a:{FD.int 1#100} b:{FD.int 1#100} c:{FD.int 1#100})

%% A number of constraints as a list of procedures
Constraints =
[proc {$} Vec.a <: 50 end
 proc {$} Vec.b =: Vec.a end
 proc {$} Vec.b <: 50 end
 proc {$} Vec.a =: Vec.b end
]


%% Tentatively executes a constraint C (represented as a procedure).
%% If it is already entailed by the current constraint store, returns false.
%% Otherwise merges the space (and thereby finally executes the constraint)
%% and returns true.
fun {ExecuteConstraint C}
   %% create a compuation space which tentatively executes C
   S = {Space.new
        proc {$ Root}
           {C}
           Root = unit
        end
       }
in
   %% check whether the computation space is entailed
   case {Space.askVerbose S}
   of succeeded(entailed) then false
   else
      {Wait {Space.merge S}}
      true
   end
end


for C in Constraints I in 1..4 break:Break do
   {System.showInfo "Trying constraint "#I#" ..."}
   if {Not {ExecuteConstraint C}} then
      {System.showInfo "Constraint "#I#" is already entailed. Stopping."}
      {Break}
   end
   {Show Vec}
end

{Show Vec}