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

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
r )

Definition at line 6936 of file z3py.py.

6936 def __init__(self, r):
6937 self.r = r
6938

Member Function Documentation

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 6939 of file z3py.py.

6939 def __deepcopy__(self, memo={}):
6940 return CheckSatResult(self.r)
6941

◆ __eq__()

__eq__ ( self,
other )

Definition at line 6942 of file z3py.py.

6942 def __eq__(self, other):
6943 return isinstance(other, CheckSatResult) and self.r == other.r
6944

Referenced by CheckSatResult.__ne__().

◆ __ne__()

__ne__ ( self,
other )

Definition at line 6945 of file z3py.py.

6945 def __ne__(self, other):
6946 return not self.__eq__(other)
6947

◆ __repr__()

__repr__ ( self)

Definition at line 6948 of file z3py.py.

6948 def __repr__(self):
6949 if in_html_mode():
6950 if self.r == Z3_L_TRUE:
6951 return "<b>sat</b>"
6952 elif self.r == Z3_L_FALSE:
6953 return "<b>unsat</b>"
6954 else:
6955 return "<b>unknown</b>"
6956 else:
6957 if self.r == Z3_L_TRUE:
6958 return "sat"
6959 elif self.r == Z3_L_FALSE:
6960 return "unsat"
6961 else:
6962 return "unknown"
6963

◆ _repr_html_()

_repr_html_ ( self)
protected

Definition at line 6964 of file z3py.py.

6964 def _repr_html_(self):
6965 in_html = in_html_mode()
6966 set_html_mode(True)
6967 res = repr(self)
6968 set_html_mode(in_html)
6969 return res
6970
6971

Field Documentation

◆ r

r = r