Hoogle Search
Within LTS Haskell 24.46 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
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.
isUltSumCommonEquiv :: forall (w :: Nat) . BVDomain w -> BVDomain w -> BVDomain w -> Boolwhat4 What4.Utils.BVDomain Check if (bvult (bvadd a c) (bvadd b c)) is equivalent to (bvult a b)
isUltSumCommonEquiv :: forall (w :: Nat) . Domain w -> Domain w -> Domain w -> Boolwhat4 What4.Utils.BVDomain.Arith Check if (bvult (bvadd a c) (bvadd b c)) is equivalent to (bvult a b). This is true if and only if for all natural values i_a, i_b, i_c in a, b, c, either both i_a + i_c and i_b + i_c are less than 2^w, or both are not. We prove this by contradiction. If i_a = i_b, then the property is trivial. Assume that i_a < i_b. Then i_a + i_c < i_b + i_c. If exactly one of the additions is less than 2^w, it must be the case that i_a + i_c < 2^w and 0 <= i_b + i_c - 2^w < 2^w. Since i_b < 2^w, it follows that i_b + i_c < 2^w + i_c, that i_b + i_c - 2^w < i_c, and that i_b + i_c - 2^w < i_a + i_c. Thus, for these values of i_a, i_b, i_c, (bvult a b) is true, but (bvult (bvadd a c) (bvadd b c)) is false, which is a contradiction. We check this property by case analysis on whether c is a single non-wrapping interval, or it wraps around and is a union of two non-wrapping intervals. For a non-wrapping (sub)interval c' of c, there are four possible cases: 1. a and b contain a single value. 2. (bvadd a c') and (bvadd b c') do not wrap around for any values in a, b, c'. 3. (bvadd a c') and (bvadd b c') wrap around for all values in a, b, c'. This is used to simplify bvult.