3

In z3, a real term's value is represented by the division of two integer numbers: numerator and denominator. I very often find real values (as solutions to my z3 problems) with very large numerators and denominators like as follows:

29176049827299110215982818410792217459/804618286561124267999713087296957062500 -556895298158182412321541102649719164259083/4272120792496289300944476637003193523343750

There are often other assignments of those real variables in the case of alternative solutions (to the same problem) with smaller numerators and denominators. I am just wondering whether I can limit the numerator and denominator (e.g., with respect to the number of digits). Actually, I am looking for a z3 feature for this purpose. Thank you in advance for your answer.

Ashiq
  • 307
  • 2
  • 10
  • 1
    There isn't any facility for bounded complexity models in Z3. It is an interesting point, but we don't have a way to control search for models with small numeric representations. – Nikolaj Bjorner Jul 28 '14 at 15:53
  • Thanks for your response. I am just wondering whether you like to add this feature. – Ashiq Sep 24 '14 at 04:12

1 Answers1

0

It's not true in general that a real number in Z3 is represented as a ratio of a numerator and a denominator. This would restrict Z3 to rationals. For an example where Z3 returns an irrational number, try:

(declare-const x Real)
(assert (= (* x x) 2.0))
(check-sat)
(get-model)

That being said, for many specific problems, Z3 will indeed respond with a rational representation of a real number. I think this often happens when it's possible for your problem to be re-normalized and solved in the integers. In these situations, you could try to force your problem to be solved in the rationals using techniques similar to the answer in this question. Then, you can assert that your number has a numerator p < p_max for some constant p_max.

Douglas B. Staple
  • 10,510
  • 8
  • 31
  • 58
  • Two more comments: (1) If you add cosmetic restrictions to your model, especially mixing real and integer arithmetic, you might cause Z3 to fail. (2) you could instead start your .smt2 file with `(set-option :pp.decimal true)` if you just want a more reasonable looking result and are OK with a decimal approximation. – Douglas B. Staple May 28 '16 at 00:47