Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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 5675 of file z3py.py.


Constructor & Destructor Documentation

def __init__ (   self,
  r 
)

Definition at line 5686 of file z3py.py.

05686 
05687     def __init__(self, r):
05688         self.r = r


Member Function Documentation

def __eq__ (   self,
  other 
)

Definition at line 5689 of file z3py.py.

Referenced by Probe.__ne__().

05689 
05690     def __eq__(self, other):
05691         return isinstance(other, CheckSatResult) and self.r == other.r

def __ne__ (   self,
  other 
)

Definition at line 5692 of file z3py.py.

05692 
05693     def __ne__(self, other):
05694         return not self.__eq__(other)

def __repr__ (   self)

Definition at line 5695 of file z3py.py.

05695 
05696     def __repr__(self):
05697         if in_html_mode():
05698             if self.r == Z3_L_TRUE:
05699                 return "<b>sat</b>"
05700             elif self.r == Z3_L_FALSE:
05701                 return "<b>unsat</b>"
05702             else:
05703                 return "<b>unknown</b>"
05704         else:
05705             if self.r == Z3_L_TRUE:
05706                 return "sat"
05707             elif self.r == Z3_L_FALSE:
05708                 return "unsat"
05709             else:
05710                 return "unknown"


Field Documentation

r

Definition at line 5686 of file z3py.py.

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

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines