evaluate package:what4

evaluate :: Monad m => (p -> m Bool) -> UnaryBV p n -> m Integer

Evaluate a unary bitvector as an integer given an evaluation function.

sym_evaluate :: (Applicative m, Monad m) => (Integer -> m r) -> (p -> r -> r -> m r) -> UnaryBV p n -> m r

Evaluate a unary bitvector given an evaluation function. This function is used to convert a unary bitvector into some other representation such as a binary bitvector or vector of bits. It is polymorphic over the result type r, and requires functions for manipulating values of type r to construct it.