Z3
Loading...
Searching...
No Matches
CheckSatResult Class Reference

Public Member Functions

 __init__ (self, r)
 __deepcopy__ (self, memo={})
 __eq__ (self, other)
 __ne__ (self, other)
 __repr__ (self)

Data Fields

 r = r

Protected Member Functions

 _repr_html_ (self)

Detailed Description

Represents the result of a satisfiability check: sat, unsat, unknown.

>>> s = Solver()
>>> s.check()
sat
>>> r = s.check()
>>> isinstance(r, CheckSatResult)
True

Definition at line 6962 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
r )

Definition at line 6973 of file z3py.py.

6973 def __init__(self, r):
6974 self.r = r
6975

Member Function Documentation

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 6976 of file z3py.py.

6976 def __deepcopy__(self, memo={}):
6977 return CheckSatResult(self.r)
6978

◆ __eq__()

__eq__ ( self,
other )

Definition at line 6979 of file z3py.py.

6979 def __eq__(self, other):
6980 return isinstance(other, CheckSatResult) and self.r == other.r
6981

Referenced by __ne__().

◆ __ne__()

__ne__ ( self,
other )

Definition at line 6982 of file z3py.py.

6982 def __ne__(self, other):
6983 return not self.__eq__(other)
6984

◆ __repr__()

__repr__ ( self)

Definition at line 6985 of file z3py.py.

6985 def __repr__(self):
6986 if in_html_mode():
6987 if self.r == Z3_L_TRUE:
6988 return "<b>sat</b>"
6989 elif self.r == Z3_L_FALSE:
6990 return "<b>unsat</b>"
6991 else:
6992 return "<b>unknown</b>"
6993 else:
6994 if self.r == Z3_L_TRUE:
6995 return "sat"
6996 elif self.r == Z3_L_FALSE:
6997 return "unsat"
6998 else:
6999 return "unknown"
7000

◆ _repr_html_()

_repr_html_ ( self)
protected

Definition at line 7001 of file z3py.py.

7001 def _repr_html_(self):
7002 in_html = in_html_mode()
7003 set_html_mode(True)
7004 res = repr(self)
7005 set_html_mode(in_html)
7006 return res
7007
7008

Field Documentation

◆ r

r = r

Definition at line 6974 of file z3py.py.

Referenced by __deepcopy__(), __eq__(), and __repr__().