指导 z3 的证明搜索

Question

我正在尝试让 z3 工作（大部分时间）来解决非常简单的非线性整数算术问题。不幸的是，我在求幂方面遇到了一些困难。我希望能够处理像 x^{a+b+2} = (x * x * x^{a} * x{b}) 这样的问题。我只需要处理非负指数。

我尝试将求幂重新定义为递归函数（这样它就可以 return 1 用于任何非正指数）并使用一种模式来促进 z3 推断 x^{a+b} = x^{a} * x^{b}，但它似乎不起作用 - 我还在超时。

(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

我是否错误地使用了模式，有没有办法为证明搜索提供更强的提示，或者有更简单的方法来实现我想要的？

Answer 1

模式（也称为触发器）只能包含未解释的函数。由于 + 是一个解释函数，您实际上提供了一个无效模式，在这种情况下几乎任何事情都可能发生。

作为第一步，我禁用了 Z3 的自动配置功能以及基于 MBQI 的量词实例化：

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

接下来，我引入了一个未解释的plus功能，并将+的每个应用程序替换为plus。这足以使您的断言得到验证（即 yield unsat）。您当然也可以根据 + 公理化 plus，即

(declare-fun plus (Int Int) Int)

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

但是您的断言已经在没有 plus.

的定义公理的情况下得到验证

指导 z3 的证明搜索

Guiding z3's proof search

z3