Z3:unknown 结果为 Z3 C API

Question

在当前的 Z3 上下文中，断言“try(X,i,j) = ((X[i][j] == i*j))”已经是 existed.the X 的类型是 ( Array Int (Array Int Int)).try(X,i,j) 是一个函数并且 return 类型是 bool.here 是 Z3 上下文：

 (kernel
      (forall ((Y (Array Int (Array Int Int))) (i Int) (j Int))
        (let ((a!1 (= (+ (select (select Y i) j) (* (- 1) j i)) 0)))
          (= (try Y i j) a!1))))

我想证明Z3 ast:

 forall i[0..99],j[0..199]. try(X,i,j) 
    =>
       (forall i[0..49],j[0..199]. try(X,i,j) 
    &&  forall i[50..99],j[0..199]. try(X,i,j))

换句话说，我检查是不是这个断言是sat。 Z3 检查结果未知。但是当我证明 Z3 ast:

forall i[0..99],j[0..199]. (X[i][j] == i*j)
=>
  (forall i[0..49],j[0..199]. (X[i][j] == i*j)
&& forall i[50..99],j[0..199]. (X[i][j] == i*j))

Z3证明结果是有效的，换句话说，不是这个断言是不满足的。

Answer 1

我不确定我是否理解这个问题，但总的来说我们不能指望 Z3 解决所有带量词的公式。在这种特殊情况下，它可能有助于启用宏查找器，它传播像

这样的函数定义

(forall ... (= (try ...) def )))

将所有出现的 try 替换为 def。该选项的名称是 smt.macro_finder.

Z3:unknown 结果为 Z3 C API

Z3:unknown result in Z3 C API

z3