建模Inox公司

類層次我想在Inox公司解算器界面下面的斯卡拉層次結構模型：建模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()

什麼是最乾淨的解決方案呢？

來源

2017-04-15 Rodrigo

不幸的是，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-15 12:33:38

建模Inox公司

回答

相關問題