add support for "constrain"

Data/SBV.hs

@@ -135,6 +135,8 @@ module Data.SBV (
   , Boolean(..)
   -- *** Generalizations of boolean operations
   , bAnd, bOr, bAny, bAll
+  -- ** Adding constraints
+  , constrain
   -- ** Pretty-printing and reading numbers in Hex & Binary
   , PrettyNum(..), readBin
   -- * Uninterpreted constants and functions

Data/SBV/BitVectors/Data.hs

@@ -22,7 +22,7 @@ module Data.SBV.BitVectors.Data
  ( SBool, SWord8, SWord16, SWord32, SWord64
  , SInt8, SInt16, SInt32, SInt64, SInteger
  , SymWord(..)
- , CW(..), cwSameType, cwIsBit, cwToBool
+ , CW(..), cwSameType, cwIsBit, cwToBool, constrain
  , mkConstCW ,liftCW2, mapCW, mapCW2
  , SW(..), trueSW, falseSW, trueCW, falseCW
  , SBV(..), NodeId(..), mkSymSBV
@@ -267,16 +267,17 @@ data Result = Result Bool                                         -- contains un
                      [(String, SBVType)]                          -- uninterpreted constants
                      [(String, [String])]                         -- axioms
                      Pgm                                          -- assignments
+                     [SW]                                         -- additional constraints (boolean)
                      [SW]                                         -- outputs
 
 getQCInfo :: Result -> [(String, CW)]
-getQCInfo (Result _ qc _ _ _ _ _ _ _ _ _) = qc
+getQCInfo (Result _ qc _ _ _ _ _ _ _ _ _ _) = qc
 
 instance Show Result where
-  show (Result _ _ _ _ cs _ _ [] [] _ [r])
+  show (Result _ _ _ _ cs _ _ [] [] _ [] [r])
     | Just c <- r `lookup` cs
     = show c
-  show (Result _ _ cgs is cs ts as uis axs xs os)  = intercalate "\n" $
+  show (Result _ _ cgs is cs ts as uis axs xs cstrs os)  = intercalate "\n" $
                    ["INPUTS"]
                 ++ map shn is
                 ++ ["CONSTANTS"]
@@ -293,6 +294,8 @@ instance Show Result where
                 ++ map shax axs
                 ++ ["DEFINE"]
                 ++ map (\(s, e) -> "  " ++ shs s ++ " = " ++ show e) (F.toList xs)
+                ++ ["CONSTRAINTS"]
+                ++ map (("  " ++) . show) cstrs
                 ++ ["OUTPUTS"]
                 ++ map (("  " ++) . show) os
     where shs sw = show sw ++ " :: " ++ showType sw
@@ -361,6 +364,7 @@ data State  = State { runMode       :: SBVRunMode
                     , rctr          :: IORef Int
                     , rInfPrec      :: IORef Bool
                     , rinps         :: IORef [(Quantifier, NamedSymVar)]
+                    , rConstraints  :: IORef [SW]
                     , routs         :: IORef [SW]
                     , rtblMap       :: IORef TableMap
                     , spgm          :: IORef Pgm
@@ -596,29 +600,31 @@ runSymbolic' currentRunMode (Symbolic c) = do
    swCache <- newIORef IMap.empty
    aiCache <- newIORef IMap.empty
    infPrec <- newIORef False
-   let st = State { runMode   = currentRunMode
-                  , rCInfo    = cInfo
-                  , rctr      = ctr
-                  , rInfPrec  = infPrec
-                  , rinps     = inps
-                  , routs     = outs
-                  , rtblMap   = tables
-                  , spgm      = pgm
-                  , rconstMap = cmap
-                  , rArrayMap = arrays
-                  , rexprMap  = emap
-                  , rUIMap    = uis
-                  , rCgMap    = cgs
-                  , raxioms   = axioms
-                  , rSWCache  = swCache
-                  , rAICache  = aiCache
+   cstrs   <- newIORef []
+   let st = State { runMode      = currentRunMode
+                  , rCInfo       = cInfo
+                  , rctr         = ctr
+                  , rInfPrec     = infPrec
+                  , rinps        = inps
+                  , routs        = outs
+                  , rtblMap      = tables
+                  , spgm         = pgm
+                  , rconstMap    = cmap
+                  , rArrayMap    = arrays
+                  , rexprMap     = emap
+                  , rUIMap       = uis
+                  , rCgMap       = cgs
+                  , raxioms      = axioms
+                  , rSWCache     = swCache
+                  , rAICache     = aiCache
+                  , rConstraints = cstrs
                   }
    _ <- newConst st (mkConstCW (False, Size (Just 1)) (0::Integer)) -- s(-2) == falseSW
    _ <- newConst st (mkConstCW (False, Size (Just 1)) (1::Integer)) -- s(-1) == trueSW
    r <- runReaderT c st
    rpgm  <- readIORef pgm
-   inpsR <- readIORef inps
-   outsR <- readIORef outs
+   inpsO <- reverse `fmap` readIORef inps
+   outsO <- reverse `fmap` readIORef outs
    let swap (a, b) = (b, a)
        cmp  (a, _) (b, _) = a `compare` b
    cnsts <- (sortBy cmp . map swap . Map.toList) `fmap` readIORef (rconstMap st)
@@ -629,7 +635,8 @@ runSymbolic' currentRunMode (Symbolic c) = do
    hasInfPrec <- readIORef infPrec
    cgMap <- Map.toList `fmap` readIORef cgs
    traceVals <- reverse `fmap` readIORef cInfo
-   return $ (r, Result hasInfPrec traceVals cgMap (reverse inpsR) cnsts tbls arrs unint axs rpgm (reverse outsR))
+   extraCstrs   <- reverse `fmap` readIORef cstrs
+   return $ (r, Result hasInfPrec traceVals cgMap inpsO cnsts tbls arrs unint axs rpgm extraCstrs outsO)
 
 -------------------------------------------------------------------------------
 -- * Symbolic Words
@@ -803,6 +810,20 @@ instance (HasSignAndSize a, HasSignAndSize b) => Show (SFunArray a b) where
 mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b
 mkSFunArray = SFunArray
 
+---------------------------------------------------------------------------------
+-- | Adding arbitrary constraints. A constraint adds a conjunction to the
+-- final formula that must always be satisfied. NB. 'constrain' is merely a
+-- convenient way of adding extra conjuncts to the final result, allowing one
+-- to express constraints much more easily earlier. A good use case is
+-- attaching a constraint to a 'forall' or 'exists' variable at the time
+-- of its creation, instead of waiting for the final returned formula.
+---------------------------------------------------------------------------------
+constrain :: SBool -> Symbolic ()
+constrain b = do
+        st <- ask
+        liftIO $ do v <- sbvToSW st b
+                    modifyIORef (rConstraints st) (v:)
+
 ---------------------------------------------------------------------------------
 -- * Cached values
 ---------------------------------------------------------------------------------
@@ -860,8 +881,8 @@ instance NFData CW where
   rnf (CW x y z) = x `seq` y `seq` z `seq` ()
 
 instance NFData Result where
-  rnf (Result isInf qcInfo cgs inps consts tbls arrs uis axs pgm outs)
-        = rnf isInf `seq` rnf qcInfo `seq` rnf cgs `seq` rnf inps `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf uis `seq` rnf axs `seq` rnf pgm `seq` rnf outs
+  rnf (Result isInf qcInfo cgs inps consts tbls arrs uis axs pgm cstr outs)
+        = rnf isInf `seq` rnf qcInfo `seq` rnf cgs `seq` rnf inps `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf uis `seq` rnf axs `seq` rnf pgm `seq` rnf cstr `seq` rnf outs
 
 instance NFData Size
 instance NFData ArrayContext

Data/SBV/BitVectors/GenTest.hs

@@ -21,6 +21,8 @@ import Data.SBV.BitVectors.Data
 -- function 'output' call to indicate what fields should be in the test result.
 genTest :: Int -> Symbolic () -> IO [([CW], [CW])]
 genTest n m = sequence [tc | _ <- [1 .. n]]
-  where tc = do (_, Result _ tvals _ _ cs _ _ _ _ _ os) <- runSymbolic' Concrete m
-                let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs)
-                return (map snd tvals, map cval os)
+  where tc = do (_, Result _ tvals _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' Concrete m
+                case cstrs of
+                  [] -> let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs)
+                        in return (map snd tvals, map cval os)
+                  _  -> error "Not yet supported: Quickcheck in the presence of explicit constraints."

Data/SBV/Compilers/C.hs

@@ -370,8 +370,9 @@ genDriver mbISize randVals fn inps outs mbRet = [pre, header, body, post]
 
 -- | Generate the C program
 genCProg :: Bool -> Maybe Int -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc]
-genCProg rtc mbISize fn proto (Result hasInfPrec _ cgs ins preConsts tbls arrs _ _ asgns _) inVars outVars mbRet extDecls
+genCProg rtc mbISize fn proto (Result hasInfPrec _ cgs ins preConsts tbls arrs _ _ asgns cstrs _) inVars outVars mbRet extDecls
   | isNothing mbISize && hasInfPrec = dieUnbounded
+  | not (null cstrs)                = tbd "Explicit constraints"
   | not (null arrs)                 = tbd "User specified arrays"
   | needsExistentials (map fst ins) = error "SBV->C: Cannot compile functions with existentially quantified variables."
   | True                            = [pre, header, post]

Data/SBV/Examples/BitPrecise/PrefixSum.hs

@@ -248,6 +248,7 @@ prefixSum i
 --   s16 :: SWord8 = s6 + s7
 --   s17 :: SWord8 = s13 + s16
 --   s18 :: SWord8 = s11 + s17
+-- CONSTRAINTS
 -- OUTPUTS
 --   s0
 --   s8
@@ -291,6 +292,7 @@ ladnerFischerTrace n = gen >>= print
 --   s12 :: SWord8 = s5 + s11
 --   s13 :: SWord8 = s6 + s12
 --   s14 :: SWord8 = s7 + s13
+-- CONSTRAINTS
 -- OUTPUTS
 --   s0
 --   s8

Data/SBV/Examples/Puzzles/Coins.hs

@@ -0,0 +1,100 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Examples.Puzzles.Coins
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Solves the following puzzle:
+--
+-- @
+-- You and a friend pass by a standard coin operated vending machine and you decide to get a candy bar.
+-- The price is US $0.95, but after checking your pockets you only have a dollar (US $1) and the machine
+-- only takes coins. You turn to your friend and have this conversation:
+--   you: Hey, do you have change for a dollar?
+--   friend: Let's see. I have 6 US coins but, although they add up to a US $1.15, I can't break a dollar.
+--   you: Huh? Can you make change for half a dollar?
+--   friend: No.
+--   you: How about a quarter?
+--   friend: Nope, and before you ask I cant make change for a dime or nickel either.
+--   you: Really? and these six coins are all US government coins currently in production? 
+--   friend: Yes.
+--   you: Well can you just put your coins into the vending machine and buy me a candy bar, and I'll pay you back?
+--   friend: Sorry, I would like to but I cant with the coins I have.
+-- What coins are your friend holding?
+-- @
+--
+-- To be fair, the problem has no solution /mathematically/. But there is a solution when one takes into account that
+-- vending machines typically do not take the 50 cent coins!
+--
+-----------------------------------------------------------------------------
+
+module Data.SBV.Examples.Puzzles.Coins where
+
+import Data.SBV
+
+-- | We will represent coins with 16-bit words (more than enough precision for coins).
+type Coin = SWord16
+
+-- | Create a coin. The argument Int argument just used for naming the coin. Note that
+-- we constrain the value to be one of the valid U.S. coin values as we create it.
+mkCoin :: Int -> Symbolic Coin
+mkCoin i = do c <- exists $ 'c' : show i
+              constrain $ bAny (.== c) [1, 5, 10, 25, 50, 100]
+              return c
+
+-- | Return all combinations of a sequence of values.
+combinations :: [a] -> [[a]]
+combinations coins = concat [combs i coins | i <- [1 .. length coins]]
+  where combs 0 _      = [[]]
+        combs _ []     = []
+        combs k (x:xs) = map (x:) (combs (k-1) xs) ++ combs k xs
+
+-- | Constraint 1: Cannot make change for a dollar.
+c1 :: [Coin] -> SBool
+c1 xs = sum xs ./= 100
+
+-- | Constraint 2: Cannot make change for half a dollar.
+c2 :: [Coin] -> SBool
+c2 xs = sum xs ./= 50
+
+-- | Constraint 3: Cannot make change for a quarter.
+c3 :: [Coin] -> SBool
+c3 xs = sum xs ./= 25
+
+-- | Constraint 4: Cannot make change for a dime.
+c4 :: [Coin] -> SBool
+c4 xs = sum xs ./= 10
+
+-- | Constraint 5: Cannot make change for a nickel
+c5 :: [Coin] -> SBool
+c5 xs = sum xs ./= 5
+
+-- | Constraint 6: Cannot buy the candy either. Here's where we need to have the extra knowledge
+-- that the vending machines do not take 50 cent coins.
+c6 :: [Coin] -> SBool
+c6 xs = sum (map val xs) ./= 95
+   where val x = ite (x .== 50) 0 x
+
+-- | Solve the puzzle. We have:
+--
+-- >>> puzzle
+-- Satisfiable. Model:
+--   c1 = 50 :: SWord16
+--   c2 = 10 :: SWord16
+--   c3 = 10 :: SWord16
+--   c4 = 10 :: SWord16
+--   c5 = 10 :: SWord16
+--   c6 = 25 :: SWord16
+--
+-- i.e., your friend has 4 dimes, a quarter, and a half dollar.
+puzzle :: IO SatResult
+puzzle = sat $ do
+        cs <- mapM mkCoin [1..6]
+        -- Assert each of the constraints for all combinations that has
+        -- at least two coins (to make change)
+        mapM_ constrain [c s | s <- combinations cs, length s >= 2, c <- [c1, c2, c3, c4, c5, c6]]
+        -- assert that the sum must be 115 cents.
+        return $ sum cs .== 115

Data/SBV/Provers/Prover.hs

@@ -345,7 +345,7 @@ simulate converter config isSat comments predicate = do
         msg $ "Generated symbolic trace:\n" ++ show res
         msg "Translating to SMT-Lib.."
         case res of
-          Result hasInfPrec _qcInfo _codeSegs is consts tbls arrs uis axs pgm [o@(SW (False, Size (Just 1)) _)] ->
+          Result hasInfPrec _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW (False, Size (Just 1)) _)] ->
              timeIf isTiming "translation" $ do let uiMap     = catMaybes (map arrayUIKind arrs) ++ map unintFnUIKind uis
                                                     skolemMap = skolemize (if isSat then is else map flipQ is)
                                                         where flipQ (ALL, x) = (EX, x)
