Vector randomization & constraints don't work correctly.

[AnthonyVH]

I'm trying out the latest code in the development branch, using boost 1.57.0 on linux (Gentoo). When I run ex5_vec_constr, the produced output is (only the first 3 iterations are shown):

src_addr_vec = 28 8 12 4 0
dest_addr_vec = 8 16 24 32 40
data_vec = 4294901760 0 10 100 10 100 10 100 10 100

src_addr_vec = 212 252 240 244 248 220 232 236 228 224
dest_addr_vec = 7 15 23 31 39 47 55 63 71 79
data_vec = 4294901760 0 10 100 10 100 10 100 10 100 10 100 10 100 10 100 10 100 10 100

src_addr_vec = 20 24 28 8 12 4 0
dest_addr_vec = 12 20 28 36 44 52 60
data_vec = 4294901760 0 10 100 10 100 10 100 10 100 10 100 10 100

The printed elements have the following types:

crave::rand_vec<unsigned> src_addr_vec;
crave::rand_vec<unsigned> dest_addr_vec;
crave::rand_vec<unsigned> data_vec;

There seem to be a couple of issues with the generated values:

• Values in src_addr_vec often repeat across consecutive randomizations. The constraints on src_addr_vec's values don't enforce this repetition. On the other hand, the generated values do seem to conform to the constraints, they're just not uniformly randomly distributed. Here's the constraints:

constraint(foreach (src_addr_vec(), src_addr_vec()[_i] < 0xFF));
constraint(foreach (src_addr_vec(), src_addr_vec()[_i] % 4 == 0));
constraint(unique(src_addr_vec()));

• The constraints on dest_addr_vec require its first element to be >= 0 and < 15. All other elements depend on this:

constraint(foreach (dest_addr_vec(), if_then(_i == 0, dest_addr_vec()[_i] < 0xF)));
constraint(foreach (dest_addr_vec(), dest_addr_vec()[_i] == dest_addr_vec()[_i - 1] + 8));
constraint(unique(dest_addr_vec()));

However, after randomizing the vector 100 times and inspecting the 1st element (index 0), it's clear that it's not uniformly randomly distributed between 0 & 14 at all. The only values assigned to it are 7, 8 and 11.

• The constraint on data_vec's values don't seem to be upheld. Here's the constraint:

constraint(foreach (data_vec(), if_then_else(_i % 2 == 0, data_vec()[_i] <= 10,
  data_vec()[_i] == data_vec()[_i - 1] * data_vec()[_i - 1])));

The 1st element (index 0) should be <= 10, which clearly isn't the case. For the 2nd element, the constraint matches, because static_cast(4294901760 ⋅ 4294901760) == 0. Then for all the next elements, there's no randomness at all anymore.

I haven't been able to figure out from the code why this is happening, but I haven't had much time to look into it.

[hoangmle]

Thanks for reporting!

• The last issue is indeed a bug: the solver treats if_then_else as a whole and thus, due to the presence of _i - 1, it implies that _i cannot be 0 and ignores the constraint on the first element. This can be fixed easily.
• Vector constraints are mainly a proof-of-concept for the syntax, so the distribution of values is not yet optimized. This is more challenging, but not impossible to fix, at least for the example :) Are vector constraints important for your project?

[AnthonyVH]

I was wondering what would happen with 0 - 1, didn't realize the whole constraint would be ignored. Good to know!

I'm currently just checking how feasible it would be to use Crave for a project in the near future, so can't say for sure how important vector constraints/randomization is, but it's likely that it would be very useful. I've been playing around with "manually" randomizing objects in an std::vector, but this triggers other bugs (see #2).