enum Z3::CheckResult

Overview

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.

Defined in:

z3/check_result.cr

Enum Members

Unsat = -1

Unknown = 0

Sat = 1

Constructors

• .from_lbool(lbool : LibZ3::LBool) : CheckResult

Instance Method Summary

• #sat?

  Returns true if this enum value equals Sat

• #unknown?

  Returns true if this enum value equals Unknown

• #unsat?

  Returns true if this enum value equals Unsat

Constructor Detail

Instance Method Detail