module
Z3::Checkable
Overview
Everything Solver and Optimize both do, expressed in terms of #check,
#model, #assert and #push / #pop, which they each implement themselves.
Direct including types
Defined in:
z3/checkable.crInstance Method Summary
-
#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.
-
#satisfiable?(*assumptions) : Bool
The splat is untyped because Crystal requires at least one argument for a splat with a type restriction, and
#checkwith no assumptions is the common case. - #unsatisfiable?(*assumptions) : Bool
Instance Method Detail
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.
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.