What4.Expr.Simplify

This module provides a minimalistic interface for manipulating Boolean formulas and execution contexts in the symbolic simulator.

Documentation

simplify :: ExprBuilder t st fs -> BoolExpr t -> IO (BoolExpr t)

Simplify a Boolean expression by distributing over ite.

count_subterms :: Expr t tp -> Map Word64 Int

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