search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
239 stars 33 forks source link

Let 'optimize' return variable values #710

Closed amigalemming closed 1 month ago

amigalemming commented 1 month ago

This is a follow-up to https://github.com/LeventErkok/sbv/issues/707 . Currently I have to retrieve optimization results from dynamically typed SMTResult. I propose an alternative to optimize:

optimizeAndQuery :: OptimizeStyle result -> Symbolic (SBV tuple) -> IO (result, tuple)

SBV tuple is the result of combining variables of type SBool, SInteger etc. via Applicative. It has two advantage over SMTResult: 1. SBV knows that the variable exists in modelAssocs. 2. SBV knows its type, namely Bool. Hm, the type IO (result, tuple) could be more precise, such that it is either an optimization error or a result tuple.

LeventErkok commented 1 month ago

How will this work with extended values?

Prelude Data.SBV> optimize Lexicographic $ do x  <- sInteger "x"; maximize "x" x
Optimal in an extension field:
  x_0 = oo :: Integer

One reason I left this a bit under-developed was precisely because optimization might result in infinities or epsilons for unbounded domains. (Integers and Reals.)

Is this an issue here?

LeventErkok commented 1 month ago

Guess you lost interest in this, and I don't immediately see how to make this fit with the current schema due to the existence of infinities and epsilons. Feel free to reopen the ticket if you have further issues/ideas.