Search code examples
mathz3solverfixed-point

In Z3 solver , is there a way to represent numbers in fixed point notation with arithmetic operations support

In Z3 solver, I want to represent numbers using fixed point notation and perform arithmetic operations with rounding.

Example: Let's say, X, Y and Z represent fixed point numbers type,

X[4,3]  Total 4 digits number with 3 digits after the decimal.
Y[4,2]   
Z[4,1]
Assign fixed point numbers to X, Y
X = 1.234  ( here there are total 4 digits & decimal digits are 3 )
Y = 45.67
Perform the Fixed point numbers Arithmetic operation

Z = X * Y (The result 56.35678 needs to be rounded and assign to Z i.e., 56.36)

I understand that, the Z3 supports floating point theory for numbers but not for fixed point theory for numbers with arithmetic operations ! Is there any plan to support fixed point theory for numbers? if not, is there any way to achieve this using any existing theory in Z3 solver with an example ?

Thank you for your help in advance!

I got information about Fixed Point theory for numbers from Z3 forum. Please find below link for information

An SMT Theory of Fixed-Point Arithmetic

which provides an API via PySMT for dealing with fixed point numbers:

SOAR Lab - PySMT - Fixed Points

Solution

  • You can always "request" such a feature at https://github.com/Z3Prover/z3/issues

    But SMT solvers in general follow the SMTLib initiative; so unless SMTLib comes up with a "logic" for fixed-point numbers, it's unlikely to be implemented. See here: http://smtlib.cs.uiowa.edu/

    There's a discussion forum for SMTLib where you can post your request and ask for guidance: https://groups.google.com/forum/#!forum/smt-lib

    Within the current capabilities, however, these kinds of numbers are not supported out of the box. Given that, I'd go with trying to model this "outside" the SMT solver and use the regular integer libraries, but the details of that depend on how much you want to invest and what sorts of problems you want to deal with. (For instance, you can represent fixed-point numbers with two integers, one for the "whole" part and one for the "fraction" part, and do all the arithmetic and rounding-etc. yourself. This can be a lot of work, but probably is your best bet given there's no direct support for these numbers currently.)