Dado um problema que é codificado usando os reais do Z3, qual das estatísticas queZ3 /smt2 /st produz pode ser útil para julgar se o motor real "tem problemas / faz muito trabalho"?

No meu caso, tenho duas codificações equivalentes do problema, ambas usando reais. A diferença "pequena" na codificação, no entanto, faz uma grande diferença no tempo de execução, ou seja, que a codificação A leva 2: 30min e codifica B 13min. As estatísticas do Z3 mostram queconflicts equant-instantiations são principalmente equivalentes, mas outros não são, por exemplogrobner, pivots enonlinear-horner.

As duas estatísticas diferentes estão disponíveis comoessência.

EDITAR (para abordar o comentário de Leo):

A codificação SMT2 gerada por ambas as versões é ~ 30k linhas e as asserções onde os reais são usados ​​são aspergidas em todo o código. A principal diferença é que a codificação B usa muitas constantes reais não especificadas do intervalo0.0 para1.0 que são limitados por desigualdades, por ex.0.0 < r1 < 1.0 ou0.0 < r3 < 0.75 - r1 - r2, enquanto na codificação A muitas dessas constantes não especificadas foram substituídas por valores reais fixos do mesmo intervalo, por exemplo,0.1 ou0.75 - 0.01. Ambas as codificações utilizam aritmética real não linear, e.r1 * (1.0 - r2).

Alguns exemplos aleatórios das duas codificações estão disponíveis comoessência. Todas as variáveis ​​que ocorrem são reais subespecificados, conforme descrito acima.

PS: introduz aliases para valores reais fixos, por exemplo,

(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 penalidades de desempenho significativas?