karandeep_ifb Imported from Blogger
Thank for the post . really helpful
Thank for the post . really helpful
Explained well by using unique sv2012 construct
Hi Tudor,
I recently started reading your blog and it is really very informative.
Can you pls. explain in detail about 'solve before" construct? If I don’t use it in the above permutation example, what will exactly happen? I will prefer some more examples on “solve before” since it is sometimes confusing.
Thanks,
Ashish
Regarding this constraint:
constraint contains_c {
2 inside { some_dynamic_array };
}
What if you want more than one element to be 2? Let’s say you want 3 of the elements to be 2.
1 reply
You can do this with the sum array reduction method. Assuming an array of ints the constraint would be:
constraint exactly_three_twos {
(array.sum() with (int’(item == 2))) == 3;
}
The int'(...) around the comparison is to force it to not treat the result of the sum as a 1 bit value.
I think the solve before is actually wrong here. It’s also a bidirectional operator, but it only changes the distribution of a solution, by making it more or less likely to be chosen, but not whether a solution is possible or not.