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)

当给定这个公式时，求解器立即输出unknown。 我的猜测是，问题在于对绑定到集合的变量进行量化。 为了检查这一点，我简化了上面的公式，得到：
然后我们将其编码为以下 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)

当给定这个公式时，求解器立即输出 不满意。 这证实了我的猜测，即问题在于量化 在绑定到集合的变量上。 我的问题是 Z3 是否支持包含以下内容的公式 对集合进行量化。而且，如果是这样，我做错了什么？

Answer 1

量词推理对于 SMT 求解器来说总是很困难，在这种情况下，你有嵌套的量词。听到 Z3 在第一种情况下简单地说“未知”，我并不感到惊讶。另请注意，您正在量化本质上是一个函数（您实现的集合实际上是函数），这使得它变得更加困难。但即使你对更简单的事物进行量化，嵌套的量词也永远不会容易排出。

您是否尝试过对您的公式进行 skolemize，将其转换为 prenex-normal 形式，并摆脱存在主义？尽管您可能必须提出适当的实例化模式，但这可能会让您走得更远。