GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-10-06 00:22:49 +03:00
Code Issues Projects Releases Wiki Activity

resolveSymBV: Make note of possible future work

Browse Source 
See also #188
This commit is contained in:
Ryan Scott 2022-02-17 12:05:13 -05:00 committed by Ryan Scott
parent 76b5e0a2b4
commit ea717ac94a
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
what4/src/What4/Utils/ResolveBounds/BV.hs
View File

@ -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"