Z3::Checkable
Everything Solver and Optimize both do, expressed in terms of #check,
#model, #assert and #push / #pop, which they each implement themselves.
Instance methods
prove!(claim : BoolExpr, io : IO = STDOUT) : Nil
Asserts the negation of the claim and prints the verdict - "Proven" if nothing
satisfies it, a counterexample if something does. The assertion is scoped, so
this leaves the solver as it found it. The Ruby gem prints to stdout; io is
here so the output can be captured.
satisfiable?(*assumptions) : Bool
The splat is untyped because Crystal requires at least one argument for a
splat with a type restriction, and #check with no assumptions is the common
case. BoolSort.cast is what refuses anything which isn't a Bool.
unsatisfiable?(*assumptions) : Bool
Source