Dado un problema que está codificado usando los reales de Z3, ¿cuál de las estadísticas queZ3 /smt2 /st produce podría ser útil para juzgar si el motor de reales "tiene problemas / hace mucho trabajo"?

En mi caso, tengo dos codificaciones del problema en su mayoría equivalentes, ambas usando datos reales. La "pequeña" diferencia en la codificación, sin embargo, hace una gran diferencia en el tiempo de ejecución, a saber, que la codificación A toma 2: 30min y la codificación B 13min. Las estadísticas de Z3 muestran queconflicts yquant-instantiations En su mayoría son equivalentes, pero otros no lo son, por ejemplo.grobner, pivots ynonlinear-horner.

Las dos estadísticas diferentes están disponibles comoesencia.

EDITAR (para abordar el comentario de Leo):

La codificación SMT2 generada por ambas versiones es de ~ 30k líneas y las aserciones donde se utilizan los reales se encuentran dispersas en todo el código. La principal diferencia es que la codificación B utiliza muchas constantes de tipo real subespecificadas del rango0.0 a1.0 que están limitados por desigualdades, por ejemplo,0.0 < r1 < 1.0 o0.0 < r3 < 0.75 - r1 - r2, mientras que en la codificación A muchas de estas constantes no especificadas se han reemplazado con valores reales fijos del mismo rango, por ejemplo,0.1 o0.75 - 0.01. Ambas codificaciones utilizan aritmética real no lineal, por ej.r1 * (1.0 - r2).

Algunos ejemplos aleatorios de las dos codificaciones están disponibles comoesencia. Todas las variables que ocurren son reales subespecificados como se describe anteriormente.

PS: ¿Introduce alias para valores reales fijos, por ejemplo,

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

¿Infligir penalizaciones significativas en el rendimiento?