consider warning when expression contains numeral outside refinement domain

[johnyf]

omega.symbolic.fol.Context arranges and uses a refinement of each variable that will be reasoned about for integer values from some finite set by a fixed finite number of variables that will be reasoned about for Boolean values only, using BDDs.

In lack of a better name, let's call the latter variables "bits". Do not mistake them for typed variables. It's just the case that we aren't going to reason about non-Boolean assignments to those "bit" variables.

In order to select how many bits to use, Context takes type hints, via the method add_vars. The user can then create new BDDs from expressions over the integer-valued variables. However, if the user uses values outside the type hints, no warning is printed.

One reason is that a 32 bit ALU is used for operators. Nevertheless, it would probably be useful to catch errors early.

We could print a warning if any numeral in the expression is outside the range of the type hint of any variable. We cannot associate such warnings with any specific variable, because addition and multiplication render it unclear which variables a potential error is associated with. Of course, we can report the variables that appear in the expression, as a hint to where an error might be.

For example:

from omega.symbolic.fol import Context

c = Context()
c.add_vars(dict(x=dict(type='int', dom=(0, 4))))  # type hint: x \in 0 .. 4
>>> c.vars
{'x': {'bitnames': ['x_0', 'x_1', 'x_2'],
  'dom': (0, 4),
  'signed': False,
  'type': 'int',
  'width': 3}}
u = c.add_expr('5 <= x /\ x <= 8')
>>> u = c.add_expr('5 <= x /\ x <= 8')
True
>>> list(c.pick_iter(u))
[{'x': 6}, {'x': 5}, {'x': 7}]

At most a warning will be raised, not an error. The variables are untyped, and there is no clear evidence that such a situation is the result of an error.