Z3
Public Member Functions | Data Fields
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
 

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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  r 
)

Definition at line 6438 of file z3py.py.

6438  def __init__(self, r):
6439  self.r = r
6440 

Member Function Documentation

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6441 of file z3py.py.

6441  def __deepcopy__(self, memo={}):
6442  return CheckSatResult(self.r)
6443 

◆ __eq__()

def __eq__ (   self,
  other 
)

Definition at line 6444 of file z3py.py.

6444  def __eq__(self, other):
6445  return isinstance(other, CheckSatResult) and self.r == other.r
6446 

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

◆ __ne__()

def __ne__ (   self,
  other 
)

Definition at line 6447 of file z3py.py.

6447  def __ne__(self, other):
6448  return not self.__eq__(other)
6449 

◆ __repr__()

def __repr__ (   self)

Definition at line 6450 of file z3py.py.

6450  def __repr__(self):
6451  if in_html_mode():
6452  if self.r == Z3_L_TRUE:
6453  return "<b>sat</b>"
6454  elif self.r == Z3_L_FALSE:
6455  return "<b>unsat</b>"
6456  else:
6457  return "<b>unknown</b>"
6458  else:
6459  if self.r == Z3_L_TRUE:
6460  return "sat"
6461  elif self.r == Z3_L_FALSE:
6462  return "unsat"
6463  else:
6464  return "unknown"
6465 

Field Documentation

◆ r

r
z3py.UserPropagateBase.__init__
def __init__(self, s, ctx=None)
Definition: z3py.py:10582