z3中量词与集合的交互作用

Question

目前，我正试图使用Z3为一种非类型化语言编写一个简单的程序逻辑集。

我的符号执行引擎需要证明以下公式的有效性：

​

为此，我们要求Z3检查以下各项的可满足性：

​

然后，我们将其编码为以下SMT-LIB公式：

(define-sort Set () (Array Real Bool))

(define-fun singleton ((x Real)) Set
    (store 
       ((as const (Array Real Bool)) false)
       x
       true))

(define-fun set-union ((x Set) (y Set)) Set
    ((_ map (or (Bool Bool) Bool)) x y)) 


(declare-const head Real)
(declare-const tail Set)
(declare-const result Set)
(declare-const value Real)

(assert (forall ((x Real)) (=> (select tail x) (> x head))))
(assert (> head value))
(assert
   (forall ((result Set))
       (let ((phi1 
                (forall ((x Real)) (=> (select result x) (> x value))))
             (phi2
                (= result (union (singleton head) tail))))
          (not (and phi1 phi2)))))
(check-sat)

当给定此公式时，求解器立即输出未知。我的猜测是，问题在于对绑定到集合的变量进行量化。为了检查这一点，我简化了上面的公式，获得：

然后，我们将其编码为以下SMT-LIB公式：

(define-sort Set () (Array Real Bool))

(define-fun singleton ((x Real)) Set
   (store 
      ((as const (Array Real Bool)) false)
       x
      true))

(define-fun set-union ((x Set) (y Set)) Set
     ((_ map (or (Bool Bool) Bool)) x y)) 


(declare-const head Real)
(declare-const tail Set)
(declare-const result Set)
(declare-const value Real)

(assert (forall ((x Real))(=> (select tail x) (> x head))))
(assert (> head value))

(assert
  (not 
     (forall ((x Real)) 
        (=> (select (union (singleton head) tail) x) 
            (not (<= x value))))))

 (check-sat)

当给定此公式时，求解器立即输出unsat。这证实了我的猜测，即问题在于对绑定到集合的变量进行量化。我的问题是Z3是否支持包含集合量化的公式。如果是的话，我做错了什么？

Answer 1

对于SMT求解程序来说，量词推理总是很困难的，在这种情况下，您有嵌套的量词。听到Z3在第一个案例中简单地说“未知”，我并不感到惊讶。还要注意的是，您是在量化什么是本质上的函数(您实现的集合实际上是函数)，这使得它更加困难。但是即使你用简单的东西来量化，嵌套的量词也永远不会很容易被释放。

你有没有试过把你的公式去掉，把它变成企业家--正常的形式，然后去掉存在的东西？这可能会让你走得更远，尽管你可能需要想出合适的模式来实例化。