CODEWITHSUNDEEP
z3smtdpll
Alexey Ignatiev
Alexey Ignatiev

Reputation: 43

Mixing theories in SMT

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.

Upvotes: 4

Views: 372

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

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

Upvotes: 2

Related Questions