@@ -355,8 +355,8 @@ simulate converter config isSat comments predicate = do
                                                                 where go []                   (_,  sofar) = reverse sofar
                                                                       go ((ALL, (v, _)):rest) (us, sofar) = go rest (v:us, Left v : sofar)
                                                                       go ((EX,  (v, _)):rest) (us, sofar) = go rest (us,   Right (v, reverse us) : sofar)
-                                                return (is, uiMap, skolemMap, converter hasInfPrec isSat comments is skolemMap consts tbls arrs uis axs pgm o)
-          Result _hasInfPrec _qcInfo _codeSegs _is _consts _tbls _arrs _uis _axs _pgm os -> case length os of
+                                                return (is, uiMap, skolemMap, converter hasInfPrec isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o)
+          Result _hasInfPrec _qcInfo _codeSegs _is _consts _tbls _arrs _uis _axs _pgm _cstrs os -> case length os of
                         0  -> error $ "Impossible happened, unexpected non-outputting result\n" ++ show res
                         1  -> error $ "Impossible happened, non-boolean output in " ++ show os
                                     ++ "\nDetected while generating the trace:\n" ++ show res

Data/SBV/SMT/SMTLib.hs

@@ -28,15 +28,16 @@ type SMTLibConverter =  Bool                                        -- ^ has inf
                      -> [(String, SBVType)]                         -- ^ uninterpreted functions/constants
                      -> [(String, [String])]                        -- ^ user given axioms
                      -> Pgm                                         -- ^ assignments
