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 b6362c3 commit 452ddf4
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 @@ -70,6 +70,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.

-- | Use an 'WPO.OnlineSolver' to attempt to resolve a 'WI.SymBV' as concrete.
-- If it cannot, return the lower and upper bounds. This is primarly intended
-- for compound expressions whose bounds cannot trivially be determined by
Expand Down

0 comments on commit 452ddf4

Please sign in to comment.