Modellierung einer Klassenhierarchie in Inox

Question

ich folgende Scala Hierarchie in der Inox-Solver-Schnittstelle zu modellieren:

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

Wie kann ich von Null verschiedenen modellieren?

Wenn ich es als Konstruktor Modell

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

Dann bin ich nicht in der Lage zu geben, dass es andere Konstrukteure hat es erstreckt. Wenn ich es als eine Art modelliere:

Dann kann ich nicht angeben, dass es ein Untertyp von Element ist.

Warum muss ich dies für

I diese Hierarchie müssen, weil ich Körpereigenschaften wie dies benötigen:

Der Satz von Nicht-Null-Elemente des Feldes mit einem, inverse und Multiplikation mit einem Element ungleich Null bildet eine Gruppe.

Ich würde einen Mechanismus benötigen dann einen Typ zu erzeugen, um die Konstrukteure von einer Art, in diesem Fall zu beschränken, beschränken die Konstrukteure von Element zu One und notZeroOne(). In diesem Fall würde ich modellieren:

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

Was ist die sauberste Lösung dafür?

Answer 1

Leider ist die "Klassenhierarchie" in Inox auf ein einzelnes abstraktes Elternteil mit einer Folge von konkreten Konstruktoren beschränkt (Untertypen zwischen Konstruktoren ist nicht möglich). Diese Einschränkung spiegelt die Beschränkung wider, die der Theorie algebraischer Datentypen auferlegt ist, die von den zugrundeliegenden SMT-Lösern unterstützt werden.

Wenn Sie Eigenschaften auf Nicht-Null-Elementen angeben möchten, warum verwenden Sie nicht einfach eine Implikation des Formulars (elem !== Zero()) ==> someProperty? Beachten Sie, dass Sie den oben vorgeschlagenen Typ nonZero() im Allgemeinen durch ein konkretes Prädikat simulieren können, das die zulässigen Konstruktoren erschöpfend aufzählt. Zum Beispiel

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

Dann können Sie Eigenschaften auf Nicht-Null-Elemente, bis zu nonZero(e) ==> property(e) verwenden.