CODEWITHSUNDEEP
z3smt
GeekInDisguise
GeekInDisguise

Reputation: 1567

Z3 precision for real and decimal values

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?

Upvotes: 1

Views: 2111

Answers (1)

alias
alias

Reputation: 30428

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.

Upvotes: 2

Related Questions