what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

Safe Haskell | None
Language | Haskell2010

What4.Serialize.Normalize

Description

Normalization and equivalence checking for expressions

Synopsis

- normSymFn :: forall sym (st :: Type -> Type) fs t (args :: Ctx BaseType) (ret :: BaseType). sym ~ ExprBuilder t st fs => sym -> ExprSymFn t args ret -> Assignment (Expr t) args -> IO (Expr t ret)
- normExpr :: forall sym (st :: Type -> Type) fs t (tp :: BaseType). sym ~ ExprBuilder t st fs => sym -> Expr t tp -> IO (Expr t tp)
- testEquivSymFn :: forall sym (st :: Type -> Type) fs t (args :: Ctx BaseType) (ret :: BaseType) (args' :: Ctx BaseType) (ret' :: BaseType). sym ~ ExprBuilder t st fs => sym -> SymFn sym args ret -> SymFn sym args' ret' -> IO ExprEquivResult
- testEquivExpr :: forall sym (st :: Type -> Type) fs t (tp :: BaseType) (tp' :: BaseType). sym ~ ExprBuilder t st fs => sym -> Expr t tp -> Expr t tp' -> IO ExprEquivResult
- data ExprEquivResult
  - = ExprEquivalent
  - | ExprNormEquivalent
  - | ExprUnequal

# Documentation

normSymFn :: forall sym (st :: Type -> Type) fs t (args :: Ctx BaseType) (ret :: BaseType). sym ~ ExprBuilder t st fs => sym -> ExprSymFn t args ret -> Assignment (Expr t) args -> IO (Expr t ret) Source #

Apply some normalizations to make function call arguments more readable. Examples include:

- Avoid wrapping single literals in a `SemiRingLiteral` and just represent them as a bare integer literals
- Attempt to reduce function calls with constant arguments where possible

normExpr :: forall sym (st :: Type -> Type) fs t (tp :: BaseType). sym ~ ExprBuilder t st fs => sym -> Expr t tp -> IO (Expr t tp) Source #

testEquivSymFn :: forall sym (st :: Type -> Type) fs t (args :: Ctx BaseType) (ret :: BaseType) (args' :: Ctx BaseType) (ret' :: BaseType). sym ~ ExprBuilder t st fs => sym -> SymFn sym args ret -> SymFn sym args' ret' -> IO ExprEquivResult Source #

testEquivExpr :: forall sym (st :: Type -> Type) fs t (tp :: BaseType) (tp' :: BaseType). sym ~ ExprBuilder t st fs => sym -> Expr t tp -> Expr t tp' -> IO ExprEquivResult Source #

data ExprEquivResult Source #

Constructors

ExprEquivalent |
ExprNormEquivalent |
ExprUnequal |