1

what is the usual precision for Real variables in Z3? Is exact arithmetic used?

Is there a way to set the accuracy level manually?

If Real means that exact arithmetic must be used, is there any other data type for floating point values which has limited precision?

Finally: from this point of view, is z3 different with respect to the other popular SMT solvers, or is this standardised in the SMT-LIB definition?

Kubuntuer82
  • 1,487
  • 3
  • 18
  • 40

1 Answers1

2

See this answer: z3 existential theory of the reals

Regarding printing precision, see this one: algebraic reals: does z3 do rounding when pretty printing?

In short, yes they are precisely represented as roots of polynomials. Not every real number can be represented by the Real type (transcendentals, e, pi, etc.); but all polynomial roots are representable.

This paper discusses how to also deal with transcendentals.

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
alias
  • 28,120
  • 2
  • 23
  • 40
  • Many thanks Levent! Then by default z3 always tries to find an exact solution? Or are there some limits on precision? – Kubuntuer82 Jun 14 '17 at 16:18
  • 1
    It's a decision procedure for `Reals`. So long as the model values are representable as roots of polynomials, Z3 will find them. (Of course, assuming you have infinite computational resources.) Note that it's very easy to break the "completeness" here: Soon as you mix `Real` and `Int` for instance, you'll immediately run into problems since the combination of the two is undecidable in general. See this answer: https://stackoverflow.com/questions/42133675/get-fractional-part-of-real-in-qf-ufnra/42147549#42147549 – alias Jun 14 '17 at 16:30