PathCond.hs

import Data.SBV
import Data.SBV.Dynamic
import Data.SBV.Control
import Data.SBV.Internals

import Control.Monad.Reader (ask)

reachableCond :: SVal -> Symbolic SVal
reachableCond cond = do
  st <- ask
  let pc = unSBV $ getPathCondition st
  return $ pc `svAnd` cond

-- A variant of ite, which returns the conditions whether we
-- can reach then/else branches explicitly
trackedIte :: SVal -> SVal -> SVal -> Symbolic (SVal, SVal, SVal)
trackedIte c t f = do tr  <- reachableCond c
                      fr  <- reachableCond (svNot c)
                      return (tr, fr, svIte c t f)

checkFeasible :: SVal -> Query Bool
checkFeasible c = do cs <- checkSatAssuming [SBV c]
                     case cs of
                       Unk   -> error "Solver said unknown"
                       Unsat -> return False
                       Sat   -> return True

example :: IO ()
example = runSMT $ do x <- sIntN 32 "x"

                      let i32 = KBounded True 32
                          y = x `svPlus` (svInteger i32 1)

                      -- compute the maximum of x and y, but keeping track of path conditions
                      (thenReachable, elseReachable, _max) <- trackedIte (x `svEqual` y) x y

                      query $ do tr <- checkFeasible thenReachable
                                 fr <- checkFeasible elseReachable
                                 io $ putStrLn $ "True  branch reachable: " ++ show tr
                                 io $ putStrLn $ "False branch reachable: " ++ show fr