Hoogle Search

Within LTS Haskell 24.45 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

Exact lookup

1. satConcurrentWithAny :: Satisfiable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)

   sbv	Data.SBV

   Find a satisfying assignment to a property using a single solver, but providing several query problems of interest, with each query running in a separate thread and return the first one that returns. This can be useful to use symbolic mode to drive to a location in the search space of the solver and then refine the problem in query mode. If the computation is very hard to solve for the solver than running in concurrent mode may provide a large performance benefit.

2. satWithAny :: Satisfiable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)

   sbv	Data.SBV

   Find a satisfying assignment to 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.

3. proveConcurrentWithAny :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO (Solver, NominalDiffTime, ThmResult)

   sbv	Data.SBV.Dynamic

   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 return the first query computation that completes, killing the others.

4. proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)

   sbv	Data.SBV.Dynamic

   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.

5. satConcurrentWithAny :: SMTConfig -> [Query b] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)

   sbv	Data.SBV.Dynamic

   Find a satisfying assignment to a property with multiple threads in query mode. The Symbolic SVal represents what is known to all child query threads. Each query thread will spawn a unique instance of the solver. Only the first one to finish will be returned and the other threads will be killed.

6. satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)

   sbv	Data.SBV.Dynamic

   Find a satisfying assignment to 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.

7. SBVAny :: Kind -> SMTLambda -> SeqOp

   sbv	Data.SBV.Internals

   any a fun. Where fun :: a -> Bool, and any :: (a -> Bool) -> [a] -> Bool

8. sAny :: (a -> SBool) -> [a] -> SBool

   sbv	Data.SBV.Internals

   Generalization of any

9. sAny :: (a -> SBool) -> [a] -> SBool

   sbv	Data.SBV.Trans

   Generalization of any

10. allAny :: IO Proof

    sbv	Documentation.SBV.Examples.KnuckleDragger.Lists

    not (all id xs) == any not xs
    

    A list of booleans is not all true, if any of them is false. We have:

    >>> allAny
    Inductive lemma: allAny
    Step: Base                            Q.E.D.
    Step: 1                               Q.E.D.
    Step: 2                               Q.E.D.
    Step: 3                               Q.E.D.
    Step: 4                               Q.E.D.
    Result:                               Q.E.D.
    [Proven] allAny
    

Page 204 of many | Previous | Next