Quantifier in Z3

Question

Basically, I want to ask Z3 to give me an arbitrary integer whose value is greater than 10. So I write the following statements:

(declare-const x (Int))
(assert (forall ((i Int)) (> i 10)))
(check-sat)
(get-value(x))

How can I apply this quantifier to my model? I know you can write (assert (> x 10)) to achieve this. But I mean I want a quantifier in my model so every time I declare an integer constant whose value is guaranteed to be over 10. So I don't have to insert statement (assert (> x 10)) for every integer constant that I declared.

Answer 1

When you use (assert (forall ((i Int)) (> i 10))), i is a bounded variable and the quantified formula is equivalent to a truth value, which is false in this case.

I think you want to define a macro using quantifiers:

(declare-fun greaterThan10 (Int) Bool)
(assert (forall ((i Int)) (= (greaterThan10 i) (> i 10))))

And you can use them to avoid code repetition:

(declare-const x (Int))
(declare-const y (Int))
(assert (greaterThan10 x))
(assert (greaterThan10 y))
(check-sat)

It is essentially the way to define macros using uninterpreted functions when you're working with Z3 API. Note that you have to set (set-option :macro-finder true) in order that Z3 replaces universal quantifiers with bodies of those functions.

However, if you're working with the textual interface, the macro define-fun in SMT-LIB v2 is an easier way to do what you want:

(define-fun greaterThan10 ((i Int)) Bool
  (> i 10))