1

我将集合编码为关系，并将集合上的操作编码为普遍量化的含义。我有一个集合上的选择运算符，它通过选择满足一元谓词 p 的元素（例如：v<4、v>4、..）来生成新集合。由于这个运算符，我的公式中有简单的算术谓词。下面给出了这种公式的示例 Z3 编码 -

(set-option :mbqi true)
(set-option :model-compact true)                                                                                 

;; Rmem and Rmem1 are sets of Int                                                                                 
(declare-fun Rmem (Int) Bool)
(declare-fun Rmem1 (Int) Bool)
(declare-const v Int)
(declare-const v1 Int)
(declare-const x Int) 
;; Rmem = Rmem1 U {x}
(assert (forall ((n Int)) (= (Rmem n)(or (Rmem1 n) (= n x)))))
;; Select(m<v1) from Rmem1 = {}
(assert (forall ((m Int)) (= false (and (Rmem1 m) (< m v1)))))
(assert (or (< v x) (= v x)))
(assert (or (< v v) (= v v1)))

(assert (exists ((q Int)) (and (Rmem q) (< q v))))
(check-sat)
(get-model)

正如预期的那样，Z3 为上述公式返回 UNSAT。但是，我的问题是——

  1. 鉴于我可以用 prenex 范式编写我的公式，它还在 EPR 类中吗？
  2. 这样的公式是可判定的吗？z3 是此类公式的决策程序吗？我应该如何约束我的谓词以使公式是可判定的？

更新 - 上述一组公式可以表示为关系代数中的联合查询，但不等式。

4

1 回答 1

2

您的公式位于 Z3 支持的可判定片段中。从技术上讲，该公式不在 EPR 中，因为您x < c在量词中使用了形式的原子。Z3 指南（量词部分）描述了许多可以由 Z3 决定的片段。请注意，其中一些片段非常昂贵（例如，NEXPTIME-hard）。因此，Z3 可能仍然无法在合理的时间内解决它们，或者内存不足。

于 2013-05-13T09:33:44.670 回答