私は集合を関係として符号化し、集合に対する操作を普遍的に定量化された含意として符号化しています。単項述語 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 を返します。しかし、私の質問は -
- 数式を前置正規形で記述できるとすれば、それはまだ EPR クラスですか?
- そのような式は決定可能ですか？z3 はそのような式の決定手順ですか? 式が決定可能になるように述語を制約するにはどうすればよいですか?
更新 - 前述の式のセットは、リレーショナル代数の結合クエリとして表現できますが、不等式があります。