1
votes

Given 3 numbers

  a:  uint (bits :2);
  b : uint (bits :2);
  c:  uint (bits :2);

What is the way to define constraints for these numbers that satisfy the following: - at least one of them has to be different than 0 - the product of all the non-zero numbers has to be in a certain range (e.g [3..20])

2

2 Answers

3
votes

The most elegant way to write it would be:

keep ((a>0?a:1) * (b>0?b:1) * (c>0?c:1)) in [3..20];

Note that it also enforces that at least one of the items to be different than 0, since if all are 0s then the product would be 1 and the constraint won't be satisfied. But to make it cleared for future readers you can add:

keep a > 0 or b > 0 or c > 0;
1
votes

You can write all of these out explicitly:

struct some_struct {
  a:  uint (bits :2);
  b : uint (bits :2);
  c:  uint (bits :2);

  keep a > 0 or b > 0 or c > 0;

  keep a > 0 and b > 0 and c > 0 => a * b * c in [ 3..20 ];

  keep a > 0 and b > 0 and c == 0 => a * b in [ 3..20 ];
  keep a > 0 and b == 0 and c > 0 => a * c in [ 3..20 ];
  keep a == 0 and b > 0 and c > 0 => b * c in [ 3..20 ];

  keep a == 0 and b == 0 and c > 0 => c in [ 3..20 ];
  keep a == 0 and b > 0 and c == 0 => b in [ 3..20 ];
  keep a > 0 and b == 0 and c == 0 => a in [ 3..20 ];
};

This is kind of a lot of code and if you need to change your range ([ 3..20]) you need to do it in quite a few places.