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

Copyright | (c) Galois Inc 2015-2022
License | BSD3
Maintainer | rdockins@galois.com
Safe Haskell | None
Language | Haskell2010

What4.Expr.Allocator

Description

Synopsis

- data ExprAllocator t = ExprAllocator {
  - appExpr :: forall (tp :: BaseType). ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
  - nonceExpr :: forall (tp :: BaseType). ProgramLoc -> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
  }
- newStorage :: NonceGenerator IO t -> IO (ExprAllocator t)
- newCachedStorage :: NonceGenerator IO t -> Int -> IO (ExprAllocator t)
- cacheStartSizeOption :: ConfigOption BaseIntegerType
- cacheStartSizeDesc :: ConfigDesc
- cacheTerms :: ConfigOption BaseBoolType
- cacheOptDesc :: NonceGenerator IO t -> IORef (ExprAllocator t) -> OptionSetting BaseIntegerType -> ConfigDesc

# 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

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

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

Create a new storage that does not do hash consing.

newCachedStorage :: 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"

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