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

Constructor & Destructor Documentation

§ __init__()

def __init__ (   self,
  r 
)

Definition at line 5871 of file z3py.py.

5871  def __init__(self, r):
5872  self.r = r
5873 

Member Function Documentation

§ __eq__()

def __eq__ (   self,
  other 
)

Definition at line 5874 of file z3py.py.

Referenced by Probe.__ne__().

5874  def __eq__(self, other):
5875  return isinstance(other, CheckSatResult) and self.r == other.r
5876 

§ __ne__()

def __ne__ (   self,
  other 
)

Definition at line 5877 of file z3py.py.

5877  def __ne__(self, other):
5878  return not self.__eq__(other)
5879 

§ __repr__()

def __repr__ (   self)

Definition at line 5880 of file z3py.py.

5880  def __repr__(self):
5881  if in_html_mode():
5882  if self.r == Z3_L_TRUE:
5883  return "<b>sat</b>"
5884  elif self.r == Z3_L_FALSE:
5885  return "<b>unsat</b>"
5886  else:
5887  return "<b>unknown</b>"
5888  else:
5889  if self.r == Z3_L_TRUE:
5890  return "sat"
5891  elif self.r == Z3_L_FALSE:
5892  return "unsat"
5893  else:
5894  return "unknown"
5895 

Field Documentation

§ r

r

Definition at line 5872 of file z3py.py.