Your formula is in decidable fragment that is supported by Z3. Technically, the formula is not in EPR because you use atoms of the form x < c
in quantifiers. The Z3 guide (Quantifiers section) describes many fragments that can be decided by Z3. Note that some of these fragments are very expensive (e.g., NEXPTIME-hard). So, Z3 may still fail to solve them in a reasonable amount of time, or run out of memory.
EPR formulas with equality and inequality
Domanda
I am encoding sets as relations and operations over sets as universally quantified implications. I have a selection operator over sets that produces new sets by selecting elements satisfying a unary predicate p (eg: v<4, v>4, ..). Due to this operator, I have simple arithmetic predicates in my formulas. An example Z3 encoding of such a formula is given below -
(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)
As expected, Z3 returns UNSAT for the above formula. However, my questions are -
- Given that I can write my formula in prenex normal form, is it still in EPR class?
- Are such formulas decidable? Is z3 a decision procedure for such formulas? How should I constrain my predicates such that the formulas are decidable?
Update - The aforementioned set of formulas can be expressed as conjunctive queries in relational algebra, but with inequality.
Soluzione
Autorizzato sotto: CC-BY-SA insieme a attribuzione
Non affiliato a StackOverflow