Manuals/calci/THEREEXISTS

Description

• THEREEXISTS returns the result of applying the set of SomeFunctions to SomeArray, if results evaluate to true for the array when the functions are applied.

• This can also be represented by the notation ∃a("x<810") etc.

Example

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

gives true

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

gives false

See Also

• FORALL
• THEREEXISTS
• THEREDOESNOTEXIST
• THEREEXISTSONE
• FORDOFFUNCTIONS

References

• List of Main Z Functions

• Z3 home

Example

THEREEXISTS(1..100,"x<=0")

gives false

See Also

• FORALL
• THEREEXISTS
• THEREDOESNOTEXIST
• THEREEXISTSONE
• FORDOFFUNCTIONS

References

• List of Main Z Functions

• Z3 home