Z3
 
Loading...
Searching...
No Matches
Public Member Functions | Data Fields | Protected Member Functions
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
 

Protected Member Functions

def _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 6845 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  r 
)

Definition at line 6856 of file z3py.py.

6856 def __init__(self, r):
6857 self.r = r
6858

Member Function Documentation

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6859 of file z3py.py.

6859 def __deepcopy__(self, memo={}):
6860 return CheckSatResult(self.r)
6861

◆ __eq__()

def __eq__ (   self,
  other 
)

Definition at line 6862 of file z3py.py.

6862 def __eq__(self, other):
6863 return isinstance(other, CheckSatResult) and self.r == other.r
6864

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

◆ __ne__()

def __ne__ (   self,
  other 
)

Definition at line 6865 of file z3py.py.

6865 def __ne__(self, other):
6866 return not self.__eq__(other)
6867

◆ __repr__()

def __repr__ (   self)

Definition at line 6868 of file z3py.py.

6868 def __repr__(self):
6869 if in_html_mode():
6870 if self.r == Z3_L_TRUE:
6871 return "<b>sat</b>"
6872 elif self.r == Z3_L_FALSE:
6873 return "<b>unsat</b>"
6874 else:
6875 return "<b>unknown</b>"
6876 else:
6877 if self.r == Z3_L_TRUE:
6878 return "sat"
6879 elif self.r == Z3_L_FALSE:
6880 return "unsat"
6881 else:
6882 return "unknown"
6883

◆ _repr_html_()

def _repr_html_ (   self)
protected

Definition at line 6884 of file z3py.py.

6884 def _repr_html_(self):
6885 in_html = in_html_mode()
6886 set_html_mode(True)
6887 res = repr(self)
6888 set_html_mode(in_html)
6889 return res
6890
6891

Field Documentation

◆ r

r