Encoder.

This module performs the encoding of data types and finite ranges into boolean domains. Having this module as a separate one makes it possible to have different encoding policies that can be more appropriate for different kinds of variables. Currently only the standard CMU SMV encoding is possible, but there are plans to integrate into this architecture other forms of encoding, e.g., those used in Word-Level SMV [25].