Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions | Data Fields
CheckSatResult Class Reference

Public Member Functions

def __init__
 
def __deepcopy__
 
def __eq__
 
def __ne__
 
def __repr__
 

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

Constructor & Destructor Documentation

def __init__ (   self,
  r 
)

Definition at line 6377 of file z3py.py.

6378  def __init__(self, r):
6379  self.r = r

Member Function Documentation

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6380 of file z3py.py.

6381  def __deepcopy__(self, memo={}):
6382  return CheckSatResult(self.r)
def __eq__ (   self,
  other 
)

Definition at line 6383 of file z3py.py.

Referenced by Probe.__ne__().

6384  def __eq__(self, other):
6385  return isinstance(other, CheckSatResult) and self.r == other.r
def __ne__ (   self,
  other 
)

Definition at line 6386 of file z3py.py.

6387  def __ne__(self, other):
6388  return not self.__eq__(other)
def __repr__ (   self)

Definition at line 6389 of file z3py.py.

6390  def __repr__(self):
6391  if in_html_mode():
6392  if self.r == Z3_L_TRUE:
6393  return "<b>sat</b>"
6394  elif self.r == Z3_L_FALSE:
6395  return "<b>unsat</b>"
6396  else:
6397  return "<b>unknown</b>"
6398  else:
6399  if self.r == Z3_L_TRUE:
6400  return "sat"
6401  elif self.r == Z3_L_FALSE:
6402  return "unsat"
6403  else:
6404  return "unknown"

Field Documentation

r

Definition at line 6378 of file z3py.py.

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