------------------------------------------------------------------------
-- |
-- 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(..)
  , 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.Reader
import           Control.Monad.ST
import           Control.Monad.State
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.AppTheory
import qualified What4.Expr.BoolMap as BM
import           What4.Expr.Builder
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))
           QuantifierInfo t tp -> NonceAppExpr t BaseBoolType
boundTopTerm :: !(NonceAppExpr t BaseBoolType)
           -- | The type of quantifier that appears
         , QuantifierInfo t tp -> BoundQuant
boundQuant :: !BoundQuant
           -- | The variable that is bound
           -- Variables may be bound multiple times.
         , QuantifierInfo t tp -> ExprBoundVar t tp
boundVar   :: !(ExprBoundVar t tp)
           -- | The term that appears inside the binding.
         , 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 { CollectedVarInfo t -> ProblemFeatures
_problemFeatures :: !ProblemFeatures
                      , CollectedVarInfo t -> Set (Some (ExprBoundVar t))
_uninterpConstants :: !(Set (Some (ExprBoundVar t)))
                      , CollectedVarInfo t -> QuantifierInfoMap t
_existQuantifiers  :: !(QuantifierInfoMap t)
                      , CollectedVarInfo t -> QuantifierInfoMap t
_forallQuantifiers :: !(QuantifierInfoMap t)
                      , CollectedVarInfo t -> Set (Some (ExprBoundVar t))
_latches  :: !(Set (Some (ExprBoundVar t)))
                        -- | List of errors found during parsing.
                      , 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 :: (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 :: ProblemFeatures
_problemFeatures = ProblemFeatures
v })

uninterpConstants :: Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))
uninterpConstants :: (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 :: Set (Some (ExprBoundVar t))
_uninterpConstants = Set (Some (ExprBoundVar t))
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 :: (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 :: QuantifierInfoMap t
_existQuantifiers = QuantifierInfoMap t
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 :: (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 :: QuantifierInfoMap t
_forallQuantifiers = QuantifierInfoMap t
v })

latches :: Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))
latches :: (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 :: Set (Some (ExprBoundVar t))
_latches = Set (Some (ExprBoundVar t))
v })

varErrors :: Simple Lens (CollectedVarInfo t) (Seq (Doc Void))
varErrors :: (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 :: Seq (Doc Void)
_varErrors = Seq (Doc Void)
v })

-- | Return variables needed to define element as a predicate
predicateVarInfo :: Expr t BaseBoolType -> CollectedVarInfo t
predicateVarInfo :: 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
Positive Expr t BaseBoolType
e

newtype VarRecorder s t a
      = VR { VarRecorder s t a
-> ReaderT
     (HashTable s Word64 (Maybe Polarity))
     (StateT (CollectedVarInfo t) (ST s))
     a
unVR :: ReaderT (H.HashTable s Word64 (Maybe Polarity))
                             (StateT (CollectedVarInfo t) (ST s))
                             a
           }
  deriving ( a -> VarRecorder s t b -> VarRecorder s t a
(a -> b) -> VarRecorder s t a -> VarRecorder s t b
(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
<$ :: a -> VarRecorder s t b -> VarRecorder s t a
$c<$ :: forall s t a b. a -> VarRecorder s t b -> VarRecorder s t a
fmap :: (a -> b) -> VarRecorder s t a -> VarRecorder s t b
$cfmap :: forall s t a b. (a -> b) -> VarRecorder s t a -> VarRecorder s t b
Functor
           , Functor (VarRecorder s t)
a -> VarRecorder s t a
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)
VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b
VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t a
VarRecorder s t (a -> b) -> VarRecorder s t a -> VarRecorder s t b
(a -> b -> c)
-> VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t c
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
<* :: VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t a
$c<* :: forall s t a b.
VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t a
*> :: 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 b
liftA2 :: (a -> b -> c)
-> VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t c
$cliftA2 :: forall s t a b c.
(a -> b -> c)
-> VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t c
<*> :: VarRecorder s t (a -> b) -> VarRecorder s t a -> VarRecorder s t b
$c<*> :: forall s t a b.
VarRecorder s t (a -> b) -> VarRecorder s t a -> VarRecorder s t b
pure :: a -> VarRecorder s t a
$cpure :: forall s t a. a -> VarRecorder s t a
$cp1Applicative :: forall s t. Functor (VarRecorder s t)
Applicative
           , Applicative (VarRecorder s t)
a -> VarRecorder s t a
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)
VarRecorder s t a -> (a -> VarRecorder s t b) -> VarRecorder s t b
VarRecorder s t a -> VarRecorder s t b -> VarRecorder s t b
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
return :: a -> VarRecorder s t a
$creturn :: forall s t a. a -> VarRecorder s t a
>> :: 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 b
>>= :: VarRecorder s t a -> (a -> VarRecorder s t b) -> VarRecorder s t b
$c>>= :: forall s t a b.
VarRecorder s t a -> (a -> VarRecorder s t b) -> VarRecorder s t b
$cp1Monad :: forall s t. Applicative (VarRecorder s t)
Monad
           , Monad (VarRecorder s t)
