在 Inox 中建模 class 层次结构

Question

我想在 Inox 求解器界面中对以下 Scala 层次结构建模：

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()

如何对非零建模？

如果我将其建模为构造函数

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)
}

然后我无法指定它有其他构造函数扩展它。而如果我将其建模为一种类型：

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)
}

那我就不能指定它是Element的子类型了

为什么我需要这个

我需要这个层次结构，因为我需要这样声明属性：

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

然后我需要一些机制来生成一个类型来限制排序的构造函数，在这种情况下，将 Element 的构造函数限制为 One 和 notZeroOne()。在那种情况下，我将建模：

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

最干净的解决方案是什么？

Answer 1

不幸的是，Inox 中的 "class hierarchy" 仅限于具有一系列具体构造函数的单个抽象父级（构造函数之间不可能有子类型）。此限制反映了对底层 SMT 求解器支持的代数数据类型理论的限制。

如果要声明非零元素的属性，为什么不直接使用 (elem !== Zero()) ==> someProperty 形式的蕴涵？请注意，通常，您可以通过详尽枚举允许的构造函数的具体谓词来模拟上面提出的 nonZero() 类型。例如，

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

然后您可以使用 nonZero(e) ==> property(e).

声明非零元素的属性

在 Inox 中建模 class 层次结构

Modelling a class hierarchy in Inox

leon