CODEWITHSUNDEEP
z3
user1779685
user1779685

Reputation: 383

z3 numerical constraints: which is better?

Which of the following two ways of writing (equivalent) constraints is preferable (performance-wise) when solving integer-real constraints using z3?

(assert (=> (and (<= 0.0009765625 value) (< value 0.001953125)) (= new-value 0.0009765625)))

                                     OR

(assert (=> (and (<= (/ 1.0 1024.0) value) (< value (/ 1.0 512.0))) (= new-value (/ 1.0 1024.0))))

Note that we have reciprocals of powers of two here (and there are many such constraints of this type involving both smaller and larger numbers).

Upvotes: 3

Views: 116

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Internally, Z3 converts all numerals in decimal notation into fractions. This transformation is performed when parsing the formula. Anyway, we do not expect to see any big difference in performance between these two encodings. The parsing time is usually insignificant in Z3 (when compared with solving time).

Upvotes: 4

Related Questions