CODEWITHSUNDEEP
z3
call me Steve
call me Steve

Reputation: 1727

unknown when using a integer division in z3 smt2

I am trying to find a solution for the function penta(n) = (n * (3n -1)) / 2 and where penta (z) = penta (a) + penta(b) for all number positives. That works until the integer division (div) is part ofthe definition, but when it is added in the definition I either got a timeout or an unknown. I would expect to get 8 , 7 , 4. Any idea on what I did wrongly? 

(declare-const a Int)
(declare-const b Int)
(declare-const z Int)

(define-fun penta ((n Int)) Int (div (* (- (* 3 n ) 1) n) 2) )  

(assert (= (penta z) (+ (penta a) (penta b))  ))
(assert (> a 1))
(assert (> b 1))
(assert (> z 1))

(check-sat)
(get-model)

I am using the version on the http://rise4fun.com/Z3 website and the version 4.1 (x64).

Upvotes: 1

Views: 287

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

The main issue is that the problem uses integer multiplication between two non-numeric arguments. There are no decision procedures for general Diophantine problems so Z3 does a best effort, which does not favor model enumeration.

When you don't use integer division, Z3 will try a partial heuristic based on converting the problem into finite domain bit-vectors to find models. It invokes this heuristic by performing a syntactic check on the formulas. THe syntactic check fails when you use the operator (div .. 2). You can encode (div x 2) so the heuristic picks up the problem by introducing fresh variables and bounding them:

(declare-const penta_z Int)
(declare-const penta_a Int)
(declare-const penta_b Int)
(assert (or (= (* 2 penta_z) (penta z)) (= (+ 1 (* 2 penta_z)) (penta z))))
(assert (or (= (* 2 penta_a) (penta a)) (= (+ 1 (* 2 penta_a)) (penta a))))
(assert (or (= (* 2 penta_b) (penta b)) (= (+ 1 (* 2 penta_b)) (penta b))))
(assert (= penta_z (+ penta_a penta_b)  ))
(assert (> a 1))
(assert (> b 1))
(assert (> z 1))
(assert (>= penta_z 0))
(assert (<= penta_z 100))

You can also directly encode your problem using bit-vectors although this starts getting error prone because you have to deal with how to handle overflows.

Upvotes: 2

Related Questions