Monad (VarRecorder s t)
-> (forall a. String -> VarRecorder s t a)
-> MonadFail (VarRecorder s t)
String -> VarRecorder s t a
forall a. String -> VarRecorder s t a
forall s t. Monad (VarRecorder s t)
forall s t a. String -> VarRecorder s t a
forall (m :: Type -> Type).
Monad m -> (forall a. String -> m a) -> MonadFail m
fail :: String -> VarRecorder s t a
$cfail :: forall s t a. String -> VarRecorder s t a
$cp1MonadFail :: forall s t. Monad (VarRecorder s t)
MonadFail
           , MonadST s
           )

collectVarInfo :: VarRecorder s t () -> ST s (CollectedVarInfo t)
collectVarInfo :: VarRecorder s t () -> ST s (CollectedVarInfo t)
collectVarInfo VarRecorder s t ()
m = do
  HashTable s Word64 (Maybe Polarity)
h <- ST s (HashTable s Word64 (Maybe Polarity))
forall s k v. ST s (HashTable s k v)
H.new
  let s :: CollectedVarInfo t
s = CollectedVarInfo :: forall t.
ProblemFeatures
-> Set (Some (ExprBoundVar t))
-> QuantifierInfoMap t
-> QuantifierInfoMap t
-> Set (Some (ExprBoundVar t))
-> Seq (Doc Void)
-> CollectedVarInfo t
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
                    }
  StateT (CollectedVarInfo t) (ST s) ()
-> CollectedVarInfo t -> ST s (CollectedVarInfo t)
forall (m :: Type -> Type) s a. Monad m => StateT s m a -> s -> m s
execStateT (ReaderT
  (HashTable s Word64 (Maybe Polarity))
  (StateT (CollectedVarInfo t) (ST s))
  ()
-> HashTable s Word64 (Maybe Polarity)
-> StateT (CollectedVarInfo t) (ST s) ()
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (VarRecorder s t ()
-> ReaderT
     (HashTable s Word64 (Maybe Polarity))
     (StateT (CollectedVarInfo t) (ST s))
     ()
forall s t a.
VarRecorder s t a
-> ReaderT
     (HashTable s Word64 (Maybe Polarity))
     (StateT (CollectedVarInfo t) (ST s))
     a
unVR VarRecorder s t ()
m) HashTable s Word64 (Maybe Polarity)
h) CollectedVarInfo t
forall t. CollectedVarInfo t
s

addFeatures :: ProblemFeatures -> VarRecorder s t ()
addFeatures :: 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. Simple Lens (CollectedVarInfo t) ProblemFeatures
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 :: BaseTypeRepr tp -> VarRecorder s t ()
addFeaturesForVarType BaseTypeRepr tp
tp =
  case BaseTypeRepr tp
tp of
    BaseTypeRepr tp
