Biorąc pod uwagę problem, który jest zakodowany za pomocą realiów Z3, która z tych statystykZ3 /smt2 /st produkowane mogą być pomocne w ocenie, czy silnik realiów „ma problemy / wykonuje dużo pracy”?

W moim przypadku mam dwa zasadniczo równoważne kodowania problemu, oba używające reali. „Mała” różnica w kodowaniu powoduje jednak dużą różnicę w czasie wykonywania, a mianowicie, że kodowanie A zajmuje 2: 30min i kodowanie B 13min. Statystyki Z3 to pokazująconflicts iquant-instantiations są w większości równoważne, ale na przykład inne nie sągrobner, pivots inonlinear-horner.

Dwie różne statystyki są dostępne jakosens.

EDYTOWAĆ (aby odpowiedzieć na komentarz Leo):

Kodowanie SMT2 generowane przez obie wersje wynosi ~ 30k linii, a twierdzenia, w których używane są reale, są rozsypywane po całym kodzie. Główna różnica polega na tym, że kodowanie B wykorzystuje wiele nieokreślonych stałych z zakresu0.0 do1.0 które są ograniczone nierównościami, np.0.0 < r1 < 1.0 lub0.0 < r3 < 0.75 - r1 - r2, podczas gdy w kodowaniu wiele tych nieokreślonych stałych zostało zastąpionych stałymi wartościami rzeczywistymi z tego samego zakresu, np.0.1 lub0.75 - 0.01. Oba kodowania wykorzystują nieliniową arytmetykę rzeczywistą, np.r1 * (1.0 - r2).

Kilka przypadkowych przykładów z dwóch kodowań jest dostępnych jakosens. Wszystkie występujące zmienne są nieokreślonymi liczbami rzeczywistymi, jak opisano powyżej.

PS: Czy wprowadzanie aliasów dla stałych wartości rzeczywistych, np.

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

wymierzać znaczące kary za wydajność?