Can I use declare-const to eliminate the forall universal quantifier?

Question

I have some confusion of using universal quantifier and declare-const without using forall

(set-option :mbqi true)
(declare-fun f (Int Int) Int)
(declare-const a Int)
(declare-const b Int)

(assert (forall ((x Int)) (>= (f x x) (+ x a))))

I can write like this:

(declare-const x Int)
(assert  (>= (f x x) (+ x a))))

with Z3 will explore all the possible values of type Int in this two cases. So what's the difference? Can I really use the declare-const to eliminate the forall quantifier?

Answer 1

No, the statements are different. Constants in Z3 are nullary (0 arity) functions, so (declare-const a Int) is just syntactic sugar for (declare-fun a () Int), so these two statements are identical. Your second statement (assert (>= (f x x) (+ x a)))) implicitly asserts existence of x, instead of for all x as in your first statement (assert (forall ((x Int)) (>= (f x x) (+ x a)))). To be clear, note that in your second statement, only a single assignment for x needs to satisfy the assertion, not all possible assignments (also note the difference in the function f, and see this Z3@rise script: http://rise4fun.com/Z3/4cif ).

Here's the text of that script:

(set-option :mbqi true)
(declare-fun f (Int Int) Int)
(declare-const a Int)
(declare-fun af () Int)
(declare-const b Int)
(declare-fun bf () Int)

(push)
(declare-const x Int)
(assert  (>= (f x x) (+ x a)))
(check-sat) ; note the explicit model value for x: this only checks a single value of x, not all of them
(get-model)
(pop)

(push)
(assert (forall ((x Int)) (>= (f x x) (+ x a))))
(check-sat)
(get-model) ; no model for x since any model must satisfy assertion
(pop)

Also, here's an example from the Z3 SMT guide ( http://rise4fun.com/z3/tutorial/guide from under the section "Uninterpreted functions and constants"):

(declare-fun f (Int) Int)
(declare-fun a () Int) ; a is a constant
(declare-const b Int) ; syntax sugar for (declare-fun b () Int)
(assert (> a 20))
(assert (> b a))
(assert (= (f 10) 1))
(check-sat)
(get-model)

Answer 2

You can eliminate a top-level exists with a declare-const. Maybe this is the source of your confusion? The following two are equivalent:

    (assert (exists ((x Int)) (> x 0)))
    (check-sat)

and

   (declare-fun x () Int)
   (assert (> x 0))
   (check-sat)

Note that this only applies to top-level existential quantifiers. If you have nested quantification of both universals (forall) and existentials (exists), then you can do skolemization to float the existentials to the top level. This process is more involved but rather straightforward from a logical point of view.

There is no general way of floating universal quantifiers to the top-level in this way, at least not in classical logic as embodied by SMT-Lib.