RetroSearch Browse

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

Booleans.

Boolean sort.

Definition at line 1532 of file z3py.py.

◆ cast()

Try to cast `val` as a Boolean.

>>> x = BoolSort().cast(True)
>>> x
True
>>> is_expr(x)
True
>>> is_expr(True)
False
>>> x.sort()
Bool

Reimplemented from SortRef.

Definition at line 1535 of file z3py.py.

1535 def

cast(self, val):

1536 """Try to cast `val` as a Boolean. 1538 >>> x = BoolSort().cast(True) 1548 if

isinstance(val, bool):

1549 return BoolVal

(val, self.ctx)

1552

msg =

"True, False or Z3 Boolean expression expected. Received %s of type %s" 1553

_z3_assert(

(val), msg % (val, type(val)))

1554 if not

self.eq(val.sort()):

1555

_z3_assert(self.eq(val.sort()),

"Value cannot be converted into a Z3 Boolean value"

)

def BoolVal(val, ctx=None)

◆ is_bool() ◆ is_int() ◆ subsort() def subsort ( self, other )

Return `True` if `self` is a subsort of `other`.

>>> IntSort().subsort(RealSort())
True

Reimplemented from SortRef.

Definition at line 1558 of file z3py.py.

1558 def

subsort(self, other):

1559 return

isinstance(other, ArithSortRef)

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