Manuals/calci/FORALL

Description

• FORALL returns the result of applying the set of SomeFunctions to SomeArray
• This can also be represented by the notation ∀a("x<101") etc.

Example

FORALL(1..100,"z<=100")

gives true

FORALL(1..100,"z<=50")

gives false

a=1..100;

[∀a("x<810"),∃a("x<810"),∄a("x<810")]

true true false

See Also

• FORALL
• THEREEXISTS
• THEREDOESNOTEXIST
• THEREEXISTSONE
• FORDOFFUNCTIONS

References

• List of Main Z Functions

• Z3 home