Z3
 
Loading...
Searching...
No Matches
Public Member Functions | Data Fields | Protected Member Functions
CheckSatResult Class Reference

Public Member Functions

 __init__ (self, r)
 
 __deepcopy__ (self, memo={})
 
 __eq__ (self, other)
 
 __ne__ (self, other)
 
 __repr__ (self)
 

Data Fields

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

Constructor & Destructor Documentation

◆ __init__()

__init__ (   self,
  r 
)

Definition at line 6848 of file z3py.py.

6848 def __init__(self, r):
6849 self.r = r
6850

Member Function Documentation

◆ __deepcopy__()

__deepcopy__ (   self,
  memo = {} 
)

Definition at line 6851 of file z3py.py.

6851 def __deepcopy__(self, memo={}):
6852 return CheckSatResult(self.r)
6853

◆ __eq__()

__eq__ (   self,
  other 
)

Definition at line 6854 of file z3py.py.

6854 def __eq__(self, other):
6855 return isinstance(other, CheckSatResult) and self.r == other.r
6856

Referenced by CheckSatResult.__ne__().

◆ __ne__()

__ne__ (   self,
  other 
)

Definition at line 6857 of file z3py.py.

6857 def __ne__(self, other):
6858 return not self.__eq__(other)
6859

◆ __repr__()

__repr__ (   self)

Definition at line 6860 of file z3py.py.

6860 def __repr__(self):
6861 if in_html_mode():
6862 if self.r == Z3_L_TRUE:
6863 return "<b>sat</b>"
6864 elif self.r == Z3_L_FALSE:
6865 return "<b>unsat</b>"
6866 else:
6867 return "<b>unknown</b>"
6868 else:
6869 if self.r == Z3_L_TRUE:
6870 return "sat"
6871 elif self.r == Z3_L_FALSE:
6872 return "unsat"
6873 else:
6874 return "unknown"
6875

◆ _repr_html_()

_repr_html_ (   self)
protected

Definition at line 6876 of file z3py.py.

6876 def _repr_html_(self):
6877 in_html = in_html_mode()
6878 set_html_mode(True)
6879 res = repr(self)
6880 set_html_mode(in_html)
6881 return res
6882
6883

Field Documentation

◆ r

r