Valid arithmetic and statistics Z3

Question

Given a problem that is encoded using Z3 reals, which of the statistics generated by Z3 /smt2 /st can be useful in judging whether a reaction engine has problems / does a lot of work?

In my case, I have two basically equivalent coding problems, like using reals. However, the "small" difference in coding is of great importance at runtime, namely, that coding A takes 2: 30 minutes and coding B 13min. Z3 statistics show that conflicts and quant-instantiations are mostly equivalent, but others are not, for example, grobner , pivots and nonlinear-horner .

Two different statistics are available as gist .

EDIT (to respond to Leo's comment):

The SMT2 encoding generated by both versions is ~ 30k lines, and statements that use reals are scattered throughout the code. The main difference is that coding B uses many constants with undefined constants in the range from 0.0 to 1.0 , which are limited by inequalities, for example. 0.0 < r1 < 1.0 or 0.0 < r3 < 0.75 - r1 - r2 , while when coding A, many of these undefined constants were replaced by fixed real values ​​from the same range, for example, 0.1 or 0.75 - 0.01 . Both encodings use nonlinear real arithmetic, for example. r1 * (1.0 - r2) .

A few random examples of the two encodings are available as gist . All arising variables are undefined actions, as described above.

PS: Does it introduce aliases for fixed real values, for example,

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

Do significant penalties apply?

Answer 1

The new nonlinear arithmetic solver is used only for problems containing only arithmetic. Since your problem uses quantifiers, the new nonlinear solver will not be used. Thus, Z3 will use the old approach based on a combination: Simplex (stage pivots), Groebner Basis (stage groebner) and Interval Propagation (horner stat). This is not a complete method. Moreover, based on the snippets you posted to gist, the Groebner framework will not be very effective. This method is usually effective for problems containing many equalities. So this is probably just overhead. You can disable it using the option NL_ARITH_GB=false . Of course, this is just an assumption based on a snippet of the problem you posted.

The differences between encoding A and B significant. Encoding A is essentially a linear task, since several constants were tied to real values. Z3 has always been complete for linear arithmetic problems. Therefore, this should explain the difference in performance.

Regarding your question about aliases, the preferred way to enter aliases is:

 (define-const $Perms.$Zero $Perms 0.0) (define-const $Perms.$Write $Perms 1.0) 

Z3 also contains a preprocessor that excludes variables using linear equations. This preprocessor is disabled by default in problems containing quantifiers. This design decision is motivated by program verification tools that widely use triggers / templates in quantifiers. The process of excluding variables can modify carefully designed triggers / patterns and affect the overall execution time. You can use the new tactic / strategy structure in Z3 to force it to apply this preprocessor. You can replace the command

 (check-sat) 

from

 (check-sat-using (then simplify solve-eqs smt)) 

This strategy tells Z3 to perform simplification, then solves the equations (and eliminates the variables), and then executes the smt default solver mechanism. You can find more about tactics and strategies in the following tutorial .