Skip to content

Commit

Permalink
resolveSymBV: Make note of possible future work
Browse files Browse the repository at this point in the history
See also #188
  • Loading branch information
RyanGlScott committed Feb 17, 2022
1 parent 3fd133c commit efe7e09
Showing 1 changed file with 8 additions and 0 deletions.
8 changes: 8 additions & 0 deletions what4/src/What4/Utils/ResolveBounds/BV.hs
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,14 @@ data SearchStrategy
-- bounds of the search and 'BV.maxUnsigned' as the rightmost bounds of
-- the search.

-- Some possibilities for additional search strategies include:
--
-- - Using Z3's minimize/maximize commands. See
-- https://github.com/GaloisInc/what4/issues/188
--
-- - A custom, user-specified strategy that uses callback(s) to guide the
-- search at each iteration.

instance PP.Pretty SearchStrategy where
pretty ExponentialSearch = PP.pretty "exponential search"
pretty BinarySearch = PP.pretty "binary search"
Expand Down

0 comments on commit efe7e09

Please sign in to comment.