A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://z3prover.github.io/api/html/classz3py_1_1_array_ref.html below:

Z3: ArrayRef Class Reference

def  sort (self)   def  domain (self)   def  domain_n (self, i)   def  range (self)   def  __getitem__ (self, arg)   def  default (self)   def  as_ast (self)   def  get_id (self)   def  sort_kind (self)   def  __eq__ (self, other)   def  __hash__ (self)   def  __ne__ (self, other)   def  params (self)   def  decl (self)   def  num_args (self)   def  arg (self, idx)   def  children (self)   def  from_string (self, s)   def  serialize (self)   def  __init__ (self, ast, ctx=None)   def  __del__ (self)   def  __deepcopy__ (self, memo={})   def  __str__ (self)   def  __repr__ (self)   def  __nonzero__ (self)   def  __bool__ (self)   def  sexpr (self)   def  ctx_ref (self)   def  eq (self, other)   def  translate (self, target)   def  __copy__ (self)   def  hash (self)   def  use_pp (self)   
Array expressions.

Definition at line 4594 of file z3py.py.

◆ __getitem__() def __getitem__ (   self,   arg  ) 
Return the Z3 expression `self[arg]`.

>>> a = Array('a', IntSort(), BoolSort())
>>> i = Int('i')
>>> a[i]
a[i]
>>> a[i].sexpr()
'(select a i)'

Definition at line 4628 of file z3py.py.

4628  def

__getitem__(self, arg):

4629  """Return the Z3 expression `self[arg]`. 4631  >>> a = Array('a', IntSort(), BoolSort()) 4638  return

_array_select(self, arg)

◆ default()

Definition at line 4640 of file z3py.py.

Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array)

Access the array default value. Produces the default range value, for arrays that can be represented ...

◆ domain() 
Shorthand for `self.sort().domain()`.

>>> a = Array('a', IntSort(), BoolSort())
>>> a.domain()
Int

Definition at line 4606 of file z3py.py.

4607  """Shorthand for `self.sort().domain()`. 4609  >>> a = Array('a', IntSort(), BoolSort()) 4613  return

self.sort().domain()

Referenced by FuncDeclRef.__call__(), and ArrayRef.default().

◆ domain_n() 
Shorthand for self.sort().domain_n(i)`.

Definition at line 4615 of file z3py.py.

4615  def

domain_n(self, i):

4616  """Shorthand for self.sort().domain_n(i)`.""" 4617  return

self.sort().domain_n(i)

Referenced by ArrayRef.default().

◆ range() 
Shorthand for `self.sort().range()`.

>>> a = Array('a', IntSort(), BoolSort())
>>> a.range()
Bool

Definition at line 4619 of file z3py.py.

4620  """Shorthand for `self.sort().range()`. 4622  >>> a = Array('a', IntSort(), BoolSort()) 4626  return

self.sort().

range

()

expr range(expr const &lo, expr const &hi)

Referenced by ArrayRef.default().

◆ sort() 
Return the array sort of the array expression `self`.

>>> a = Array('a', IntSort(), BoolSort())
>>> a.sort()
Array(Int, Bool)

Reimplemented from ExprRef.

Definition at line 4597 of file z3py.py.

4598  """Return the array sort of the array expression `self`. 4600  >>> a = Array('a', IntSort(), BoolSort()) 4604  return

ArraySortRef(

Z3_get_sort

(self.ctx_ref(), self.as_ast()), self.ctx)

Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)

Return the sort of an AST node.

Referenced by FPNumRef.as_string(), ArrayRef.domain(), ArrayRef.domain_n(), FPRef.ebits(), ArithRef.is_int(), ArithRef.is_real(), ArrayRef.range(), FPRef.sbits(), BitVecRef.size(), and ExprRef.sort_kind().

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4