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.
assumeFormulaWithName :: SMTWriter h => WriterConn t h -> Term h -> Text -> IO ()what4 What4.Protocol.SMTWriter No documentation available.
bvSumExpr :: forall (w :: Nat) . SupportTermOps v => NatRepr w -> [v] -> vwhat4 What4.Protocol.SMTWriter No documentation available.
checkWithAssumptionsCommands :: SMTWriter h => f h -> [Text] -> [Command h]what4 What4.Protocol.SMTWriter Check if a collection of assumptions is satisfiable in the current context. The assumptions must be given as the names of literals already in scope.
getUnsatAssumptionsCommand :: SMTWriter h => f h -> Command hwhat4 What4.Protocol.SMTWriter Ask the solver to return an unsatisfiable core from among the assumptions passed into the previous "check with assumptions" command.
smtUnsatAssumptionsResult :: SMTReadWriter h => f h -> WriterConn t h -> IO [(Bool, Text)]what4 What4.Protocol.SMTWriter Parse a list of names of assumptions that form an unsatisfiable core. The boolean indicates the polarity of the atom: true for an ordinary atom, false for a negated atom.
consumeUntilEnd :: (LogEvent -> Bool) -> (LogEvent -> IO ()) -> LogCfg -> IO ()what4 What4.Serialize.Log Consume a log channel until it receives a shutdown message (i.e. a Nothing). Only messages that satisfy the predicate will be passed to the continuation. For example, using const True will process all log messages, and using (>= Info) . leLevel will only process messsages with LogLevel equal to Info or higher, ignoring Debug level messages.
fileLogEventConsumer :: FilePath -> (LogEvent -> Bool) -> LogCfg -> IO ()what4 What4.Serialize.Log A logger that writes to a user-specified file Note that logs are opened in the w mode (i.e., overwrite). Callers should preserve old log files if they really want.
stdErrLogEventConsumer :: (LogEvent -> Bool) -> LogCfg -> IO ()what4 What4.Serialize.Log A log event consumer that prints formatted log events to stderr.
tmpFileLogEventConsumer :: (LogEvent -> Bool) -> LogCfg -> IO ()what4 What4.Serialize.Log A log event consumer that writes formatted log events to a tmp file.
assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()what4 What4.Solver.Yices Write assume formula predicates for asserting predicate holds.