z3smtz3py

forall usage in SMT

How does forall statement work in SMT? I could not find information about usage. Can you please simply explain this? There is an example from
https://rise4fun.com/Z3/Po5.

(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (forall ((x Int))
                (! (= (f (g x)) x)
                   :pattern ((g x)))))
(assert (= (g a) c))
(assert (= (g b) c))
(assert (not (= a b)))
(check-sat)
Solution

  • For general information on quantifiers (and everything else SMTLib) see The SMT-LIB Standard, Version 2.6.

    Quoting from Section 3.6.1:

    Exists and forall quantifiers. These binders correspond to the usual universal and existential quantifiers of first-order logic, except that each variable they quantify is also associated with a sort. Both binders have a non-empty list of variables, which abbreviates a sequential nesting of quantifiers. Specifically, a formula of the form

    (forall ((x1 σ1) (x2 σ2) ··· (xn σn)) ϕ)                            (3.1)

    has the same semantics as the formula

    (forall ((x1 σ1)) (forall ((x2 σ2)) (··· (forall ((xn σn)) ϕ) ···)  (3.2)

    Note that the variables in the list ((x1 σ1) (x2 σ2) ··· (xn σn)) of (3.1) are not required to be pairwise disjoint. However, because of the nested quantifier semantics, earlier occurrences of same variable in the list are shadowed by the last occurrence—making those earlier occurrences useless. The same argument applies to the exists binder.

    If you have a quantified assertion, that means the solver has to find a satisfying instance that makes that formula true. For a forall quantifier, this means it has to find a model that the assertion is true for all assignments to the quantified variables of the relevant sorts. And likewise, for exists the model needs to be able to exhibit a particular value satisfying the assertion.

    Top-level exists quantifiers are usually left-out in SMTLib: By skolemization, declaring a top-level variable fills that need, and also has the advantage of showing up automatically in models. (That is, any top-level declared variable is automatically existentially quantified.)

    Using forall will typically make the logic semi-decidable. So, you're likely to get unknown as an answer if you use quantifiers, unless some heuristic can find a satisfying assignment. Similarly, while the syntax allows for nested quantifiers, most solvers will have very hard time dealing with them. Patterns can help, but they remain hard-to-use to this day. To sum up: If you use quantifiers, then SMT solvers are no longer decision-procedures: They may or may not terminate.

    If you are using the Python interface for z3, also take a look at the “Quantifiers” section of Z3 API in Python, Advanced Topics. It does contain some quantification examples that can clarify things for you. (Even if you don’t use the Python interface, I heartily recommend going over that page to see what the capabilities are. They more or less translate to SMTLib directly.)

    Hope that gets you started. Stack Overflow works the best if you ask specific questions, so feel free to ask clarification on actual code as you need.