Z3
Public Member Functions | Data Fields
CheckSatResult Class Reference

Public Member Functions

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

Constructor & Destructor Documentation

def __init__ (   self,
  r 
)

Definition at line 6848 of file z3py.py.

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

Member Function Documentation

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6851 of file z3py.py.

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

Definition at line 6854 of file z3py.py.

Referenced by Probe.__ne__().

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

Definition at line 6857 of file z3py.py.

6857  def __ne__(self, other):
6858  return not self.__eq__(other)
6859 
def __eq__(self, other)
Definition: z3py.py:6854
def __ne__(self, other)
Definition: z3py.py:6857
def __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 
def __repr__(self)
Definition: z3py.py:6860

Field Documentation

r