+                     -> [SW]                                        -- ^ extra constraints
                      -> SW                                          -- ^ output variable
                      -> SMTLibPgm
 
 toSMTLib1, toSMTLib2 :: SMTLibConverter
 (toSMTLib1, toSMTLib2) = (cvt SMTLib1, cvt SMTLib2)
-  where cvt v hasInfPrec isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq out = SMTLibPgm v (aliasTable, pre, post)
+  where cvt v hasInfPrec isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out = SMTLibPgm v (aliasTable, pre, post)
          where aliasTable  = map (\(_, (x, y)) -> (y, x)) qinps
                converter   = if v == SMTLib1 then SMT1.cvt else SMT2.cvt
-               (pre, post) = converter hasInfPrec isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq out
+               (pre, post) = converter hasInfPrec isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out
 
 addNonEqConstraints :: [(Quantifier, NamedSymVar)] -> [[(String, CW)]] -> SMTLibPgm -> Maybe String
 addNonEqConstraints _qinps cs p@(SMTLibPgm SMTLib1 _) = SMT1.addNonEqConstraints cs p

RELEASENOTES

@@ -20,6 +20,10 @@ Version 0.9.24, Not yet released
      commands are all interchangeable with obvious meanings.
    * Add support for concrete test case generation, see the genTest function.
    * Improve optimize routines and add support for iterative optimization.
