Z3
Public Member Functions | Data Fields
CheckSatResult Class Reference

Public Member Functions

def __init__ (self, r)
 
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 5698 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  r 
)

Definition at line 5709 of file z3py.py.

5709  def __init__(self, r):
5710  self.r = r
5711 
def __init__(self, r)
Definition: z3py.py:5709

Member Function Documentation

def __eq__ (   self,
  other 
)

Definition at line 5712 of file z3py.py.

Referenced by Probe.__ne__().

5712  def __eq__(self, other):
5713  return isinstance(other, CheckSatResult) and self.r == other.r
5714 
def __eq__(self, other)
Definition: z3py.py:5712
def __ne__ (   self,
  other 
)

Definition at line 5715 of file z3py.py.

5715  def __ne__(self, other):
5716  return not self.__eq__(other)
5717 
def __eq__(self, other)
Definition: z3py.py:5712
def __ne__(self, other)
Definition: z3py.py:5715
def __repr__ (   self)

Definition at line 5718 of file z3py.py.

5718  def __repr__(self):
5719  if in_html_mode():
5720  if self.r == Z3_L_TRUE:
5721  return "<b>sat</b>"
5722  elif self.r == Z3_L_FALSE:
5723  return "<b>unsat</b>"
5724  else:
5725  return "<b>unknown</b>"
5726  else:
5727  if self.r == Z3_L_TRUE:
5728  return "sat"
5729  elif self.r == Z3_L_FALSE:
5730  return "unsat"
5731  else:
5732  return "unknown"
5733 
def __repr__(self)
Definition: z3py.py:5718

Field Documentation

r

Definition at line 5710 of file z3py.py.

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