MiniZinc / MiniSearch

the source code for the MiniSearch meta-search language
Other
5 stars 0 forks source link

Post predicate in MiniSearch apparently not posting the constraint #5

Open jacopoMauro opened 8 years ago

jacopoMauro commented 8 years ago

It seems that the post predicate in minisearch is not properly behaving.

Consider for instance the following program that is using an array of 4 variables with 0..1 domain.

include "minisearch.mzn";

% locations
set of int: locations;
locations = 1..4;
array[ locations ] of var 0..1: used_locations;

constraint sum( used_locations ) = 3; 

function ann: test1(array[int] of var int: used_locations) = (
    next() /\  
    commit() /\
    print() /\
      repeat (i in 1..5) (
        print("% Enter iteration " ++ show(i) ++ "\n") /\
        let {
          int: a = 0;
          int: b = 0;
        } in (
          a := uniform(1,length(used_locations)) /\
          b := uniform(1,length(used_locations)) /\
          if sol(used_locations[a]) > sol(used_locations[b])
          then
            print("% Trying to swap " ++ show(a) ++ " with " ++ show(b) ++ "\n") /\
            scope(
              post(
               used_locations[a] = 0 /\ trace("used_locations[" ++ show(a) ++"] = 0" ++ "\n") /\
               forall (i in index_set(used_locations))(
                 if i != a /\ i != b
                 then used_locations[i] = sol(used_locations[i])
                 else true endif) 
              ) /\
              repeat (next() /\ commit() /\ print() \/ break)
            )
          else skip endif
        )
      )
);

solve search test1(used_locations);

output ["used locations: "++show(used_locations)];

Initially I ask that 3 of the 4 variables are set to be 1. Then I try to find a solution. As soon as I have a solution I try to swap the value of the variable a having sol(a) = 0 with another variable preserving the value of the other two variables. I do this by posting the constraint used_locations[a] = 0. At this point I search for all the possible solutions of the problem. I was expecting in output just one solution (only one solution exists) but instead I got 4 different outputs that are inconsistent with the constraint that I added using the post predicate.

The output look indeed as:

% Enter iteration 5
% Trying to swap 3 with 4
used_locations[3] = 0
used locations: [1, 1, 1, 0]
----------
used locations: [1, 1, 0, 1]
----------
used locations: [1, 0, 1, 1]
----------
used locations: [0, 1, 1, 1]
----------
==========

It seems that the constraints added by using the post predicate are not added into the model. Is this a bug?