Z3 存在量词时的插值

Question

我正在对 iZ3 进行试验，看看是否可以利用 iZ3 的 get-interpolant 功能推导出量化的不变量。这是我的例子：

(set-option :auto-config false)                                             
(set-option :smt.mbqi true)
(set-option :smt.macro-finder true)
(set-option :produce-interpolants true)                                         
(declare-sort T0)
(declare-const l1 T0)                                                       
(declare-const l2 T0)                                                       
(declare-const v T0)                                                        
(declare-sort T1)
(declare-const z1 T1)                                                       
(declare-const z2 T1)                                                       
(declare-const z3 T1)
(declare-fun Rmem (T0 T1) Bool)                                             
(declare-const phi1 Bool)                                                   
(declare-const phi2 Bool)                                                   
(declare-const assn1 Bool)
(declare-const assn2 Bool)
;; A fact: \forall x. (Rmem(l1) = {x}) => (Rmem(v) = {x} \union Rmem(l2))
(assert (! (= phi1 (forall ((x T1))
    (=> (forall ((bv0 T1)) (= (Rmem l1 bv0) (= bv0 x)))                     
        (forall ((bv0 T1)) (= (Rmem v bv0)
                           (or (Rmem l2 bv0) (= bv0 x))))))) :named f1))               
;; An observation: When (Rmem(l1) = {z1}) and (Rmem(l2)= {z2,z3}), then
;;                 Rmem(v) was observed to be {z1,z2,z3}
(assert (! (= phi2 (! (=> (and (forall ((bv0 T1))
                            (= (Rmem l1 bv0) (= bv0 z1)))                   
                         (forall ((bv0 T1))
                            (= (Rmem l2 bv0) (or (= bv0 z2) (= bv0 z3)))))  
                    (forall ((bv0 T1))
                        (= (Rmem v bv0) (or (= bv0 z1) (= bv0 z2)           
                                            (= bv0 z3))))))) :named f2))
(assert (= assn2 (and phi1 (not phi2))))
(assert assn2)                                      
(check-sat)                                                                 
;; Can Z3 derive the following invariant: Rmem(v) = Rmem(l1) \union Rmem(l2)?
(get-interpolant f1 f2)

对于上面的示例，Z3 打印Unsat（如预期的那样），但没有其他内容。

1. 这是否意味着 Z3 无法从不可满足的证明中推导出插值？
2. 我了解 iZ3 对量词的支持有限。尽管如此，我希望插值能够成功，因为我的示例采用可判定 (EPR) 逻辑。失败是因为Z3的固有限制吗？如果没有，是否有其他方法可以构建我的查询？

Answer 1

我得到了你的文件的这个结果：

unsat
(forall ((%0 T1))
  (! (let ((a!1 (exists ((%1 T1)) (! (= (not (Rmem l1 %1)) (= %1 %0)) :qid itp)))
           (a!2 (forall ((bv0 T1))
                  (! (= (Rmem v bv0) (or (Rmem l2 bv0) (= bv0 %0)))
                     :pattern ((Rmem v bv0))
                     :pattern ((Rmem l2 bv0))))))
       (or a!1 a!2))
     :qid itp))

您能说一下您使用的是什么版本/架构吗？