CheckSatResult Class Reference

Public Member Functions
	__init__ (self, r)
	__deepcopy__ (self, memo={})
	__eq__ (self, other)
	__ne__ (self, other)
	__repr__ (self)

Data Fields
	r

Protected Member Functions
	_repr_html_ (self)

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

Constructor & Destructor Documentation

__init__()

__init__	(		self,
			r
	)

Definition at line 7503 of file z3py.py.

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

Member Function Documentation

__deepcopy__()

__deepcopy__	(		self,
			memo = {}
	)

Definition at line 7506 of file z3py.py.

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

__eq__()

__eq__	(		self,
			other
	)

Definition at line 7509 of file z3py.py.

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

Referenced by CheckSatResult.__ne__().

__ne__()

__ne__	(		self,
			other
	)

Definition at line 7512 of file z3py.py.

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

__repr__()

__repr__

(

self

)

Definition at line 7515 of file z3py.py.

    def __repr__(self):
        if in_html_mode():
            if self.r == Z3_L_TRUE:
                return "<b>sat</b>"
            elif self.r == Z3_L_FALSE:
                return "<b>unsat</b>"
            else:
                return "<b>unknown</b>"
        else:
            if self.r == Z3_L_TRUE:
                return "sat"
            elif self.r == Z3_L_FALSE:
                return "unsat"
            else:
                return "unknown"
 

_repr_html_()

_repr_html_ (   self )

protected

Definition at line 7531 of file z3py.py.

    def _repr_html_(self):
        in_html = in_html_mode()
        set_html_mode(True)
        res = repr(self)
        set_html_mode(in_html)
        return res
 
 

Field Documentation

r

r

Definition at line 7504 of file z3py.py.

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