+   * Add function "constrain", simplifying conjunctive constraints, especially
+     useful for adding constraints at variable generation time via forall/exists.
+  Examples
+   * Add Data/SBV/Examples/Puzzles/Coins.hs. (Shows the usage of "constrain".)
   Dependencies
    * Bump up random package dependency to 1.0.1.1 (from 1.0.0.2)
   Internal

SBVUnitTest/GoldFiles/auf-1.gold

@@ -27,5 +27,6 @@ DEFINE
   s15 :: SWord64 = uninterpreted_f s14
   s16 :: SBool = s11 == s15
   s17 :: SBool = s6 | s16
+CONSTRAINTS
 OUTPUTS
   s17

SBVUnitTest/GoldFiles/basic-2_1.gold

@@ -13,5 +13,6 @@ DEFINE
   s2 :: SWord8 = s0 + s1
   s3 :: SWord8 = s1 - s0
   s4 :: SWord8 = s2 * s3
+CONSTRAINTS
 OUTPUTS
   s4

SBVUnitTest/GoldFiles/basic-2_2.gold

@@ -12,5 +12,6 @@ AXIOMS
 DEFINE
   s2 :: SWord8 = s0 * s0
   s3 :: SWord8 = s1 - s2
+CONSTRAINTS
 OUTPUTS
   s3

SBVUnitTest/GoldFiles/basic-2_3.gold

@@ -12,5 +12,6 @@ AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s1
   s3 :: SWord8 = s2 * s2
+CONSTRAINTS
 OUTPUTS
   s3

SBVUnitTest/GoldFiles/basic-2_4.gold

@@ -12,5 +12,6 @@ AXIOMS
 DEFINE
   s2 :: SWord8 = s0 + s1
   s3 :: SWord8 = s2 * s2
+CONSTRAINTS
 OUTPUTS
   s3

SBVUnitTest/GoldFiles/basic-3_1.gold

@@ -13,5 +13,6 @@ DEFINE
   s2 :: SWord8 = s0 + s1
   s3 :: SWord8 = s0 - s1
   s4 :: SWord8 = s2 * s3
+CONSTRAINTS
 OUTPUTS
   s4

SBVUnitTest/GoldFiles/basic-3_2.gold

@@ -13,5 +13,6 @@ DEFINE
   s2 :: SWord8 = s0 * s0
   s3 :: SWord8 = s1 * s1
   s4 :: SWord8 = s2 - s3
+CONSTRAINTS
 OUTPUTS
   s4