what4-1.6.2: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2015-2022
LicenseBSD3
Maintainerrdockins@galois.com
Safe HaskellSafe-Inferred
LanguageHaskell2010

What4.Expr.Allocator

Description

 
Synopsis

Documentation

data ExprAllocator t Source #

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

Constructors

ExprAllocator 

Fields

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

Create a new storage that does not do hash consing.

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

Create a storage that does hash consing.

cacheStartSizeOption :: ConfigOption BaseIntegerType Source #

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 Source #

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

cacheTerms :: ConfigOption BaseBoolType Source #

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"