{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
module What4.Expr.VarIdentification
(
CollectedVarInfo
, uninterpConstants
, latches
, QuantifierInfo(..)
, BoundQuant(..)
, QuantifierInfoMap
, problemFeatures
, existQuantifiers
, forallQuantifiers
, varErrors
, 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
data QuantifierInfo t tp
= BVI {
forall t (tp :: BaseType).
QuantifierInfo t tp -> NonceAppExpr t BaseBoolType
boundTopTerm :: !(NonceAppExpr t BaseBoolType)
, forall t (tp :: BaseType). QuantifierInfo t tp -> BoundQuant
boundQuant :: !BoundQuant
, forall t (tp :: BaseType). QuantifierInfo t tp -> ExprBoundVar t tp
boundVar :: !(ExprBoundVar t tp)
, forall t (tp :: BaseType).
QuantifierInfo t tp -> Expr t BaseBoolType
boundInnerTerm :: !(Expr t BaseBoolType)
}
type QuantifierInfoMap t = Map (NonceAppExpr t BaseBoolType) (Some (QuantifierInfo t))
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)))
, forall t. CollectedVarInfo t -> Seq (Doc Void)
_varErrors :: !(Seq (Doc Void))
}
problemFeatures :: Simple Lens (CollectedVarInfo t) ProblemFeatures
problemFeatures :: forall t. Simple Lens (CollectedVarInfo t) ProblemFeatures
problemFeatures = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens 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 :: forall t.
Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))
uninterpConstants = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens 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 })
existQuantifiers :: Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)
existQuantifiers :: forall t. Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)
existQuantifiers = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall t. CollectedVarInfo t -> QuantifierInfoMap t
_existQuantifiers (\CollectedVarInfo t
s QuantifierInfoMap t
v -> CollectedVarInfo t
s { _existQuantifiers :: QuantifierInfoMap t
_existQuantifiers = QuantifierInfoMap t
v })
forallQuantifiers :: Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)
forallQuantifiers :: forall t. Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)
forallQuantifiers = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens 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 :: forall t.
Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))
latches = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens 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 :: forall t. Simple Lens (CollectedVarInfo t) (Seq (Doc Void))
varErrors = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens 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 })
predicateVarInfo :: Expr t BaseBoolType -> CollectedVarInfo t
predicateVarInfo :: forall t. Expr t BaseBoolType -> CollectedVarInfo t
predicateVarInfo Expr t BaseBoolType
e = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ forall s t. VarRecorder s t () -> ST s (CollectedVarInfo t)
collectVarInfo forall a b. (a -> b) -> a -> b
$ 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 -> 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
<$ :: forall a b. 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 :: forall a b. (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
, 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
<* :: forall a b.
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
*> :: 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 b
liftA2 :: forall a b c.
(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
<*> :: forall a b.
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 :: forall a. a -> VarRecorder s t a
$cpure :: forall s t a. a -> VarRecorder s t a
Applicative
, 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 :: forall a. a -> VarRecorder s t a
$creturn :: forall s t a. a -> VarRecorder s t a
>> :: 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 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 -> (a -> VarRecorder s t b) -> VarRecorder s t b
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
HashTable s Word64 (Maybe Polarity)
h <- forall s k v. ST s (HashTable s k v)
H.new
let s :: CollectedVarInfo t
s = CollectedVarInfo { _problemFeatures :: ProblemFeatures
_problemFeatures = ProblemFeatures
noFeatures
, _uninterpConstants :: Set (Some (ExprBoundVar t))
_uninterpConstants = forall a. Set a
Set.empty
, _existQuantifiers :: QuantifierInfoMap t
_existQuantifiers = forall k a. Map k a
Map.empty
, _forallQuantifiers :: QuantifierInfoMap t
_forallQuantifiers = forall k a. Map k a
Map.empty
, _latches :: Set (Some (ExprBoundVar t))
_latches = forall a. Set a
Set.empty
, _varErrors :: Seq (Doc Void)
_varErrors = forall a. Seq a
Seq.empty
}
forall (m :: Type -> Type) s a. Monad m => StateT s m a -> s -> m s
execStateT (forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (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) forall {t}. CollectedVarInfo t
s
addFeatures :: ProblemFeatures -> VarRecorder s t ()
addFeatures :: forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
f = forall s t a.
ReaderT
(HashTable s Word64 (Maybe Polarity))
(StateT (CollectedVarInfo t) (ST s))
a
-> VarRecorder s t a
VR forall a b. (a -> b) -> a -> b
$ forall t. Simple Lens (CollectedVarInfo t) ProblemFeatures
problemFeatures forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (forall a. Bits a => a -> a -> a
.|. ProblemFeatures
f)
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 -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
BaseBVRepr NatRepr w
_ -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useBitvectors
BaseTypeRepr tp
BaseIntegerRepr -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useIntegerArithmetic
BaseTypeRepr tp
BaseRealRepr -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useLinearArithmetic
BaseTypeRepr tp
BaseComplexRepr -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useLinearArithmetic
BaseStringRepr StringInfoRepr si
_ -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useStrings
BaseArrayRepr{} -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useSymbolicArrays
BaseStructRepr{} -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useStructs
BaseFloatRepr FloatPrecisionRepr fpp
_ -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useFloatingPoint
data Scope
= ExistsOnly
| ExistsForall
addExistVar :: Scope
-> BM.Polarity
-> NonceAppExpr t BaseBoolType
-> BoundQuant
-> 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
}
forall s t a.
ReaderT
(HashTable s Word64 (Maybe Polarity))
(StateT (CollectedVarInfo t) (ST s))
a
-> VarRecorder s t a
VR forall a b. (a -> b) -> a -> b
$ forall t. Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)
existQuantifiers forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NonceAppExpr t BaseBoolType
e (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some QuantifierInfo t tp
info)
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
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"what4 does not allow existental variables to appear inside forall quantifier."
addForallVar :: BM.Polarity
-> NonceAppExpr t BaseBoolType
-> BoundQuant
-> ExprBoundVar t tp
-> Expr t BaseBoolType
-> 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
}
forall s t a.
ReaderT
(HashTable s Word64 (Maybe Polarity))
(StateT (CollectedVarInfo t) (ST s))
a
-> VarRecorder s t a
VR forall a b. (a -> b) -> a -> b
$ forall t. Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)
forallQuantifiers forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NonceAppExpr t BaseBoolType
e (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some QuantifierInfo t tp
info)
forall t s.
Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
recordAssertionVars Scope
ExistsForall Polarity
p Expr t BaseBoolType
x
addBothVar :: Scope
-> NonceAppExpr t BaseBoolType
-> BoundQuant
-> ExprBoundVar t tp
-> Expr t BaseBoolType
-> 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
}
forall s t a.
ReaderT
(HashTable s Word64 (Maybe Polarity))
(StateT (CollectedVarInfo t) (ST s))
a
-> VarRecorder s t a
VR forall a b. (a -> b) -> a -> b
$ forall t. Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)
existQuantifiers forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NonceAppExpr t BaseBoolType
e (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some QuantifierInfo t tp
info)
forall s t a.
ReaderT
(HashTable s Word64 (Maybe Polarity))
(StateT (CollectedVarInfo t) (ST s))
a
-> VarRecorder s t a
VR forall a b. (a -> b) -> a -> b
$ forall t. Simple Lens (CollectedVarInfo t) (QuantifierInfoMap t)
forallQuantifiers forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NonceAppExpr t BaseBoolType
e (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some QuantifierInfo t tp
info)
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
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"what4 does not allow existental variables to appear inside forall quantifier."
recordAssertionVars :: Scope
-> BM.Polarity
-> Expr t BaseBoolType
-> 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
HashTable s Word64 (Maybe Polarity)
ht <- forall s t a.
ReaderT
(HashTable s Word64 (Maybe Polarity))
(StateT (CollectedVarInfo t) (ST s))
a
-> VarRecorder s t a
VR forall r (m :: Type -> Type). MonadReader r m => m r
ask
let idx :: Word64
idx = forall k s (tp :: k). Nonce s tp -> Word64
indexValue (forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t BaseBoolType
ae)
Maybe (Maybe Polarity)
mp <- forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
liftST forall a b. (a -> b) -> a -> b
$ 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 -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
Just (Just Polarity
oldp) -> do
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Polarity
oldp forall a. Eq a => a -> a -> Bool
/= Polarity
p) forall a b. (a -> b) -> a -> b
$ do
forall t s.
Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
recurseAssertedAppExprVars Scope
scope Polarity
p Expr t BaseBoolType
e
forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
liftST forall a b. (a -> b) -> a -> b
$ 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 forall a. Maybe a
Nothing
Maybe (Maybe Polarity)
Nothing -> do
forall t s.
Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
recurseAssertedAppExprVars Scope
scope Polarity
p Expr t BaseBoolType
e
forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
liftST forall a b. (a -> b) -> a -> b
$ 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 (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 <- forall s t a.
ReaderT
(HashTable s Word64 (Maybe Polarity))
(StateT (CollectedVarInfo t) (ST s))
a
-> VarRecorder s t a
VR forall r (m :: Type -> Type). MonadReader r m => m r
ask
let idx :: Word64
idx = forall k s (tp :: k). Nonce s tp -> Word64
indexValue (forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t BaseBoolType
ae)
Maybe (Maybe Polarity)
mp <- forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
liftST forall a b. (a -> b) -> a -> b
$ 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 -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
Just (Just Polarity
oldp) -> do
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Polarity
oldp forall a. Eq a => a -> a -> Bool
/= Polarity
p) forall a b. (a -> b) -> a -> b
$ do
forall t s.
Scope
-> Polarity -> NonceAppExpr t BaseBoolType -> VarRecorder s t ()
recurseAssertedNonceAppExprVars Scope
scope Polarity
p NonceAppExpr t BaseBoolType
ae
forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
liftST forall a b. (a -> b) -> a -> b
$ 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 forall a. Maybe a
Nothing
Maybe (Maybe Polarity)
Nothing -> do
forall t s.
Scope
-> Polarity -> NonceAppExpr t BaseBoolType -> VarRecorder s t ()
recurseAssertedNonceAppExprVars Scope
scope Polarity
p NonceAppExpr t BaseBoolType
ae
forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
liftST forall a b. (a -> b) -> a -> b
$ 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 (forall a. a -> Maybe a
Just Polarity
p)
recordAssertionVars Scope
scope Polarity
_ Expr t BaseBoolType
e = do
forall t (tp :: BaseType) s.
Scope -> Expr t tp -> VarRecorder s t ()
recordExprVars Scope
scope Expr t BaseBoolType
e
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 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
forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useExistForall
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 ->
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 ->
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
forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useExistForall
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
_ -> forall s t (tp :: BaseType).
Scope -> NonceAppExpr t tp -> VarRecorder s t ()
recurseNonceAppVars Scope
scope NonceAppExpr t BaseBoolType
ea0
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{} = forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
go (forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (NotPred Expr t BaseBoolType
x)) =
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 (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) = 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) = 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 forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
BM.viewBoolMap BoolMap (Expr t)
xs of
BoolMapView (Expr t)
BM.BoolMapUnit -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
BoolMapView (Expr t)
BM.BoolMapDualUnit -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
BM.BoolMapTerms ((Expr t BaseBoolType, Polarity)
t:|[(Expr t BaseBoolType, Polarity)]
ts) -> 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)
tforall a. a -> [a] -> [a]
:[(Expr t BaseBoolType, Polarity)]
ts)
go (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 forall t (tp :: BaseType) s.
Scope -> Expr t tp -> VarRecorder s t ()
recordExprVars Scope
scope Expr t BaseBoolType
c
forall t s.
Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
recordAssertionVars Scope
scope Polarity
p Expr t BaseBoolType
x
forall t s.
Scope -> Polarity -> Expr t BaseBoolType -> VarRecorder s t ()
recordAssertionVars Scope
scope Polarity
p Expr t BaseBoolType
y
go Expr t BaseBoolType
_ = 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 = forall k s (tp :: k). Nonce s tp -> Word64
indexValue Nonce t tp
n
HashTable s Word64 (Maybe Polarity)
ht <- forall s t a.
ReaderT
(HashTable s Word64 (Maybe Polarity))
(StateT (CollectedVarInfo t) (ST s))
a
-> VarRecorder s t a
VR forall r (m :: Type -> Type). MonadReader r m => m r
ask
Maybe (Maybe Polarity)
mp <- forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
liftST forall a b. (a -> b) -> a -> b
$ 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 -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
Maybe (Maybe Polarity)
_ -> do
VarRecorder s t ()
recurse
forall s (m :: Type -> Type) a. MonadST s m => ST s a -> m a
liftST forall a b. (a -> b) -> a -> b
$ 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 forall a. Maybe a
Nothing
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
_ -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useBitvectors
SemiRingRepr sr
_ -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useLinearArithmetic
recordExprVars Scope
_ StringExpr{} = forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useStrings
recordExprVars Scope
_ FloatExpr{} = forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useFloatingPoint
recordExprVars Scope
_ BoolExpr{} = forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
recordExprVars Scope
scope (NonceAppExpr NonceAppExpr t tp
e0) = do
forall t (tp :: BaseType) s.
Nonce t tp -> VarRecorder s t () -> VarRecorder s t ()
memoExprVars (forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t tp
e0) forall a b. (a -> b) -> a -> b
$ do
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
forall t (tp :: BaseType) s.
Nonce t tp -> VarRecorder s t () -> VarRecorder s t ()
memoExprVars (forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t tp
e0) forall a b. (a -> b) -> a -> b
$ do
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
forall (tp :: BaseType) s t. BaseTypeRepr tp -> VarRecorder s t ()
addFeaturesForVarType (forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar t tp
info)
case forall t (tp :: BaseType). ExprBoundVar t tp -> VarKind
bvarKind ExprBoundVar t tp
info of
VarKind
QuantifierVarKind ->
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
VarKind
LatchVarKind ->
forall s t a.
ReaderT
(HashTable s Word64 (Maybe Polarity))
(StateT (CollectedVarInfo t) (ST s))
a
-> VarRecorder s t a
VR forall a b. (a -> b) -> a -> b
$ forall t.
Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))
latches forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= forall a. Ord a => a -> Set a -> Set a
Set.insert (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some ExprBoundVar t tp
info)
VarKind
UninterpVarKind ->
forall s t a.
ReaderT
(HashTable s Word64 (Maybe Polarity))
(StateT (CollectedVarInfo t) (ST s))
a
-> VarRecorder s t a
VR forall a b. (a -> b) -> a -> b
$ forall t.
Simple Lens (CollectedVarInfo t) (Set (Some (ExprBoundVar t)))
uninterpConstants forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= forall a. Ord a => a -> Set a -> Set a
Set.insert (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 forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SymFnInfo t args ret
symFnInfo ExprSymFn t args ret
f of
UninterpFnInfo{} ->
forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useUninterpFunctions
DefinedFnInfo Assignment (ExprBoundVar t) args
_ Expr t ret
d UnfoldPolicy
_ ->
do forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useDefinedFunctions
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 forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useDefinedFunctions
forall t (tp :: BaseType) s.
Scope -> Expr t tp -> VarRecorder s t ()
recordExprVars Scope
ExistsForall Expr t ret
d
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 = 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 ->
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 ->
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
ea0 BoundQuant
ForallBound ExprBoundVar t tp1
v Expr t BaseBoolType
x
Exists ExprBoundVar t tp1
v Expr t BaseBoolType
x ->
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
ea0 BoundQuant
ExistBound ExprBoundVar t tp1
v Expr t BaseBoolType
x
ArrayFromFn ExprSymFn t (idx ::> itp) ret
f -> do
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
forall t (args :: Ctx BaseType) (ret :: BaseType) s.
ExprSymFn t args ret -> VarRecorder s t ()
recordFnVars ExprSymFn t (ctx ::> d) r
f
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) -> 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
forall t (args :: Ctx BaseType) (ret :: BaseType) s.
ExprSymFn t args ret -> VarRecorder s t ()
recordFnVars ExprSymFn t (idx ::> itp) BaseBoolType
f
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
forall t (args :: Ctx BaseType) (ret :: BaseType) s.
ExprSymFn t args ret -> VarRecorder s t ()
recordFnVars ExprSymFn t args tp
f
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_ (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 -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
AppTheory
LinearArithTheory -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useLinearArithmetic
AppTheory
NonlinearArithTheory -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useNonlinearArithmetic
AppTheory
ComputableArithTheory -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useComputableReals
AppTheory
BitvectorTheory -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useBitvectors
AppTheory
ArrayTheory -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useSymbolicArrays
AppTheory
StructTheory -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useStructs
AppTheory
StringTheory -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useStrings
AppTheory
FloatingPointTheory -> forall s t. ProblemFeatures -> VarRecorder s t ()
addFeatures ProblemFeatures
useFloatingPoint
AppTheory
QuantifierTheory -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
AppTheory
FnTheory -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
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
forall s t. AppTheory -> VarRecorder s t ()
addTheoryFeatures (forall t (tp :: BaseType). App (Expr t) tp -> AppTheory
appTheory (forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t tp
ea0))
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_ (forall t (tp :: BaseType) s.
Scope -> Expr t tp -> VarRecorder s t ()
recordExprVars Scope
scope) (forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t tp
ea0)