CODEWITHSUNDEEP
z3
Probie
Probie

Reputation: 1361

Guiding z3's proof search

I'm trying to get z3 to work (most of the time) for very simple non-linear integer arithmetic problems. Unfortunately, I've hit a bit of a wall with exponentiation. I want to be able handle problems like x^{a+b+2} = (x * x * x^{a} * x{b}). I only need to handle non-negative exponents.

I tried redefining exponentiation as a recursive function (so that it's just allowed to return 1 for any non-positive exponent) and using a pattern to facilitate z3 inferring that x^{a+b} = x^{a} * x^{b}, but it doesn't seem to work - I'm still timing out.

(define-fun-rec pow ((x!1 Int) (x!2 Int)) Int
  (if (<= x!2 0) 1 (* x!1 (pow x!1 (- x!2 1)))))
; split +
(assert (forall ((a Int) (b Int) (c Int)) 
  (! (=> 
      (and (>= b 0) (>= c 0)) 
      (= (pow a (+ b c)) (* (pow a c) (pow a b)))) 
   :pattern ((pow a (+ b c))))))

; small cases
(assert (forall ((a Int)) (= 1 (pow a 0))))
(assert (forall ((a Int)) (= a (pow a 1))))
(assert (forall ((a Int)) (= (* a a) (pow a 2))))
(assert (forall ((a Int)) (= (* a a a) (pow a 3))))

; Our problem
(declare-const x Int)
(declare-const i Int)
(assert (>= i 0))

; This should be provably unsat, by splitting and the small case for 2
(assert (not (= (* (* x x) (pow x i)) (pow x (+ i 2)))))

(check-sat) ;times out

Am I using patterns incorrectly, is there a way to give stronger hints to the proof search, or an easier way to do achieve what I want?

Upvotes: 2

Views: 86

Answers (1)

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

Pattern (also called triggers) may only contain uninterpreted functions. Since + is an interpreted function, you essentially provide an invalid pattern, in which case virtually anything can happen.

As a first step, I disabled Z3's auto-configuration feature and also MBQI-based quantifier instantiation:

(set-option :auto_config false)
(set-option :smt.mbqi false)

Next, I introduced an uninterpreted plus function and replaced each application of + by plus. That sufficed to make your assertion verify (i.e. yield unsat). You can of course also axiomatise plus in terms of +, i.e.

(declare-fun plus (Int Int) Int)

(assert (forall ((a Int) (b Int)) 
  (! (= (plus a b) (+ a b))
   :pattern ((plus a b)))))

but your assertion already verifies without the definitional axioms for plus.

Upvotes: 3

Related Questions