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

Public Member Functions

def __init__
 
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 5735 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  r 
)

Definition at line 5746 of file z3py.py.

5746 
5747  def __init__(self, r):
5748  self.r = r

Member Function Documentation

def __eq__ (   self,
  other 
)

Definition at line 5749 of file z3py.py.

Referenced by Probe.__ne__().

5749 
5750  def __eq__(self, other):
5751  return isinstance(other, CheckSatResult) and self.r == other.r
def __ne__ (   self,
  other 
)

Definition at line 5752 of file z3py.py.

5752 
5753  def __ne__(self, other):
5754  return not self.__eq__(other)
def __repr__ (   self)

Definition at line 5755 of file z3py.py.

5755 
5756  def __repr__(self):
5757  if in_html_mode():
5758  if self.r == Z3_L_TRUE:
5759  return "<b>sat</b>"
5760  elif self.r == Z3_L_FALSE:
5761  return "<b>unsat</b>"
5762  else:
5763  return "<b>unknown</b>"
5764  else:
5765  if self.r == Z3_L_TRUE:
5766  return "sat"
5767  elif self.r == Z3_L_FALSE:
5768  return "unsat"
5769  else:
5770  return "unknown"

Field Documentation

r

Definition at line 5747 of file z3py.py.

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

Generated on Fri Apr 12 2019 11:38:54 for Z3 by   doxygen 1.8.5