BaseBoolRepr     -> () -> VarRecorder s t ()
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
            -> 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 :: 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 :: forall t (tp :: BaseType).
NonceAppExpr t BaseBoolType
-> BoundQuant
-> ExprBoundVar t tp
-> Expr t BaseBoolType
-> QuantifierInfo t tp
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. Simple Lens (CollectedVarInfo t) (QuantifierInfoMap 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
  String -> VarRecorder s t ()
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> VarRecorder s t ()) -> String -> VarRecorder s t ()
forall a b. (a -> b) -> a -> b
$ String
"what4 does not allow existental variables to appear inside forall quantifier."

addForallVar :: 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 :: 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 :: forall t (tp :: BaseType).
NonceAppExpr t BaseBoolType
-> BoundQuant
-> ExprBoundVar t tp
-> Expr t BaseBoolType
-> QuantifierInfo t tp
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. Simple Lens (CollectedVarInfo t) (QuantifierInfoMap 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 :: 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 :: forall t (tp :: BaseType).
NonceAppExpr t BaseBoolType
-> BoundQuant
-> ExprBoundVar t tp
-> Expr t BaseBoolType
-> QuantifierInfo t tp
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. Simple Lens (CollectedVarInfo t) (QuantifierInfoMap 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. Simple Lens (CollectedVarInfo t) (QuantifierInfoMap 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
  String -> VarRecorder s t ()
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> VarRecorder s t ()) -> String -> VarRecorder s t ()
forall a b. (a -> b) -> a -> b
$ String
"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
                    -> Polarity
                       -- ^ Polarity of this formula.
                    -> Expr t BaseBoolType
                       -- ^ Predicate to assert
                    -> VarRecorder s t ()
recordAssertionVars :: Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
recordAssertionVars Scope
scope Polarity
p e :: Expr t BaseBoolType
e@(AppExpr AppExpr t BaseBoolType
ae) = do
  HashTable s Word64 (Maybe Polarity)
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 :: Word64
idx = Nonce t BaseBoolType -> Word64
forall s k (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)
  Maybe (Maybe Polarity)
mp <- ST s (Maybe (Maybe Polarity))
-> VarRecorder s t (Maybe (Maybe Polarity))
forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
liftST (ST s (Maybe (Maybe Polarity))
 -> VarRecorder s t (Maybe (Maybe Polarity)))
-> ST s (Maybe (Maybe Polarity))
-> VarRecorder s t (Maybe (Maybe Polarity))
forall a b. (a -> b) -> a -> b
$ HashTable s Word64 (Maybe Polarity)
-> Word64 -> ST s (Maybe (Maybe Polarity))
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> ST s (Maybe v)
H.lookup HashTable s Word64 (Maybe Polarity)
ht Word64
idx
  case Maybe (Maybe Polarity)
mp of
    -- We've seen this element in both positive and negative contexts.
    Just Maybe Polarity
Nothing -> () -> VarRecorder s t ()
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 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 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
  HashTable s Word64 (Maybe Polarity)
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 :: Word64
idx = Nonce t BaseBoolType -> Word64
forall s k (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)
  Maybe (Maybe Polarity)
mp <- ST s (Maybe (Maybe Polarity))
-> VarRecorder s t (Maybe (Maybe Polarity))
forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
liftST (ST s (Maybe (Maybe Polarity))
 -> VarRecorder s t (Maybe (Maybe Polarity)))
-> ST s (Maybe (Maybe Polarity))
-> VarRecorder s t (Maybe (Maybe Polarity))
forall a b. (a -> b) -> a -> b
$ HashTable s Word64 (Maybe Polarity)
-> Word64 -> ST s (Maybe (Maybe Polarity))
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> ST s (Maybe v)
H.lookup HashTable s Word64 (Maybe Polarity)
ht Word64
idx
  case Maybe (Maybe Polarity)
mp of
    -- We've seen this element in both positive and negative contexts.
    Just Maybe Polarity
Nothing -> () -> VarRecorder s t ()
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 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 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
                           -> Polarity
                           -> NonceAppExpr t BaseBoolType
                           -> VarRecorder s t ()
recurseAssertedNonceAppExprVars :: 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 tp
v Expr t BaseBoolType
x -> do
      case Polarity
p of
        Polarity
Positive -> do
          ProblemFeatures -> VarRecorder s t ()
forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useExistForall
          Polarity
-> NonceAppExpr t BaseBoolType
-> BoundQuant
-> ExprBoundVar t tp
-> 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 tp
v Expr t BaseBoolType
x
        Polarity
Negative ->
          Scope
-> Polarity
-> NonceAppExpr t BaseBoolType
-> BoundQuant
-> ExprBoundVar t tp
-> 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 tp
v Expr t BaseBoolType
x
    Exists ExprBoundVar t tp
v Expr t BaseBoolType
x -> do
      case Polarity
p of
        Polarity
Positive ->
          Scope
-> Polarity
-> NonceAppExpr t BaseBoolType
-> BoundQuant
-> ExprBoundVar t tp
-> 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 tp
v Expr t BaseBoolType
x
        Polarity
Negative -> do
          ProblemFeatures -> VarRecorder s t ()
forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useExistForall
          Polarity
-> NonceAppExpr t BaseBoolType
-> BoundQuant
-> ExprBoundVar t tp
-> 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 tp
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 -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
recurseAssertedAppExprVars :: 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 (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
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
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
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
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 (m :: Type -> Type) a. Monad m => a -> m a
return ()
     BoolMapView (Expr t)
BM.BoolMapDualUnit -> () -> VarRecorder s t ()
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 :: 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 s k (tp :: k). Nonce s tp -> Word64
indexValue Nonce t tp
n
  HashTable s Word64 (Maybe Polarity)
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
  Maybe (Maybe Polarity)
mp <- ST s (Maybe (Maybe Polarity))
-> VarRecorder s t (Maybe (Maybe Polarity))
forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
liftST (ST s (Maybe (Maybe Polarity))
 -> VarRecorder s t (Maybe (Maybe Polarity)))
-> ST s (Maybe (Maybe Polarity))
-> VarRecorder s t (Maybe (Maybe Polarity))
forall a b. (a -> b) -> a -> b
$ HashTable s Word64 (Maybe Polarity)
-> Word64 -> ST s (Maybe (Maybe Polarity))
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> ST s (Maybe v)
H.lookup HashTable s Word64 (Maybe Polarity)
ht Word64
idx
  case Maybe (Maybe Polarity)
mp of
    Just Maybe Polarity
Nothing -> () -> VarRecorder s t ()
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 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 :: 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 (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 (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.
Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar 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.
Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar 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 :: 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{}  -> () -> VarRecorder s t ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
    DefinedFnInfo Assignment (ExprBoundVar t) args
_ Expr t ret
d UnfoldPolicy
_ -> 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 -> 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 :: 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 tp
v Expr t BaseBoolType
x ->
      Scope
-> NonceAppExpr t BaseBoolType
-> BoundQuant
-> ExprBoundVar t tp
-> 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 tp
v Expr t BaseBoolType
x
    Exists ExprBoundVar t tp
v Expr t BaseBoolType
x ->
      Scope
-> NonceAppExpr t BaseBoolType
-> BoundQuant
-> ExprBoundVar t tp
-> 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 tp
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 ())
-> Assignment
     (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
-> 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 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 ())
-> Assignment (Expr t) args -> 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 :: AppTheory -> VarRecorder s t ()
addTheoryFeatures AppTheory
th =
  case AppTheory
th of
    AppTheory
BoolTheory -> () -> VarRecorder s t ()
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 (m :: Type -> Type) a. Monad m => a -> m a
return ()
    AppTheory
FnTheory         -> () -> VarRecorder s t ()
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 :: 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 ())
-> App (Expr t) tp -> 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)