a package:sbv

Helper type synonym

Default configuration for the ABC synthesis and verification tool.

Convert an AlgReal to a Rational. If the AlgReal is exact, then you get a Left value. Otherwise, you get a Right value which is simply an approximation.

Returns (symbolic) sTrue if all the elements of the given list are the same.

Find all satisfying assignments, using the default solver. Equivalent to allSatWith defaultSMTCfg. See allSatWith for details. NB. For a version which generalizes over the underlying monad, see allSat

In a allSat call, return at most this many models. If nothing, return all.

Did we reach the user given model count limit?

In a allSat call, print models as they are found.

All satisfying models

Did the solver report delta-satisfiable at the end?

Did the solver report unknown at the end?

In a allSat call, should we try to extract values of uninterpreted functions?

Return all satisfying assignments for a predicate. Note that this call will block until all satisfying assignments are found. If you have a problem with infinitely many satisfying models (consider SInteger) or a very large number of them, you might have to wait for a long time. To avoid such cases, use the allSatMaxModelCount parameter in the configuration. NB. Uninterpreted constant/function values and counter-examples for array values are ignored for the purposes of allSat. That is, only the satisfying assignments modulo uninterpreted functions and array inputs will be returned. This is due to the limitation of not having a robust means of getting a function counter-example back from the SMT solver. Find all satisfying assignments using the given SMT-solver NB. For a version which generalizes over the underlying monad, see allSatWith

Introduce a soft assertion, with an optional penalty NB. For a version which generalizes over the underlying monad, see assertWithPenalty

Find all satisfying assignments using the given SMT-solver

Generalization of addSValOptGoal

Check all elements satisfy the predicate.

>>> let isEven x = x `sMod` 2 .== 0

>>> all isEven [2, 4, 6, 8, 10 :: Integer]
True

>>> all isEven [2, 4, 6, 1, 8, 10 :: Integer]
False

Check some element satisfies the predicate. -- >>> let isEven x = x sMod 2 .== 0 >>> any (sNot . isEven) [2, 4, 6, 8, 10 :: Integer] False >>> any isEven [2, 4, 6, 1, 8, 10 :: Integer] True

Match any character, i.e., strings of length 1

>>> prove $ \(s :: SString) -> s `match` anyChar .<=> length s .== 1
Q.E.D.

Recognize an alphabet letter, i.e., A..Z, a..z.

Recognize an ASCII lower case letter

>>> asciiLower
(re.range "a" "z")

>>> prove $ \c -> (c :: SChar) `match` asciiLower  .=> c `match` asciiLetter
Q.E.D.

>>> prove $ \c -> c `match` asciiLower  .=> toUpperL1 c `match` asciiUpper
Q.E.D.

>>> prove $ \c -> c `match` asciiLetter .=> toLowerL1 c `match` asciiLower
Q.E.D.

Recognize an upper case letter

>>> asciiUpper
(re.range "A" "Z")

>>> prove $ \c -> (c :: SChar) `match` asciiUpper  .=> c `match` asciiLetter
Q.E.D.

>>> prove $ \c -> c `match` asciiUpper  .=> toLowerL1 c `match` asciiLower
Q.E.D.

>>> prove $ \c -> c `match` asciiLetter .=> toUpperL1 c `match` asciiUpper
Q.E.D.

Add two polynomials

An assert is a quick way of ensuring some condition holds. If it does, then it's equivalent to Skip. Otherwise, it is equivalent to Abort.