What exactly are Bernie-Schonfinkel class of formulas?

Question

I have a simple proposition. I would like to assert that first element from a strictly sorted list of integers is the minimum of all elements in the list. The way I define sorted list is by defining a local invariant that every element is less than its next element. I have formulated my proposition in following way in Z3 -

---

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

(declare-fun S (Int) Bool)
(declare-fun preceeds (Int Int) Bool)
(declare-fun occurs-before (Int Int) Bool)

;; preceeds is anti-reflexive
(assert (forall ((x Int)) (=> (S x) (not (preceeds x x)))))

;; preceeds is monotonic
(assert (forall ((x Int) (y Int)) (=> (and (S x) (and (S y) (and (preceeds x y))))
                                       (not (preceeds y x)))))
;; preceeds is a function
(assert (forall ((x Int) (y Int) (z Int)) (=> (and (S x) (and (S y) (and (S z) (and (preceeds x y)
                                             (preceeds x z)))))
                                             (= y z))))
;; preceeds induces local order
(assert (forall ((x Int) (y Int)) (=> (and (S x) (and (S y) (preceeds x y)))
                                       (< x y))))

;; preceeds implies occurs-before
(assert (forall ((x Int) (y Int)) (=> (and (and (S x) (S y)) (preceeds x y))
                                             (occurs-before x y))))

;;occurs-before is transitivie
(assert (forall ((x Int)(y Int)(z Int))
  (=> (and (S x) (and (S y) (and (S z)(and (occurs-before x y) (occurs-before y z)))))
    (occurs-before x z))
))             

(declare-const h Int)
(assert (S h))
(assert (forall ((x Int)) (=> (S x) (occurs-before h x))))
(assert (forall ((y Int)) (=> (S y) (< h y))))
(check-sat)
(get-model)                                                            

---

Firstly, I would like to know exactly what class of formulas are effectively propositional. Can my assertion be classified as effectively propositional? Secondly, is my formulation shown above correct? Thirdly, what options should I set in Z3 to make it accept quantified formulas only if they are effectively propositional?

Answer 1

We say a formula is in the effectively propositional fragment when it contains only predicates, constants, universal quantifiers, and does not use theories (e.g., arithmetic). It is very common to find alternative definitions that says that the formula has a Exists* Forall* quantifier prefix and uses only predicates. These definitions are equivalent since the existential quantifier can be eliminated using fresh uninterpreted constants. For more information see here.

Your assertions are not in the effectively propositional fragment because you use arithmetic. Z3 can decide other fragments. The Z3 tutorial has a list of fragments that can be decided by Z3. Your assertions is not in any of the fragments listed, but Z3 should be able to handle them and other similar assertions without problems.

Regarding the correctness of your assertions, the following two assertions cannot be satisfied.

(assert (S h))
(assert (forall ((y Int)) (=> (S y) (< h y))))

If we instantiate the quantifier with h we can deduce (< h h) which is false. I see what you are trying to do. You may also consider the following simple encoding (maybe it is too simple). It is also available online here.

;; Encode a 'list' as a "mapping" from position to value
(declare-fun list (Int) Int)

;; Asserting that the list is sorted
(assert (forall ((i Int) (j Int)) (=> (<= i j) (<= (list i) (list j)))))

;; Now, we prove that for every i >= 0 the element at position 0 is less than equal to element at position i
;; That is, we show that the negation is unsatisfiable with the previous assertion
(assert (not (forall ((i Int)) (=> (>= i 0) (<= (list 0) (list i))))))

(check-sat)

Finally, Z3 does not have any command line for checking whether a formula is in the effectively propositional fragment or not.