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 6953 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
r )

Definition at line 6964 of file z3py.py.

6964 def __init__(self, r):
6965 self.r = r
6966

Member Function Documentation

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 6967 of file z3py.py.

6967 def __deepcopy__(self, memo={}):
6968 return CheckSatResult(self.r)
6969

◆ __eq__()

__eq__ ( self,
other )

Definition at line 6970 of file z3py.py.

6970 def __eq__(self, other):
6971 return isinstance(other, CheckSatResult) and self.r == other.r
6972

Referenced by __ne__().

◆ __ne__()

__ne__ ( self,
other )

Definition at line 6973 of file z3py.py.

6973 def __ne__(self, other):
6974 return not self.__eq__(other)
6975

◆ __repr__()

__repr__ ( self)

Definition at line 6976 of file z3py.py.

6976 def __repr__(self):
6977 if in_html_mode():
6978 if self.r == Z3_L_TRUE:
6979 return "<b>sat</b>"
6980 elif self.r == Z3_L_FALSE:
6981 return "<b>unsat</b>"
6982 else:
6983 return "<b>unknown</b>"
6984 else:
6985 if self.r == Z3_L_TRUE:
6986 return "sat"
6987 elif self.r == Z3_L_FALSE:
6988 return "unsat"
6989 else:
6990 return "unknown"
6991

◆ _repr_html_()

_repr_html_ ( self)
protected

Definition at line 6992 of file z3py.py.

6992 def _repr_html_(self):
6993 in_html = in_html_mode()
6994 set_html_mode(True)
6995 res = repr(self)
6996 set_html_mode(in_html)
6997 return res
6998
6999

Field Documentation

◆ r

r = r

Definition at line 6965 of file z3py.py.

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