Sortiervererbung in z3

Question

Gibt es eine Möglichkeit, Vererbung zwischen Sortierungen in z3 zu definieren? (Ich benutze die Python-API)

Ich versuche, zwei verschiedene Arten von Ereignissen zu modellieren, Ereignisse zu schreiben und Ereignisse zu lesen; für jede von ihnen verwende ich eine Sort (WriteSort und ReadSort). Allerdings hätte ich gerne eine "Summe" Sort (EventSort), die entweder ein Schreib- oder ein Leseereignis ist.

ich definieren Funktionen mit folgender Domain:

f1 = Function('f1', WriteSort, WriteSort, BoolSort()) 
f2 = Function('f2', ReadSort, ReadSort, BoolSort()) 
f3 = Function('f3', EventSort, EventSort, BoolSort()) 

Eine Möglichkeit Veranstaltung wie und abstrakten Datentyp, aber dann die Domäne aller meiner Funktionen sein sollte zu definieren wäre (Veranstaltung x Veranstaltung) und die einzige Möglichkeit, solche Domains einzuschränken, ist es manuell zu machen.

Gibt es trotzdem beide WriteSort und ReadSort als "subsort" von Veranstaltung zu definieren?

Answer 1

Nach meinem Wissen wird die Untersortierung von Z3 (oder einem anderen SMT-Solver) nicht unterstützt. Sie könnten eine nicht interpretierte Sortier- und Verwendungsfunktion Top deklarieren, um die Unterorts in Top einzubetten, z. box_int(i: Int): Top, und eine Umkehrfunktion unbox_int(t: Top): Int, zusammen mit dem Axiom forall i: Int :: unbox_int(box_int(i)) = i.

Wenn Sie ein Typ-System kodiert, Subtyping eine Möglichkeit der Codierung ist es, eine uninterpretierte Type Art, zusammen mit Funktionen typeOf(o: Object): Type und subtype(t1: Type, t2: Type): Bool und ein transitivity Axiom für die Subtyp-Beziehung (und möglicherweise ein Reflexivität Axiom) einzuführen.

Eine schöne Diskussion über die Übersetzung eines Typs Systeme zu SMTLIB finden Sie in this paper.