Формулы ЭПР с равенством и неравенством

Question

Я кодирую множества как отношения, а операции над множествами - как универсально выраженные значения. У меня есть оператор выбора для наборов, который создает новые наборы путем выбора элементов, удовлетворяющих унарному предикату 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. Учитывая, что я могу написать свою формулу в пренекс-нормальной форме, она все еще в классе EPR?
2. Такие формулы разрешимы? Является ли z3 процедурой принятия решений для таких формул? Как мне ограничить мои предикаты так, чтобы формулы были разрешимыми?

Обновление - вышеупомянутый набор формул может быть выражен как конъюнктивные запросы в реляционной алгебре, но с неравенством.

Answer 1

Ваша формула находится в разрешимом фрагменте, который поддерживается Z3. Технически, формула не в EPR, потому что вы используете атомы в форме x < c в квантификаторах. Руководство Z3 (раздел Квантификаторы) описывает множество фрагментов, которые могут быть определены Z3. Обратите внимание, что некоторые из этих фрагментов очень дороги (например, NEXPTIME-hard). Таким образом, Z3 все равно может не решить их за разумное время или не хватит памяти.