Hoogle Search

Within LTS Haskell 24.34 (ghc-9.10.3)

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

Exact lookup

1. checkWithAssumptions :: SMTReadWriter solver => SolverProcess scope solver -> String -> [BoolExpr scope] -> IO ([Text], SatResult () ())

   what4	What4.Protocol.Online

   No documentation available.

2. checkWithAssumptionsAndModel :: SMTReadWriter solver => SolverProcess scope solver -> String -> [BoolExpr scope] -> IO (SatResult (GroundEvalFn scope) ())

   what4	What4.Protocol.Online

   No documentation available.

3. getUnsatAssumptions :: SMTReadWriter solver => SolverProcess scope solver -> IO [(Bool, Text)]

   what4	What4.Protocol.Online

   After an unsatisfiable check-with-assumptions command, compute a set of the supplied assumptions that (together with previous assertions) form an unsatisfiable core. Note: the returned unsatisfiable set might not be minimal. The boolean value returned along with the name indicates if the assumption was negated or not: True indidcates a positive atom, and False represents a negated atom.

4. assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()

   what4	What4.Protocol.SMTLib2

   Write assume formula predicates for asserting predicate holds.

5. checkSatAssuming :: [Term] -> Command

   what4	What4.Protocol.SMTLib2.Syntax

   Check the satisfiability of the current assertions and the additional ones in the list.

6. checkSatWithAssumptions :: [Text] -> Command

   what4	What4.Protocol.SMTLib2.Syntax

   Check satisfiability of the given atomic assumptions in the current context. NOTE! The names of variables passed to this function MUST be generated using a `declare-fun` statement, and NOT a `define-fun` statement. Thus, if you want to bind an arbitrary term, you must declare a new term and assert that it is equal to it's definition. Yes, this is quite irritating.

7. getUnsatAssumptions :: Command

   what4	What4.Protocol.SMTLib2.Syntax

   No documentation available.

8. assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()

   what4	What4.Protocol.SMTWriter

   Write assume formula predicates for asserting predicate holds.

9. assumeFormula :: SMTWriter h => WriterConn t h -> Term h -> IO ()

   what4	What4.Protocol.SMTWriter

   Assume that the given formula holds.

10. assumeFormulaWithFreshName :: SMTWriter h => WriterConn t h -> Term h -> IO Text

    what4	What4.Protocol.SMTWriter

    No documentation available.

Page 184 of many | Previous | Next