Z3 |

Public Member Functions | Data Fields
CheckSatResult Class Reference

## Public Member Functions
def | __init__ (self, r)
def | __deepcopy__ (self, memo={})
def | __eq__ (self, other)
def | __ne__ (self, other)
def | __repr__ (self)

## Data Fields
| r

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

## Constructor & Destructor Documentation

## ◆ __init__()

def __init__ | ( |  | self,
|  |  | r
| ) |  |

Definition at line 6746 of file z3py.py.

6746 def __init__(self, r):
6747 self.r = r
6748

## Member Function Documentation

## ◆ __deepcopy__()

def __deepcopy__ | ( |  | self,
|  |  | memo = `{}`
| ) |  |

Definition at line 6749 of file z3py.py.

6749 def __deepcopy__(self, memo={}):
6750 return CheckSatResult(self.r)
6751

## ◆ __eq__()

def __eq__ | ( |  | self,
|  |  | other
| ) |  |

Definition at line 6752 of file z3py.py.

6752 def __eq__(self, other):
6753 return isinstance(other, CheckSatResult) and self.r == other.r
6754

Referenced by CheckSatResult.__ne__(), and Probe.__ne__().

## ◆ __ne__()

def __ne__ | ( |  | self,
|  |  | other
| ) |  |

Definition at line 6755 of file z3py.py.

6755 def __ne__(self, other):
6756 return not self.__eq__(other)
6757

## ◆ __repr__()

def __repr__ | ( |  | self | ) |

Definition at line 6758 of file z3py.py.

6758 def __repr__(self):
6759 if in_html_mode():
6760 if self.r == Z3_L_TRUE:
6761 return "<b>sat</b>"
6762 elif self.r == Z3_L_FALSE:
6763 return "<b>unsat</b>"
6764 else:
6765 return "<b>unknown</b>"
6766 else:
6767 if self.r == Z3_L_TRUE:
6768 return "sat"
6769 elif self.r == Z3_L_FALSE:
6770 return "unsat"
6771 else:
6772 return "unknown"
6773

## Field Documentation

## ◆ r

r

Definition at line 6747 of file z3py.py.

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