sbv
sbv copied to clipboard
LeventErkok
Query Mode Optimisation
Following on from the discussion in #358, this issue aims to discuss an interface for performing optimisation in query mode in sbv.
This'll require a bit of experimenting to find the API. My first thought is that the functions of minimize/maximize should move to the SolverContext class. The types will most likely look something like:
minimize :: (SolverContext m, Metric a) => String -> a -> m (Extremum a)
where Extremum is essentially a newtype wrapper:
newtype Extremum a = Extremum a
We would also need a function:
getOptimalValue :: Extremum a -> Query (Extended a)
where
data Extended a = Infinite | Epsilon | Interval a a | Fixed a | AddExtended a a | MulExtended a a
Note that Extended is very similar to the existing ExtCW; so we would also get rid of the current ExtCW type and simply replace it with Extended CW for internal purposes.
Then there's the entire issue of how one goes about Lexicographic/Pareto/Independent value extractions, and soft-assumptions, and all that. But, I'd recommend starting simple: Please go ahead and fork SBV, and see if we can get the above implemented in Query mode. (You can call it minQ/maxQ so it can live together with the current infrastructure. We can merge the two down the road.)
I'm excited to see what you'll come up with!
I'm currently in a bit of a crunch with the project for which all my questions were intended, but once that ends I'll gladly give this a shot!
I'm going to give this more thought over the coming days, however, and I'll jot down any ideas I have here for future reference!
I'm sorry to have left this so long without a comment, but it's starting to seem like I will not be able to dedicate nearly enough time to this to do a good job any time soon. I'm very sorry to flake on you like this. :(
No worries. I firmly believe in "need based development." Looks like you do not need this feature, so it's best to focus on other parts instead. Cheers.
Closing this; unless there's some real customer request (and help!); I doubt this'll ever happen.