建模Inox公司

Question

类层次我想在Inox公司解算器界面下面的斯卡拉层次结构模型：

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

为什么我需要这个

我需要这个层次，因为我需要状态属性是：

在组领域的非零元素的一个，逆和 乘以非零元素形成一个组。

我需要那么一些机制来产生一个类型来限制一类的构造函数，在这种情况下，限制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中的“类层次结构”仅限于具有一系列具体构造函数的单个抽象父类（构造函数之间不能进行子类型化）。此限制反映了底层SMT解算器支持的代数数据类型理论的限制。

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

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

然后，可以通过使用nonZero(e) ==> property(e)陈述上的非零元素的属性。