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

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.