RetroSearch Browse

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

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

Z3: BoolRef Class Reference

def sort (self) def __add__ (self, other) def __radd__ (self, other) def __rmul__ (self, other) def __mul__ (self, other) def __and__ (self, other) def __or__ (self, other) def __xor__ (self, other) def __invert__ (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)

All Boolean expressions are instances of this class.

Definition at line 1568 of file z3py.py.

◆ __add__() def __add__ ( self, other )

Definition at line 1574 of file z3py.py.

1574 def

__add__(self, other):

1575 if

isinstance(other, BoolRef):

1576

other =

(other, 1, 0)

1577 return If

(self, 1, 0) + other

def If(a, b, c, ctx=None)

◆ __and__() def __and__ ( self, other )

Definition at line 1596 of file z3py.py.

1596 def

__and__(self, other):

1597 return And

(self, other)

◆ __invert__()

Definition at line 1605 of file z3py.py.

1605 def

__invert__(self):

◆ __mul__() def __mul__ ( self, other )

Create the Z3 expression `self * other`.

Definition at line 1585 of file z3py.py.

1585 def

__mul__(self, other):

1586 """Create the Z3 expression `self * other`. 1588 if

isinstance(other, int)

and

other == 1:

1589 return If

(self, 1, 0)

1590 if

isinstance(other, int)

and

other == 0:

1591 return IntVal

(0, self.ctx)

1592 if

isinstance(other, BoolRef):

1593

other =

(other, 1, 0)

1594 return If

(self, other, 0)

def IntVal(val, ctx=None)

◆ __or__() def __or__ ( self, other )

Definition at line 1599 of file z3py.py.

1599 def

__or__(self, other):

1600 return Or

(self, other)

◆ __radd__() def __radd__ ( self, other )

Definition at line 1579 of file z3py.py.

1579 def

__radd__(self, other):

◆ __rmul__() def __rmul__ ( self, other )

Definition at line 1582 of file z3py.py.

1582 def

__rmul__(self, other):

◆ __xor__() def __xor__ ( self, other )

Definition at line 1602 of file z3py.py.

1602 def

__xor__(self, other):

1603 return Xor

(self, other)

◆ sort()

Return the sort of expression `self`.

>>> x = Int('x')
>>> (x + 1).sort()
Int
>>> y = Real('y')
>>> (x + y).sort()
Real

Reimplemented from ExprRef.

Reimplemented in QuantifierRef.

Definition at line 1571 of file z3py.py.

1572 return

BoolSortRef(

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