parameters: (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
return_statement: return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
docstring: Create a Z3 exists formula.
  
      The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
  
  
      >>> f = Function('f', IntSort(), IntSort(), IntSort())
      >>> x = Int('x')
      >>> y = Int('y')
      >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
      >>> q
      Exists([x, y], f(x, y) >= x)
      >>> is_quantifier(q)
      True
      >>> r = Tactic('nnf')(q).as_expr()
      >>> is_quantifier(r)
      False
docstring_summary: Create a Z3 exists formula.
docstring_tokens: Create a Z3 exists formula .
function: def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
      """Create a Z3 exists formula.
  
      The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
  
  
      >>> f = Function('f', IntSort(), IntSort(), IntSort())
      >>> x = Int('x')
      >>> y = Int('y')
      >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
      >>> q
      Exists([x, y], f(x, y) >= x)
      >>> is_quantifier(q)
      True
      >>> r = Tactic('nnf')(q).as_expr()
      >>> is_quantifier(r)
      False
      """
      return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
function_tokens: def Exists ( vs , body , weight = 1 , qid = "" , skid = "" , patterns = [ ] , no_patterns = [ ] ) : return _mk_quantifier ( False , vs , body , weight , qid , skid , patterns , no_patterns )