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.

Return a map from nonce indices to the number of times an elt with that nonce appears in the subterm.