Rule-based solving of flag constraints

[chriseth]

We can use the rule-based system to solve some of the flag constraints where we otherwise use exhaustive search. If we apply the rule-based system first, this could speed up solving considerably.

The constraints are of the form:

// at most one set:
flag1 + flag2 + flag3 + flag4 = 1
flag1 + 2 * flag2 + 3 * flag3 + 4 * flag4 = c

Rules (need to make them more flexible wrt factors):

ExactlyOneSet(e) <-
  ExpressionSumHeadTail(e, head, tail),
  AtMostOneSet(tail),
  LinearExpression(head, v, T::from(1)),
  BooleanVar(v);
ExactlyOneSet(e) <- Constant(e, T::from(1));

// Affine expressions with the same variables
// (this works because the summands are sorted)
SameVars(e1, e2) <- Constant(e1), Constant(e2);
SameVars(e1, e2) <-
  ExpressionSumHeadTail(e1, head1, tail1),
  ExpressionSumHeadTail(e2, head2, tail2),
  SameVars(tail1, tail2),
  LinearExpression(head1, _, v),
  LinearExpression(head2, _, v);

Assignment(v, T::from(1)) <-
  ExactlyOneSet(e1),
  Constraint(e1),
  SameVars(e1, e2),
  Constraint(e2),
  IsAffine(e2),
  HasSummand(e2, c_e), Constant(c_e, -c), // TODO need to check if HasSummand can also extract the constant part
  HasSummand(e2, v_e), LinearExpression(c_e, c, v);
Assignment(v, T::from(0)) <-
  ExactlyOneSet(e1),
  Constraint(e1),
  SameVars(e1, e2),
  Constraint(e2),
  IsAffine(e2),
  HasSummand(e2, c_e), Constant(c_e, c1), // TODO need to check if HasSummand can also extract the constant part
  HasSummand(e2, v_e), LinearExpression(c_e, c2, v),
  c1 != c2;