Copyright | (c) Galois Inc 2016-2020 |
---|---|
License | BSD3 |
Maintainer | Joe Hendrix <jhendrix@galois.com> |
Safe Haskell | None |
Language | Haskell2010 |
What4.Expr.Simplify
Description
This module provides a minimalistic interface for manipulating Boolean formulas and execution contexts in the symbolic simulator.
Synopsis
- simplify :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> BoolExpr t -> IO (BoolExpr t)
- count_subterms :: forall t (tp :: BaseType). Expr t tp -> Map Word64 Int
Documentation
simplify :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> BoolExpr t -> IO (BoolExpr t) Source #
Simplify a Boolean expression by distributing over ite.
count_subterms :: forall t (tp :: BaseType). Expr t tp -> Map Word64 Int Source #
Return a map from nonce indices to the number of times an elt with that nonce appears in the subterm.