Angesichts eines Problems, das mit Z3s Reals codiert ist, welche Statistik das istZ3 /smt2 /st Produziert könnte hilfreich sein, um zu beurteilen, ob die Reals-Engine "Probleme hat / viel Arbeit leistet"?

In meinem Fall habe ich zwei meist äquivalente Kodierungen des Problems, beide unter Verwendung von Real. Der "kleine" Unterschied in der Codierung macht jedoch einen großen Unterschied in der Laufzeit aus, nämlich dass die Codierung A 2: 30 Minuten und die Codierung B 13 Minuten dauert. Die Z3-Statistiken zeigen dasconflicts undquant-instantiations sind meist gleichwertig, andere zum Beispiel nichtgrobner, pivots undnonlinear-horner.

Die zwei verschiedenen Statistiken sind als verfügbarKern.

BEARBEITEN (um Leos Kommentar anzusprechen):

Die von beiden Versionen generierte SMT2-Codierung beträgt ~ 30.000 Zeilen, und die Aussagen, bei denen Real verwendet werden, werden über den gesamten Code verteilt. Der Hauptunterschied besteht darin, dass die Codierung B viele unterbestimmte reelle Konstanten aus dem Bereich verwendet0.0 zu1.0 die durch Ungleichungen begrenzt sind, z.B.0.0 < r1 < 1.0 oder0.0 < r3 < 0.75 - r1 - r2Während beim Codieren von A viele dieser unterbestimmten Konstanten durch feste reelle Werte aus demselben Bereich ersetzt wurden, z.0.1 oder0.75 - 0.01. Beide Codierungen verwenden eine nichtlineare reelle Arithmetik, z.r1 * (1.0 - r2).

Einige zufällige Beispiele aus den beiden Kodierungen sind als a verfügbarKern. Alle vorkommenden Variablen sind wie oben beschrieben nicht spezifizierte reelle Variablen.

PS: Führt man Aliase für feste reelle Werte ein, z.

(define-sort $Perms () Real)
(declare-const $Perms.$Full $Perms)
(declare-const $Perms.$None $Perms)
(assert (= $Perms.Zero 0.0))
(assert (= $Perms.Write 1.0))

erhebliche Leistungseinbußen verursachen?