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

Copyright(c) Galois Inc 2016-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellNone
LanguageHaskell2010

What4.Expr.Simplify

Description

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

Synopsis

Documentation

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

Simplify a Boolean expression by distributing over ite.

count_subterms :: 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.