Get fractional part of real in QF_UFNRA

Question

Using smtlib I would like to make something like modulo using QF_UFNRA. This disables me from using mod, to_int, to_real an such things.

In the end I want to get the fractional part of z in the following code:

(set-logic QF_UFNRA)

(declare-fun z () Real)
(declare-fun z1 () Real)
(define-fun zval_1 ((x Real)) Real
         x
)
(declare-fun zval (Real) Real)

(assert (= z 1.5));
(assert (=> (and (<= 0.0 z) (< z 1.0)) (= (zval z) (zval_1 z))))
(assert (=> (>= z 1.0) (= (zval z) (zval (- z 1.0)))))
(assert (= z1 (zval z)))

Of course, as I am asking this question here, implies, that it didn't work out.

Has anybody got an idea how to get the fractional part of z into z1 using logic QF_UFNRA?

Answer 1

This is a great question. Unfortunately, what you want to do is not possible in general if you restrict yourself to QF_UFNRA.

If you could encode such functionality, then you can decide arbitrary Diophantine equations. You would simply cast a given Diophantine equation over reals, compute the "fraction" of the real solution with this alleged method, and assert that the fraction is 0. Since reals are decidable, this would give you a decision procedure for Diophantine equations, accomplishing the impossible. (This is known as Hilbert's 10th problem.)

So, as innocent as the task looks, it is actually not doable. But that doesn't mean you cannot encode this with some extensions, and possibly have the solver successfully decide instances of it.

If you allow quantifiers and recursive functions

If you allow yourself quantifiers and recursive-functions, then you can write:

(set-logic UFNRA)

(define-fun-rec frac ((x Real)) Real (ite (< x 1) x (frac (- x 1))))

(declare-fun res () Real)
(assert (= (frac 1.5) res))

(check-sat)
(get-value (res))

To which z3 responds:

sat
((res (/ 1.0 2.0)))

Note that we used the UFNRA logic allowing quantification, which is required here implicitly due to the use of the define-fun-rec construct. (See the SMTLib manual for details.) This is essentially what you tried to encode in your question, but instead using the recursive-function-definition facilities instead of implicit encoding. There are several caveats in using recursive functions in SMTLib however: In particular, you can write functions that render your system inconsistent rather easily. See Section 4.2.3 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-draft.pdf for details.

If you can use QF_UFNIRA

If you move to QF_UFNIRA, i.e., allow mixing reals and integers, the encoding is easy:

(set-logic QF_UFNIRA)

(declare-fun z  () Real)
(declare-fun zF () Real)
(declare-fun zI () Int)

(assert (= z (+ zF zI)))
(assert (<= 0 zF))
(assert (< zF 1))

(assert (= z 1.5))
(check-sat)
(get-value (zF zI))

z3 responds:

sat
((zF (/ 1.0 2.0))
 (zI 1))

(You might have to be careful about the computation of zI when z < 0, but the idea is the same.)

Note that just because the encoding is easy doesn't mean z3 will always be able to answer the query successfully. Due to mixing of Real's and Integer's, the problem remains undecidable as discussed before. If you have other constraints on z, z3 might very well respond unknown to this encoding. In this particular case, it happens to be simple enough so z3 is able to find a model.

If you have sin and pi:

This is more of a thought experiment than a real alternative. If SMTLib allowed for sin and pi, then you can check whether sin (zI * pi) is 0, for a suitably constrained zI. Any satisfying model to this query would ensure that zI is integer. You can then use this value to extract the fractional part by subtracting zI from z.

But this is futile as SMTLib neither allows for sin nor pi. And for good reason: Decidability would be lost. Having said that, maybe some brave soul can design a logic that supported sin, pi, etc., and successfully answered your query correctly, while returning unknown when the problem becomes too hard for the solver. This is already the case for nonlinear arithmetic and the QF_UFNIRA fragment: The solver may give up in general, but the heuristics it employs might solve problems of practical interest.

Restriction to Rationals

As a theoretical aside, it turns out that if you restrict yourself to rationals only (instead of actual reals) then you can indeed write a first-order formula to recognize integers. The encoding is not for the faint of heart, however: http://math.mit.edu/~poonen/papers/ae.pdf. Furthermore, since the encoding involves quantifiers, it's probably quite unlikely that SMT solvers will do well with a formulation based on this idea.

[Incidentally, I should extend thanks to my work colleagues; this question made for a great lunch-time conversation!]