Modelling a class hierarchy in Inox

Question

I want to model the following Scala hierarchy in the Inox solver interface:

abstract class Element()
abstract class nonZero() extends Element
final case class Zero() extends Element
final case class One() extends nonZero()
final case class notOne() extends nonZero()

How can I model nonZero?

If I model it as an constructor

def mkConstructor(id: Identifier, flags: Flag*)
                 (tParamNames: String*)
                 (sort: Option[Identifier])
                 (fieldBuilder: Seq[TypeParameter] => Seq[ValDef]) = {
  val tParams = tParamNames map TypeParameter.fresh
  val tParamDefs = tParams map (TypeParameterDef(_))
  val fields = fieldBuilder(tParams)
  new ADTConstructor(id, tParamDefs, sort, fields, flags.toSet)
}

Then I'm not able to specify that it has other constructors extending it. Whereas if I model it as a sort:

def mkSort(id: Identifier, flags: Flag*)
          (tParamNames: String*)
          (cons: Seq[Identifier]) = {
  val tParams = tParamNames map TypeParameter.fresh
  val tParamDefs = tParams map (TypeParameterDef(_))
  new ADTSort(id, tParamDefs, cons, flags.toSet)
}

Then I cannot specify that it is a subtype of Element.

Why do I need this for

I need this hierarchy because I need to state properties as this:

The set of non zero elements of the field with one, inverse and multiplication by a non zero element forms a group.

I would need then some mechanism to generate a type to restrict the constructors of a sort, in this case, restrict the constructors of Element to One and notZeroOne(). In that case I would be modelling:

abstract class Element()
final case class Zero() extends Element
final case class One() extends Element()
final case class notZeroOne() extends Element()

What is the cleanest solution for this?

score 1 · Accepted Answer · answered Apr 15 '17 at 12:33

Unfortunately, the "class hierarchy" in Inox is limited to a single abstract parent with a sequence of concrete constructors (no subtyping between constructors is possible). This limitation reflects the limitation imposed on the theory of algebraic datatypes supported by the underlying SMT solvers.

If you want to state properties on non-zero elements, why don't you just use an implication of the form (elem !== Zero()) ==> someProperty? Note that in general, you can simulate the nonZero() type proposed above through a concrete predicate that exhaustively enumerates the allowed constructors. For example,

def nonZero(e: Expr): Expr = e.isInstOf(T(one)()) || e.isInstOf(T(notOne)())

Then you can state properties on non-zero elements by using nonZero(e) ==> property(e).

Modelling a class hierarchy in Inox

1 Answers1