私はイノックスソルバーインターフェースで、次のScalaの階層をモデル化するイノックス

Question

でクラス階層のモデル化：

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のサブタイプであると指定することはできません。

1、逆と とフィールドの非ゼロ要素のセット：私はこのような状態のプロパティに必要なので、私はこの階層を必要とする

のためにこれを必要な理由

非ゼロ要素による乗算はグループを形成する。

私は、このケースでは、ソートのコンストラクタを制限OneとnotZeroOne()にElementのコンストラクタを制限するタイプを生成するために、その後、いくつかのメカニズムが必要になります。その場合、私はモデリングするでしょう：

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)を使用すると、非ゼロ要素のプロパティを指定できます。