p package:sbv

A simple goal with three constraints, two of which are conflicting with each other. The third is irrelevant, in the sense that it does not contribute to the fact that the goal is unsatisfiable.

Declare a carrier data-type in Haskell named P, representing all the people in a bar.

sTrue if at least k of the input arguments are sTrue

sTrue if at most k of the input arguments are sTrue

sTrue if the sum of coefficients for sTrue elements is exactly least k. Useful for coding exactly K-of-N constraints, and in particular mutex constraints.

sTrue if exactly k of the input arguments are sTrue

sTrue if the sum of coefficients for sTrue elements is at least k. Generalizes pbAtLeast.

sTrue if the sum of coefficients for sTrue elements is at most k. Generalizes pbAtMost.

sTrue if there is at most one set bit

sTrue if there is exactly one set bit

pred, same as in the Enum class

Each line sent to the solver will be passed through this function (typically id)

Print integral literals in this base (2, 10, and 16 are supported.)

Print algebraic real values with this precision. (SReal, default: 16)

Print time/statistics. If quiet is True, then measureTime is ignored.

^ Extract the current value in a SAT context

Prove a predicate, using the default solver. NB. For a version which generalizes over the underlying monad, see prove

Prove a property by running many queries each isolated to their own thread concurrently and wait for each to finish returning all results

Prove a property by running many queries each isolated to their own thread concurrently and return the first that finishes, killing the others

Prove the predicate using the given SMT-solver. NB. For a version which generalizes over the underlying monad, see proveWith

Prove a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

Prove a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed. Note that we send an exception to the losing processes, but we do *not* actually wait for them to finish. In rare cases this can lead to zombie processes. In previous experiments, we found that some processes take their time to terminate. So, this solution favors quick turnaround.

Pop the context, exiting a new one. Pops multiple levels if n > 1. It's an error to pop levels that don't exist. NB. For a version which generalizes over the underlying monad, see pop

Push the context, entering a new one. Pushes multiple levels if n > 1. NB. For a version which generalizes over the underlying monad, see push

Prove a property with query mode using multiple threads. Each query computation will spawn a thread and a unique instance of your solver to run asynchronously. The Symbolic SVal is duplicated for each thread. This function will block until all child threads return.