q package:sbv

The quotient

Monad for querying a solver.

A new data-type that we expect to use in an uninterpreted fashion in the backend SMT solver.

Negation of a quantified formula. This operation essentially lifts sNot to quantified formulae. Note that you can achieve the same using sNot . quantifiedBool, but that will hide the quantifiers, so prefer this version if you want to keep them around.

Turn a quantified boolean into a regular boolean. That is, this function turns an exists/forall quantified formula to a simple boolean that can be used as a regular boolean value. An example is:

quantifiedBool $ \(Forall x) (Exists y) -> y .> (x :: SInteger)

is equivalent to sTrue. You can think of this function as performing quantifier-elimination: It takes a quantified formula, and reduces it to a simple boolean that is equivalent to it, but has no quantifiers.

No messages what-so-ever for successful steps. (Will print if something fails)

Run a custom query

If verbose is True, print the message, useful for debugging messages in custom queries. Note that redirectVerbose will be respected: If a file redirection is given, the output will go to the file. NB. For a version which generalizes over the underlying monad, see queryDebug

A quick-check step, taking number of tests.

A quick-check step, with specific quick-check args.

Mark the end of a calculational proof.

Run a custom query.

Generalization of queryDebug

Collection of queries

Helper to turn quantified formula to a regular boolean. We can think of this as quantifier elimination, hence the name qe.

Helper for turning an invariant predicate to a boolean.