support for enum types

[garganti]

It would be good if java-smt could support enum types (datatypes). An enum type has a name and a set of symbols. Variables can then be declared of that type and basic operations like = and distinctcan be performed on formulas of that variables. Enum types are supported by SMT_LIB format (pag 61 of the language ref manual):

; an enumeration datatype
( declare - datatypes ( ( Color 0) ) (
( ( red ) ( green ) ( blue ) ))
)

Most of the solvers support them natively. For instance Z3, the following command creates a type S with three possible values: (declare-datatypes () ((S A B C))) which has the corresponding java type in the APIs (DatatypeExpr)

Other solvers have similar APIs. For instance yices: type_t yices_new_scalar_type(uint32_t card)

[kfriedberger]

Interesting idea. Enum sort is available in several solvers. We just need to find a common basis for an implementation.

Overall, we could start with a few solvers supporting enumertion logic, and if we know enough about this kind of logic, then extend it to other solvers, based on a sub-set of datatype-logic.

Lets start with collecting some API examples:

Z3:

• Z3_mk_enumeration_sort: https://z3prover.github.io/api/html/group__capi.html#ga84a4ecc3d5585ac586d2a57fe8e364b3
• input: a list of N names for the elements and one name for the sort.
• output: N functions for constants and N predicates for instance-check.
• todo: I would assume that we can ignore predicates and just model them as "elem == constant". And the name of sort never used, except for printing?

MathSAT5 (API needs to be updated to 5.6.9 or later, plus see the other issue: https://github.com/sosy-lab/java-smt/issues/290):

• msat_get_enum_type: https://mathsat.fbk.eu/apireference.html#add63c2237a3af41389ae72452a1e9dea
• input: a list of N names for the elements and one name for the sort (name never used, except for printing?).
• output: a new sort.
• additional: "isEnumValue(t)" return whether a formula t is from any enum type.
• todo: how to create constants/variables for the enumeration?

Yices (our internal API skipped all scalar types, needs to be updated for enumration types):

• scalar-type and scalar-based terms seem to work here.
• todo: there is no name, but only an index. We would need to implement naming in JavaSMT, which is ok.

CVC4 and CVC5, and other solvers seem to use datatypes for enumeration logic:

• CVC4: https://cvc4.github.io/datatypes.html
• todo: is enumeration logic a sub-logic of datatype-logic?
• todo: how to model accessors?

Next step: We need to refine that information and test simple examples. :-)

[kfriedberger]

I started with an initial interface, which is quite simple and understandable. We just need to wire the internals for each solver.

[baierd]

I've created a branch for this. Also, @RSoegtrop will take a look.

[kfriedberger]

The new release JavaSMT 4.0.0 contains the requested enumeration theory, at least for some SMT solvers. We would be happy to get feedback or reports if there are any further issues.