0

我想在 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 的子类型。

为什么我需要这个

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

字段的非零元素的集合与非零元素的一、逆和乘积形成一个群。

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

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

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

4

1 回答 1

1

不幸的是，Inox 中的“类层次结构”仅限于具有一系列具体构造函数的单个抽象父对象（构造函数之间不能进行子类型化）。这种限制反映了对底层 SMT 求解器支持的代数数据类型理论的限制。

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

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

然后，您可以使用 . 声明非零元素的属性nonZero(e) ==> property(e)。

于 2017-04-15T12:33:38.160 回答