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

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
r )

Definition at line 6902 of file z3py.py.

6902 def __init__(self, r):
6903 self.r = r
6904

Member Function Documentation

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 6905 of file z3py.py.

6905 def __deepcopy__(self, memo={}):
6906 return CheckSatResult(self.r)
6907

◆ __eq__()

__eq__ ( self,
other )

Definition at line 6908 of file z3py.py.

6908 def __eq__(self, other):
6909 return isinstance(other, CheckSatResult) and self.r == other.r
6910

Referenced by CheckSatResult.__ne__().

◆ __ne__()

__ne__ ( self,
other )

Definition at line 6911 of file z3py.py.

6911 def __ne__(self, other):
6912 return not self.__eq__(other)
6913

◆ __repr__()

__repr__ ( self)

Definition at line 6914 of file z3py.py.

6914 def __repr__(self):
6915 if in_html_mode():
6916 if self.r == Z3_L_TRUE:
6917 return "<b>sat</b>"
6918 elif self.r == Z3_L_FALSE:
6919 return "<b>unsat</b>"
6920 else:
6921 return "<b>unknown</b>"
6922 else:
6923 if self.r == Z3_L_TRUE:
6924 return "sat"
6925 elif self.r == Z3_L_FALSE:
6926 return "unsat"
6927 else:
6928 return "unknown"
6929

◆ _repr_html_()

_repr_html_ ( self)
protected

Definition at line 6930 of file z3py.py.

6930 def _repr_html_(self):
6931 in_html = in_html_mode()
6932 set_html_mode(True)
6933 res = repr(self)
6934 set_html_mode(in_html)
6935 return res
6936
6937

Field Documentation

◆ r

r = r