Difference between revisions of "Manuals/calci/THEREEXISTS"

From ZCubes Wiki
Jump to navigation Jump to search
Line 1: Line 1:
==THEREEXISTS(SomeArray,SomeFunctions)  ==
 
 
 
 
==THEREEXISTS (SomeArray,SomeFunctions)  ==
 
==THEREEXISTS (SomeArray,SomeFunctions)  ==
 
  
 
==Description==
 
==Description==
Line 9: Line 5:
  
 
*This can also be represented by the notation ∃a("x<810") etc.  
 
*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==
 
  
 
THEREEXISTS(1..100,"x<=0")
 
THEREEXISTS(1..100,"x<=0")

Revision as of 15:02, 4 February 2020

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.

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

gives false


See Also

References