    ------------------------------------------------------------------------
    -- |
    -- Module           : What4.Expr.VarIdentification
    -- Description      : Compute the bound and free variables appearing in expressions
    -- Copyright        : (c) Galois, Inc 2015-2020
    -- License          : BSD3
    -- Maintainer       : Rob Dockins <rdockins@galois.com>
    -- Stability        : provisional
    ------------------------------------------------------------------------

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE ViewPatterns #-}
    module What4.Expr.VarIdentification
      ( -- * CollectedVarInfo
        CollectedVarInfo
      , uninterpConstants
      , latches
      , QuantifierInfo(..)
      , BoundQuant(..)
      , QuantifierInfoMap
      , problemFeatures
      , existQuantifiers
      , forallQuantifiers
      , varErrors
        -- * CollectedVarInfo generation
      , Scope(..)
      , BM.Polarity(..)
      , VarRecorder
      , collectVarInfo
      , recordExprVars
      , predicateVarInfo
      ) where

    #if !MIN_VERSION_base(4,13,0)
    import Control.Monad.Fail( MonadFail )
    #endif

    import           Control.Lens
    import           Control.Monad (when)
    import           Control.Monad.Reader (MonadReader(..), ReaderT(..))
    import           Control.Monad.ST
    import           Control.Monad.State (StateT, execStateT)
    import           Data.Bits
    import qualified Data.HashTable.ST.Basic as H
    import           Data.List.NonEmpty (NonEmpty(..))
    import           Data.Map.Strict as Map
    import           Data.Parameterized.Nonce
    import           Data.Parameterized.Some
    import           Data.Parameterized.TraversableFC
    import           Data.Sequence (Seq)
    import qualified Data.Sequence as Seq
    import           Data.Set (Set)
    import qualified Data.Set as Set
    import           Data.Void
    import           Data.Word
    import           Prettyprinter (Doc)

    import           What4.BaseTypes
    import           What4.Expr.App
    import           What4.Expr.AppTheory
    import qualified What4.Expr.BoolMap as BM
    import           What4.Interface
    import           What4.ProblemFeatures
    import qualified What4.SemiRing as SR
    import           What4.Utils.MonadST

    data BoundQuant = ForallBound | ExistBound

    -- | Contains all information about a bound variable appearing in the
    -- expression.
    data QuantifierInfo t tp
       = BVI { -- | The outer term containing the binding (e.g., Ax.f(x))
               forall t (tp :: BaseType).
    QuantifierInfo t tp -> NonceAppExpr t BaseBoolType
    boundTopTerm :: !(NonceAppExpr t BaseBoolType)
               -- | The type of quantifier that appears
             , forall t (tp :: BaseType). QuantifierInfo t tp -> BoundQuant
    boundQuant :: !BoundQuant
               -- | The variable that is bound
               -- Variables may be bound multiple times.
             , forall t (tp :: BaseType). QuantifierInfo t tp -> ExprBoundVar t tp
    boundVar   :: !(ExprBoundVar t tp)
               -- | The term that appears inside the binding.
             , forall t (tp :: BaseType).
    QuantifierInfo t tp -> Expr t BaseBoolType
    boundInnerTerm :: !(Expr t BaseBoolType)
             }

    -- This is a map from quantified formulas to the information about the
    -- formula.
    type QuantifierInfoMap t = Map (NonceAppExpr t BaseBoolType) (Some (QuantifierInfo t))

    -- Due to sharing, a variable may be both existentially and universally quantified even
    -- though it is technically bound once.
    data CollectedVarInfo t
       = CollectedVarInfo { forall t. CollectedVarInfo t -> ProblemFeatures
    _problemFeatures :: !ProblemFeatures
                          , forall t. CollectedVarInfo t -> Set (Some (ExprBoundVar t))
    _uninterpConstants :: !(Set (Some (ExprBoundVar t)))
                          , forall t. CollectedVarInfo t -> QuantifierInfoMap t
    _existQuantifiers  :: !(QuantifierInfoMap t)
                          , forall t. CollectedVarInfo t -> QuantifierInfoMap t
    _forallQuantifiers :: !(QuantifierInfoMap t)
                          , forall t. CollectedVarInfo t -> Set (Some (ExprBoundVar t))
    _latches  :: !(Set (Some (ExprBoundVar t)))
                            -- | List of errors found during parsing.
                          , forall t. CollectedVarInfo t -> Seq (Doc Void)
    _varErrors :: !(Seq (Doc Void))
                          }

    -- | Describes types of functionality required by solver based on the problem.
    problemFeatures :: Simple Lens (CollectedVarInfo t) ProblemFeatures
    problemFeatures :: forall t (f :: Type -> Type).
    Functor f =>
    (ProblemFeatures -> f ProblemFeatures)
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    problemFeatures = (CollectedVarInfo t -> ProblemFeatures)
    -> (CollectedVarInfo t -> ProblemFeatures -> CollectedVarInfo t)
    -> Lens
         (CollectedVarInfo t)
         (CollectedVarInfo t)
         ProblemFeatures
         ProblemFeatures
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    lens CollectedVarInfo t -> ProblemFeatures
    forall t. CollectedVarInfo t -> ProblemFeatures
    _problemFeatures (\CollectedVarInfo t
    s ProblemFeatures
    v -> CollectedVarInfo t
    s { _problemFeatures = v })

    uninterpConstants :: Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))
    uninterpConstants :: forall t (f :: Type -> Type).
    Functor f =>
    (Set (Some (ExprBoundVar t)) -> f (Set (Some (ExprBoundVar t))))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    uninterpConstants = (CollectedVarInfo t -> Set (Some (ExprBoundVar t)))
    -> (CollectedVarInfo t
        -> Set (Some (ExprBoundVar t)) -> CollectedVarInfo t)
    -> Lens
         (CollectedVarInfo t)
         (CollectedVarInfo t)
         (Set (Some (ExprBoundVar t)))
         (Set (Some (ExprBoundVar t)))
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    lens CollectedVarInfo t -> Set (Some (ExprBoundVar t))
    forall t. CollectedVarInfo t -> Set (Some (ExprBoundVar t))
    _uninterpConstants (\CollectedVarInfo t
    s Set (Some (ExprBoundVar t))
    v -> CollectedVarInfo t
    s { _uninterpConstants = v })

    -- | Expressions appearing in the problem as existentially quantified when
    -- the problem is expressed in negation normal form.  This is a map
    -- from the existential quantifier element to the info.
    existQuantifiers :: Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)
    existQuantifiers :: forall t (f :: Type -> Type).
    Functor f =>
    (QuantifierInfoMap t -> f (QuantifierInfoMap t))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    existQuantifiers = (CollectedVarInfo t -> QuantifierInfoMap t)
    -> (CollectedVarInfo t
        -> QuantifierInfoMap t -> CollectedVarInfo t)
    -> Lens
         (CollectedVarInfo t)
         (CollectedVarInfo t)
         (QuantifierInfoMap t)
         (QuantifierInfoMap t)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    lens CollectedVarInfo t -> QuantifierInfoMap t
    forall t. CollectedVarInfo t -> QuantifierInfoMap t
    _existQuantifiers (\CollectedVarInfo t
    s QuantifierInfoMap t
    v -> CollectedVarInfo t
    s { _existQuantifiers = v })

    -- | Expressions appearing in the problem as existentially quantified when
    -- the problem is expressed in negation normal form.  This is a map
    -- from the existential quantifier element to the info.
    forallQuantifiers :: Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)
    forallQuantifiers :: forall t (f :: Type -> Type).
    Functor f =>
    (QuantifierInfoMap t -> f (QuantifierInfoMap t))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    forallQuantifiers = (CollectedVarInfo t -> QuantifierInfoMap t)
    -> (CollectedVarInfo t
        -> QuantifierInfoMap t -> CollectedVarInfo t)
    -> Lens
         (CollectedVarInfo t)
         (CollectedVarInfo t)
         (QuantifierInfoMap t)
         (QuantifierInfoMap t)
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    lens CollectedVarInfo t -> QuantifierInfoMap t
    forall t. CollectedVarInfo t -> QuantifierInfoMap t
    _forallQuantifiers (\CollectedVarInfo t
    s QuantifierInfoMap t
    v -> CollectedVarInfo t
    s { _forallQuantifiers = v })

    latches :: Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))
    latches :: forall t (f :: Type -> Type).
    Functor f =>
    (Set (Some (ExprBoundVar t)) -> f (Set (Some (ExprBoundVar t))))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    latches = (CollectedVarInfo t -> Set (Some (ExprBoundVar t)))
    -> (CollectedVarInfo t
        -> Set (Some (ExprBoundVar t)) -> CollectedVarInfo t)
    -> Lens
         (CollectedVarInfo t)
         (CollectedVarInfo t)
         (Set (Some (ExprBoundVar t)))
         (Set (Some (ExprBoundVar t)))
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    lens CollectedVarInfo t -> Set (Some (ExprBoundVar t))
    forall t. CollectedVarInfo t -> Set (Some (ExprBoundVar t))
    _latches (\CollectedVarInfo t
    s Set (Some (ExprBoundVar t))
    v -> CollectedVarInfo t
    s { _latches = v })

    varErrors :: Simple Lens (CollectedVarInfo t) (Seq (Doc Void))
    varErrors :: forall t (f :: Type -> Type).
    Functor f =>
    (Seq (Doc Void) -> f (Seq (Doc Void)))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    varErrors = (CollectedVarInfo t -> Seq (Doc Void))
    -> (CollectedVarInfo t -> Seq (Doc Void) -> CollectedVarInfo t)
    -> Lens
         (CollectedVarInfo t)
         (CollectedVarInfo t)
         (Seq (Doc Void))
         (Seq (Doc Void))
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    lens CollectedVarInfo t -> Seq (Doc Void)
    forall t. CollectedVarInfo t -> Seq (Doc Void)
    _varErrors (\CollectedVarInfo t
    s Seq (Doc Void)
    v -> CollectedVarInfo t
    s { _varErrors = v })

    -- | Return variables needed to define element as a predicate
    predicateVarInfo :: Expr t BaseBoolType -> CollectedVarInfo t
    predicateVarInfo :: forall t. Expr t BaseBoolType -> CollectedVarInfo t
    predicateVarInfo Expr t BaseBoolType
    e = (forall s. ST s (CollectedVarInfo t)) -> CollectedVarInfo t
    forall a. (forall s. ST s a) -> a
    runST ((forall s. ST s (CollectedVarInfo t)) -> CollectedVarInfo t)
    -> (forall s. ST s (CollectedVarInfo t)) -> CollectedVarInfo t
    forall a b. (a -> b) -> a -> b
    $ VarRecorder s t () -> ST s (CollectedVarInfo t)
    forall s t. VarRecorder s t () -> ST s (CollectedVarInfo t)
    collectVarInfo (VarRecorder s t () -> ST s (CollectedVarInfo t))
    -> VarRecorder s t () -> ST s (CollectedVarInfo t)
    forall a b. (a -> b) -> a -> b
    $ Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recordAssertionVars Scope
    ExistsOnly Polarity
    BM.Positive Expr t BaseBoolType
    e

    newtype VarRecorder s t a
          = VR { forall s t a.
    VarRecorder s t a
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         a
    unVR :: ReaderT (H.HashTable s Word64 (Maybe BM.Polarity))
                                 (StateT (CollectedVarInfo t) (ST s))
                                 a
               }
      deriving ( (forall a b. (a -> b) -> VarRecorder s t a -> VarRecorder s t b)
    -> (forall a b. a -> VarRecorder s t b -> VarRecorder s t a)
    -> Functor (VarRecorder s t)
    forall a b. a -> VarRecorder s t b -> VarRecorder s t a
    forall a b. (a -> b) -> VarRecorder s t a -> VarRecorder s t b
    forall s t a b. a -> VarRecorder s t b -> VarRecorder s t a
    forall s t a b. (a -> b) -> VarRecorder s t a -> VarRecorder s t b
    forall (f :: Type -> Type).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall s t a b. (a -> b) -> VarRecorder s t a -> VarRecorder s t b
    fmap :: forall a b. (a -> b) -> VarRecorder s t a -> VarRecorder s t b
    $c<$ :: forall s t a b. a -> VarRecorder s t b -> VarRecorder s t a
    <$ :: forall a b. a -> VarRecorder s t b -> VarRecorder s t a
    Functor
               , Functor (VarRecorder s t)
    Functor (VarRecorder s t) =>
    (forall a. a -> VarRecorder s t a)
    -> (forall a b.
        VarRecorder s t (a -> b) -> VarRecorder s t a -> VarRecorder s t b)
    -> (forall a b c.
        (a -> b -> c)
        -> VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t c)
    -> (forall a b.
        VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b)
    -> (forall a b.
        VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t a)
    -> Applicative (VarRecorder s t)
    forall a. a -> VarRecorder s t a
    forall s t. Functor (VarRecorder s t)
    forall a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t a
    forall a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b
    forall a b.
    VarRecorder s t (a -> b) -> VarRecorder s t a -> VarRecorder s t b
    forall s t a. a -> VarRecorder s t a
    forall a b c.
    (a -> b -> c)
    -> VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t c
    forall s t a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t a
    forall s t a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b
    forall s t a b.
    VarRecorder s t (a -> b) -> VarRecorder s t a -> VarRecorder s t b
    forall s t a b c.
    (a -> b -> c)
    -> VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t c
    forall (f :: Type -> Type).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    $cpure :: forall s t a. a -> VarRecorder s t a
    pure :: forall a. a -> VarRecorder s t a
    $c<*> :: forall s t a b.
    VarRecorder s t (a -> b) -> VarRecorder s t a -> VarRecorder s t b
    <*> :: forall a b.
    VarRecorder s t (a -> b) -> VarRecorder s t a -> VarRecorder s t b
    $cliftA2 :: forall s t a b c.
    (a -> b -> c)
    -> VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t c
    liftA2 :: forall a b c.
    (a -> b -> c)
    -> VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t c
    $c*> :: forall s t a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b
    *> :: forall a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b
    $c<* :: forall s t a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t a
    <* :: forall a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t a
    Applicative
               , Applicative (VarRecorder s t)
    Applicative (VarRecorder s t) =>
    (forall a b.
     VarRecorder s t a -> (a -> VarRecorder s t b) -> VarRecorder s t b)
    -> (forall a b.
        VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b)
    -> (forall a. a -> VarRecorder s t a)
    -> Monad (VarRecorder s t)
    forall a. a -> VarRecorder s t a
    forall s t. Applicative (VarRecorder s t)
    forall a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b
    forall a b.
    VarRecorder s t a -> (a -> VarRecorder s t b) -> VarRecorder s t b
    forall s t a. a -> VarRecorder s t a
    forall s t a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b
    forall s t a b.
    VarRecorder s t a -> (a -> VarRecorder s t b) -> VarRecorder s t b
    forall (m :: Type -> Type).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall s t a b.
    VarRecorder s t a -> (a -> VarRecorder s t b) -> VarRecorder s t b
    >>= :: forall a b.
    VarRecorder s t a -> (a -> VarRecorder s t b) -> VarRecorder s t b
    $c>> :: forall s t a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b
    >> :: forall a b.
    VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b
    $creturn :: forall s t a. a -> VarRecorder s t a
    return :: forall a. a -> VarRecorder s t a
    Monad
               , MonadST s
               )

    collectVarInfo :: VarRecorder s t () -> ST s (CollectedVarInfo t)
    collectVarInfo :: forall s t. VarRecorder s t () -> ST s (CollectedVarInfo t)
    collectVarInfo VarRecorder s t ()
    m = do
      h <- ST s (HashTable s Word64 (Maybe Polarity))
    forall s k v. ST s (HashTable s k v)
    H.new
      let s = CollectedVarInfo { _problemFeatures :: ProblemFeatures
    _problemFeatures = ProblemFeatures
    noFeatures
                        , _uninterpConstants :: Set (Some (ExprBoundVar t))
    _uninterpConstants = Set (Some (ExprBoundVar t))
    forall a. Set a
    Set.empty
                        , _existQuantifiers :: QuantifierInfoMap t
    _existQuantifiers  = QuantifierInfoMap t
    forall k a. Map k a
    Map.empty
                        , _forallQuantifiers :: QuantifierInfoMap t
    _forallQuantifiers = QuantifierInfoMap t
    forall k a. Map k a
    Map.empty
                        , _latches :: Set (Some (ExprBoundVar t))
    _latches   = Set (Some (ExprBoundVar t))
    forall a. Set a
    Set.empty
                        , _varErrors :: Seq (Doc Void)
    _varErrors = Seq (Doc Void)
    forall a. Seq a
    Seq.empty
                        }
      execStateT (runReaderT (unVR m) h) s

    addFeatures :: ProblemFeatures -> VarRecorder s t ()
    addFeatures :: forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    f = ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      ()
    -> VarRecorder s t ()
    forall s t a.
    ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      a
    -> VarRecorder s t a
    VR (ReaderT
       (HashTable s Word64 (Maybe Polarity))
       (StateT (CollectedVarInfo t) (ST s))
       ()
     -> VarRecorder s t ())
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ (ProblemFeatures -> Identity ProblemFeatures)
    -> CollectedVarInfo t -> Identity (CollectedVarInfo t)
    forall t (f :: Type -> Type).
    Functor f =>
    (ProblemFeatures -> f ProblemFeatures)
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    problemFeatures ((ProblemFeatures -> Identity ProblemFeatures)
     -> CollectedVarInfo t -> Identity (CollectedVarInfo t))
    -> (ProblemFeatures -> ProblemFeatures)
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    forall s (m :: Type -> Type) a b.
    MonadState s m =>
    ASetter s s a b -> (a -> b) -> m ()
    %= (ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    f)

    -- | Add the featured expected by a variable with the given type.
    addFeaturesForVarType :: BaseTypeRepr tp -> VarRecorder s t ()
    addFeaturesForVarType :: forall (tp :: BaseType) s t. BaseTypeRepr tp -> VarRecorder s t ()
    addFeaturesForVarType BaseTypeRepr tp
    tp =
      case BaseTypeRepr tp
    tp of
        BaseTypeRepr tp
    BaseBoolRepr     -> () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
        BaseBVRepr NatRepr w
    _     -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useBitvectors
        BaseTypeRepr tp
    BaseIntegerRepr  -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useIntegerArithmetic
        BaseTypeRepr tp
    BaseRealRepr     -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useLinearArithmetic
        BaseTypeRepr tp
    BaseComplexRepr  -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useLinearArithmetic
        BaseStringRepr StringInfoRepr si
    _ -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useStrings
        BaseArrayRepr{}  -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useSymbolicArrays
        BaseStructRepr{} -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useStructs
        BaseFloatRepr FloatPrecisionRepr fpp
    _  -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useFloatingPoint

    -- | Information about bound variables outside this context.
    data Scope
       = ExistsOnly
       | ExistsForall

    addExistVar :: Scope -- ^ Quantifier scope
                -> BM.Polarity -- ^ Polarity of variable
                -> NonceAppExpr t BaseBoolType -- ^ Top term
                -> BoundQuant                 -- ^ Quantifier appearing in top term.
                -> ExprBoundVar t tp
                -> Expr t BaseBoolType
                -> VarRecorder s t ()
    addExistVar :: forall t (tp :: BaseType) s.
    Scope
    -> Polarity
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    addExistVar Scope
    ExistsOnly Polarity
    p NonceAppExpr t BaseBoolType
    e BoundQuant
    q ExprBoundVar t tp
    v Expr t BaseBoolType
    x = do
      let info :: QuantifierInfo t tp
    info = BVI { boundTopTerm :: NonceAppExpr t BaseBoolType
    boundTopTerm = NonceAppExpr t BaseBoolType
    e
                     , boundQuant :: BoundQuant
    boundQuant = BoundQuant
    q
                     , boundVar :: ExprBoundVar t tp
    boundVar = ExprBoundVar t tp
    v
                     , boundInnerTerm :: Expr t BaseBoolType
    boundInnerTerm = Expr t BaseBoolType
    x
                     }
      ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      ()
    -> VarRecorder s t ()
    forall s t a.
    ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      a
    -> VarRecorder s t a
    VR (ReaderT
       (HashTable s Word64 (Maybe Polarity))
       (StateT (CollectedVarInfo t) (ST s))
       ()
     -> VarRecorder s t ())
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ (QuantifierInfoMap t -> Identity (QuantifierInfoMap t))
    -> CollectedVarInfo t -> Identity (CollectedVarInfo t)
    forall t (f :: Type -> Type).
    Functor f =>
    (QuantifierInfoMap t -> f (QuantifierInfoMap t))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    existQuantifiers ((QuantifierInfoMap t -> Identity (QuantifierInfoMap t))
     -> CollectedVarInfo t -> Identity (CollectedVarInfo t))
    -> (QuantifierInfoMap t -> QuantifierInfoMap t)
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    forall s (m :: Type -> Type) a b.
    MonadState s m =>
    ASetter s s a b -> (a -> b) -> m ()
    %= NonceAppExpr t BaseBoolType
    -> Some (QuantifierInfo t)
    -> QuantifierInfoMap t
    -> QuantifierInfoMap t
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert NonceAppExpr t BaseBoolType
    e (QuantifierInfo t tp -> Some (QuantifierInfo t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some QuantifierInfo t tp
    info)
      Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recordAssertionVars Scope
    ExistsOnly Polarity
    p Expr t BaseBoolType
    x
    addExistVar Scope
    ExistsForall Polarity
    _ NonceAppExpr t BaseBoolType
    _ BoundQuant
    _ ExprBoundVar t tp
    _ Expr t BaseBoolType
    _ = do
      [Char] -> VarRecorder s t ()
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> VarRecorder s t ()) -> [Char] -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "what4 does not allow existental variables to appear inside forall quantifier."

    addForallVar :: BM.Polarity -- ^ Polarity of formula
                 -> NonceAppExpr t BaseBoolType -- ^ Top term
                 -> BoundQuant            -- ^ Quantifier appearing in top term.
                 -> ExprBoundVar t tp   -- ^ Bound variable
                 -> Expr t BaseBoolType    -- ^ Expression inside quant
                 -> VarRecorder s t ()
    addForallVar :: forall t (tp :: BaseType) s.
    Polarity
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    addForallVar Polarity
    p NonceAppExpr t BaseBoolType
    e BoundQuant
    q ExprBoundVar t tp
    v Expr t BaseBoolType
    x = do
      let info :: QuantifierInfo t tp
    info = BVI { boundTopTerm :: NonceAppExpr t BaseBoolType
    boundTopTerm = NonceAppExpr t BaseBoolType
    e
                     , boundQuant :: BoundQuant
    boundQuant = BoundQuant
    q
                     , boundVar :: ExprBoundVar t tp
    boundVar = ExprBoundVar t tp
    v
                     , boundInnerTerm :: Expr t BaseBoolType
    boundInnerTerm = Expr t BaseBoolType
    x
                     }
      ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      ()
    -> VarRecorder s t ()
    forall s t a.
    ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      a
    -> VarRecorder s t a
    VR (ReaderT
       (HashTable s Word64 (Maybe Polarity))
       (StateT (CollectedVarInfo t) (ST s))
       ()
     -> VarRecorder s t ())
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ (QuantifierInfoMap t -> Identity (QuantifierInfoMap t))
    -> CollectedVarInfo t -> Identity (CollectedVarInfo t)
    forall t (f :: Type -> Type).
    Functor f =>
    (QuantifierInfoMap t -> f (QuantifierInfoMap t))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    forallQuantifiers ((QuantifierInfoMap t -> Identity (QuantifierInfoMap t))
     -> CollectedVarInfo t -> Identity (CollectedVarInfo t))
    -> (QuantifierInfoMap t -> QuantifierInfoMap t)
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    forall s (m :: Type -> Type) a b.
    MonadState s m =>
    ASetter s s a b -> (a -> b) -> m ()
    %= NonceAppExpr t BaseBoolType
    -> Some (QuantifierInfo t)
    -> QuantifierInfoMap t
    -> QuantifierInfoMap t
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert NonceAppExpr t BaseBoolType
    e (QuantifierInfo t tp -> Some (QuantifierInfo t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some QuantifierInfo t tp
    info)
      Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recordAssertionVars Scope
    ExistsForall Polarity
    p Expr t BaseBoolType
    x

    -- | Record a Forall/Exists quantifier is found in a context where
    -- it will appear both positively and negatively.
    addBothVar :: Scope                 -- ^ Scope where binding is seen.
               -> NonceAppExpr t BaseBoolType -- ^ Top term
               -> BoundQuant            -- ^ Quantifier appearing in top term.
               -> ExprBoundVar t tp   -- ^ Variable that is bound.
               -> Expr t BaseBoolType    -- ^ Predicate over bound variable.
               -> VarRecorder s t ()
    addBothVar :: forall t (tp :: BaseType) s.
    Scope
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    addBothVar Scope
    ExistsOnly NonceAppExpr t BaseBoolType
    e BoundQuant
    q ExprBoundVar t tp
    v Expr t BaseBoolType
    x = do
      let info :: QuantifierInfo t tp
    info = BVI { boundTopTerm :: NonceAppExpr t BaseBoolType
    boundTopTerm = NonceAppExpr t BaseBoolType
    e
                     , boundQuant :: BoundQuant
    boundQuant = BoundQuant
    q
                     , boundVar :: ExprBoundVar t tp
    boundVar = ExprBoundVar t tp
    v
                     , boundInnerTerm :: Expr t BaseBoolType
    boundInnerTerm = Expr t BaseBoolType
    x
                     }
      ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      ()
    -> VarRecorder s t ()
    forall s t a.
    ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      a
    -> VarRecorder s t a
    VR (ReaderT
       (HashTable s Word64 (Maybe Polarity))
       (StateT (CollectedVarInfo t) (ST s))
       ()
     -> VarRecorder s t ())
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ (QuantifierInfoMap t -> Identity (QuantifierInfoMap t))
    -> CollectedVarInfo t -> Identity (CollectedVarInfo t)
    forall t (f :: Type -> Type).
    Functor f =>
    (QuantifierInfoMap t -> f (QuantifierInfoMap t))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    existQuantifiers  ((QuantifierInfoMap t -> Identity (QuantifierInfoMap t))
     -> CollectedVarInfo t -> Identity (CollectedVarInfo t))
    -> (QuantifierInfoMap t -> QuantifierInfoMap t)
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    forall s (m :: Type -> Type) a b.
    MonadState s m =>
    ASetter s s a b -> (a -> b) -> m ()
    %= NonceAppExpr t BaseBoolType
    -> Some (QuantifierInfo t)
    -> QuantifierInfoMap t
    -> QuantifierInfoMap t
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert NonceAppExpr t BaseBoolType
    e (QuantifierInfo t tp -> Some (QuantifierInfo t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some QuantifierInfo t tp
    info)
      ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      ()
    -> VarRecorder s t ()
    forall s t a.
    ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      a
    -> VarRecorder s t a
    VR (ReaderT
       (HashTable s Word64 (Maybe Polarity))
       (StateT (CollectedVarInfo t) (ST s))
       ()
     -> VarRecorder s t ())
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ (QuantifierInfoMap t -> Identity (QuantifierInfoMap t))
    -> CollectedVarInfo t -> Identity (CollectedVarInfo t)
    forall t (f :: Type -> Type).
    Functor f =>
    (QuantifierInfoMap t -> f (QuantifierInfoMap t))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    forallQuantifiers ((QuantifierInfoMap t -> Identity (QuantifierInfoMap t))
     -> CollectedVarInfo t -> Identity (CollectedVarInfo t))
    -> (QuantifierInfoMap t -> QuantifierInfoMap t)
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    forall s (m :: Type -> Type) a b.
    MonadState s m =>
    ASetter s s a b -> (a -> b) -> m ()
    %= NonceAppExpr t BaseBoolType
    -> Some (QuantifierInfo t)
    -> QuantifierInfoMap t
    -> QuantifierInfoMap t
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert NonceAppExpr t BaseBoolType
    e (QuantifierInfo t tp -> Some (QuantifierInfo t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some QuantifierInfo t tp
    info)
      Scope -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    ExistsForall Expr t BaseBoolType
    x
    addBothVar Scope
    ExistsForall NonceAppExpr t BaseBoolType
    _ BoundQuant
    _ ExprBoundVar t tp
    _ Expr t BaseBoolType
    _ = do
      [Char] -> VarRecorder s t ()
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> VarRecorder s t ()) -> [Char] -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "what4 does not allow existental variables to appear inside forall quantifier."

    -- | Record variables in a predicate that we are checking satisfiability of.
    recordAssertionVars :: Scope
                           -- ^ Scope of assertion
                        -> BM.Polarity
                           -- ^ BM.Polarity of this formula.
                        -> Expr t BaseBoolType
                           -- ^ Predicate to assert
                        -> VarRecorder s t ()
    recordAssertionVars :: forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recordAssertionVars Scope
    scope Polarity
    p e :: Expr t BaseBoolType
    e@(AppExpr AppExpr t BaseBoolType
    ae) = do
      ht <- ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      (HashTable s Word64 (Maybe Polarity))
    -> VarRecorder s t (HashTable s Word64 (Maybe Polarity))
    forall s t a.
    ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      a
    -> VarRecorder s t a
    VR ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      (HashTable s Word64 (Maybe Polarity))
    forall r (m :: Type -> Type). MonadReader r m => m r
    ask
      let idx = Nonce t BaseBoolType -> Word64
    forall k s (tp :: k). Nonce s tp -> Word64
    indexValue (AppExpr t BaseBoolType -> Nonce t BaseBoolType
    forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
    appExprId AppExpr t BaseBoolType
    ae)
      mp <- liftST $ H.lookup ht idx
      case mp of
        -- We've seen this element in both positive and negative contexts.
        Just Maybe Polarity
    Nothing -> () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
        -- We've already seen the element in the context @oldp@.
        Just (Just Polarity
    oldp) -> do
          Bool -> VarRecorder s t () -> VarRecorder s t ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    when (Polarity
    oldp Polarity -> Polarity -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Polarity
    p) (VarRecorder s t () -> VarRecorder s t ())
    -> VarRecorder s t () -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ do
            Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recurseAssertedAppExprVars Scope
    scope Polarity
    p Expr t BaseBoolType
    e
            ST s () -> VarRecorder s t ()
    forall a. ST s a -> VarRecorder s t a
    forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
    liftST (ST s () -> VarRecorder s t ()) -> ST s () -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ HashTable s Word64 (Maybe Polarity)
    -> Word64 -> Maybe Polarity -> ST s ()
    forall k s v.
    (Eq k, Hashable k) =>
    HashTable s k v -> k -> v -> ST s ()
    H.insert HashTable s Word64 (Maybe Polarity)
    ht Word64
    idx Maybe Polarity
    forall a. Maybe a
    Nothing
        -- We have not seen this element yet.
        Maybe (Maybe Polarity)
    Nothing -> do
          Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recurseAssertedAppExprVars Scope
    scope Polarity
    p Expr t BaseBoolType
    e
          ST s () -> VarRecorder s t ()
    forall a. ST s a -> VarRecorder s t a
    forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
    liftST (ST s () -> VarRecorder s t ()) -> ST s () -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ HashTable s Word64 (Maybe Polarity)
    -> Word64 -> Maybe Polarity -> ST s ()
    forall k s v.
    (Eq k, Hashable k) =>
    HashTable s k v -> k -> v -> ST s ()
    H.insert HashTable s Word64 (Maybe Polarity)
    ht Word64
    idx (Polarity -> Maybe Polarity
    forall a. a -> Maybe a
    Just Polarity
    p)
    recordAssertionVars Scope
    scope Polarity
    p (NonceAppExpr NonceAppExpr t BaseBoolType
    ae) = do
      ht <- ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      (HashTable s Word64 (Maybe Polarity))
    -> VarRecorder s t (HashTable s Word64 (Maybe Polarity))
    forall s t a.
    ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      a
    -> VarRecorder s t a
    VR ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      (HashTable s Word64 (Maybe Polarity))
    forall r (m :: Type -> Type). MonadReader r m => m r
    ask
      let idx = Nonce t BaseBoolType -> Word64
    forall k s (tp :: k). Nonce s tp -> Word64
    indexValue (NonceAppExpr t BaseBoolType -> Nonce t BaseBoolType
    forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
    nonceExprId NonceAppExpr t BaseBoolType
    ae)
      mp <- liftST $ H.lookup ht idx
      case mp of
        -- We've seen this element in both positive and negative contexts.
        Just Maybe Polarity
    Nothing -> () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
        -- We've already seen the element in the context @oldp@.
        Just (Just Polarity
    oldp) -> do
          Bool -> VarRecorder s t () -> VarRecorder s t ()
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
    when (Polarity
    oldp Polarity -> Polarity -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Polarity
    p) (VarRecorder s t () -> VarRecorder s t ())
    -> VarRecorder s t () -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ do
            Scope
    -> Polarity -> NonceAppExpr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope
    -> Polarity -> NonceAppExpr t BaseBoolType -> VarRecorder s t ()
    recurseAssertedNonceAppExprVars Scope
    scope Polarity
    p NonceAppExpr t BaseBoolType
    ae
            ST s () -> VarRecorder s t ()
    forall a. ST s a -> VarRecorder s t a
    forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
    liftST (ST s () -> VarRecorder s t ()) -> ST s () -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ HashTable s Word64 (Maybe Polarity)
    -> Word64 -> Maybe Polarity -> ST s ()
    forall k s v.
    (Eq k, Hashable k) =>
    HashTable s k v -> k -> v -> ST s ()
    H.insert HashTable s Word64 (Maybe Polarity)
    ht Word64
    idx Maybe Polarity
    forall a. Maybe a
    Nothing
        -- We have not seen this element yet.
        Maybe (Maybe Polarity)
    Nothing -> do
          Scope
    -> Polarity -> NonceAppExpr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope
    -> Polarity -> NonceAppExpr t BaseBoolType -> VarRecorder s t ()
    recurseAssertedNonceAppExprVars Scope
    scope Polarity
    p NonceAppExpr t BaseBoolType
    ae
          ST s () -> VarRecorder s t ()
    forall a. ST s a -> VarRecorder s t a
    forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
    liftST (ST s () -> VarRecorder s t ()) -> ST s () -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ HashTable s Word64 (Maybe Polarity)
    -> Word64 -> Maybe Polarity -> ST s ()
    forall k s v.
    (Eq k, Hashable k) =>
    HashTable s k v -> k -> v -> ST s ()
    H.insert HashTable s Word64 (Maybe Polarity)
    ht Word64
    idx (Polarity -> Maybe Polarity
    forall a. a -> Maybe a
    Just Polarity
    p)
    recordAssertionVars Scope
    scope Polarity
    _ Expr t BaseBoolType
    e = do
      Scope -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    scope Expr t BaseBoolType
    e

    -- | This records asserted variables in an app expr.
    recurseAssertedNonceAppExprVars :: Scope
                               -> BM.Polarity
                               -> NonceAppExpr t BaseBoolType
                               -> VarRecorder s t ()
    recurseAssertedNonceAppExprVars :: forall t s.
    Scope
    -> Polarity -> NonceAppExpr t BaseBoolType -> VarRecorder s t ()
    recurseAssertedNonceAppExprVars Scope
    scope Polarity
    p NonceAppExpr t BaseBoolType
    ea0 =
      case NonceAppExpr t BaseBoolType -> NonceApp t (Expr t) BaseBoolType
    forall t (tp :: BaseType).
    NonceAppExpr t tp -> NonceApp t (Expr t) tp
    nonceExprApp NonceAppExpr t BaseBoolType
    ea0 of
        Forall ExprBoundVar t tp1
    v Expr t BaseBoolType
    x -> do
          case Polarity
    p of
            Polarity
    BM.Positive -> do
              ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useExistForall
              Polarity
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp1
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Polarity
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    addForallVar      Polarity
    p NonceAppExpr t BaseBoolType
    ea0 BoundQuant
    ForallBound ExprBoundVar t tp1
    v Expr t BaseBoolType
    x
            Polarity
    BM.Negative ->
              Scope
    -> Polarity
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp1
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope
    -> Polarity
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    addExistVar Scope
    scope Polarity
    p NonceAppExpr t BaseBoolType
    ea0 BoundQuant
    ForallBound ExprBoundVar t tp1
    v Expr t BaseBoolType
    x
        Exists ExprBoundVar t tp1
    v Expr t BaseBoolType
    x -> do
          case Polarity
    p of
            Polarity
    BM.Positive ->
              Scope
    -> Polarity
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp1
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope
    -> Polarity
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    addExistVar Scope
    scope Polarity
    p NonceAppExpr t BaseBoolType
    ea0 BoundQuant
    ExistBound ExprBoundVar t tp1
    v Expr t BaseBoolType
    x
            Polarity
    BM.Negative -> do
              ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useExistForall
              Polarity
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp1
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Polarity
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    addForallVar      Polarity
    p NonceAppExpr t BaseBoolType
    ea0 BoundQuant
    ExistBound ExprBoundVar t tp1
    v Expr t BaseBoolType
    x
        NonceApp t (Expr t) BaseBoolType
    _ -> Scope -> NonceAppExpr t BaseBoolType -> VarRecorder s t ()
    forall s t (tp :: BaseType).
    Scope -> NonceAppExpr t tp -> VarRecorder s t ()
    recurseNonceAppVars Scope
    scope NonceAppExpr t BaseBoolType
    ea0

    -- | This records asserted variables in an app expr.
    recurseAssertedAppExprVars :: Scope -> BM.Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recurseAssertedAppExprVars :: forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recurseAssertedAppExprVars Scope
    scope Polarity
    p Expr t BaseBoolType
    e = Expr t BaseBoolType -> VarRecorder s t ()
    go Expr t BaseBoolType
    e
     where
     go :: Expr t BaseBoolType -> VarRecorder s t ()
    go BoolExpr{} = () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()

     go (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
    forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
    asApp -> Just (NotPred Expr t BaseBoolType
    x)) =
            Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recordAssertionVars Scope
    scope (Polarity -> Polarity
    BM.negatePolarity Polarity
    p) Expr t BaseBoolType
    x

     go (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
    forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
    asApp -> Just (ConjPred BoolMap (Expr t)
    xs)) =
       let pol :: (Expr t BaseBoolType, Polarity) -> VarRecorder s t ()
    pol (Expr t BaseBoolType
    x,Polarity
    BM.Positive) = Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recordAssertionVars Scope
    scope Polarity
    p Expr t BaseBoolType
    x
           pol (Expr t BaseBoolType
    x,Polarity
    BM.Negative) = Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recordAssertionVars Scope
    scope (Polarity -> Polarity
    BM.negatePolarity Polarity
    p) Expr t BaseBoolType
    x
       in
       case BoolMap (Expr t) -> BoolMapView (Expr t)
    forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
    BM.viewBoolMap BoolMap (Expr t)
    xs of
         BoolMapView (Expr t)
    BM.BoolMapUnit -> () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
         BoolMapView (Expr t)
    BM.BoolMapDualUnit -> () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
         BM.BoolMapTerms ((Expr t BaseBoolType, Polarity)
    t:|[(Expr t BaseBoolType, Polarity)]
    ts) -> ((Expr t BaseBoolType, Polarity) -> VarRecorder s t ())
    -> [(Expr t BaseBoolType, Polarity)] -> VarRecorder s t ()
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Expr t BaseBoolType, Polarity) -> VarRecorder s t ()
    pol ((Expr t BaseBoolType, Polarity)
    t(Expr t BaseBoolType, Polarity)
    -> [(Expr t BaseBoolType, Polarity)]
    -> [(Expr t BaseBoolType, Polarity)]
    forall a. a -> [a] -> [a]
    :[(Expr t BaseBoolType, Polarity)]
    ts)

     go (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
    forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
    asApp -> Just (BaseIte BaseTypeRepr BaseBoolType
    BaseBoolRepr Integer
    _ Expr t BaseBoolType
    c Expr t BaseBoolType
    x Expr t BaseBoolType
    y)) =
       do Scope -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    scope Expr t BaseBoolType
    c
          Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recordAssertionVars Scope
    scope Polarity
    p Expr t BaseBoolType
    x
          Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t s.
    Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
    recordAssertionVars Scope
    scope Polarity
    p Expr t BaseBoolType
    y

     go Expr t BaseBoolType
    _ = Scope -> Expr t BaseBoolType -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    scope Expr t BaseBoolType
    e

    memoExprVars :: Nonce t (tp::BaseType) -> VarRecorder s t () -> VarRecorder s t ()
    memoExprVars :: forall t (tp :: BaseType) s.
    Nonce t tp -> VarRecorder s t () -> VarRecorder s t ()
    memoExprVars Nonce t tp
    n VarRecorder s t ()
    recurse = do
      let idx :: Word64
    idx = Nonce t tp -> Word64
    forall k s (tp :: k). Nonce s tp -> Word64
    indexValue Nonce t tp
    n
      ht <- ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      (HashTable s Word64 (Maybe Polarity))
    -> VarRecorder s t (HashTable s Word64 (Maybe Polarity))
    forall s t a.
    ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      a
    -> VarRecorder s t a
    VR ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      (HashTable s Word64 (Maybe Polarity))
    forall r (m :: Type -> Type). MonadReader r m => m r
    ask
      mp <- liftST $ H.lookup ht idx
      case mp of
        Just Maybe Polarity
    Nothing -> () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
        Maybe (Maybe Polarity)
    _ -> do
          VarRecorder s t ()
    recurse
          ST s () -> VarRecorder s t ()
    forall a. ST s a -> VarRecorder s t a
    forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
    liftST (ST s () -> VarRecorder s t ()) -> ST s () -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ HashTable s Word64 (Maybe Polarity)
    -> Word64 -> Maybe Polarity -> ST s ()
    forall k s v.
    (Eq k, Hashable k) =>
    HashTable s k v -> k -> v -> ST s ()
    H.insert HashTable s Word64 (Maybe Polarity)
    ht Word64
    idx Maybe Polarity
    forall a. Maybe a
    Nothing

    -- | Record the variables in an element.
    recordExprVars :: Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars :: forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    _ (SemiRingLiteral SemiRingRepr sr
    sr Coefficient sr
    _ ProgramLoc
    _) =
      case SemiRingRepr sr
    sr of
        SR.SemiRingBVRepr BVFlavorRepr fv
    _ NatRepr w
    _ -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useBitvectors
        SemiRingRepr sr
    _                     -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useLinearArithmetic
    recordExprVars Scope
    _ StringExpr{} = ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useStrings
    recordExprVars Scope
    _ FloatExpr{} = ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useFloatingPoint
    recordExprVars Scope
    _ BoolExpr{} = () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
    recordExprVars Scope
    scope (NonceAppExpr NonceAppExpr t tp
    e0) = do
      Nonce t tp -> VarRecorder s t () -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Nonce t tp -> VarRecorder s t () -> VarRecorder s t ()
    memoExprVars (NonceAppExpr t tp -> Nonce t tp
    forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
    nonceExprId NonceAppExpr t tp
    e0) (VarRecorder s t () -> VarRecorder s t ())
    -> VarRecorder s t () -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ do
        Scope -> NonceAppExpr t tp -> VarRecorder s t ()
    forall s t (tp :: BaseType).
    Scope -> NonceAppExpr t tp -> VarRecorder s t ()
    recurseNonceAppVars Scope
    scope NonceAppExpr t tp
    e0
    recordExprVars Scope
    scope (AppExpr AppExpr t tp
    e0) = do
      Nonce t tp -> VarRecorder s t () -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Nonce t tp -> VarRecorder s t () -> VarRecorder s t ()
    memoExprVars (AppExpr t tp -> Nonce t tp
    forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
    appExprId AppExpr t tp
    e0) (VarRecorder s t () -> VarRecorder s t ())
    -> VarRecorder s t () -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ do
        Scope -> AppExpr t tp -> VarRecorder s t ()
    forall s t (tp :: BaseType).
    Scope -> AppExpr t tp -> VarRecorder s t ()
    recurseExprVars Scope
    scope AppExpr t tp
    e0
    recordExprVars Scope
    _ (BoundVarExpr ExprBoundVar t tp
    info) = do
      BaseTypeRepr tp -> VarRecorder s t ()
    forall (tp :: BaseType) s t. BaseTypeRepr tp -> VarRecorder s t ()
    addFeaturesForVarType (ExprBoundVar t tp -> BaseTypeRepr tp
    forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
    bvarType ExprBoundVar t tp
    info)
      case ExprBoundVar t tp -> VarKind
    forall t (tp :: BaseType). ExprBoundVar t tp -> VarKind
    bvarKind ExprBoundVar t tp
    info of
        VarKind
    QuantifierVarKind ->
          () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
        VarKind
    LatchVarKind ->
          ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      ()
    -> VarRecorder s t ()
    forall s t a.
    ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      a
    -> VarRecorder s t a
    VR (ReaderT
       (HashTable s Word64 (Maybe Polarity))
       (StateT (CollectedVarInfo t) (ST s))
       ()
     -> VarRecorder s t ())
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ (Set (Some (ExprBoundVar t))
     -> Identity (Set (Some (ExprBoundVar t))))
    -> CollectedVarInfo t -> Identity (CollectedVarInfo t)
    forall t (f :: Type -> Type).
    Functor f =>
    (Set (Some (ExprBoundVar t)) -> f (Set (Some (ExprBoundVar t))))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    latches ((Set (Some (ExprBoundVar t))
      -> Identity (Set (Some (ExprBoundVar t))))
     -> CollectedVarInfo t -> Identity (CollectedVarInfo t))
    -> (Set (Some (ExprBoundVar t)) -> Set (Some (ExprBoundVar t)))
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    forall s (m :: Type -> Type) a b.
    MonadState s m =>
    ASetter s s a b -> (a -> b) -> m ()
    %= Some (ExprBoundVar t)
    -> Set (Some (ExprBoundVar t)) -> Set (Some (ExprBoundVar t))
    forall a. Ord a => a -> Set a -> Set a
    Set.insert (ExprBoundVar t tp -> Some (ExprBoundVar t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some ExprBoundVar t tp
    info)
        VarKind
    UninterpVarKind ->
          ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      ()
    -> VarRecorder s t ()
    forall s t a.
    ReaderT
      (HashTable s Word64 (Maybe Polarity))
      (StateT (CollectedVarInfo t) (ST s))
      a
    -> VarRecorder s t a
    VR (ReaderT
       (HashTable s Word64 (Maybe Polarity))
       (StateT (CollectedVarInfo t) (ST s))
       ()
     -> VarRecorder s t ())
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    -> VarRecorder s t ()
    forall a b. (a -> b) -> a -> b
    $ (Set (Some (ExprBoundVar t))
     -> Identity (Set (Some (ExprBoundVar t))))
    -> CollectedVarInfo t -> Identity (CollectedVarInfo t)
    forall t (f :: Type -> Type).
    Functor f =>
    (Set (Some (ExprBoundVar t)) -> f (Set (Some (ExprBoundVar t))))
    -> CollectedVarInfo t -> f (CollectedVarInfo t)
    uninterpConstants ((Set (Some (ExprBoundVar t))
      -> Identity (Set (Some (ExprBoundVar t))))
     -> CollectedVarInfo t -> Identity (CollectedVarInfo t))
    -> (Set (Some (ExprBoundVar t)) -> Set (Some (ExprBoundVar t)))
    -> ReaderT
         (HashTable s Word64 (Maybe Polarity))
         (StateT (CollectedVarInfo t) (ST s))
         ()
    forall s (m :: Type -> Type) a b.
    MonadState s m =>
    ASetter s s a b -> (a -> b) -> m ()
    %= Some (ExprBoundVar t)
    -> Set (Some (ExprBoundVar t)) -> Set (Some (ExprBoundVar t))
    forall a. Ord a => a -> Set a -> Set a
    Set.insert (ExprBoundVar t tp -> Some (ExprBoundVar t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some ExprBoundVar t tp
    info)

    recordFnVars :: ExprSymFn t args ret -> VarRecorder s t ()
    recordFnVars :: forall t (args :: Ctx BaseType) (ret :: BaseType) s.
    ExprSymFn t args ret -> VarRecorder s t ()
    recordFnVars ExprSymFn t args ret
    f = do
      case ExprSymFn t args ret -> SymFnInfo t args ret
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> SymFnInfo t args ret
    symFnInfo ExprSymFn t args ret
    f of
        UninterpFnInfo{}  ->
          ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useUninterpFunctions
        DefinedFnInfo Assignment (ExprBoundVar t) args
    _ Expr t ret
    d UnfoldPolicy
    _ ->
          do ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useDefinedFunctions
             Scope -> Expr t ret -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    ExistsForall Expr t ret
    d
        MatlabSolverFnInfo MatlabSolverFn (Expr t) args ret
    _ Assignment (ExprBoundVar t) args
    _ Expr t ret
    d ->
          do ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useDefinedFunctions
             Scope -> Expr t ret -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    ExistsForall Expr t ret
    d

    -- | Recurse through the variables in the element, adding bound variables
    -- as both exist and forall vars.
    recurseNonceAppVars :: forall s t tp. Scope -> NonceAppExpr t tp -> VarRecorder s t ()
    recurseNonceAppVars :: forall s t (tp :: BaseType).
    Scope -> NonceAppExpr t tp -> VarRecorder s t ()
    recurseNonceAppVars Scope
    scope NonceAppExpr t tp
    ea0 = do
      let a0 :: NonceApp t (Expr t) tp
    a0 = NonceAppExpr t tp -> NonceApp t (Expr t) tp
    forall t (tp :: BaseType).
    NonceAppExpr t tp -> NonceApp t (Expr t) tp
    nonceExprApp NonceAppExpr t tp
    ea0
      case NonceApp t (Expr t) tp
    a0 of
        Annotation BaseTypeRepr tp
    _ Nonce t tp
    _ Expr t tp
    x ->
          Scope -> Expr t tp -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    scope Expr t tp
    x
        Forall ExprBoundVar t tp1
    v Expr t BaseBoolType
    x ->
          Scope
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp1
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    addBothVar Scope
    scope NonceAppExpr t tp
    NonceAppExpr t BaseBoolType
    ea0 BoundQuant
    ForallBound ExprBoundVar t tp1
    v Expr t BaseBoolType
    x
        Exists ExprBoundVar t tp1
    v Expr t BaseBoolType
    x ->
          Scope
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp1
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope
    -> NonceAppExpr t BaseBoolType
    -> BoundQuant
    -> ExprBoundVar t tp
    -> Expr t BaseBoolType
    -> VarRecorder s t ()
    addBothVar Scope
    scope NonceAppExpr t tp
    NonceAppExpr t BaseBoolType
    ea0 BoundQuant
    ExistBound  ExprBoundVar t tp1
    v Expr t BaseBoolType
    x
        ArrayFromFn ExprSymFn t (idx ::> itp) ret
    f -> do
          ExprSymFn t (idx ::> itp) ret -> VarRecorder s t ()
    forall t (args :: Ctx BaseType) (ret :: BaseType) s.
    ExprSymFn t args ret -> VarRecorder s t ()
    recordFnVars ExprSymFn t (idx ::> itp) ret
    f
        MapOverArrays ExprSymFn t (ctx ::> d) r
    f Assignment BaseTypeRepr (idx ::> itp)
    _ Assignment (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
    a -> do
          ExprSymFn t (ctx ::> d) r -> VarRecorder s t ()
    forall t (args :: Ctx BaseType) (ret :: BaseType) s.
    ExprSymFn t args ret -> VarRecorder s t ()
    recordFnVars ExprSymFn t (ctx ::> d) r
    f
          (forall (x :: BaseType).
     ArrayResultWrapper (Expr t) (idx ::> itp) x -> VarRecorder s t ())
    -> forall (x :: Ctx BaseType).
       Assignment (ArrayResultWrapper (Expr t) (idx ::> itp)) x
       -> VarRecorder s t ()
    forall {k} {l} (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
           (f :: k -> Type) a.
    (FoldableFC t, Applicative m) =>
    (forall (x :: k). f x -> m a) -> forall (x :: l). t f x -> m ()
    traverseFC_ (\(ArrayResultWrapper Expr t (BaseArrayType (idx ::> itp) x)
    e) -> Scope
    -> Expr t (BaseArrayType (idx ::> itp) x) -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    scope Expr t (BaseArrayType (idx ::> itp) x)
    e) Assignment (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
    a
        ArrayTrueOnEntries ExprSymFn t (idx ::> itp) BaseBoolType
    f Expr t (BaseArrayType (idx ::> itp) BaseBoolType)
    a -> do
          ExprSymFn t (idx ::> itp) BaseBoolType -> VarRecorder s t ()
    forall t (args :: Ctx BaseType) (ret :: BaseType) s.
    ExprSymFn t args ret -> VarRecorder s t ()
    recordFnVars ExprSymFn t (idx ::> itp) BaseBoolType
    f
          Scope
    -> Expr t (BaseArrayType (idx ::> itp) BaseBoolType)
    -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    scope Expr t (BaseArrayType (idx ::> itp) BaseBoolType)
    a
        FnApp ExprSymFn t args tp
    f Assignment (Expr t) args
    a -> do
          ExprSymFn t args tp -> VarRecorder s t ()
    forall t (args :: Ctx BaseType) (ret :: BaseType) s.
    ExprSymFn t args ret -> VarRecorder s t ()
    recordFnVars ExprSymFn t args tp
    f
          (forall (x :: BaseType). Expr t x -> VarRecorder s t ())
    -> forall (x :: Ctx BaseType).
       Assignment (Expr t) x -> VarRecorder s t ()
    forall {k} {l} (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
           (f :: k -> Type) a.
    (FoldableFC t, Applicative m) =>
    (forall (x :: k). f x -> m a) -> forall (x :: l). t f x -> m ()
    traverseFC_ (Scope -> Expr t x -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    scope) Assignment (Expr t) args
    a

    addTheoryFeatures :: AppTheory -> VarRecorder s t ()
    addTheoryFeatures :: forall s t. AppTheory -> VarRecorder s t ()
    addTheoryFeatures AppTheory
    th =
      case AppTheory
    th of
        AppTheory
    BoolTheory -> () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
        AppTheory
    LinearArithTheory     -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useLinearArithmetic
        AppTheory
    NonlinearArithTheory  -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useNonlinearArithmetic
        AppTheory
    ComputableArithTheory -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useComputableReals
        AppTheory
    BitvectorTheory       -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useBitvectors
        AppTheory
    ArrayTheory           -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useSymbolicArrays
        AppTheory
    StructTheory          -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useStructs
        AppTheory
    StringTheory          -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useStrings
        AppTheory
    FloatingPointTheory   -> ProblemFeatures -> VarRecorder s t ()
    forall s t. ProblemFeatures -> VarRecorder s t ()
    addFeatures ProblemFeatures
    useFloatingPoint
        AppTheory
    QuantifierTheory -> () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()
        AppTheory
    FnTheory         -> () -> VarRecorder s t ()
    forall a. a -> VarRecorder s t a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()

    -- | Recurse through the variables in the element, adding bound variables
    -- as both exist and forall vars.
    recurseExprVars :: forall s t tp. Scope -> AppExpr t tp -> VarRecorder s t ()
    recurseExprVars :: forall s t (tp :: BaseType).
    Scope -> AppExpr t tp -> VarRecorder s t ()
    recurseExprVars Scope
    scope AppExpr t tp
    ea0 = do
      AppTheory -> VarRecorder s t ()
    forall s t. AppTheory -> VarRecorder s t ()
    addTheoryFeatures (App (Expr t) tp -> AppTheory
    forall t (tp :: BaseType). App (Expr t) tp -> AppTheory
    appTheory (AppExpr t tp -> App (Expr t) tp
    forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
    appExprApp AppExpr t tp
    ea0))
      (forall (x :: BaseType). Expr t x -> VarRecorder s t ())
    -> forall (x :: BaseType). App (Expr t) x -> VarRecorder s t ()
    forall {k} {l} (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
           (f :: k -> Type) a.
    (FoldableFC t, Applicative m) =>
    (forall (x :: k). f x -> m a) -> forall (x :: l). t f x -> m ()
    traverseFC_ (Scope -> Expr t x -> VarRecorder s t ()
    forall t (tp :: BaseType) s.
    Scope -> Expr t tp -> VarRecorder s t ()
    recordExprVars Scope
    scope) (AppExpr t tp -> App (Expr t) tp
    forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
    appExprApp AppExpr t tp
    ea0)