Optimization: Carefully handle signed bv goals. #333

WIP. Still need test cases.

Data/SBV/Control/Query.hs

@@ -317,13 +317,16 @@ getObjectiveValues = do let cmd = "(get-objectives)"
         getObjValue :: (forall a. Maybe [String] -> Query a) -> [NamedSymVar] -> SExpr -> Query (Maybe (String, GeneralizedCW))
         getObjValue bailOut inputs expr =
                 case expr of
-                  EApp [_]          -> return Nothing  -- Happens when a soft-assertion has no associated group.
-                  EApp [ECon nm, v] -> case listToMaybe [p | p@(sw, _) <- inputs, show sw == nm] of
-                                         Nothing               -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names
-                                         Just (sw, actualName) -> grab sw v >>= \val -> return $ Just (actualName, val)
-                  _                 -> dontUnderstand (show expr)
+                  EApp [_]                                       -> return Nothing            -- Happens when a soft-assertion has no associated group.
+                  EApp [ECon nm, v]                              -> locate nm v               -- Regular case
+                  EApp [EApp [ECon "bvadd", ECon nm, ENum _], v] -> locate nm v               -- Happens when we "adjust" a signed-bounded objective
+                  _                                              -> dontUnderstand (show expr)
 
-          where dontUnderstand s = bailOut $ Just [ "Unable to understand solver output."
+          where locate nm v = case listToMaybe [p | p@(sw, _) <- inputs, show sw == nm] of
+                                Nothing               -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names
+                                Just (sw, actualName) -> grab sw v >>= \val -> return $ Just (actualName, val)
+
+                dontUnderstand s = bailOut $ Just [ "Unable to understand solver output."
                                                   , "While trying to process: " ++ s
                                                   ]
 

Data/SBV/Provers/Prover.hs

@@ -48,6 +48,7 @@ import Data.SBV.Core.Data
 import Data.SBV.Core.Symbolic
 import Data.SBV.SMT.SMT
 import Data.SBV.Utils.TDiff
+import Data.SBV.Utils.PrettyNum
 
 import qualified Data.SBV.Control       as Control
 import qualified Data.SBV.Control.Query as Control
@@ -262,9 +263,9 @@ class Provable a where
 
                    let optimizerDirectives = concatMap minmax objectives ++ priority style
                          where mkEq (x, y) = "(assert (= " ++ show x ++ " " ++ show y ++ "))"
-                               minmax (Minimize   _  xy@(_, v))     = [mkEq xy, "(minimize "    ++ show v ++ ")"]
-                               minmax (Maximize   _  xy@(_, v))     = [mkEq xy, "(maximize "    ++ show v ++ ")"]
-                               minmax (AssertSoft nm xy@(_, v) mbp) = [mkEq xy, "(assert-soft " ++ show v ++ penalize mbp ++ ")"]
+                               minmax (Minimize   _  xy@(_, v))     = [mkEq xy, "(minimize "    ++ signAdjust v (show v) ++ ")"]
+                               minmax (Maximize   _  xy@(_, v))     = [mkEq xy, "(maximize "    ++ signAdjust v (show v) ++ ")"]
+                               minmax (AssertSoft nm xy@(_, v) mbp) = [mkEq xy, "(assert-soft " ++ signAdjust v (show v) ++ penalize mbp ++ ")"]
                                  where penalize DefaultPenalty    = ""
                                        penalize (Penalty w mbGrp)
                                           | w <= 0         = error $ unlines [ "SBV.AssertSoft: Goal " ++ show nm ++ " is assigned a non-positive penalty: " ++ shw
@@ -279,6 +280,21 @@ class Provable a where
                                priority Independent   = ["(set-option :opt.priority box)"]
                                priority (Pareto _)    = ["(set-option :opt.priority pareto)"]
 
+                               -- if the goal is a signed-BV, then we need to add 2^{n-1} to the maximal value
+                               -- is properly placed in the correct range. See http://github.com/Z3Prover/z3/issues/1339 for
+                               -- details on why we have to do this:
+                               signAdjust :: SW -> String -> String
+                               signAdjust v o = case kindOf v of
+                                                  -- NB. The order we spit out the addition here (i.e., "bvadd v constant")
+                                                  -- is important as we parse it back in precisely that form when we
+                                                  -- get the objective. Don't change it!
+                                                  KBounded True sz -> "(bvadd " ++ o ++ " " ++ adjust sz ++ ")"
+                                                  _                -> o
+                                  where adjust :: Int -> String
+                                        adjust sz = cwToSMTLib RoundNearestTiesToEven -- rounding mode doesn't matter here, just pick one
+                                                              (mkConstCW (KBounded False sz)
+                                                                         ((2::Integer)^(fromIntegral sz - (1::Integer))))
+
                    mapM_ (Control.send True) optimizerDirectives
 
                    case style of

Data/SBV/Utils/SExpr.hs

@@ -109,12 +109,13 @@ parseSExpr inp = do (sexp, extras) <- parse inpToks
         parseApp (tok:toks) sofar = do t <- pTok tok
                                        parseApp toks (t : sofar)
 
-        pTok "false"              = return $ ENum (0, Nothing)
-        pTok "true"               = return $ ENum (1, Nothing)
-        pTok ('0':'b':r)          = mkNum (Just (length r))     $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r
-        pTok ('b':'v':r)          = mkNum Nothing               $ readDec (takeWhile (/= '[') r)
-        pTok ('#':'b':r)          = mkNum (Just (length r))     $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r
-        pTok ('#':'x':r)          = mkNum (Just (4 * length r)) $ readHex r
+        pTok "false" = return $ ENum (0, Nothing)
+        pTok "true"  = return $ ENum (1, Nothing)
+
+        pTok ('0':'b':r)                                 = mkNum (Just (length r))     $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r
+        pTok ('b':'v':r) | not (null r) && all isDigit r = mkNum Nothing               $ readDec (takeWhile (/= '[') r)
+        pTok ('#':'b':r)                                 = mkNum (Just (length r))     $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r
+        pTok ('#':'x':r)                                 = mkNum (Just (4 * length r)) $ readHex r
         pTok n
           | not (null n) && isDigit (head n)
           = if '.' `elem` n then getReal n