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.

  1. bvSum :: forall t (st :: Type -> Type) fs (flv :: BVFlavor) (w :: Nat) . ExprBuilder t st fs -> WeightedSum (Expr t) (SemiRingBV flv w) -> IO (BVExpr t w)

    what4 What4.Expr.Builder

    No documentation available.

  2. intSum :: forall t (st :: Type -> Type) fs . ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingInteger -> IO (IntegerExpr t)

    what4 What4.Expr.Builder

    Evaluate a weighted sum of integer values.

  3. realSum :: forall t (st :: Type -> Type) fs . ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingReal -> IO (RealExpr t)

    what4 What4.Expr.Builder

    Evaluate a weighted sum of real values.

  4. module What4.Expr.WeightedSum

    Declares a weighted sum type used for representing sums over variables and an offset in one of the supported semirings. This module also implements a representation of semiring products.

  5. data WeightedSum (f :: BaseType -> Type) (sr :: SemiRing)

    what4 What4.Expr.WeightedSum

    A weighted sum of semiring values. Mathematically, this represents an affine operation on the underlying expressions.

  6. reduceIntSumMod :: forall (f :: BaseType -> Type) . Tm f => WeightedSum f SemiRingInteger -> Integer -> WeightedSum f SemiRingInteger

    what4 What4.Expr.WeightedSum

    Reduce a weighted sum of integers modulo a concrete integer. This reduces each of the coefficients modulo the given integer, removing any that are congruent to 0; the offset value is also reduced.

  7. transformSum :: forall m g (sr' :: SemiRing) (sr :: SemiRing) f . (Applicative m, Tm g) => SemiRingRepr sr' -> (Coefficient sr -> m (Coefficient sr')) -> (f (SemiRingBase sr) -> m (g (SemiRingBase sr'))) -> WeightedSum f sr -> m (WeightedSum g sr')

    what4 What4.Expr.WeightedSum

    Apply update functions to the terms and coefficients of a weighted sum.

  8. useUnsatAssumptions :: ProblemFeatures

    what4 What4.ProblemFeatures

    Indicates if the solver is able and configured to compute UNSAT assumptions.

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

    what4 What4.Protocol.Online

    No documentation available.

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

    what4 What4.Protocol.Online

    No documentation available.

Page 184 of many | Previous | Next