enum

Z3::CheckResult

Inherits Enum < Comparable < Value < Object

What #check came back with. Z3 answers an LBool, whose False means "no model exists" rather than anything about a Bool expression, so it gets a type of its own rather than leaking LibZ3 into every #check.

Constants

Unsat = -1

Unknown = 0

Sat = 1

Constructors

from_lbool(lbool : LibZ3::LBool) : CheckResult

Source

Instance methods

sat?

Returns true if this enum value equals Sat

Source

unknown?

Returns true if this enum value equals Unknown

Source

unsat?

Returns true if this enum value equals Unsat

Source