Improve the SMT generated for array lookups with symbolic indices

What4 attempts to simplify array lookups of values with concrete indices.  In
cases where the index to look up in symbolic, that fails and it instead
generates a huge mux over all possible indexes, which is very expensive and
counterproductive.

This commit removes the special handling of symbolic indices, allowing the
generated SMT to fall back on just issuing an SMT array lookup.

Fixes #371

what4/src/What4/Expr/Builder.hs

@@ -3473,22 +3473,6 @@ evalBoundVars sym e vars exprs = do
  }
  evalBoundVars' tbls sym e
 
--- | Return true if corresponding expressions in contexts are equivalent.
-allEq :: forall sym ctx
- . IsExprBuilder sym
- => sym
- -> Ctx.Assignment (SymExpr sym) ctx
- -> Ctx.Assignment (SymExpr sym) ctx
- -> IO (Pred sym)
-allEq sym x y = Ctx.forIndex (Ctx.size x) joinEq (pure (truePred sym))
- where joinEq :: IO (Pred sym) -> Ctx.Index ctx tp -> IO (Pred sym)
- joinEq mp i = do
- q <- isEq sym (x Ctx.! i) (y Ctx.! i)
- case asConstantPred q of
- Just True -> mp
- Just False -> return (falsePred sym)
- Nothing -> andPred sym q =<< mp
-
 -- | This attempts to lookup an entry in a symbolic array.
 --
 -- It patterns maps on the array constructor.
@@ -3505,18 +3489,11 @@ sbConcreteLookup :: forall t st fs d tp range
  -> IO (Expr t range)
 sbConcreteLookup sym arr0 mcidx idx
  -- Try looking up a write to a concrete address.
- | Just (ArrayMap _ _ entry_map def) <- asApp arr0 = do
- case mcidx of
- Just cidx -> do
- case Hash.mapLookup cidx entry_map of
- Just v -> return v
- Nothing -> sbConcreteLookup sym def mcidx idx
- Nothing -> Map.foldrWithKey f (sbConcreteLookup sym def mcidx idx) (Hash.hashedMap entry_map)
- where f updated_cidx c m = do
- updated_idx <- traverseFC (indexLit sym) updated_cidx
- p <- allEq sym updated_idx idx
- iteM baseTypeIte sym p (pure c) m
-
+ | Just (ArrayMap _ _ entry_map def) <- asApp arr0
+ , Just cidx <- mcidx =
+ case Hash.mapLookup cidx entry_map of
+ Just v -> return v
+ Nothing -> sbConcreteLookup sym def mcidx idx
  -- Evaluate function arrays on ground values.
  | Just (ArrayFromFn f) <- asNonceApp arr0 = do
  betaReduce sym f idx