Search code examples
haskelloptimizationsmtsatsbv

Efficient way to do n-ary branch / tabulated functions?

I'm trying to get some basic information on the performance characteristics of branches in SBV.

Let's suppose I have an SInt16 and a very sparse lookup table Map Int16 a. I can implement the lookup with nested ite:

sCase :: (Mergeable a) => SInt16 -> a -> Map Int16 a -> a
sCase x def = go . toList
  where
    go [] = def
    go ((k,v):kvs) = ite (x .== literal k) v (go kvs)

However, this means the generated tree will be very deep.

  1. Does that matter?
  2. If yes, is it better to instead generate a balanced tree of branches, effectively mirroring the Map's structure? Or is there some other scheme that would give even better performance?
  3. If there are less than 256 entries in the map, would it change anything to "compress" it so that sCase works on an SInt8 and a Map Int8 a?
  4. Is there some built-in SBV combinator for this use case that works better than iterated ite?

EDIT: It turns out that it matters a lot what my a is, so let me add some more detail to that. I am currently using sCase to branch in a stateful computation modeled as an RWS r w s a, with the following instances:

instance forall a. Mergeable a => Mergeable (Identity a) where
    symbolicMerge force cond thn els = Identity $ symbolicMerge force cond (runIdentity thn) (runIdentity els)

instance (Mergeable s, Mergeable w, Mergeable a, forall a. Mergeable a => Mergeable (m a)) => Mergeable (RWST r w s m a) where
        symbolicMerge force cond thn els = Lazy.RWST $
            symbolicMerge force cond (runRWST thn) (runRWST els)

So stripping away all the newtypes, I'd like to branch into something of type r -> s -> (a, s, w) s.t. Mergeable s, Mergeable w and Mergeable a.

Solution

  • Symbolic look-ups are expensive

    Symbolic array lookup will be expensive regardless of what data-structure you use. It boils down to the fact that there's no information available to the symbolic execution engine to cut-down on the state-space, so it ends up doing more or less what you coded yourself.

    SMTLib Arrays

    However, the best solution in these cases is to actually use SMT's support for arrays: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml

    SMTLib arrays are different than what you'd consider as an array in a regular programming language: It does not have bounds. In that sense, it's more of a map from inputs to outputs, spanning the entire domain. (i.e., they are equivalent to functions.) But SMT has custom theories to deal with arrays and thus they can handle problems involving arrays much more efficiently. (On the down-side, there's no notion of index-out-of-bounds or somehow controlling the range of elements you can access. You can code those up yourself on top of the abstraction though, leaving it up to you to decide how you want to handle such invalid accesses.)

    If you are interested in learning more about how SMT solvers deal with arrays, the classic reference is: http://theory.stanford.edu/~arbrad/papers/arrays.pdf

    Arrays in SBV

    SBV supports arrays, through the SymArray class: https://hackage.haskell.org/package/sbv-8.7/docs/Data-SBV.html#t:SymArray

    There are some differences between these types, and the above links describe them. However, for most purposes, you can use them interchangeably.

    Converting a Haskell map to an SBV array

    Going back to your original question, I'd be tempted to use an SArray to model such a look up. I'd code it as:

    {-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV
import qualified Data.Map as M
import Data.Int

-- Fill an SBV array from a map
mapToSArray :: (SymArray array, SymVal a, SymVal b) => M.Map a (SBV b) -> array a b -> array a b
mapToSArray m a = foldl (\arr (k, v) -> writeArray arr (literal k) v) a (M.toList m)

    And use it as:

    g :: Symbolic SBool
g = do let def = 0

       -- get a symbolic array, initialized with def
       arr <- newArray "myArray" (Just def)

       let m :: M.Map Int16 SInt16
           m = M.fromList [(5, 2), (10, 5)]

       -- Fill the array from the map
       let arr' :: SArray Int16 Int16 = mapToSArray m arr

       -- A simple problem:
       idx1 <- free "idx1"
       idx2 <- free "idx2"

       pure $ 2 * readArray arr' idx1 + 1 .== readArray arr' idx2

    When I run this, I get:

    *Main> sat g
Satisfiable. Model:
  idx1 =  5 :: Int16
  idx2 = 10 :: Int16

    You can run it as satWith z3{verbose=True} g to see the SMTLib output it generates, which avoids costly lookups by simply delegating those tasks to the backend solver.

    Efficiency

    The question of whether this will be "efficient" really depends on how many elements your map has that you're constructing the array from. The larger the number of elements and the trickier the constraints, the less efficient it will be. In particular, if you ever write to an index that is symbolic, I'd expect slow-downs in solving time. If they're all constants, it should be relatively performant. As is usual in symbolic programming, it's really hard to predict any performance without seeing the actual problem and experimenting with it.

    Arrays in the query context

    The function newArray works in the symbolic context. If you're in a query context, instead use freshArray: https://hackage.haskell.org/package/sbv-8.7/docs/Data-SBV-Control.html#v:freshArray