What4.Expr.Allocator

Documentation

data ExprAllocator t

ExprAllocator provides an interface for creating expressions from an applications. Parameter t is a phantom type brand used to track nonces.

Constructors

ExprAllocator

Fields

• appExpr :: forall tp. ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
• nonceExpr :: forall tp. ProgramLoc -> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)

newStorage :: NonceGenerator IO t -> IO (ExprAllocator t)

Create a new storage that does not do hash consing.

newCachedStorage :: forall t. NonceGenerator IO t -> Int -> IO (ExprAllocator t)

Create a storage that does hash consing.

cacheStartSizeOption :: ConfigOption BaseIntegerType

Starting size for element cache when caching is enabled. The default value is 100000 elements.

This option is named "backend.cache_start_size"

cacheStartSizeDesc :: ConfigDesc

The configuration option for setting the size of the initial hash set used by simple builder (measured in number of elements).

cacheTerms :: ConfigOption BaseBoolType

Indicates if we should cache terms. When enabled, hash-consing is used to find and deduplicate common subexpressions. Toggling this option from disabled to enabled will allocate a new hash table; toggling it from enabled to disabled will discard the current hash table. The default value for this option is False.

This option is named "use_cache"

cacheOptDesc :: NonceGenerator IO t -> IORef (ExprAllocator t) -> OptionSetting BaseIntegerType -> ConfigDesc