Difference between revisions of "Manuals/calci/THEREEXISTS"
Jump to navigation
Jump to search
(Created page with "==THEREEXISTS(SomeArray,SomeFunctions) == ==Description== *THEREEXISTS returns the result of applying the set of SomeFunctions to SomeArray, if results evaluate to true for...") |
|||
| Line 1: | Line 1: | ||
==THEREEXISTS(SomeArray,SomeFunctions) == | ==THEREEXISTS(SomeArray,SomeFunctions) == | ||
| + | |||
| + | |||
| + | ==THEREEXISTS (SomeArray,SomeFunctions) == | ||
==Description== | ==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. | *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== | ||
| + | |||
| + | *[[Manuals/calci/FORALL| FORALL]] | ||
| + | *[[Manuals/calci/THEREEXISTS| THEREEXISTS]] | ||
| + | *[[Manuals/calci/THEREDOESNOTEXIST| THEREDOESNOTEXIST]] | ||
| + | *[[Manuals/calci/THEREEXISTSONE| THEREEXISTSONE]] | ||
| + | *[[Manuals/calci/FORDOFFUNCTIONS| FORDOFFUNCTIONS]] | ||
| + | |||
| + | ==References== | ||
| + | |||
| + | *[[Z_API_Functions | List of Main Z Functions]] | ||
| + | |||
| + | *[[ Z3 | Z3 home ]] | ||
==Example== | ==Example== | ||
Revision as of 15:01, 4 February 2020
THEREEXISTS(SomeArray,SomeFunctions)
THEREEXISTS (SomeArray,SomeFunctions)
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
References
Example
THEREEXISTS(1..100,"x<=0")
gives false