Mixing theories in SMT

Question

I would like to construct an SMT formula having a number of assertions over integer linear arithmetic and Boolean variables as well as some assertions over real non-linear arithmetic and again Boolean variables. The assertions over integers and reals share only the Boolean variables. As an example, consider the following formula:

(declare-fun b () Bool)
(assert (= b true))

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (or (not b) (>= (+ x y) (- x (+ (* 2 z) 1)))))

(declare-fun r () Real)
(assert (or (not b) (= (+ (* r r) (* 3 r) (- 4)) 0)))

If I feed z3 with this formula, it immediately reports "unknown". But if I remove the integer part of it, I get the solution right away, which satisfies the constraint with variable "r". I presume this means that the non-linear constraint on its own is not hard for the solver. The issue should be in mixing (linear) constraints over integers and (non-linear) constraints over reals.

So my question is the following. What is the correct way to handle this kind of mixed formulas using z3 (if there is any)? My understanding of DPLL(T) is that it should be able to deal with such formulas using different theory solvers for different constraints. Please, correct me if I am wrong.

From my experience, non-linear arithmetic handler in Z3 is rather fragile, and can work or not depending on whether a pre-processing pass succeeds. In many cases you would be better off performing linearization on your side (e.g. replacing non-linear arithmetic with intervalization) — George Karpenkov
Thank you! So you believe the problem has nothing to do theory mixing? — Alexey Ignatiev
There are two reasonable interpretations of which theories are involved in the above: the theory of mixed real and Integer, or the union of the theory of reals and the the theory of integers. AFAIK all SMT solvers interpret this as the theory of mixed reals and integers. QF non-linear mixed integer and real theory subsumes Hilbert's 10th problem. So there is one theory involved, it is undecidable, and it is outside of what the nlsat algorithm solves. You are likely outside of the guards for "do I apply nlsat?" and hitting a linear mixed solver. (Christoph, how can Alexey confirm that?) — Tim
OK, thanks! I known about undecidability of non-linear integer arithmetic. But I am not an expert in SMT. So I though that a typical SMT solver should somehow be able to detect, which theory an assertion belongs to, and use the corresponding theory solver for that assertion (e.g. in my case linear integers solver for first assertion and non-linear reals solver for the second assertion). This was my understanding of how DPLL(T) works. But maybe in practice it is not the case (or my understanding is simply wrong) and SMT solvers try to use one theory solver for all assertions if that's possible. — Alexey Ignatiev

Christoph Wintersteiger Christoph Wintersteiger · Accepted Answer · 2016-05-11T12:47:29

As George said in his comment, the non-linear solver in Z3 is rather fragile and the out-of-the-box performance isn't great. That said, there are a number of questions and answers about this problem here on stackoverflow, e.g., see these:

Z3 Performance with Non-Linear Arithmetic

How does Z3 handle non-linear integer arithmetic?

Z3 : strange behavior with non linear arithmetic

Non-linear arithmetic and uninterpreted functions

Z3 Theorem Prover: Pythagorean Theorem (Non-Linear Artithmetic)

Which techniques are used to handle Non-linear Integer Real problems in z3?

Satisfiablity checking in non-linear integer arithmetic by approximation

Mixing theories in SMT

1 Answers