{-|
Module      : What4.Expr.Builder
Description : Main definitions of the What4 expression representation
Copyright   : (c) Galois Inc, 2015-2020
License     : BSD3
Maintainer  : jhendrix@galois.com

This module defines the canonical implementation of the solver interface
from "What4.Interface". Type @'ExprBuilder' t st@ is
an instance of the classes 'IsExprBuilder' and 'IsSymExprBuilder'.

Notes regarding concurrency: The expression builder datatype contains
a number of mutable storage locations.  These are designed so they
may reasonably be used in a multithreaded context.  In particular,
nonce values are generated atomically, and other IORefs used in this
module are modified or written atomically, so modifications should
propagate in the expected sequentially-consistent ways.  Of course,
threads may still clobber state others have set (e.g., the current 
program location) so the potential for truly multithreaded use is
somewhat limited.
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module What4.Expr.Builder
  ( -- * ExprBuilder
    ExprBuilder
  , newExprBuilder
  , getSymbolVarBimap
  , sbMakeExpr
  , sbNonceExpr
  , curProgramLoc
  , sbUnaryThreshold
  , sbCacheStartSize
  , sbBVDomainRangeLimit
  , sbUserState
  , exprCounter
  , startCaching
  , stopCaching

    -- * Specialized representations
  , bvUnary
  , intSum
  , realSum
  , bvSum
  , scalarMul

    -- * configuration options
  , unaryThresholdOption
  , bvdomainRangeLimitOption
  , cacheStartSizeOption
  , cacheTerms

    -- * Expr
  , Expr(..)
  , asApp
  , asNonceApp
  , iteSize
  , exprLoc
  , ppExpr
  , ppExprTop
  , exprMaybeId
  , asConjunction
  , asDisjunction
  , Polarity(..)
  , BM.negatePolarity
    -- ** AppExpr
  , AppExpr
  , appExprId
  , appExprLoc
  , appExprApp
    -- ** NonceAppExpr
  , NonceAppExpr
  , nonceExprId
  , nonceExprLoc
  , nonceExprApp
    -- ** Type abbreviations
  , BoolExpr
  , IntegerExpr
  , RealExpr
  , FloatExpr
  , BVExpr
  , CplxExpr
  , StringExpr

    -- * App
  , App(..)
  , traverseApp
  , appType
    -- * NonceApp
  , NonceApp(..)
  , nonceAppType

    -- * Bound Variable information
  , ExprBoundVar
  , bvarId
  , bvarLoc
  , bvarName
  , bvarType
  , bvarKind
  , bvarAbstractValue
  , VarKind(..)
  , boundVars
  , ppBoundVar
  , evalBoundVars

    -- * Symbolic Function
  , ExprSymFn(..)
  , SymFnInfo(..)
  , symFnArgTypes
  , symFnReturnType

    -- * SymbolVarBimap
  , SymbolVarBimap
  , SymbolBinding(..)
  , emptySymbolVarBimap
  , lookupBindingOfSymbol
  , lookupSymbolOfBinding

    -- * IdxCache
  , IdxCache
  , newIdxCache
  , lookupIdx
  , lookupIdxValue
  , insertIdxValue
  , deleteIdxValue
  , clearIdxCache
  , idxCacheEval
  , idxCacheEval'

    -- * Flags
  , type FloatMode
  , FloatModeRepr(..)
  , FloatIEEE
  , FloatUninterpreted
  , FloatReal
  , Flags

    -- * BV Or Set
  , BVOrSet
  , bvOrToList
  , bvOrSingleton
  , bvOrInsert
  , bvOrUnion
  , bvOrAbs
  , traverseBVOrSet

    -- * Re-exports
  , SymExpr
  , What4.Interface.bvWidth
  , What4.Interface.exprType
  , What4.Interface.IndexLit(..)
  , What4.Interface.ArrayResultWrapper(..)
  ) where

import qualified Control.Exception as Ex
import           Control.Lens hiding (asIndex, (:>), Empty)
import           Control.Monad
import           Control.Monad.IO.Class
import           Control.Monad.ST
import           Control.Monad.Trans.Writer.Strict (writer, runWriter)
import qualified Data.BitVector.Sized as BV
import           Data.Bimap (Bimap)
import qualified Data.Bimap as Bimap
import qualified Data.Binary.IEEE754 as IEEE754
import           Data.Hashable
import           Data.IORef
import           Data.Kind
import           Data.List.NonEmpty (NonEmpty(..))
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Maybe
import           Data.Monoid (Any(..))
import           Data.Parameterized.Classes
import           Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.HashTable as PH
import qualified Data.Parameterized.Map as PM
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Nonce
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC
import           Data.Ratio (numerator, denominator)
import           Data.Set (Set)
import qualified Data.Set as Set
import qualified LibBF as BF

import           What4.BaseTypes
import           What4.Concrete
import qualified What4.Config as CFG
import           What4.Interface
import           What4.InterpretedFloatingPoint
import           What4.ProgramLoc
import qualified What4.SemiRing as SR
import           What4.Symbol
import           What4.Expr.App
import qualified What4.Expr.ArrayUpdateMap as AUM
import           What4.Expr.BoolMap (BoolMap, Polarity(..), BoolMapView(..))
import qualified What4.Expr.BoolMap as BM
import           What4.Expr.MATLAB
import           What4.Expr.WeightedSum (WeightedSum, SemiRingProduct)
import qualified What4.Expr.WeightedSum as WSum
import qualified What4.Expr.StringSeq as SSeq
import           What4.Expr.UnaryBV (UnaryBV)
import qualified What4.Expr.UnaryBV as UnaryBV

import           What4.Utils.AbstractDomains
import           What4.Utils.Arithmetic
import qualified What4.Utils.BVDomain as BVD
import           What4.Utils.Complex
import           What4.Utils.FloatHelpers
import           What4.Utils.StringLiteral

------------------------------------------------------------------------
-- Utilities

toDouble :: Rational -> Double
toDouble :: Rational -> Double
toDouble = Rational -> Double
forall a. Fractional a => Rational -> a
fromRational

cachedEval :: (HashableF k, TestEquality k)
           => PH.HashTable RealWorld k a
           -> k tp
           -> IO (a tp)
           -> IO (a tp)
cachedEval :: HashTable RealWorld k a -> k tp -> IO (a tp) -> IO (a tp)
cachedEval HashTable RealWorld k a
tbl k tp
k IO (a tp)
action = do
  Maybe (a tp)
mr <- ST RealWorld (Maybe (a tp)) -> IO (Maybe (a tp))
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (Maybe (a tp)) -> IO (Maybe (a tp)))
-> ST RealWorld (Maybe (a tp)) -> IO (Maybe (a tp))
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld k a -> k tp -> ST RealWorld (Maybe (a tp))
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s (Maybe (val tp))
PH.lookup HashTable RealWorld k a
tbl k tp
k
  case Maybe (a tp)
mr of
    Just a tp
r -> a tp -> IO (a tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return a tp
r
    Maybe (a tp)
Nothing -> do
      a tp
r <- IO (a tp)
action
      a tp -> IO (a tp) -> IO (a tp)
seq a tp
r (IO (a tp) -> IO (a tp)) -> IO (a tp) -> IO (a tp)
forall a b. (a -> b) -> a -> b
$ do
      ST RealWorld () -> IO ()
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld () -> IO ()) -> ST RealWorld () -> IO ()
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld k a -> k tp -> a tp -> ST RealWorld ()
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
PH.insert HashTable RealWorld k a
tbl k tp
k a tp
r
      a tp -> IO (a tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return a tp
r

------------------------------------------------------------------------
-- SymbolVarBimap

-- | A bijective map between vars and their canonical name for printing
-- purposes.
-- Parameter @t@ is a phantom type brand used to track nonces.
newtype SymbolVarBimap t = SymbolVarBimap (Bimap SolverSymbol (SymbolBinding t))

-- | This describes what a given SolverSymbol is associated with.
-- Parameter @t@ is a phantom type brand used to track nonces.
data SymbolBinding t
   = forall tp . VarSymbolBinding !(ExprBoundVar t tp)
     -- ^ Solver
   | forall args ret . FnSymbolBinding  !(ExprSymFn t args ret)

instance Eq (SymbolBinding t) where
  VarSymbolBinding ExprBoundVar t tp
x == :: SymbolBinding t -> SymbolBinding t -> Bool
== VarSymbolBinding ExprBoundVar t tp
y = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (ExprBoundVar t tp -> ExprBoundVar t tp -> Maybe (tp :~: tp)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality ExprBoundVar t tp
x ExprBoundVar t tp
y)
  FnSymbolBinding  ExprSymFn t args ret
x == FnSymbolBinding  ExprSymFn t args ret
y = Maybe ((args ::> ret) :~: (args ::> ret)) -> Bool
forall a. Maybe a -> Bool
isJust (Nonce t (args ::> ret)
-> Nonce t (args ::> ret)
-> Maybe ((args ::> ret) :~: (args ::> ret))
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (ExprSymFn t args ret -> Nonce t (args ::> ret)
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
symFnId ExprSymFn t args ret
x) (ExprSymFn t args ret -> Nonce t (args ::> ret)
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
symFnId ExprSymFn t args ret
y))
  SymbolBinding t
_ == SymbolBinding t
_ = Bool
False

instance Ord (SymbolBinding t) where
  compare :: SymbolBinding t -> SymbolBinding t -> Ordering
compare (VarSymbolBinding ExprBoundVar t tp
x) (VarSymbolBinding ExprBoundVar t tp
y) =
    OrderingF tp tp -> Ordering
forall k (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (ExprBoundVar t tp -> ExprBoundVar t tp -> OrderingF tp tp
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF ExprBoundVar t tp
x ExprBoundVar t tp
y)
  compare VarSymbolBinding{} SymbolBinding t
_ = Ordering
LT
  compare SymbolBinding t
_ VarSymbolBinding{} = Ordering
GT
  compare (FnSymbolBinding  ExprSymFn t args ret
x) (FnSymbolBinding  ExprSymFn t args ret
y) =
    OrderingF (args ::> ret) (args ::> ret) -> Ordering
forall k (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (Nonce t (args ::> ret)
-> Nonce t (args ::> ret)
-> OrderingF (args ::> ret) (args ::> ret)
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF (ExprSymFn t args ret -> Nonce t (args ::> ret)
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
symFnId ExprSymFn t args ret
x) (ExprSymFn t args ret -> Nonce t (args ::> ret)
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
symFnId ExprSymFn t args ret
y))

-- | Empty symbol var bimap
emptySymbolVarBimap :: SymbolVarBimap t
emptySymbolVarBimap :: SymbolVarBimap t
emptySymbolVarBimap = Bimap SolverSymbol (SymbolBinding t) -> SymbolVarBimap t
forall t. Bimap SolverSymbol (SymbolBinding t) -> SymbolVarBimap t
SymbolVarBimap Bimap SolverSymbol (SymbolBinding t)
forall a b. Bimap a b
Bimap.empty

lookupBindingOfSymbol :: SolverSymbol -> SymbolVarBimap t -> Maybe (SymbolBinding t)
lookupBindingOfSymbol :: SolverSymbol -> SymbolVarBimap t -> Maybe (SymbolBinding t)
lookupBindingOfSymbol SolverSymbol
s (SymbolVarBimap Bimap SolverSymbol (SymbolBinding t)
m) = SolverSymbol
-> Bimap SolverSymbol (SymbolBinding t) -> Maybe (SymbolBinding t)
forall a b (m :: Type -> Type).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
Bimap.lookup SolverSymbol
s Bimap SolverSymbol (SymbolBinding t)
m

lookupSymbolOfBinding :: SymbolBinding t -> SymbolVarBimap t -> Maybe SolverSymbol
lookupSymbolOfBinding :: SymbolBinding t -> SymbolVarBimap t -> Maybe SolverSymbol
lookupSymbolOfBinding SymbolBinding t
b (SymbolVarBimap Bimap SolverSymbol (SymbolBinding t)
m) = SymbolBinding t
-> Bimap SolverSymbol (SymbolBinding t) -> Maybe SolverSymbol
forall a b (m :: Type -> Type).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR SymbolBinding t
b Bimap SolverSymbol (SymbolBinding t)
m

------------------------------------------------------------------------
-- MatlabSolverFn

-- Parameter @t@ is a phantom type brand used to track nonces.
data MatlabFnWrapper t c where
   MatlabFnWrapper :: !(MatlabSolverFn (Expr t) a r) -> MatlabFnWrapper t (a::> r)

instance TestEquality (MatlabFnWrapper t) where
  testEquality :: MatlabFnWrapper t a -> MatlabFnWrapper t b -> Maybe (a :~: b)
testEquality (MatlabFnWrapper MatlabSolverFn (Expr t) a r
f) (MatlabFnWrapper MatlabSolverFn (Expr t) a r
g) = do
    (a ::> r) :~: (a ::> r)
Refl <- MatlabSolverFn (Expr t) a r
-> MatlabSolverFn (Expr t) a r -> Maybe ((a ::> r) :~: (a ::> r))
forall (f :: BaseType -> Type) (ax :: Ctx BaseType)
       (rx :: BaseType) (ay :: Ctx BaseType) (ry :: BaseType).
TestEquality f =>
MatlabSolverFn f ax rx
-> MatlabSolverFn f ay ry -> Maybe ((ax ::> rx) :~: (ay ::> ry))
testSolverFnEq MatlabSolverFn (Expr t) a r
f MatlabSolverFn (Expr t) a r
g
    (a :~: a) -> Maybe (a :~: a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
forall k (a :: k). a :~: a
Refl


instance HashableF (MatlabFnWrapper t) where
  hashWithSaltF :: Int -> MatlabFnWrapper t tp -> Int
hashWithSaltF Int
s (MatlabFnWrapper MatlabSolverFn (Expr t) a r
f) = Int -> MatlabSolverFn (Expr t) a r -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s MatlabSolverFn (Expr t) a r
f

data ExprSymFnWrapper t c
   = forall a r . (c ~ (a ::> r)) => ExprSymFnWrapper (ExprSymFn t a r)

data SomeSymFn sym = forall args ret . SomeSymFn (SymFn sym args ret)

------------------------------------------------------------------------
-- ExprBuilder

-- | Mode flag for how floating-point values should be interpreted.
data FloatMode where
  FloatIEEE :: FloatMode
  FloatUninterpreted :: FloatMode
  FloatReal :: FloatMode
type FloatIEEE = 'FloatIEEE
type FloatUninterpreted = 'FloatUninterpreted
type FloatReal = 'FloatReal

data Flags (fi :: FloatMode)


data FloatModeRepr :: FloatMode -> Type where
  FloatIEEERepr          :: FloatModeRepr FloatIEEE
  FloatUninterpretedRepr :: FloatModeRepr FloatUninterpreted
  FloatRealRepr          :: FloatModeRepr FloatReal

instance Show (FloatModeRepr fm) where
  showsPrec :: Int -> FloatModeRepr fm -> ShowS
showsPrec Int
_ FloatModeRepr fm
FloatIEEERepr          = String -> ShowS
showString String
"FloatIEEE"
  showsPrec Int
_ FloatModeRepr fm
FloatUninterpretedRepr = String -> ShowS
showString String
"FloatUninterpreted"
  showsPrec Int
_ FloatModeRepr fm
FloatRealRepr          = String -> ShowS
showString String
"FloatReal"

instance ShowF FloatModeRepr

instance KnownRepr FloatModeRepr FloatIEEE          where knownRepr :: FloatModeRepr FloatIEEE
knownRepr = FloatModeRepr FloatIEEE
FloatIEEERepr
instance KnownRepr FloatModeRepr FloatUninterpreted where knownRepr :: FloatModeRepr FloatUninterpreted
knownRepr = FloatModeRepr FloatUninterpreted
FloatUninterpretedRepr
instance KnownRepr FloatModeRepr FloatReal          where knownRepr :: FloatModeRepr FloatReal
knownRepr = FloatModeRepr FloatReal
FloatRealRepr

instance TestEquality FloatModeRepr where
  testEquality :: FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b)
testEquality FloatModeRepr a
FloatIEEERepr           FloatModeRepr b
FloatIEEERepr           = (a :~: a) -> Maybe (a :~: a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality FloatModeRepr a
FloatUninterpretedRepr  FloatModeRepr b
FloatUninterpretedRepr  = (a :~: a) -> Maybe (a :~: a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality FloatModeRepr a
FloatRealRepr           FloatModeRepr b
FloatRealRepr           = (a :~: a) -> Maybe (a :~: a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality FloatModeRepr a
_ FloatModeRepr b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing


-- | Cache for storing dag terms.
-- Parameter @t@ is a phantom type brand used to track nonces.
data ExprBuilder t (st :: Type -> Type) (fs :: Type)
   = forall fm. (fs ~ (Flags fm)) =>
     SB { ExprBuilder t st fs -> BoolExpr t
sbTrue  :: !(BoolExpr t)
        , ExprBuilder t st fs -> BoolExpr t
sbFalse :: !(BoolExpr t)
          -- | Constant zero.
        , ExprBuilder t st fs -> RealExpr t
sbZero  :: !(RealExpr t)
          -- | Configuration object for this symbolic backend
        , ExprBuilder t st fs -> Config
sbConfiguration :: !CFG.Config
          -- | Flag used to tell the backend whether to evaluate
          -- ground rational values as double precision floats when
          -- a function cannot be evaluated as a rational.
        , ExprBuilder t st fs -> Bool
sbFloatReduce :: !Bool
          -- | The maximum number of distinct values a term may have and use the
          -- unary representation.
        , ExprBuilder t st fs -> OptionSetting BaseIntegerType
sbUnaryThreshold :: !(CFG.OptionSetting BaseIntegerType)
          -- | The maximum number of distinct ranges in a BVDomain expression.
        , ExprBuilder t st fs -> OptionSetting BaseIntegerType
sbBVDomainRangeLimit :: !(CFG.OptionSetting BaseIntegerType)
          -- | The starting size when building a new cache
        , ExprBuilder t st fs -> OptionSetting BaseIntegerType
sbCacheStartSize :: !(CFG.OptionSetting BaseIntegerType)
          -- | Counter to generate new unique identifiers for elements and functions.
        , ExprBuilder t st fs -> NonceGenerator IO t
exprCounter :: !(NonceGenerator IO t)
          -- | Reference to current allocator for expressions.
        , ExprBuilder t st fs -> IORef (ExprAllocator t)
curAllocator :: !(IORef (ExprAllocator t))
          -- | Number of times an 'Expr' for a non-linear operation has been
          -- created.
        , ExprBuilder t st fs -> IORef Integer
sbNonLinearOps :: !(IORef Integer)
          -- | The current program location
        , ExprBuilder t st fs -> IORef ProgramLoc
sbProgramLoc :: !(IORef ProgramLoc)
          -- | Additional state maintained by the state manager
        , ExprBuilder t st fs -> st t
sbUserState :: !(st t)

        , ExprBuilder t st fs -> IORef (SymbolVarBimap t)
sbVarBindings :: !(IORef (SymbolVarBimap t))
        , ExprBuilder t st fs
-> IORef
     (Map
        (SolverSymbol, Some (Assignment BaseTypeRepr))
        (SomeSymFn (ExprBuilder t st fs)))
sbUninterpFnCache :: !(IORef (Map (SolverSymbol, Some (Ctx.Assignment BaseTypeRepr)) (SomeSymFn (ExprBuilder t st fs))))
          -- | Cache for Matlab functions
        , ExprBuilder t st fs
-> HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t)
sbMatlabFnCache
          :: !(PH.HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))
        , ExprBuilder t st fs -> IORef (Maybe (SolverEvent -> IO ()))
sbSolverLogger
          :: !(IORef (Maybe (SolverEvent -> IO ())))
          -- | Flag dictating how floating-point values/operations are translated
          -- when passed to the solver.
        , ()
sbFloatMode :: !(FloatModeRepr fm)
        }

type instance SymFn (ExprBuilder t st fs) = ExprSymFn t
type instance SymExpr (ExprBuilder t st fs) = Expr t
type instance BoundVar (ExprBuilder t st fs) = ExprBoundVar t
type instance SymAnnotation (ExprBuilder t st fs) = Nonce t

------------------------------------------------------------------------
-- | ExprAllocator provides an interface for creating expressions from
-- an applications.
-- Parameter @t@ is a phantom type brand used to track nonces.
data ExprAllocator t
   = ExprAllocator { ExprAllocator t
-> forall (tp :: BaseType).
   ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
appExpr  :: forall tp
                            .  ProgramLoc
                            -> App (Expr t) tp
                            -> AbstractValue tp
                            -> IO (Expr t tp)
                  , ExprAllocator t
-> forall (tp :: BaseType).
   ProgramLoc
   -> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
nonceExpr :: forall tp
                             .  ProgramLoc
                             -> NonceApp t (Expr t) tp
                             -> AbstractValue tp
                             -> IO (Expr t tp)
                  }


------------------------------------------------------------------------
-- Uncached storage

-- | Create a new storage that does not do hash consing.
newStorage :: NonceGenerator IO t -> IO (ExprAllocator t)
newStorage :: NonceGenerator IO t -> IO (ExprAllocator t)
newStorage NonceGenerator IO t
g = do
  ExprAllocator t -> IO (ExprAllocator t)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExprAllocator t -> IO (ExprAllocator t))
-> ExprAllocator t -> IO (ExprAllocator t)
forall a b. (a -> b) -> a -> b
$! ExprAllocator :: forall t.
(forall (tp :: BaseType).
 ProgramLoc
 -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp))
-> (forall (tp :: BaseType).
    ProgramLoc
    -> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp))
-> ExprAllocator t
ExprAllocator { appExpr :: forall (tp :: BaseType).
ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
appExpr = NonceGenerator IO t
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
forall t (tp :: BaseType).
NonceGenerator IO t
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedExprFn NonceGenerator IO t
g
                         , nonceExpr :: forall (tp :: BaseType).
ProgramLoc
-> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
nonceExpr = NonceGenerator IO t
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
forall t (tp :: BaseType).
NonceGenerator IO t
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedNonceExpr NonceGenerator IO t
g
                         }

uncachedExprFn :: NonceGenerator IO t
              -> ProgramLoc
              -> App (Expr t) tp
              -> AbstractValue tp
              -> IO (Expr t tp)
uncachedExprFn :: NonceGenerator IO t
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedExprFn NonceGenerator IO t
g ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v = do
  Nonce t tp
n <- NonceGenerator IO t -> IO (Nonce t tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
  Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr t tp -> IO (Expr t tp)) -> Expr t tp -> IO (Expr t tp)
forall a b. (a -> b) -> a -> b
$! Nonce t tp
-> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
mkExpr Nonce t tp
n ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v

uncachedNonceExpr :: NonceGenerator IO t
                 -> ProgramLoc
                 -> NonceApp t (Expr t) tp
                 -> AbstractValue tp
                 -> IO (Expr t tp)
uncachedNonceExpr :: NonceGenerator IO t
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedNonceExpr NonceGenerator IO t
g ProgramLoc
pc NonceApp t (Expr t) tp
p AbstractValue tp
v = do
  Nonce t tp
n <- NonceGenerator IO t -> IO (Nonce t tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
  Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr t tp -> IO (Expr t tp)) -> Expr t tp -> IO (Expr t tp)
forall a b. (a -> b) -> a -> b
$! NonceAppExpr t tp -> Expr t tp
forall t (tp :: BaseType). NonceAppExpr t tp -> Expr t tp
NonceAppExpr (NonceAppExpr t tp -> Expr t tp) -> NonceAppExpr t tp -> Expr t tp
forall a b. (a -> b) -> a -> b
$ NonceAppExprCtor :: forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> NonceAppExpr t tp
NonceAppExprCtor { nonceExprId :: Nonce t tp
nonceExprId = Nonce t tp
n
                                          , nonceExprLoc :: ProgramLoc
nonceExprLoc = ProgramLoc
pc
                                          , nonceExprApp :: NonceApp t (Expr t) tp
nonceExprApp = NonceApp t (Expr t) tp
p
                                          , nonceExprAbsValue :: AbstractValue tp
nonceExprAbsValue = AbstractValue tp
v
                                          }

------------------------------------------------------------------------
-- Cached storage

cachedNonceExpr :: NonceGenerator IO t
               -> PH.HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
               -> ProgramLoc
               -> NonceApp t (Expr t) tp
               -> AbstractValue tp
               -> IO (Expr t tp)
cachedNonceExpr :: NonceGenerator IO t
-> HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedNonceExpr NonceGenerator IO t
g HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
h ProgramLoc
pc NonceApp t (Expr t) tp
p AbstractValue tp
v = do
  Maybe (Expr t tp)
me <- ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp)))
-> ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> NonceApp t (Expr t) tp -> ST RealWorld (Maybe (Expr t tp))
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s (Maybe (val tp))
PH.lookup HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
h NonceApp t (Expr t) tp
p
  case Maybe (Expr t tp)
me of
    Just Expr t tp
e -> Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e
    Maybe (Expr t tp)
Nothing -> do
      Nonce t tp
n <- NonceGenerator IO t -> IO (Nonce t tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
      let e :: Expr t tp
e = NonceAppExpr t tp -> Expr t tp
forall t (tp :: BaseType). NonceAppExpr t tp -> Expr t tp
NonceAppExpr (NonceAppExpr t tp -> Expr t tp) -> NonceAppExpr t tp -> Expr t tp
forall a b. (a -> b) -> a -> b
$ NonceAppExprCtor :: forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> NonceAppExpr t tp
NonceAppExprCtor { nonceExprId :: Nonce t tp
nonceExprId = Nonce t tp
n
                                            , nonceExprLoc :: ProgramLoc
nonceExprLoc = ProgramLoc
pc
                                            , nonceExprApp :: NonceApp t (Expr t) tp
nonceExprApp = NonceApp t (Expr t) tp
p
                                            , nonceExprAbsValue :: AbstractValue tp
nonceExprAbsValue = AbstractValue tp
v
                                            }
      Expr t tp -> IO () -> IO ()
seq Expr t tp
e (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ ST RealWorld () -> IO ()
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld () -> IO ()) -> ST RealWorld () -> IO ()
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> NonceApp t (Expr t) tp -> Expr t tp -> ST RealWorld ()
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
PH.insert HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
h NonceApp t (Expr t) tp
p Expr t tp
e
      Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr t tp -> IO (Expr t tp)) -> Expr t tp -> IO (Expr t tp)
forall a b. (a -> b) -> a -> b
$! Expr t tp
e


cachedAppExpr :: forall t tp
               . NonceGenerator IO t
              -> PH.HashTable RealWorld (App (Expr t)) (Expr t)
              -> ProgramLoc
              -> App (Expr t) tp
              -> AbstractValue tp
              -> IO (Expr t tp)
cachedAppExpr :: NonceGenerator IO t
-> HashTable RealWorld (App (Expr t)) (Expr t)
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedAppExpr NonceGenerator IO t
g HashTable RealWorld (App (Expr t)) (Expr t)
h ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v = do
  Maybe (Expr t tp)
me <- ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp)))
-> ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (App (Expr t)) (Expr t)
-> App (Expr t) tp -> ST RealWorld (Maybe (Expr t tp))
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s (Maybe (val tp))
PH.lookup HashTable RealWorld (App (Expr t)) (Expr t)
h App (Expr t) tp
a
  case Maybe (Expr t tp)
me of
    Just Expr t tp
e -> Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e
    Maybe (Expr t tp)
Nothing -> do
      Nonce t tp
n <- NonceGenerator IO t -> IO (Nonce t tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
      let e :: Expr t tp
e = Nonce t tp
-> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
mkExpr Nonce t tp
n ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v
      Expr t tp -> IO () -> IO ()
seq Expr t tp
e (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ ST RealWorld () -> IO ()
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld () -> IO ()) -> ST RealWorld () -> IO ()
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (App (Expr t)) (Expr t)
-> App (Expr t) tp -> Expr t tp -> ST RealWorld ()
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
PH.insert HashTable RealWorld (App (Expr t)) (Expr t)
h App (Expr t) tp
a Expr t tp
e
      Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e

-- | Create a storage that does hash consing.
newCachedStorage :: forall t
                  . NonceGenerator IO t
                 -> Int
                 -> IO (ExprAllocator t)
newCachedStorage :: NonceGenerator IO t -> Int -> IO (ExprAllocator t)
newCachedStorage NonceGenerator IO t
g Int
sz = ST RealWorld (ExprAllocator t) -> IO (ExprAllocator t)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (ExprAllocator t) -> IO (ExprAllocator t))
-> ST RealWorld (ExprAllocator t) -> IO (ExprAllocator t)
forall a b. (a -> b) -> a -> b
$ do
  HashTable RealWorld (App (Expr t)) (Expr t)
appCache  <- Int -> ST RealWorld (HashTable RealWorld (App (Expr t)) (Expr t))
forall k1 s (k2 :: k1 -> Type) (v :: k1 -> Type).
Int -> ST s (HashTable s k2 v)
PH.newSized Int
sz
  HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
predCache <- Int
-> ST
     RealWorld (HashTable RealWorld (NonceApp t (Expr t)) (Expr t))
forall k1 s (k2 :: k1 -> Type) (v :: k1 -> Type).
Int -> ST s (HashTable s k2 v)
PH.newSized Int
sz
  ExprAllocator t -> ST RealWorld (ExprAllocator t)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExprAllocator t -> ST RealWorld (ExprAllocator t))
-> ExprAllocator t -> ST RealWorld (ExprAllocator t)
forall a b. (a -> b) -> a -> b
$ ExprAllocator :: forall t.
(forall (tp :: BaseType).
 ProgramLoc
 -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp))
-> (forall (tp :: BaseType).
    ProgramLoc
    -> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp))
-> ExprAllocator t
ExprAllocator { appExpr :: forall (tp :: BaseType).
ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
appExpr = NonceGenerator IO t
-> HashTable RealWorld (App (Expr t)) (Expr t)
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
forall t (tp :: BaseType).
NonceGenerator IO t
-> HashTable RealWorld (App (Expr t)) (Expr t)
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedAppExpr NonceGenerator IO t
g HashTable RealWorld (App (Expr t)) (Expr t)
appCache
                        , nonceExpr :: forall (tp :: BaseType).
ProgramLoc
-> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
nonceExpr = NonceGenerator IO t
-> HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
forall t (tp :: BaseType).
NonceGenerator IO t
-> HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedNonceExpr NonceGenerator IO t
g HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
predCache
                        }


------------------------------------------------------------------------
-- IdxCache

-- | An IdxCache is used to map expressions with type @Expr t tp@ to
-- values with a corresponding type @f tp@. It is a mutable map using
-- an 'IO' hash table. Parameter @t@ is a phantom type brand used to
-- track nonces.
newtype IdxCache t (f :: BaseType -> Type)
      = IdxCache { IdxCache t f -> IORef (MapF (Nonce t) f)
cMap :: IORef (PM.MapF (Nonce t) f) }

-- | Create a new IdxCache
newIdxCache :: MonadIO m => m (IdxCache t f)
newIdxCache :: m (IdxCache t f)
newIdxCache = IO (IdxCache t f) -> m (IdxCache t f)
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (IdxCache t f) -> m (IdxCache t f))
-> IO (IdxCache t f) -> m (IdxCache t f)
forall a b. (a -> b) -> a -> b
$ IORef (MapF (Nonce t) f) -> IdxCache t f
forall t (f :: BaseType -> Type).
IORef (MapF (Nonce t) f) -> IdxCache t f
IdxCache (IORef (MapF (Nonce t) f) -> IdxCache t f)
-> IO (IORef (MapF (Nonce t) f)) -> IO (IdxCache t f)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> MapF (Nonce t) f -> IO (IORef (MapF (Nonce t) f))
forall a. a -> IO (IORef a)
newIORef MapF (Nonce t) f
forall v (k :: v -> Type) (a :: v -> Type). MapF k a
PM.empty

{-# INLINE lookupIdxValue #-}
-- | Return the value associated to the expr in the index.
lookupIdxValue :: MonadIO m => IdxCache t f -> Expr t tp -> m (Maybe (f tp))
lookupIdxValue :: IdxCache t f -> Expr t tp -> m (Maybe (f tp))
lookupIdxValue IdxCache t f
_ SemiRingLiteral{} = Maybe (f tp) -> m (Maybe (f tp))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (f tp)
forall a. Maybe a
Nothing
lookupIdxValue IdxCache t f
_ StringExpr{} = Maybe (f tp) -> m (Maybe (f tp))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (f tp)
forall a. Maybe a
Nothing
lookupIdxValue IdxCache t f
_ BoolExpr{} = Maybe (f tp) -> m (Maybe (f tp))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (f tp)
forall a. Maybe a
Nothing
lookupIdxValue IdxCache t f
_ FloatExpr{} = Maybe (f tp) -> m (Maybe (f tp))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (f tp)
forall a. Maybe a
Nothing
lookupIdxValue IdxCache t f
c (NonceAppExpr NonceAppExpr t tp
e) = IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
forall (m :: Type -> Type) t (f :: BaseType -> Type)
       (tp :: BaseType).
MonadIO m =>
IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
lookupIdx IdxCache t f
c (NonceAppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t tp
e)
lookupIdxValue IdxCache t f
c (AppExpr AppExpr t tp
e)  = IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
forall (m :: Type -> Type) t (f :: BaseType -> Type)
       (tp :: BaseType).
MonadIO m =>
IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
lookupIdx IdxCache t f
c (AppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t tp
e)
lookupIdxValue IdxCache t f
c (BoundVarExpr ExprBoundVar t tp
i) = IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
forall (m :: Type -> Type) t (f :: BaseType -> Type)
       (tp :: BaseType).
MonadIO m =>
IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
lookupIdx IdxCache t f
c (ExprBoundVar t tp -> Nonce t tp
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t tp
i)

{-# INLINE lookupIdx #-}
lookupIdx :: (MonadIO m) => IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
lookupIdx :: IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
lookupIdx IdxCache t f
c Nonce t tp
n = IO (Maybe (f tp)) -> m (Maybe (f tp))
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe (f tp)) -> m (Maybe (f tp)))
-> IO (Maybe (f tp)) -> m (Maybe (f tp))
forall a b. (a -> b) -> a -> b
$ Nonce t tp -> MapF (Nonce t) f -> Maybe (f tp)
forall v (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
PM.lookup Nonce t tp
n (MapF (Nonce t) f -> Maybe (f tp))
-> IO (MapF (Nonce t) f) -> IO (Maybe (f tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (MapF (Nonce t) f) -> IO (MapF (Nonce t) f)
forall a. IORef a -> IO a
readIORef (IdxCache t f -> IORef (MapF (Nonce t) f)
forall t (f :: BaseType -> Type).
IdxCache t f -> IORef (MapF (Nonce t) f)
cMap IdxCache t f
c)

{-# INLINE insertIdxValue #-}
-- | Bind the value to the given expr in the index.
insertIdxValue :: MonadIO m => IdxCache t f -> Nonce t tp -> f tp -> m ()
insertIdxValue :: IdxCache t f -> Nonce t tp -> f tp -> m ()
insertIdxValue IdxCache t f
c Nonce t tp
e f tp
v = f tp -> m () -> m ()
seq f tp
v (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> m ()
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef (MapF (Nonce t) f)
-> (MapF (Nonce t) f -> (MapF (Nonce t) f, ())) -> IO ()
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' (IdxCache t f -> IORef (MapF (Nonce t) f)
forall t (f :: BaseType -> Type).
IdxCache t f -> IORef (MapF (Nonce t) f)
cMap IdxCache t f
c) ((MapF (Nonce t) f -> (MapF (Nonce t) f, ())) -> IO ())
-> (MapF (Nonce t) f -> (MapF (Nonce t) f, ())) -> IO ()
forall a b. (a -> b) -> a -> b
$ (\MapF (Nonce t) f
m -> (Nonce t tp -> f tp -> MapF (Nonce t) f -> MapF (Nonce t) f
forall v (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
PM.insert Nonce t tp
e f tp
v MapF (Nonce t) f
m, ()))

{-# INLINE deleteIdxValue #-}
-- | Remove a value from the IdxCache
deleteIdxValue :: MonadIO m => IdxCache t f -> Nonce t (tp :: BaseType) -> m ()
deleteIdxValue :: IdxCache t f -> Nonce t tp -> m ()
deleteIdxValue IdxCache t f
c Nonce t tp
e = IO () -> m ()
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef (MapF (Nonce t) f)
-> (MapF (Nonce t) f -> (MapF (Nonce t) f, ())) -> IO ()
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' (IdxCache t f -> IORef (MapF (Nonce t) f)
forall t (f :: BaseType -> Type).
IdxCache t f -> IORef (MapF (Nonce t) f)
cMap IdxCache t f
c) ((MapF (Nonce t) f -> (MapF (Nonce t) f, ())) -> IO ())
-> (MapF (Nonce t) f -> (MapF (Nonce t) f, ())) -> IO ()
forall a b. (a -> b) -> a -> b
$ (\MapF (Nonce t) f
m -> (Nonce t tp -> MapF (Nonce t) f -> MapF (Nonce t) f
forall v (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> MapF k a
PM.delete Nonce t tp
e MapF (Nonce t) f
m, ()))

-- | Remove all values from the IdxCache
clearIdxCache :: MonadIO m => IdxCache t f -> m ()
clearIdxCache :: IdxCache t f -> m ()
clearIdxCache IdxCache t f
c = IO () -> m ()
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef (MapF (Nonce t) f) -> MapF (Nonce t) f -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef (IdxCache t f -> IORef (MapF (Nonce t) f)
forall t (f :: BaseType -> Type).
IdxCache t f -> IORef (MapF (Nonce t) f)
cMap IdxCache t f
c) MapF (Nonce t) f
forall v (k :: v -> Type) (a :: v -> Type). MapF k a
PM.empty

exprMaybeId :: Expr t tp -> Maybe (Nonce t tp)
exprMaybeId :: Expr t tp -> Maybe (Nonce t tp)
exprMaybeId SemiRingLiteral{} = Maybe (Nonce t tp)
forall a. Maybe a
Nothing
exprMaybeId StringExpr{} = Maybe (Nonce t tp)
forall a. Maybe a
Nothing
exprMaybeId BoolExpr{} = Maybe (Nonce t tp)
forall a. Maybe a
Nothing
exprMaybeId FloatExpr{} = Maybe (Nonce t tp)
forall a. Maybe a
Nothing
exprMaybeId (NonceAppExpr NonceAppExpr t tp
e) = Nonce t tp -> Maybe (Nonce t tp)
forall a. a -> Maybe a
Just (Nonce t tp -> Maybe (Nonce t tp))
-> Nonce t tp -> Maybe (Nonce t tp)
forall a b. (a -> b) -> a -> b
$! NonceAppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t tp
e
exprMaybeId (AppExpr  AppExpr t tp
e) = Nonce t tp -> Maybe (Nonce t tp)
forall a. a -> Maybe a
Just (Nonce t tp -> Maybe (Nonce t tp))
-> Nonce t tp -> Maybe (Nonce t tp)
forall a b. (a -> b) -> a -> b
$! AppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t tp
e
exprMaybeId (BoundVarExpr ExprBoundVar t tp
e) = Nonce t tp -> Maybe (Nonce t tp)
forall a. a -> Maybe a
Just (Nonce t tp -> Maybe (Nonce t tp))
-> Nonce t tp -> Maybe (Nonce t tp)
forall a b. (a -> b) -> a -> b
$! ExprBoundVar t tp -> Nonce t tp
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t tp
e

-- | Implements a cached evaluated using the given element.  Given an element
-- this function returns the value of the element if bound, and otherwise
-- calls the evaluation function, stores the result in the cache, and
-- returns the value.
{-# INLINE idxCacheEval #-}
idxCacheEval :: (MonadIO m)
             => IdxCache t f
             -> Expr t tp
             -> m (f tp)
             -> m (f tp)
idxCacheEval :: IdxCache t f -> Expr t tp -> m (f tp) -> m (f tp)
idxCacheEval IdxCache t f
c Expr t tp
e m (f tp)
m = do
  case Expr t tp -> Maybe (Nonce t tp)
forall t (tp :: BaseType). Expr t tp -> Maybe (Nonce t tp)
exprMaybeId Expr t tp
e of
    Maybe (Nonce t tp)
Nothing -> m (f tp)
m
    Just Nonce t tp
n -> IdxCache t f -> Nonce t tp -> m (f tp) -> m (f tp)
forall (m :: Type -> Type) t (f :: BaseType -> Type)
       (tp :: BaseType).
MonadIO m =>
IdxCache t f -> Nonce t tp -> m (f tp) -> m (f tp)
idxCacheEval' IdxCache t f
c Nonce t tp
n m (f tp)
m

-- | Implements a cached evaluated using the given element.  Given an element
-- this function returns the value of the element if bound, and otherwise
-- calls the evaluation function, stores the result in the cache, and
-- returns the value.
{-# INLINE idxCacheEval' #-}
idxCacheEval' :: (MonadIO m)
              => IdxCache t f
              -> Nonce t tp
              -> m (f tp)
              -> m (f tp)
idxCacheEval' :: IdxCache t f -> Nonce t tp -> m (f tp) -> m (f tp)
idxCacheEval' IdxCache t f
c Nonce t tp
n m (f tp)
m = do
  Maybe (f tp)
mr <- IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
forall (m :: Type -> Type) t (f :: BaseType -> Type)
       (tp :: BaseType).
MonadIO m =>
IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
lookupIdx IdxCache t f
c Nonce t tp
n
  case Maybe (f tp)
mr of
    Just f tp
r -> f tp -> m (f tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return f tp
r
    Maybe (f tp)
Nothing -> do
      f tp
r <- m (f tp)
m
      IdxCache t f -> Nonce t tp -> f tp -> m ()
forall (m :: Type -> Type) t (f :: BaseType -> Type)
       (tp :: BaseType).
MonadIO m =>
IdxCache t f -> Nonce t tp -> f tp -> m ()
insertIdxValue IdxCache t f
c Nonce t tp
n f tp
r
      f tp -> m (f tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return f tp
r

------------------------------------------------------------------------
-- ExprBuilder operations

curProgramLoc :: ExprBuilder t st fs -> IO ProgramLoc
curProgramLoc :: ExprBuilder t st fs -> IO ProgramLoc
curProgramLoc ExprBuilder t st fs
sym = IORef ProgramLoc -> IO ProgramLoc
forall a. IORef a -> IO a
readIORef (ExprBuilder t st fs -> IORef ProgramLoc
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IORef ProgramLoc
sbProgramLoc ExprBuilder t st fs
sym)

-- | Create an element from a nonce app.
sbNonceExpr :: ExprBuilder t st fs
           -> NonceApp t (Expr t) tp
           -> IO (Expr t tp)
sbNonceExpr :: ExprBuilder t st fs -> NonceApp t (Expr t) tp -> IO (Expr t tp)
sbNonceExpr ExprBuilder t st fs
sym NonceApp t (Expr t) tp
a = do
  ExprAllocator t
s <- IORef (ExprAllocator t) -> IO (ExprAllocator t)
forall a. IORef a -> IO a
readIORef (ExprBuilder t st fs -> IORef (ExprAllocator t)
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IORef (ExprAllocator t)
curAllocator ExprBuilder t st fs
sym)
  ProgramLoc
pc <- ExprBuilder t st fs -> IO ProgramLoc
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO ProgramLoc
curProgramLoc ExprBuilder t st fs
sym
  ExprAllocator t
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
forall t.
ExprAllocator t
-> forall (tp :: BaseType).
   ProgramLoc
   -> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
nonceExpr ExprAllocator t
s ProgramLoc
pc NonceApp t (Expr t) tp
a ((forall (u :: BaseType). Expr t u -> AbstractValue u)
-> NonceApp t (Expr t) tp -> AbstractValue tp
forall (e :: BaseType -> Type) t (tp :: BaseType).
IsExpr e =>
(forall (u :: BaseType). e u -> AbstractValue u)
-> NonceApp t e tp -> AbstractValue tp
quantAbsEval forall t (tp :: BaseType). Expr t tp -> AbstractValue tp
forall (u :: BaseType). Expr t u -> AbstractValue u
exprAbsValue NonceApp t (Expr t) tp
a)

semiRingLit :: ExprBuilder t st fs
            -> SR.SemiRingRepr sr
            -> SR.Coefficient sr
            -> IO (Expr t (SR.SemiRingBase sr))
semiRingLit :: ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
semiRingLit ExprBuilder t st fs
sb SemiRingRepr sr
sr Coefficient sr
x = do
  ProgramLoc
l <- ExprBuilder t st fs -> IO ProgramLoc
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO ProgramLoc
curProgramLoc ExprBuilder t st fs
sb
  Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr)))
-> Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall a b. (a -> b) -> a -> b
$! SemiRingRepr sr
-> Coefficient sr -> ProgramLoc -> Expr t (SemiRingBase sr)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Coefficient sr -> ProgramLoc -> Expr t (SemiRingBase sr)
SemiRingLiteral SemiRingRepr sr
sr Coefficient sr
x ProgramLoc
l

sbMakeExpr :: ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr :: ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym App (Expr t) tp
a = do
  ExprAllocator t
s <- IORef (ExprAllocator t) -> IO (ExprAllocator t)
forall a. IORef a -> IO a
readIORef (ExprBuilder t st fs -> IORef (ExprAllocator t)
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IORef (ExprAllocator t)
curAllocator ExprBuilder t st fs
sym)
  ProgramLoc
pc <- ExprBuilder t st fs -> IO ProgramLoc
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO ProgramLoc
curProgramLoc ExprBuilder t st fs
sym
  let v :: AbstractValue tp
v = (forall (u :: BaseType). Expr t u -> AbstractValue u)
-> App (Expr t) tp -> AbstractValue tp
forall (e :: BaseType -> Type) (tp :: BaseType).
(IsExpr e, HashableF e, OrdF e) =>
(forall (u :: BaseType). e u -> AbstractValue u)
-> App e tp -> AbstractValue tp
abstractEval forall t (tp :: BaseType). Expr t tp -> AbstractValue tp
forall (u :: BaseType). Expr t u -> AbstractValue u
exprAbsValue App (Expr t) tp
a
  Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (App (Expr t) tp -> Bool
forall (e :: BaseType -> Type) (tp :: BaseType). App e tp -> Bool
isNonLinearApp App (Expr t) tp
a) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
    IORef Integer -> (Integer -> (Integer, ())) -> IO ()
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' (ExprBuilder t st fs -> IORef Integer
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IORef Integer
sbNonLinearOps ExprBuilder t st fs
sym) (\Integer
n -> (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1,()))
  case App (Expr t) tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
App e tp -> BaseTypeRepr tp
appType App (Expr t) tp
a of
    -- Check if abstract interpretation concludes this is a constant.
    BaseTypeRepr tp
BaseBoolRepr | Just b <- AbstractValue tp
v -> Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr t tp -> IO (Expr t tp)) -> Expr t tp -> IO (Expr t tp)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> Bool -> Pred (ExprBuilder t st fs)
forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
backendPred ExprBuilder t st fs
sym Bool
b
    BaseTypeRepr tp
BaseIntegerRepr | Just Integer
c <- ValueRange Integer -> Maybe Integer
forall tp. ValueRange tp -> Maybe tp
asSingleRange AbstractValue tp
ValueRange Integer
v -> ExprBuilder t st fs
-> Integer -> IO (SymInteger (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit ExprBuilder t st fs
sym Integer
c
    BaseTypeRepr tp
BaseRealRepr | Just Rational
c <- ValueRange Rational -> Maybe Rational
forall tp. ValueRange tp -> Maybe tp
asSingleRange (RealAbstractValue -> ValueRange Rational
ravRange AbstractValue tp
RealAbstractValue
v) -> ExprBuilder t st fs
-> Rational -> IO (SymReal (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit ExprBuilder t st fs
sym Rational
c
    BaseBVRepr NatRepr w
w | Just Integer
x <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
BVD.asSingleton BVDomain w
AbstractValue tp
v -> ExprBuilder t st fs
-> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit ExprBuilder t st fs
sym NatRepr w
w (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
x)
    BaseTypeRepr tp
_ -> ExprAllocator t
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
forall t.
ExprAllocator t
-> forall (tp :: BaseType).
   ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
appExpr ExprAllocator t
s ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v

-- | Update the binding to point to the current variable.
updateVarBinding :: ExprBuilder t st fs
                 -> SolverSymbol
                 -> SymbolBinding t
                 -> IO ()
updateVarBinding :: ExprBuilder t st fs -> SolverSymbol -> SymbolBinding t -> IO ()
updateVarBinding ExprBuilder t st fs
sym SolverSymbol
nm SymbolBinding t
v
  | SolverSymbol
nm SolverSymbol -> SolverSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== SolverSymbol
emptySymbol = () -> IO ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
  | Bool
otherwise =
    IORef (SymbolVarBimap t)
-> (SymbolVarBimap t -> (SymbolVarBimap t, ())) -> IO ()
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' (ExprBuilder t st fs -> IORef (SymbolVarBimap t)
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IORef (SymbolVarBimap t)
sbVarBindings ExprBuilder t st fs
sym) ((SymbolVarBimap t -> (SymbolVarBimap t, ())) -> IO ())
-> (SymbolVarBimap t -> (SymbolVarBimap t, ())) -> IO ()
forall a b. (a -> b) -> a -> b
$ (\SymbolVarBimap t
x -> SymbolBinding t
v SymbolBinding t -> (SymbolVarBimap t, ()) -> (SymbolVarBimap t, ())
`seq` (SolverSymbol
-> SymbolBinding t -> SymbolVarBimap t -> SymbolVarBimap t
forall t.
SolverSymbol
-> SymbolBinding t -> SymbolVarBimap t -> SymbolVarBimap t
ins SolverSymbol
nm SymbolBinding t
v SymbolVarBimap t
x, ()))
  where ins :: SolverSymbol
-> SymbolBinding t -> SymbolVarBimap t -> SymbolVarBimap t
ins SolverSymbol
n SymbolBinding t
x (SymbolVarBimap Bimap SolverSymbol (SymbolBinding t)
m) = Bimap SolverSymbol (SymbolBinding t) -> SymbolVarBimap t
forall t. Bimap SolverSymbol (SymbolBinding t) -> SymbolVarBimap t
SymbolVarBimap (SolverSymbol
-> SymbolBinding t
-> Bimap SolverSymbol (SymbolBinding t)
-> Bimap SolverSymbol (SymbolBinding t)
forall a b. (Ord a, Ord b) => a -> b -> Bimap a b -> Bimap a b
Bimap.insert SolverSymbol
n SymbolBinding t
x Bimap SolverSymbol (SymbolBinding t)
m)

-- | Creates a new bound var.
sbMakeBoundVar :: ExprBuilder t st fs
               -> SolverSymbol
               -> BaseTypeRepr tp
               -> VarKind
               -> Maybe (AbstractValue tp)
               -> IO (ExprBoundVar t tp)
sbMakeBoundVar :: ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr tp
-> VarKind
-> Maybe (AbstractValue tp)
-> IO (ExprBoundVar t tp)
sbMakeBoundVar ExprBuilder t st fs
sym SolverSymbol
nm BaseTypeRepr tp
tp VarKind
k Maybe (AbstractValue tp)
absVal = do
  Nonce t tp
n  <- ExprBuilder t st fs -> IO (Nonce t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> IO (Nonce t tp)
sbFreshIndex ExprBuilder t st fs
sym
  ProgramLoc
pc <- ExprBuilder t st fs -> IO ProgramLoc
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO ProgramLoc
curProgramLoc ExprBuilder t st fs
sym
  ExprBoundVar t tp -> IO (ExprBoundVar t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExprBoundVar t tp -> IO (ExprBoundVar t tp))
-> ExprBoundVar t tp -> IO (ExprBoundVar t tp)
forall a b. (a -> b) -> a -> b
$! BVar :: forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc
-> SolverSymbol
-> BaseTypeRepr tp
-> VarKind
-> Maybe (AbstractValue tp)
-> ExprBoundVar t tp
BVar { bvarId :: Nonce t tp
bvarId   = Nonce t tp
n
                 , bvarLoc :: ProgramLoc
bvarLoc  = ProgramLoc
pc
                 , bvarName :: SolverSymbol
bvarName = SolverSymbol
nm
                 , bvarType :: BaseTypeRepr tp
bvarType = BaseTypeRepr tp
tp
                 , bvarKind :: VarKind
bvarKind = VarKind
k
                 , bvarAbstractValue :: Maybe (AbstractValue tp)
bvarAbstractValue = Maybe (AbstractValue tp)
absVal
                 }

-- | Create fresh index
sbFreshIndex :: ExprBuilder t st fs -> IO (Nonce t (tp::BaseType))
sbFreshIndex :: ExprBuilder t st fs -> IO (Nonce t tp)
sbFreshIndex ExprBuilder t st fs
sb = NonceGenerator IO t -> IO (Nonce t tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce (ExprBuilder t st fs -> NonceGenerator IO t
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> NonceGenerator IO t
exprCounter ExprBuilder t st fs
sb)

sbFreshSymFnNonce :: ExprBuilder t st fs -> IO (Nonce t (ctx:: Ctx BaseType))
sbFreshSymFnNonce :: ExprBuilder t st fs -> IO (Nonce t ctx)
sbFreshSymFnNonce ExprBuilder t st fs
sb = NonceGenerator IO t -> IO (Nonce t ctx)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce (ExprBuilder t st fs -> NonceGenerator IO t
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> NonceGenerator IO t
exprCounter ExprBuilder t st fs
sb)

------------------------------------------------------------------------
-- Configuration option for controlling the maximum number of value a unary
-- threshold may have.

-- | Maximum number of values in unary bitvector encoding.
--
--   This option is named \"backend.unary_threshold\"
unaryThresholdOption :: CFG.ConfigOption BaseIntegerType
unaryThresholdOption :: ConfigOption BaseIntegerType
unaryThresholdOption = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
CFG.configOption BaseTypeRepr BaseIntegerType
BaseIntegerRepr String
"backend.unary_threshold"

-- | The configuration option for setting the maximum number of
-- values a unary threshold may have.
unaryThresholdDesc :: CFG.ConfigDesc
unaryThresholdDesc :: ConfigDesc
unaryThresholdDesc = ConfigOption BaseIntegerType
-> OptionStyle BaseIntegerType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseIntegerType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
CFG.mkOpt ConfigOption BaseIntegerType
unaryThresholdOption OptionStyle BaseIntegerType
sty Maybe (Doc Void)
help (ConcreteVal BaseIntegerType -> Maybe (ConcreteVal BaseIntegerType)
forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
0))
  where sty :: OptionStyle BaseIntegerType
sty = Bound Integer -> OptionStyle BaseIntegerType
CFG.integerWithMinOptSty (Integer -> Bound Integer
forall r. r -> Bound r
CFG.Inclusive Integer
0)
        help :: Maybe (Doc Void)
help = Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Maximum number of values in unary bitvector encoding."

------------------------------------------------------------------------
-- Configuration option for controlling how many disjoint ranges
-- should be allowed in bitvector domains.

-- | Maximum number of ranges in bitvector abstract domains.
--
--   This option is named \"backend.bvdomain_range_limit\"
bvdomainRangeLimitOption :: CFG.ConfigOption BaseIntegerType
bvdomainRangeLimitOption :: ConfigOption BaseIntegerType
bvdomainRangeLimitOption = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
CFG.configOption BaseTypeRepr BaseIntegerType
BaseIntegerRepr String
"backend.bvdomain_range_limit"

bvdomainRangeLimitDesc :: CFG.ConfigDesc
bvdomainRangeLimitDesc :: ConfigDesc
bvdomainRangeLimitDesc = ConfigOption BaseIntegerType
-> OptionStyle BaseIntegerType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseIntegerType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
CFG.mkOpt ConfigOption BaseIntegerType
bvdomainRangeLimitOption OptionStyle BaseIntegerType
sty Maybe (Doc Void)
help (ConcreteVal BaseIntegerType -> Maybe (ConcreteVal BaseIntegerType)
forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
2))
  where sty :: OptionStyle BaseIntegerType
sty = Bound Integer -> OptionStyle BaseIntegerType
CFG.integerWithMinOptSty (Integer -> Bound Integer
forall r. r -> Bound r
CFG.Inclusive Integer
0)
        help :: Maybe (Doc Void)
help = Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Maximum number of ranges in bitvector domains."

------------------------------------------------------------------------
-- Cache start size

-- | Starting size for element cache when caching is enabled.
--
--   This option is named \"backend.cache_start_size\"
cacheStartSizeOption :: CFG.ConfigOption BaseIntegerType
cacheStartSizeOption :: ConfigOption BaseIntegerType
cacheStartSizeOption = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
CFG.configOption BaseTypeRepr BaseIntegerType
BaseIntegerRepr String
"backend.cache_start_size"

-- | The configuration option for setting the size of the initial hash set
-- used by simple builder
cacheStartSizeDesc :: CFG.ConfigDesc
cacheStartSizeDesc :: ConfigDesc
cacheStartSizeDesc = ConfigOption BaseIntegerType
-> OptionStyle BaseIntegerType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseIntegerType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
CFG.mkOpt ConfigOption BaseIntegerType
cacheStartSizeOption OptionStyle BaseIntegerType
sty Maybe (Doc Void)
help (ConcreteVal BaseIntegerType -> Maybe (ConcreteVal BaseIntegerType)
forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
100000))
  where sty :: OptionStyle BaseIntegerType
sty = Bound Integer -> OptionStyle BaseIntegerType
CFG.integerWithMinOptSty (Integer -> Bound Integer
forall r. r -> Bound r
CFG.Inclusive Integer
0)
        help :: Maybe (Doc Void)
help = Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Starting size for element cache"

------------------------------------------------------------------------
-- Cache terms

-- | Indicates if we should cache terms.  When enabled, hash-consing
--   is used to find and deduplicate common subexpressions.
--
--   This option is named \"use_cache\"
cacheTerms :: CFG.ConfigOption BaseBoolType
cacheTerms :: ConfigOption BaseBoolType
cacheTerms = BaseTypeRepr BaseBoolType -> String -> ConfigOption BaseBoolType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
CFG.configOption BaseTypeRepr BaseBoolType
BaseBoolRepr String
"use_cache"

cacheOptStyle ::
  NonceGenerator IO t ->
  IORef (ExprAllocator t) ->
  CFG.OptionSetting BaseIntegerType ->
  CFG.OptionStyle BaseBoolType
cacheOptStyle :: NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> OptionStyle BaseBoolType
cacheOptStyle NonceGenerator IO t
gen IORef (ExprAllocator t)
storageRef OptionSetting BaseIntegerType
szSetting =
  OptionStyle BaseBoolType
CFG.boolOptSty OptionStyle BaseBoolType
-> (OptionStyle BaseBoolType -> OptionStyle BaseBoolType)
-> OptionStyle BaseBoolType
forall a b. a -> (a -> b) -> b
& (Maybe (ConcreteVal BaseBoolType)
 -> ConcreteVal BaseBoolType -> IO OptionSetResult)
-> OptionStyle BaseBoolType -> OptionStyle BaseBoolType
forall (tp :: BaseType).
(Maybe (ConcreteVal tp) -> ConcreteVal tp -> IO OptionSetResult)
-> OptionStyle tp -> OptionStyle tp
CFG.set_opt_onset
        (\Maybe (ConcreteVal BaseBoolType)
mb ConcreteVal BaseBoolType
b -> Maybe Bool -> Bool -> IO ()
f ((ConcreteVal BaseBoolType -> Bool)
-> Maybe (ConcreteVal BaseBoolType) -> Maybe Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ConcreteVal BaseBoolType -> Bool
fromConcreteBool Maybe (ConcreteVal BaseBoolType)
mb) (ConcreteVal BaseBoolType -> Bool
fromConcreteBool ConcreteVal BaseBoolType
b) IO () -> IO OptionSetResult -> IO OptionSetResult
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> OptionSetResult -> IO OptionSetResult
forall (m :: Type -> Type) a. Monad m => a -> m a
return OptionSetResult
CFG.optOK)
 where
 f :: Maybe Bool -> Bool -> IO ()
 f :: Maybe Bool -> Bool -> IO ()
f Maybe Bool
mb Bool
b | Maybe Bool
mb Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b = if Bool
b then IO ()
start else IO ()
stop
        | Bool
otherwise = () -> IO ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

 stop :: IO ()
stop  = do ExprAllocator t
s <- NonceGenerator IO t -> IO (ExprAllocator t)
forall t. NonceGenerator IO t -> IO (ExprAllocator t)
newStorage NonceGenerator IO t
gen
            IORef (ExprAllocator t) -> ExprAllocator t -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef IORef (ExprAllocator t)
storageRef ExprAllocator t
s

 start :: IO ()
start = do Integer
sz <- OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
CFG.getOpt OptionSetting BaseIntegerType
szSetting
            ExprAllocator t
s <- NonceGenerator IO t -> Int -> IO (ExprAllocator t)
forall t. NonceGenerator IO t -> Int -> IO (ExprAllocator t)
newCachedStorage NonceGenerator IO t
gen (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
sz)
            IORef (ExprAllocator t) -> ExprAllocator t -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef IORef (ExprAllocator t)
storageRef ExprAllocator t
s

cacheOptDesc ::
  NonceGenerator IO t ->
  IORef (ExprAllocator t) ->
  CFG.OptionSetting BaseIntegerType ->
  CFG.ConfigDesc
cacheOptDesc :: NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> ConfigDesc
cacheOptDesc NonceGenerator IO t
gen IORef (ExprAllocator t)
storageRef OptionSetting BaseIntegerType
szSetting =
  ConfigOption BaseBoolType
-> OptionStyle BaseBoolType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseBoolType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
CFG.mkOpt
    ConfigOption BaseBoolType
cacheTerms
    (NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> OptionStyle BaseBoolType
forall t.
NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> OptionStyle BaseBoolType
cacheOptStyle NonceGenerator IO t
gen IORef (ExprAllocator t)
storageRef OptionSetting BaseIntegerType
szSetting)
    (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Use hash-consing during term construction")
    (ConcreteVal BaseBoolType -> Maybe (ConcreteVal BaseBoolType)
forall a. a -> Maybe a
Just (Bool -> ConcreteVal BaseBoolType
ConcreteBool Bool
False))


newExprBuilder ::
  FloatModeRepr fm
  -- ^ Float interpretation mode (i.e., how are floats translated for the solver).
  -> st t
  -- ^ Initial state for the expression builder
  -> NonceGenerator IO t
  -- ^ Nonce generator for names
  ->  IO (ExprBuilder t st (Flags fm))
newExprBuilder :: FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
newExprBuilder FloatModeRepr fm
floatMode st t
st NonceGenerator IO t
gen = do
  ExprAllocator t
es <- NonceGenerator IO t -> IO (ExprAllocator t)
forall t. NonceGenerator IO t -> IO (ExprAllocator t)
newStorage NonceGenerator IO t
gen

  let t :: Expr t BaseBoolType
t = Bool -> ProgramLoc -> Expr t BaseBoolType
forall t. Bool -> ProgramLoc -> Expr t BaseBoolType
BoolExpr Bool
True ProgramLoc
initializationLoc
  let f :: Expr t BaseBoolType
f = Bool -> ProgramLoc -> Expr t BaseBoolType
forall t. Bool -> ProgramLoc -> Expr t BaseBoolType
BoolExpr Bool
False ProgramLoc
initializationLoc
  let z :: Expr t (SemiRingBase SemiRingReal)
z = SemiRingRepr SemiRingReal
-> Coefficient SemiRingReal
-> ProgramLoc
-> Expr t (SemiRingBase SemiRingReal)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Coefficient sr -> ProgramLoc -> Expr t (SemiRingBase sr)
SemiRingLiteral SemiRingRepr SemiRingReal
SR.SemiRingRealRepr Coefficient SemiRingReal
0 ProgramLoc
initializationLoc

  IORef ProgramLoc
loc_ref       <- ProgramLoc -> IO (IORef ProgramLoc)
forall a. a -> IO (IORef a)
newIORef ProgramLoc
initializationLoc
  IORef (ExprAllocator t)
storage_ref   <- ExprAllocator t -> IO (IORef (ExprAllocator t))
forall a. a -> IO (IORef a)
newIORef ExprAllocator t
es
  IORef (SymbolVarBimap t)
bindings_ref  <- SymbolVarBimap t -> IO (IORef (SymbolVarBimap t))
forall a. a -> IO (IORef a)
newIORef SymbolVarBimap t
forall t. SymbolVarBimap t
emptySymbolVarBimap
  IORef
  (Map
     (SolverSymbol, Some (Assignment BaseTypeRepr))
     (SomeSymFn (ExprBuilder t st (Flags fm))))
uninterp_fn_cache_ref <- Map
  (SolverSymbol, Some (Assignment BaseTypeRepr))
  (SomeSymFn (ExprBuilder t st (Flags fm)))
-> IO
     (IORef
        (Map
           (SolverSymbol, Some (Assignment BaseTypeRepr))
           (SomeSymFn (ExprBuilder t st (Flags fm)))))
forall a. a -> IO (IORef a)
newIORef Map
  (SolverSymbol, Some (Assignment BaseTypeRepr))
  (SomeSymFn (ExprBuilder t st (Flags fm)))
forall k a. Map k a
Map.empty
  HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t)
matlabFnCache <- ST
  RealWorld
  (HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))
-> IO
     (HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))
forall a. ST RealWorld a -> IO a
stToIO (ST
   RealWorld
   (HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))
 -> IO
      (HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t)))
-> ST
     RealWorld
     (HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))
-> IO
     (HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))
forall a b. (a -> b) -> a -> b
$ ST
  RealWorld
  (HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))
forall k s (key :: k -> Type) (val :: k -> Type).
ST s (HashTable s key val)
PH.new
  IORef (Maybe (SolverEvent -> IO ()))
loggerRef     <- Maybe (SolverEvent -> IO ())
-> IO (IORef (Maybe (SolverEvent -> IO ())))
forall a. a -> IO (IORef a)
newIORef Maybe (SolverEvent -> IO ())
forall a. Maybe a
Nothing

  -- Set up configuration options
  Config
cfg <- Integer -> [ConfigDesc] -> IO Config
CFG.initialConfig Integer
0
           [ ConfigDesc
unaryThresholdDesc
           , ConfigDesc
bvdomainRangeLimitDesc
           , ConfigDesc
cacheStartSizeDesc
           ]
  OptionSetting BaseIntegerType
unarySetting       <- ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
CFG.getOptionSetting ConfigOption BaseIntegerType
unaryThresholdOption Config
cfg
  OptionSetting BaseIntegerType
domainRangeSetting <- ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
CFG.getOptionSetting ConfigOption BaseIntegerType
bvdomainRangeLimitOption Config
cfg
  OptionSetting BaseIntegerType
cacheStartSetting  <- ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
CFG.getOptionSetting ConfigOption BaseIntegerType
cacheStartSizeOption Config
cfg
  [ConfigDesc] -> Config -> IO ()
CFG.extendConfig [NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> ConfigDesc
forall t.
NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> ConfigDesc
cacheOptDesc NonceGenerator IO t
gen IORef (ExprAllocator t)
storage_ref OptionSetting BaseIntegerType
cacheStartSetting] Config
cfg
  IORef Integer
nonLinearOps <- Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef Integer
0

  ExprBuilder t st (Flags fm) -> IO (ExprBuilder t st (Flags fm))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExprBuilder t st (Flags fm) -> IO (ExprBuilder t st (Flags fm)))
-> ExprBuilder t st (Flags fm) -> IO (ExprBuilder t st (Flags fm))
forall a b. (a -> b) -> a -> b
$! SB :: forall t (st :: Type -> Type) fs (fm :: FloatMode).
(fs ~ Flags fm) =>
BoolExpr t
-> BoolExpr t
-> RealExpr t
-> Config
-> Bool
-> OptionSetting BaseIntegerType
-> OptionSetting BaseIntegerType
-> OptionSetting BaseIntegerType
-> NonceGenerator IO t
-> IORef (ExprAllocator t)
-> IORef Integer
-> IORef ProgramLoc
-> st t
-> IORef (SymbolVarBimap t)
-> IORef
     (Map
        (SolverSymbol, Some (Assignment BaseTypeRepr))
        (SomeSymFn (ExprBuilder t st fs)))
-> HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t)
-> IORef (Maybe (SolverEvent -> IO ()))
-> FloatModeRepr fm
-> ExprBuilder t st fs
SB { sbTrue :: BoolExpr t
sbTrue  = BoolExpr t
forall t. Expr t BaseBoolType
t
               , sbFalse :: BoolExpr t
sbFalse = BoolExpr t
forall t. Expr t BaseBoolType
f
               , sbZero :: RealExpr t
sbZero = RealExpr t
forall t. Expr t BaseRealType
z
               , sbConfiguration :: Config
sbConfiguration = Config
cfg
               , sbFloatReduce :: Bool
sbFloatReduce = Bool
True
               , sbUnaryThreshold :: OptionSetting BaseIntegerType
sbUnaryThreshold = OptionSetting BaseIntegerType
unarySetting
               , sbBVDomainRangeLimit :: OptionSetting BaseIntegerType
sbBVDomainRangeLimit = OptionSetting BaseIntegerType
domainRangeSetting
               , sbCacheStartSize :: OptionSetting BaseIntegerType
sbCacheStartSize = OptionSetting BaseIntegerType
cacheStartSetting
               , sbProgramLoc :: IORef ProgramLoc
sbProgramLoc = IORef ProgramLoc
loc_ref
               , exprCounter :: NonceGenerator IO t
exprCounter = NonceGenerator IO t
gen
               , curAllocator :: IORef (ExprAllocator t)
curAllocator = IORef (ExprAllocator t)
storage_ref
               , sbNonLinearOps :: IORef Integer
sbNonLinearOps = IORef Integer
nonLinearOps
               , sbUserState :: st t
sbUserState = st t
st
               , sbVarBindings :: IORef (SymbolVarBimap t)
sbVarBindings = IORef (SymbolVarBimap t)
bindings_ref
               , sbUninterpFnCache :: IORef
  (Map
     (SolverSymbol, Some (Assignment BaseTypeRepr))
     (SomeSymFn (ExprBuilder t st (Flags fm))))
sbUninterpFnCache = IORef
  (Map
     (SolverSymbol, Some (Assignment BaseTypeRepr))
     (SomeSymFn (ExprBuilder t st (Flags fm))))
uninterp_fn_cache_ref
               , sbMatlabFnCache :: HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t)
sbMatlabFnCache = HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t)
matlabFnCache
               , sbSolverLogger :: IORef (Maybe (SolverEvent -> IO ()))
sbSolverLogger = IORef (Maybe (SolverEvent -> IO ()))
loggerRef
               , sbFloatMode :: FloatModeRepr fm
sbFloatMode = FloatModeRepr fm
floatMode
               }

-- | Get current variable bindings.
getSymbolVarBimap :: ExprBuilder t st fs -> IO (SymbolVarBimap t)
getSymbolVarBimap :: ExprBuilder t st fs -> IO (SymbolVarBimap t)
getSymbolVarBimap ExprBuilder t st fs
sym = IORef (SymbolVarBimap t) -> IO (SymbolVarBimap t)
forall a. IORef a -> IO a
readIORef (ExprBuilder t st fs -> IORef (SymbolVarBimap t)
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IORef (SymbolVarBimap t)
sbVarBindings ExprBuilder t st fs
sym)

-- | Stop caching applications in backend.
stopCaching :: ExprBuilder t st fs -> IO ()
stopCaching :: ExprBuilder t st fs -> IO ()
stopCaching ExprBuilder t st fs
sb = do
  ExprAllocator t
s <- NonceGenerator IO t -> IO (ExprAllocator t)
forall t. NonceGenerator IO t -> IO (ExprAllocator t)
newStorage (ExprBuilder t st fs -> NonceGenerator IO t
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> NonceGenerator IO t
exprCounter ExprBuilder t st fs
sb)
  IORef (ExprAllocator t) -> ExprAllocator t -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef (ExprBuilder t st fs -> IORef (ExprAllocator t)
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IORef (ExprAllocator t)
curAllocator ExprBuilder t st fs
sb) ExprAllocator t
s

-- | Restart caching applications in backend (clears cache if it is currently caching).
startCaching :: ExprBuilder t st fs -> IO ()
startCaching :: ExprBuilder t st fs -> IO ()
startCaching ExprBuilder t st fs
sb = do
  Integer
sz <- OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
CFG.getOpt (ExprBuilder t st fs -> OptionSetting BaseIntegerType
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> OptionSetting BaseIntegerType
sbCacheStartSize ExprBuilder t st fs
sb)
  ExprAllocator t
s <- NonceGenerator IO t -> Int -> IO (ExprAllocator t)
forall t. NonceGenerator IO t -> Int -> IO (ExprAllocator t)
newCachedStorage (ExprBuilder t st fs -> NonceGenerator IO t
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> NonceGenerator IO t
exprCounter ExprBuilder t st fs
sb) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
sz)
  IORef (ExprAllocator t) -> ExprAllocator t -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef (ExprBuilder t st fs -> IORef (ExprAllocator t)
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IORef (ExprAllocator t)
curAllocator ExprBuilder t st fs
sb) ExprAllocator t
s

bvBinDivOp :: (1 <= w)
            => (NatRepr w -> BV.BV w -> BV.BV w -> BV.BV w)
            -> (NatRepr w -> BVExpr t w -> BVExpr t w -> App (Expr t) (BaseBVType w))
            -> ExprBuilder t st fs
            -> BVExpr t w
            -> BVExpr t w
            -> IO (BVExpr t w)
bvBinDivOp :: (NatRepr w -> BV w -> BV w -> BV w)
-> (NatRepr w
    -> BVExpr t w -> BVExpr t w -> App (Expr t) (BaseBVType w))
-> ExprBuilder t st fs
-> BVExpr t w
-> BVExpr t w
-> IO (BVExpr t w)
bvBinDivOp NatRepr w -> BV w -> BV w -> BV w
f NatRepr w
-> BVExpr t w -> BVExpr t w -> App (Expr t) (BaseBVType w)
c ExprBuilder t st fs
sb BVExpr t w
x BVExpr t w
y = do
  let w :: NatRepr w
w = BVExpr t w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth BVExpr t w
x
  case (BVExpr t w -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV BVExpr t w
x, BVExpr t w -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV BVExpr t w
y) of
    (Just BV w
i, Just BV w
j) | BV w
j BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
/= NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w -> ExprBuilder t st fs
-> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit ExprBuilder t st fs
sb NatRepr w
w (BV w -> IO (SymBV (ExprBuilder t st fs) w))
-> BV w -> IO (SymBV (ExprBuilder t st fs) w)
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> BV w -> BV w
f NatRepr w
w BV w
i BV w
j
    (Maybe (BV w), Maybe (BV w))
_ -> ExprBuilder t st fs
-> App (Expr t) (BaseBVType w) -> IO (BVExpr t w)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sb (App (Expr t) (BaseBVType w) -> IO (BVExpr t w))
-> App (Expr t) (BaseBVType w) -> IO (BVExpr t w)
forall a b. (a -> b) -> a -> b
$ NatRepr w
-> BVExpr t w -> BVExpr t w -> App (Expr t) (BaseBVType w)
c NatRepr w
w BVExpr t w
x BVExpr t w
y

asConcreteIndices :: IsExpr e
                  => Ctx.Assignment e ctx
                  -> Maybe (Ctx.Assignment IndexLit ctx)
asConcreteIndices :: Assignment e ctx -> Maybe (Assignment IndexLit ctx)
asConcreteIndices = (forall (x :: BaseType). e x -> Maybe (IndexLit x))
-> forall (x :: Ctx BaseType).
   Assignment e x -> Maybe (Assignment IndexLit x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC forall (x :: BaseType). e x -> Maybe (IndexLit x)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> Maybe (IndexLit tp)
f
  where f :: IsExpr e => e tp -> Maybe (IndexLit tp)
        f :: e tp -> Maybe (IndexLit tp)
f e tp
x =
          case e tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType e tp
x of
            BaseTypeRepr tp
BaseIntegerRepr  -> Integer -> IndexLit BaseIntegerType
IntIndexLit (Integer -> IndexLit BaseIntegerType)
-> Maybe Integer -> Maybe (IndexLit BaseIntegerType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e BaseIntegerType -> Maybe Integer
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
asInteger e tp
e BaseIntegerType
x
            BaseBVRepr NatRepr w
w -> NatRepr w -> BV w -> IndexLit (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> IndexLit (BaseBVType w)
BVIndexLit NatRepr w
w (BV w -> IndexLit (BaseBVType w))
-> Maybe (BV w) -> Maybe (IndexLit (BaseBVType w))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV e tp
e (BaseBVType w)
x
            BaseTypeRepr tp
_ -> Maybe (IndexLit tp)
forall a. Maybe a
Nothing

symbolicIndices :: forall sym ctx
                 . IsExprBuilder sym
                => sym
                -> Ctx.Assignment IndexLit ctx
                -> IO (Ctx.Assignment (SymExpr sym) ctx)
symbolicIndices :: sym -> Assignment IndexLit ctx -> IO (Assignment (SymExpr sym) ctx)
symbolicIndices sym
sym = (forall (x :: BaseType). IndexLit x -> IO (SymExpr sym x))
-> forall (x :: Ctx BaseType).
   Assignment IndexLit x -> IO (Assignment (SymExpr sym) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC forall (x :: BaseType). IndexLit x -> IO (SymExpr sym x)
f
  where f :: IndexLit tp -> IO (SymExpr sym tp)
        f :: IndexLit tp -> IO (SymExpr sym tp)
f (IntIndexLit Integer
n)  = sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
n
        f (BVIndexLit NatRepr w
w BV w
i) = sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
i

-- | This evaluate a symbolic function against a set of arguments.
betaReduce :: ExprBuilder t st fs
           -> ExprSymFn t args ret
           -> Ctx.Assignment (Expr t) args
           -> IO (Expr t ret)
betaReduce :: ExprBuilder t st fs
-> ExprSymFn t args ret
-> Assignment (Expr t) args
-> IO (Expr t ret)
betaReduce ExprBuilder t st fs
sym ExprSymFn t args ret
f Assignment (Expr t) args
args =
  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{} ->
      ExprBuilder t st fs -> NonceApp t (Expr t) ret -> IO (Expr t ret)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> NonceApp t (Expr t) tp -> IO (Expr t tp)
sbNonceExpr ExprBuilder t st fs
sym (NonceApp t (Expr t) ret -> IO (Expr t ret))
-> NonceApp t (Expr t) ret -> IO (Expr t ret)
forall a b. (a -> b) -> a -> b
$! ExprSymFn t args ret
-> Assignment (Expr t) args -> NonceApp t (Expr t) ret
forall t (args :: Ctx BaseType) (ret :: BaseType)
       (e :: BaseType -> Type).
ExprSymFn t args ret -> Assignment e args -> NonceApp t e ret
FnApp ExprSymFn t args ret
f Assignment (Expr t) args
args
    DefinedFnInfo Assignment (ExprBoundVar t) args
bound_vars Expr t ret
e UnfoldPolicy
_ -> do
      ExprBuilder t st fs
-> Expr t ret
-> Assignment (ExprBoundVar t) args
-> Assignment (Expr t) args
-> IO (Expr t ret)
forall t (st :: Type -> Type) fs (ret :: BaseType)
       (args :: Ctx BaseType).
ExprBuilder t st fs
-> Expr t ret
-> Assignment (ExprBoundVar t) args
-> Assignment (Expr t) args
-> IO (Expr t ret)
evalBoundVars ExprBuilder t st fs
sym Expr t ret
e Assignment (ExprBoundVar t) args
bound_vars Assignment (Expr t) args
args
    MatlabSolverFnInfo MatlabSolverFn (Expr t) args ret
fn_id Assignment (ExprBoundVar t) args
_ Expr t ret
_ -> do
      MatlabSolverFn (SymExpr (ExprBuilder t st fs)) args ret
-> ExprBuilder t st fs
-> Assignment (SymExpr (ExprBuilder t st fs)) args
-> IO (SymExpr (ExprBuilder t st fs) ret)
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsExprBuilder sym =>
MatlabSolverFn (SymExpr sym) args ret
-> sym -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
evalMatlabSolverFn MatlabSolverFn (SymExpr (ExprBuilder t st fs)) args ret
MatlabSolverFn (Expr t) args ret
fn_id ExprBuilder t st fs
sym Assignment (SymExpr (ExprBuilder t st fs)) args
Assignment (Expr t) args
args

-- | This runs one action, and if it returns a value different from the input,
-- then it runs the second.  Otherwise it returns the result value passed in.
--
-- It is used when an action may modify a value, and we only want to run a
-- second action if the value changed.
runIfChanged :: Eq e
             => e
             -> (e -> IO e) -- ^ First action to run
             -> r           -- ^ Result if no change.
             -> (e -> IO r) -- ^ Second action to run
             -> IO r
runIfChanged :: e -> (e -> IO e) -> r -> (e -> IO r) -> IO r
runIfChanged e
x e -> IO e
f r
unChanged e -> IO r
onChange = do
  e
y <- e -> IO e
f e
x
  if e
x e -> e -> Bool
forall a. Eq a => a -> a -> Bool
== e
y then
    r -> IO r
forall (m :: Type -> Type) a. Monad m => a -> m a
return r
unChanged
   else
    e -> IO r
onChange e
y

-- | This adds a binding from the variable to itself in the hashtable
-- to ensure it can't be rebound.
recordBoundVar :: PH.HashTable RealWorld (Expr t) (Expr t)
                  -> ExprBoundVar t tp
                  -> IO ()
recordBoundVar :: HashTable RealWorld (Expr t) (Expr t) -> ExprBoundVar t tp -> IO ()
recordBoundVar HashTable RealWorld (Expr t) (Expr t)
tbl ExprBoundVar t tp
v = do
  let e :: Expr t tp
e = ExprBoundVar t tp -> Expr t tp
forall t (tp :: BaseType). ExprBoundVar t tp -> Expr t tp
BoundVarExpr ExprBoundVar t tp
v
  Maybe (Expr t tp)
mr <- ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp)))
-> ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (Expr t) (Expr t)
-> Expr t tp -> ST RealWorld (Maybe (Expr t tp))
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s (Maybe (val tp))
PH.lookup HashTable RealWorld (Expr t) (Expr t)
tbl Expr t tp
e
  case Maybe (Expr t tp)
mr of
    Just Expr t tp
r -> do
      Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Expr t tp
r Expr t tp -> Expr t tp -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr t tp
e) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        String -> IO ()
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Simulator internal error; do not support rebinding variables."
    Maybe (Expr t tp)
Nothing -> do
      -- Bind variable to itself to ensure we catch when it is used again.
      ST RealWorld () -> IO ()
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld () -> IO ()) -> ST RealWorld () -> IO ()
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (Expr t) (Expr t)
-> Expr t tp -> Expr t tp -> ST RealWorld ()
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
PH.insert HashTable RealWorld (Expr t) (Expr t)
tbl Expr t tp
e Expr t tp
e


-- | The CachedSymFn is used during evaluation to store the results of reducing
-- the definitions of symbolic functions.
--
-- For each function it stores a pair containing a 'Bool' that is true if the
-- function changed as a result of evaluating it, and the reduced function
-- after evaluation.
--
-- The second arguments contains the arguments with the return type appended.
data CachedSymFn t c
  = forall a r
    . (c ~ (a ::> r))
    => CachedSymFn Bool (ExprSymFn t a r)

-- | Data structure used for caching evaluation.
data EvalHashTables t
   = EvalHashTables { EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
exprTable :: !(PH.HashTable RealWorld (Expr t) (Expr t))
                    , EvalHashTables t -> HashTable RealWorld (Nonce t) (CachedSymFn t)
fnTable  :: !(PH.HashTable RealWorld (Nonce t) (CachedSymFn t))
                    }

-- | Evaluate a simple function.
--
-- This returns whether the function changed as a Boolean and the function itself.
evalSimpleFn :: EvalHashTables t
             -> ExprBuilder t st fs
             -> ExprSymFn t idx ret
             -> IO (Bool,ExprSymFn t idx ret)
evalSimpleFn :: EvalHashTables t
-> ExprBuilder t st fs
-> ExprSymFn t idx ret
-> IO (Bool, ExprSymFn t idx ret)
evalSimpleFn EvalHashTables t
tbl ExprBuilder t st fs
sym ExprSymFn t idx ret
f =
  case ExprSymFn t idx ret -> SymFnInfo t idx ret
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SymFnInfo t args ret
symFnInfo ExprSymFn t idx ret
f of
    UninterpFnInfo{} -> (Bool, ExprSymFn t idx ret) -> IO (Bool, ExprSymFn t idx ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool
False, ExprSymFn t idx ret
f)
    DefinedFnInfo Assignment (ExprBoundVar t) idx
vars Expr t ret
e UnfoldPolicy
evalFn -> do
      let n :: Nonce t (idx ::> ret)
n = ExprSymFn t idx ret -> Nonce t (idx ::> ret)
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
symFnId ExprSymFn t idx ret
f
      let nm :: SolverSymbol
nm = ExprSymFn t idx ret -> SolverSymbol
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SolverSymbol
symFnName ExprSymFn t idx ret
f
      CachedSymFn Bool
changed ExprSymFn t a r
f' <-
        HashTable RealWorld (Nonce t) (CachedSymFn t)
-> Nonce t (idx ::> ret)
-> IO (CachedSymFn t (idx ::> ret))
-> IO (CachedSymFn t (idx ::> ret))
forall k (k :: k -> Type) (a :: k -> Type) (tp :: k).
(HashableF k, TestEquality k) =>
HashTable RealWorld k a -> k tp -> IO (a tp) -> IO (a tp)
cachedEval (EvalHashTables t -> HashTable RealWorld (Nonce t) (CachedSymFn t)
forall t.
EvalHashTables t -> HashTable RealWorld (Nonce t) (CachedSymFn t)
fnTable EvalHashTables t
tbl) Nonce t (idx ::> ret)
n (IO (CachedSymFn t (idx ::> ret))
 -> IO (CachedSymFn t (idx ::> ret)))
-> IO (CachedSymFn t (idx ::> ret))
-> IO (CachedSymFn t (idx ::> ret))
forall a b. (a -> b) -> a -> b
$ do
          (forall (x :: BaseType). ExprBoundVar t x -> IO ())
-> Assignment (ExprBoundVar t) idx -> IO ()
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_ (HashTable RealWorld (Expr t) (Expr t) -> ExprBoundVar t x -> IO ()
forall t (tp :: BaseType).
HashTable RealWorld (Expr t) (Expr t) -> ExprBoundVar t tp -> IO ()
recordBoundVar (EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
forall t. EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
exprTable EvalHashTables t
tbl)) Assignment (ExprBoundVar t) idx
vars
          Expr t ret
e' <- EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
forall t (st :: Type -> Type) fs (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
evalBoundVars' EvalHashTables t
tbl ExprBuilder t st fs
sym Expr t ret
e
          if Expr t ret
e Expr t ret -> Expr t ret -> Bool
forall a. Eq a => a -> a -> Bool
== Expr t ret
e' then
            CachedSymFn t (idx ::> ret) -> IO (CachedSymFn t (idx ::> ret))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (CachedSymFn t (idx ::> ret) -> IO (CachedSymFn t (idx ::> ret)))
-> CachedSymFn t (idx ::> ret) -> IO (CachedSymFn t (idx ::> ret))
forall a b. (a -> b) -> a -> b
$! Bool -> ExprSymFn t idx ret -> CachedSymFn t (idx ::> ret)
forall t (c :: Ctx BaseType) (a :: Ctx BaseType) (r :: BaseType).
(c ~ (a ::> r)) =>
Bool -> ExprSymFn t a r -> CachedSymFn t c
CachedSymFn Bool
False ExprSymFn t idx ret
f
           else
            Bool -> ExprSymFn t idx ret -> CachedSymFn t (idx ::> ret)
forall t (c :: Ctx BaseType) (a :: Ctx BaseType) (r :: BaseType).
(c ~ (a ::> r)) =>
Bool -> ExprSymFn t a r -> CachedSymFn t c
CachedSymFn Bool
True (ExprSymFn t idx ret -> CachedSymFn t (idx ::> ret))
-> IO (ExprSymFn t idx ret) -> IO (CachedSymFn t (idx ::> ret))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> Assignment (BoundVar (ExprBuilder t st fs)) idx
-> SymExpr (ExprBuilder t st fs) ret
-> UnfoldPolicy
-> IO (SymFn (ExprBuilder t st fs) idx ret)
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment (BoundVar sym) args
-> SymExpr sym ret
-> UnfoldPolicy
-> IO (SymFn sym args ret)
definedFn ExprBuilder t st fs
sym SolverSymbol
nm Assignment (BoundVar (ExprBuilder t st fs)) idx
Assignment (ExprBoundVar t) idx
vars SymExpr (ExprBuilder t st fs) ret
Expr t ret
e' UnfoldPolicy
evalFn
      (Bool, ExprSymFn t a r) -> IO (Bool, ExprSymFn t a r)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool
changed, ExprSymFn t a r
f')
    MatlabSolverFnInfo{} -> (Bool, ExprSymFn t idx ret) -> IO (Bool, ExprSymFn t idx ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool
False, ExprSymFn t idx ret
f)

evalBoundVars' :: forall t st fs ret
               .  EvalHashTables t
               -> ExprBuilder t st fs
               -> Expr t ret
               -> IO (Expr t ret)
evalBoundVars' :: EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
evalBoundVars' EvalHashTables t
tbls ExprBuilder t st fs
sym Expr t ret
e0 =
  case Expr t ret
e0 of
    SemiRingLiteral{} -> Expr t ret -> IO (Expr t ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t ret
e0
    StringExpr{} -> Expr t ret -> IO (Expr t ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t ret
e0
    BoolExpr{} -> Expr t ret -> IO (Expr t ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t ret
e0
    FloatExpr{} -> Expr t ret -> IO (Expr t ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t ret
e0
    AppExpr AppExpr t ret
ae -> HashTable RealWorld (Expr t) (Expr t)
-> Expr t ret -> IO (Expr t ret) -> IO (Expr t ret)
forall k (k :: k -> Type) (a :: k -> Type) (tp :: k).
(HashableF k, TestEquality k) =>
HashTable RealWorld k a -> k tp -> IO (a tp) -> IO (a tp)
cachedEval (EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
forall t. EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
exprTable EvalHashTables t
tbls) Expr t ret
e0 (IO (Expr t ret) -> IO (Expr t ret))
-> IO (Expr t ret) -> IO (Expr t ret)
forall a b. (a -> b) -> a -> b
$ do
      let a :: App (Expr t) ret
a = AppExpr t ret -> App (Expr t) ret
forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t ret
ae
      App (Expr t) ret
a' <- (forall (tp :: BaseType). Expr t tp -> IO (Expr t tp))
-> App (Expr t) ret -> IO (App (Expr t) ret)
forall (m :: Type -> Type) (f :: BaseType -> Type)
       (e :: BaseType -> Type) (utp :: BaseType).
(Applicative m, OrdF f, Eq (f BaseBoolType), HashableF f,
 HasAbsValue f) =>
(forall (tp :: BaseType). e tp -> m (f tp))
-> App e utp -> m (App f utp)
traverseApp (EvalHashTables t
-> ExprBuilder t st fs -> Expr t tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
evalBoundVars' EvalHashTables t
tbls ExprBuilder t st fs
sym) App (Expr t) ret
a
      if App (Expr t) ret
a App (Expr t) ret -> App (Expr t) ret -> Bool
forall a. Eq a => a -> a -> Bool
== App (Expr t) ret
a' then
        Expr t ret -> IO (Expr t ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t ret
e0
       else
        ExprBuilder t st fs
-> (forall (w :: Nat).
    (1 <= w) =>
    ExprBuilder t st fs
    -> UnaryBV (Pred (ExprBuilder t st fs)) w
    -> IO (SymExpr (ExprBuilder t st fs) (BaseBVType w)))
-> App (SymExpr (ExprBuilder t st fs)) ret
-> IO (SymExpr (ExprBuilder t st fs) ret)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> UnaryBV (Pred sym) w -> IO (SymExpr sym (BaseBVType w)))
-> App (SymExpr sym) tp
-> IO (SymExpr sym tp)
reduceApp ExprBuilder t st fs
sym forall (w :: Nat).
(1 <= w) =>
ExprBuilder t st fs
-> UnaryBV (Pred (ExprBuilder t st fs)) w
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType w))
forall (w :: Nat) t (st :: Type -> Type) fs.
(1 <= w) =>
ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w)
bvUnary App (SymExpr (ExprBuilder t st fs)) ret
App (Expr t) ret
a'
    NonceAppExpr NonceAppExpr t ret
ae -> HashTable RealWorld (Expr t) (Expr t)
-> Expr t ret -> IO (Expr t ret) -> IO (Expr t ret)
forall k (k :: k -> Type) (a :: k -> Type) (tp :: k).
(HashableF k, TestEquality k) =>
HashTable RealWorld k a -> k tp -> IO (a tp) -> IO (a tp)
cachedEval (EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
forall t. EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
exprTable EvalHashTables t
tbls) Expr t ret
e0 (IO (Expr t ret) -> IO (Expr t ret))
-> IO (Expr t ret) -> IO (Expr t ret)
forall a b. (a -> b) -> a -> b
$ do
      case NonceAppExpr t ret -> NonceApp t (Expr t) ret
forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp NonceAppExpr t ret
ae of
        Annotation BaseTypeRepr ret
tpr Nonce t ret
n Expr t ret
a -> do
          Expr t ret
a' <- EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
forall t (st :: Type -> Type) fs (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
evalBoundVars' EvalHashTables t
tbls ExprBuilder t st fs
sym Expr t ret
a
          if Expr t ret
a Expr t ret -> Expr t ret -> Bool
forall a. Eq a => a -> a -> Bool
== Expr t ret
a' then
            Expr t ret -> IO (Expr t ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t ret
e0
          else
            ExprBuilder t st fs -> NonceApp t (Expr t) ret -> IO (Expr t ret)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> NonceApp t (Expr t) tp -> IO (Expr t tp)
sbNonceExpr ExprBuilder t st fs
sym (NonceApp t (Expr t) ret -> IO (Expr t ret))
-> NonceApp t (Expr t) ret -> IO (Expr t ret)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr ret
-> Nonce t ret -> Expr t ret -> NonceApp t (Expr t) ret
forall (tp :: BaseType) t (e :: BaseType -> Type).
BaseTypeRepr tp -> Nonce t tp -> e tp -> NonceApp t e tp
Annotation BaseTypeRepr ret
tpr Nonce t ret
n Expr t ret
a'
        Forall ExprBoundVar t tp
v Expr t BaseBoolType
e -> do
          HashTable RealWorld (Expr t) (Expr t) -> ExprBoundVar t tp -> IO ()
forall t (tp :: BaseType).
HashTable RealWorld (Expr t) (Expr t) -> ExprBoundVar t tp -> IO ()
recordBoundVar (EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
forall t. EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
exprTable EvalHashTables t
tbls) ExprBoundVar t tp
v
          -- Regenerate forallPred if e is changed by evaluation.
          Expr t BaseBoolType
-> (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> Expr t ret
-> (Expr t BaseBoolType -> IO (Expr t ret))
-> IO (Expr t ret)
forall e r. Eq e => e -> (e -> IO e) -> r -> (e -> IO r) -> IO r
runIfChanged Expr t BaseBoolType
e (EvalHashTables t
-> ExprBuilder t st fs
-> Expr t BaseBoolType
-> IO (Expr t BaseBoolType)
forall t (st :: Type -> Type) fs (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
evalBoundVars' EvalHashTables t
tbls ExprBuilder t st fs
sym) Expr t ret
e0 (ExprBuilder t st fs
-> BoundVar (ExprBuilder t st fs) tp
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
forallPred ExprBuilder t st fs
sym BoundVar (ExprBuilder t st fs) tp
ExprBoundVar t tp
v)
        Exists ExprBoundVar t tp
v Expr t BaseBoolType
e -> do
          HashTable RealWorld (Expr t) (Expr t) -> ExprBoundVar t tp -> IO ()
forall t (tp :: BaseType).
HashTable RealWorld (Expr t) (Expr t) -> ExprBoundVar t tp -> IO ()
recordBoundVar (EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
forall t. EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
exprTable EvalHashTables t
tbls) ExprBoundVar t tp
v
          -- Regenerate forallPred if e is changed by evaluation.
          Expr t BaseBoolType
-> (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> Expr t ret
-> (Expr t BaseBoolType -> IO (Expr t ret))
-> IO (Expr t ret)
forall e r. Eq e => e -> (e -> IO e) -> r -> (e -> IO r) -> IO r
runIfChanged Expr t BaseBoolType
e (EvalHashTables t
-> ExprBuilder t st fs
-> Expr t BaseBoolType
-> IO (Expr t BaseBoolType)
forall t (st :: Type -> Type) fs (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
evalBoundVars' EvalHashTables t
tbls ExprBuilder t st fs
sym) Expr t ret
e0 (ExprBuilder t st fs
-> BoundVar (ExprBuilder t st fs) tp
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
existsPred ExprBuilder t st fs
sym BoundVar (ExprBuilder t st fs) tp
ExprBoundVar t tp
v)
        ArrayFromFn ExprSymFn t (idx ::> itp) ret
f -> do
          (Bool
changed, ExprSymFn t (idx ::> itp) ret
f') <- EvalHashTables t
-> ExprBuilder t st fs
-> ExprSymFn t (idx ::> itp) ret
-> IO (Bool, ExprSymFn t (idx ::> itp) ret)
forall t (st :: Type -> Type) fs (idx :: Ctx BaseType)
       (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs
-> ExprSymFn t idx ret
-> IO (Bool, ExprSymFn t idx ret)
evalSimpleFn EvalHashTables t
tbls ExprBuilder t st fs
sym ExprSymFn t (idx ::> itp) ret
f
          if Bool -> Bool
not Bool
changed then
            Expr t ret -> IO (Expr t ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t ret
e0
           else
            ExprBuilder t st fs
-> SymFn (ExprBuilder t st fs) (idx ::> itp) ret
-> IO (SymArray (ExprBuilder t st fs) (idx ::> itp) ret)
forall sym (idx :: Ctx BaseType) (itp :: BaseType)
       (ret :: BaseType).
IsExprBuilder sym =>
sym
-> SymFn sym (idx ::> itp) ret
-> IO (SymArray sym (idx ::> itp) ret)
arrayFromFn ExprBuilder t st fs
sym SymFn (ExprBuilder t st fs) (idx ::> itp) ret
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)
args -> do
          (Bool
changed, ExprSymFn t (ctx ::> d) r
f') <- EvalHashTables t
-> ExprBuilder t st fs
-> ExprSymFn t (ctx ::> d) r
-> IO (Bool, ExprSymFn t (ctx ::> d) r)
forall t (st :: Type -> Type) fs (idx :: Ctx BaseType)
       (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs
-> ExprSymFn t idx ret
-> IO (Bool, ExprSymFn t idx ret)
evalSimpleFn EvalHashTables t
tbls ExprBuilder t st fs
sym ExprSymFn t (ctx ::> d) r
f
          let evalWrapper :: ArrayResultWrapper (Expr t) (idx ::> itp) utp
                          -> IO (ArrayResultWrapper (Expr t) (idx ::> itp) utp)
              evalWrapper :: ArrayResultWrapper (Expr t) (idx ::> itp) utp
-> IO (ArrayResultWrapper (Expr t) (idx ::> itp) utp)
evalWrapper (ArrayResultWrapper Expr t (BaseArrayType (idx ::> itp) utp)
a) =
                Expr t (BaseArrayType (idx ::> itp) utp)
-> ArrayResultWrapper (Expr t) (idx ::> itp) utp
forall (f :: BaseType -> Type) (idx :: Ctx BaseType)
       (tp :: BaseType).
f (BaseArrayType idx tp) -> ArrayResultWrapper f idx tp
ArrayResultWrapper (Expr t (BaseArrayType (idx ::> itp) utp)
 -> ArrayResultWrapper (Expr t) (idx ::> itp) utp)
-> IO (Expr t (BaseArrayType (idx ::> itp) utp))
-> IO (ArrayResultWrapper (Expr t) (idx ::> itp) utp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> EvalHashTables t
-> ExprBuilder t st fs
-> Expr t (BaseArrayType (idx ::> itp) utp)
-> IO (Expr t (BaseArrayType (idx ::> itp) utp))
forall t (st :: Type -> Type) fs (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
evalBoundVars' EvalHashTables t
tbls ExprBuilder t st fs
sym Expr t (BaseArrayType (idx ::> itp) utp)
a
          Assignment (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
args' <- (forall (x :: BaseType).
 ArrayResultWrapper (Expr t) (idx ::> itp) x
 -> IO (ArrayResultWrapper (Expr t) (idx ::> itp) x))
-> Assignment
     (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
-> IO
     (Assignment
        (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d))
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC forall (idx :: Ctx BaseType) (itp :: BaseType) (utp :: BaseType).
ArrayResultWrapper (Expr t) (idx ::> itp) utp
-> IO (ArrayResultWrapper (Expr t) (idx ::> itp) utp)
forall (x :: BaseType).
ArrayResultWrapper (Expr t) (idx ::> itp) x
-> IO (ArrayResultWrapper (Expr t) (idx ::> itp) x)
evalWrapper Assignment (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
args
          if Bool -> Bool
not Bool
changed Bool -> Bool -> Bool
&& Assignment (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
args Assignment (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
-> Assignment
     (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
-> Bool
forall a. Eq a => a -> a -> Bool
== Assignment (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
args' then
            Expr t ret -> IO (Expr t ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t ret
e0
           else
            ExprBuilder t st fs
-> SymFn (ExprBuilder t st fs) (ctx ::> d) r
-> Assignment
     (ArrayResultWrapper (SymExpr (ExprBuilder t st fs)) (idx ::> itp))
     (ctx ::> d)
-> IO (SymArray (ExprBuilder t st fs) (idx ::> itp) r)
forall sym (ctx :: Ctx BaseType) (d :: BaseType) (r :: BaseType)
       (idx :: Ctx BaseType) (itp :: BaseType).
IsExprBuilder sym =>
sym
-> SymFn sym (ctx ::> d) r
-> Assignment
     (ArrayResultWrapper (SymExpr sym) (idx ::> itp)) (ctx ::> d)
-> IO (SymArray sym (idx ::> itp) r)
arrayMap ExprBuilder t st fs
sym SymFn (ExprBuilder t st fs) (ctx ::> d) r
ExprSymFn t (ctx ::> d) r
f' Assignment
  (ArrayResultWrapper (SymExpr (ExprBuilder t st fs)) (idx ::> itp))
  (ctx ::> d)
Assignment (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
args'
        ArrayTrueOnEntries ExprSymFn t (idx ::> itp) BaseBoolType
f Expr t (BaseArrayType (idx ::> itp) BaseBoolType)
a -> do
          (Bool
changed, ExprSymFn t (idx ::> itp) BaseBoolType
f') <- EvalHashTables t
-> ExprBuilder t st fs
-> ExprSymFn t (idx ::> itp) BaseBoolType
-> IO (Bool, ExprSymFn t (idx ::> itp) BaseBoolType)
forall t (st :: Type -> Type) fs (idx :: Ctx BaseType)
       (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs
-> ExprSymFn t idx ret
-> IO (Bool, ExprSymFn t idx ret)
evalSimpleFn EvalHashTables t
tbls ExprBuilder t st fs
sym ExprSymFn t (idx ::> itp) BaseBoolType
f
          Expr t (BaseArrayType (idx ::> itp) BaseBoolType)
a' <- EvalHashTables t
-> ExprBuilder t st fs
-> Expr t (BaseArrayType (idx ::> itp) BaseBoolType)
-> IO (Expr t (BaseArrayType (idx ::> itp) BaseBoolType))
forall t (st :: Type -> Type) fs (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
evalBoundVars' EvalHashTables t
tbls ExprBuilder t st fs
sym Expr t (BaseArrayType (idx ::> itp) BaseBoolType)
a
          if Bool -> Bool
not Bool
changed Bool -> Bool -> Bool
&& Expr t (BaseArrayType (idx ::> itp) BaseBoolType)
a Expr t (BaseArrayType (idx ::> itp) BaseBoolType)
-> Expr t (BaseArrayType (idx ::> itp) BaseBoolType) -> Bool
forall a. Eq a => a -> a -> Bool
== Expr t (BaseArrayType (idx ::> itp) BaseBoolType)
a' then
            Expr t ret -> IO (Expr t ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t ret
e0
           else
            ExprBuilder t st fs
-> SymFn (ExprBuilder t st fs) (idx ::> itp) BaseBoolType
-> SymArray (ExprBuilder t st fs) (idx ::> itp) BaseBoolType
-> IO (Pred (ExprBuilder t st fs))
forall sym (idx :: Ctx BaseType) (itp :: BaseType).
IsExprBuilder sym =>
sym
-> SymFn sym (idx ::> itp) BaseBoolType
-> SymArray sym (idx ::> itp) BaseBoolType
-> IO (Pred sym)
arrayTrueOnEntries ExprBuilder t st fs
sym SymFn (ExprBuilder t st fs) (idx ::> itp) BaseBoolType
ExprSymFn t (idx ::> itp) BaseBoolType
f' SymArray (ExprBuilder t st fs) (idx ::> itp) BaseBoolType
Expr t (BaseArrayType (idx ::> itp) BaseBoolType)
a'
        FnApp ExprSymFn t args ret
f Assignment (Expr t) args
a -> do
          (Bool
changed, ExprSymFn t args ret
f') <- EvalHashTables t
-> ExprBuilder t st fs
-> ExprSymFn t args ret
-> IO (Bool, ExprSymFn t args ret)
forall t (st :: Type -> Type) fs (idx :: Ctx BaseType)
       (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs
-> ExprSymFn t idx ret
-> IO (Bool, ExprSymFn t idx ret)
evalSimpleFn EvalHashTables t
tbls ExprBuilder t st fs
sym ExprSymFn t args ret
f
          Assignment (Expr t) args
a' <- (forall (tp :: BaseType). Expr t tp -> IO (Expr t tp))
-> Assignment (Expr t) args -> IO (Assignment (Expr t) args)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC (EvalHashTables t
-> ExprBuilder t st fs -> Expr t x -> IO (Expr t x)
forall t (st :: Type -> Type) fs (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
evalBoundVars' EvalHashTables t
tbls ExprBuilder t st fs
sym) Assignment (Expr t) args
a
          if Bool -> Bool
not Bool
changed Bool -> Bool -> Bool
&& Assignment (Expr t) args
a Assignment (Expr t) args -> Assignment (Expr t) args -> Bool
forall a. Eq a => a -> a -> Bool
== Assignment (Expr t) args
a' then
            Expr t ret -> IO (Expr t ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t ret
e0
           else
            ExprBuilder t st fs
-> SymFn (ExprBuilder t st fs) args ret
-> Assignment (SymExpr (ExprBuilder t st fs)) args
-> IO (SymExpr (ExprBuilder t st fs) ret)
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
applySymFn ExprBuilder t st fs
sym SymFn (ExprBuilder t st fs) args ret
ExprSymFn t args ret
f' Assignment (SymExpr (ExprBuilder t st fs)) args
Assignment (Expr t) args
a'

    BoundVarExpr{} -> HashTable RealWorld (Expr t) (Expr t)
-> Expr t ret -> IO (Expr t ret) -> IO (Expr t ret)
forall k (k :: k -> Type) (a :: k -> Type) (tp :: k).
(HashableF k, TestEquality k) =>
HashTable RealWorld k a -> k tp -> IO (a tp) -> IO (a tp)
cachedEval (EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
forall t. EvalHashTables t -> HashTable RealWorld (Expr t) (Expr t)
exprTable EvalHashTables t
tbls) Expr t ret
e0 (IO (Expr t ret) -> IO (Expr t ret))
-> IO (Expr t ret) -> IO (Expr t ret)
forall a b. (a -> b) -> a -> b
$ Expr t ret -> IO (Expr t ret)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t ret
e0

initHashTable :: (HashableF key, TestEquality key)
              => Ctx.Assignment key args
              -> Ctx.Assignment val args
              -> ST s (PH.HashTable s key val)
initHashTable :: Assignment key args
-> Assignment val args -> ST s (HashTable s key val)
initHashTable Assignment key args
keys Assignment val args
vals = do
  let sz :: Size args
sz = Assignment key args -> Size args
forall k (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment key args
keys
  HashTable s key val
tbl <- Int -> ST s (HashTable s key val)
forall k1 s (k2 :: k1 -> Type) (v :: k1 -> Type).
Int -> ST s (HashTable s k2 v)
PH.newSized (Size args -> Int
forall k (ctx :: Ctx k). Size ctx -> Int
Ctx.sizeInt Size args
sz)
  Size args
-> (forall (tp :: k). Index args tp -> ST s ()) -> ST s ()
forall k (ctx :: Ctx k) (m :: Type -> Type).
Applicative m =>
Size ctx -> (forall (tp :: k). Index ctx tp -> m ()) -> m ()
Ctx.forIndexM Size args
sz ((forall (tp :: k). Index args tp -> ST s ()) -> ST s ())
-> (forall (tp :: k). Index args tp -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Index args tp
i -> do
    HashTable s key val -> key tp -> val tp -> ST s ()
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
PH.insert HashTable s key val
tbl (Assignment key args
keys Assignment key args -> Index args tp -> key tp
forall k (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index args tp
i) (Assignment val args
vals Assignment val args -> Index args tp -> val tp
forall k (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index args tp
i)
  HashTable s key val -> ST s (HashTable s key val)
forall (m :: Type -> Type) a. Monad m => a -> m a
return HashTable s key val
tbl

-- | This evaluates the term with the given bound variables rebound to
-- the given arguments.
--
-- The algorithm works by traversing the subterms in the term in a bottom-up
-- fashion while using a hash-table to memoize results for shared subterms.  The
-- hash-table is pre-populated so that the bound variables map to the element,
-- so we do not need any extra map lookup when checking to see if a variable is
-- bound.
--
-- NOTE: This function assumes that variables in the substitution are not
-- themselves bound in the term (e.g. in a function definition or quantifier).
-- If this is not respected, then 'evalBoundVars' will call 'fail' with an
-- error message.
evalBoundVars :: ExprBuilder t st fs
              -> Expr t ret
              -> Ctx.Assignment (ExprBoundVar t) args
              -> Ctx.Assignment (Expr t) args
              -> IO (Expr t ret)
evalBoundVars :: ExprBuilder t st fs
-> Expr t ret
-> Assignment (ExprBoundVar t) args
-> Assignment (Expr t) args
-> IO (Expr t ret)
evalBoundVars ExprBuilder t st fs
sym Expr t ret
e Assignment (ExprBoundVar t) args
vars Assignment (Expr t) args
exprs = do
  HashTable RealWorld (Expr t) (Expr t)
expr_tbl <- ST RealWorld (HashTable RealWorld (Expr t) (Expr t))
-> IO (HashTable RealWorld (Expr t) (Expr t))
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (HashTable RealWorld (Expr t) (Expr t))
 -> IO (HashTable RealWorld (Expr t) (Expr t)))
-> ST RealWorld (HashTable RealWorld (Expr t) (Expr t))
-> IO (HashTable RealWorld (Expr t) (Expr t))
forall a b. (a -> b) -> a -> b
$ Assignment (Expr t) args
-> Assignment (Expr t) args
-> ST RealWorld (HashTable RealWorld (Expr t) (Expr t))
forall k (key :: k -> Type) (args :: Ctx k) (val :: k -> Type) s.
(HashableF key, TestEquality key) =>
Assignment key args
-> Assignment val args -> ST s (HashTable s key val)
initHashTable ((forall (x :: BaseType). ExprBoundVar t x -> Expr t x)
-> Assignment (ExprBoundVar t) args -> Assignment (Expr t) args
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall t (tp :: BaseType). ExprBoundVar t tp -> Expr t tp
forall (x :: BaseType). ExprBoundVar t x -> Expr t x
BoundVarExpr Assignment (ExprBoundVar t) args
vars) Assignment (Expr t) args
exprs
  HashTable RealWorld (Nonce t) (CachedSymFn t)
fn_tbl  <- ST RealWorld (HashTable RealWorld (Nonce t) (CachedSymFn t))
-> IO (HashTable RealWorld (Nonce t) (CachedSymFn t))
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (HashTable RealWorld (Nonce t) (CachedSymFn t))
 -> IO (HashTable RealWorld (Nonce t) (CachedSymFn t)))
-> ST RealWorld (HashTable RealWorld (Nonce t) (CachedSymFn t))
-> IO (HashTable RealWorld (Nonce t) (CachedSymFn t))
forall a b. (a -> b) -> a -> b
$ ST RealWorld (HashTable RealWorld (Nonce t) (CachedSymFn t))
forall k s (key :: k -> Type) (val :: k -> Type).
ST s (HashTable s key val)
PH.new
  let tbls :: EvalHashTables t
tbls = EvalHashTables :: forall t.
HashTable RealWorld (Expr t) (Expr t)
-> HashTable RealWorld (Nonce t) (CachedSymFn t)
-> EvalHashTables t
EvalHashTables { exprTable :: HashTable RealWorld (Expr t) (Expr t)
exprTable = HashTable RealWorld (Expr t) (Expr t)
expr_tbl
                            , fnTable :: HashTable RealWorld (Nonce t) (CachedSymFn t)
fnTable  = HashTable RealWorld (Nonce t) (CachedSymFn t)
fn_tbl
                            }
  EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
forall t (st :: Type -> Type) fs (ret :: BaseType).
EvalHashTables t
-> ExprBuilder t st fs -> Expr t ret -> IO (Expr t ret)
evalBoundVars' EvalHashTables t
tbls ExprBuilder t st fs
sym Expr t ret
e

-- | This attempts to lookup an entry in a symbolic array.
--
-- It patterns maps on the array constructor.
sbConcreteLookup :: forall t st fs d tp range
                 . ExprBuilder t st fs
                   -- ^ Simple builder for creating terms.
                 -> Expr t (BaseArrayType (d::>tp) range)
                    -- ^ Array to lookup value in.
                 -> Maybe (Ctx.Assignment IndexLit (d::>tp))
                    -- ^ A concrete index that corresponds to the index or nothing
                    -- if the index is symbolic.
                 -> Ctx.Assignment (Expr t) (d::>tp)
                    -- ^ The index to lookup.
                 -> IO (Expr t range)
sbConcreteLookup :: ExprBuilder t st fs
-> Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (Assignment IndexLit (d ::> tp))
-> Assignment (Expr t) (d ::> tp)
-> IO (Expr t range)
sbConcreteLookup ExprBuilder t st fs
sym Expr t (BaseArrayType (d ::> tp) range)
arr0 Maybe (Assignment IndexLit (d ::> tp))
mcidx Assignment (Expr t) (d ::> tp)
idx
    -- Try looking up a write to a concrete address.
  | Just (ArrayMap Assignment BaseTypeRepr (i ::> itp)
_ BaseTypeRepr tp
_ ArrayUpdateMap (Expr t) (i ::> itp) tp
entry_map Expr t (BaseArrayType (i ::> itp) tp)
def) <- Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (App (Expr t) (BaseArrayType (d ::> tp) range))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (BaseArrayType (d ::> tp) range)
arr0
  , Just Assignment IndexLit (d ::> tp)
cidx <- Maybe (Assignment IndexLit (d ::> tp))
mcidx =
      case Assignment IndexLit (d ::> tp)
-> ArrayUpdateMap (Expr t) (d ::> tp) tp -> Maybe (Expr t tp)
forall (ctx :: Ctx BaseType) (e :: BaseType -> Type)
       (tp :: BaseType).
Assignment IndexLit ctx -> ArrayUpdateMap e ctx tp -> Maybe (e tp)
AUM.lookup Assignment IndexLit (d ::> tp)
cidx ArrayUpdateMap (Expr t) (d ::> tp) tp
ArrayUpdateMap (Expr t) (i ::> itp) tp
entry_map of
        Just Expr t tp
v -> Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
v
        Maybe (Expr t tp)
Nothing -> ExprBuilder t st fs
-> Expr t (BaseArrayType (i ::> itp) tp)
-> Maybe (Assignment IndexLit (i ::> itp))
-> Assignment (Expr t) (i ::> itp)
-> IO (Expr t tp)
forall t (st :: Type -> Type) fs (d :: Ctx BaseType)
       (tp :: BaseType) (range :: BaseType).
ExprBuilder t st fs
-> Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (Assignment IndexLit (d ::> tp))
-> Assignment (Expr t) (d ::> tp)
-> IO (Expr t range)
sbConcreteLookup ExprBuilder t st fs
sym Expr t (BaseArrayType (i ::> itp) tp)
def Maybe (Assignment IndexLit (d ::> tp))
Maybe (Assignment IndexLit (i ::> itp))
mcidx Assignment (Expr t) (d ::> tp)
Assignment (Expr t) (i ::> itp)
idx
    -- Evaluate function arrays on ground values.
  | Just (ArrayFromFn ExprSymFn t (idx ::> itp) ret
f) <- Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (NonceApp t (Expr t) (BaseArrayType (d ::> tp) range))
forall t (tp :: BaseType).
Expr t tp -> Maybe (NonceApp t (Expr t) tp)
asNonceApp Expr t (BaseArrayType (d ::> tp) range)
arr0 = do
      ExprBuilder t st fs
-> ExprSymFn t (idx ::> itp) ret
-> Assignment (Expr t) (idx ::> itp)
-> IO (Expr t ret)
forall t (st :: Type -> Type) fs (args :: Ctx BaseType)
       (ret :: BaseType).
ExprBuilder t st fs
-> ExprSymFn t args ret
-> Assignment (Expr t) args
-> IO (Expr t ret)
betaReduce ExprBuilder t st fs
sym ExprSymFn t (idx ::> itp) ret
f Assignment (Expr t) (d ::> tp)
Assignment (Expr t) (idx ::> itp)
idx

    -- Lookups on constant arrays just return value
  | Just (ConstantArray Assignment BaseTypeRepr (i ::> tp)
_ BaseTypeRepr b
_ Expr t b
v) <- Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (App (Expr t) (BaseArrayType (d ::> tp) range))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (BaseArrayType (d ::> tp) range)
arr0 = do
      Expr t b -> IO (Expr t b)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t b
v
    -- Lookups on mux arrays just distribute over mux.
  | Just (BaseIte BaseTypeRepr (BaseArrayType (d ::> tp) range)
_ Integer
_ Expr t BaseBoolType
p Expr t (BaseArrayType (d ::> tp) range)
x Expr t (BaseArrayType (d ::> tp) range)
y) <- Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (App (Expr t) (BaseArrayType (d ::> tp) range))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (BaseArrayType (d ::> tp) range)
arr0 = do
      Expr t range
xv <- ExprBuilder t st fs
-> Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (Assignment IndexLit (d ::> tp))
-> Assignment (Expr t) (d ::> tp)
-> IO (Expr t range)
forall t (st :: Type -> Type) fs (d :: Ctx BaseType)
       (tp :: BaseType) (range :: BaseType).
ExprBuilder t st fs
-> Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (Assignment IndexLit (d ::> tp))
-> Assignment (Expr t) (d ::> tp)
-> IO (Expr t range)
sbConcreteLookup ExprBuilder t st fs
sym Expr t (BaseArrayType (d ::> tp) range)
x Maybe (Assignment IndexLit (d ::> tp))
mcidx Assignment (Expr t) (d ::> tp)
idx
      Expr t range
yv <- ExprBuilder t st fs
-> Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (Assignment IndexLit (d ::> tp))
-> Assignment (Expr t) (d ::> tp)
-> IO (Expr t range)
forall t (st :: Type -> Type) fs (d :: Ctx BaseType)
       (tp :: BaseType) (range :: BaseType).
ExprBuilder t st fs
-> Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (Assignment IndexLit (d ::> tp))
-> Assignment (Expr t) (d ::> tp)
-> IO (Expr t range)
sbConcreteLookup ExprBuilder t st fs
sym Expr t (BaseArrayType (d ::> tp) range)
y Maybe (Assignment IndexLit (d ::> tp))
mcidx Assignment (Expr t) (d ::> tp)
idx
      ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymExpr (ExprBuilder t st fs) range
-> SymExpr (ExprBuilder t st fs) range
-> IO (SymExpr (ExprBuilder t st fs) range)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
baseTypeIte ExprBuilder t st fs
sym Pred (ExprBuilder t st fs)
Expr t BaseBoolType
p SymExpr (ExprBuilder t st fs) range
Expr t range
xv SymExpr (ExprBuilder t st fs) range
Expr t range
yv
  | Just (MapOverArrays ExprSymFn t (ctx ::> d) r
f Assignment BaseTypeRepr (idx ::> itp)
_ Assignment (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
args) <- Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (NonceApp t (Expr t) (BaseArrayType (d ::> tp) range))
forall t (tp :: BaseType).
Expr t tp -> Maybe (NonceApp t (Expr t) tp)
asNonceApp Expr t (BaseArrayType (d ::> tp) range)
arr0 = do
      let eval :: ArrayResultWrapper (Expr t) (d::>tp) utp
               -> IO (Expr t utp)
          eval :: ArrayResultWrapper (Expr t) (d ::> tp) utp -> IO (Expr t utp)
eval ArrayResultWrapper (Expr t) (d ::> tp) utp
a = ExprBuilder t st fs
-> Expr t (BaseArrayType (d ::> tp) utp)
-> Maybe (Assignment IndexLit (d ::> tp))
-> Assignment (Expr t) (d ::> tp)
-> IO (Expr t utp)
forall t (st :: Type -> Type) fs (d :: Ctx BaseType)
       (tp :: BaseType) (range :: BaseType).
ExprBuilder t st fs
-> Expr t (BaseArrayType (d ::> tp) range)
-> Maybe (Assignment IndexLit (d ::> tp))
-> Assignment (Expr t) (d ::> tp)
-> IO (Expr t range)
sbConcreteLookup ExprBuilder t st fs
sym (ArrayResultWrapper (Expr t) (d ::> tp) utp
-> Expr t (BaseArrayType (d ::> tp) utp)
forall (f :: BaseType -> Type) (idx :: Ctx BaseType)
       (tp :: BaseType).
ArrayResultWrapper f idx tp -> f (BaseArrayType idx tp)
unwrapArrayResult ArrayResultWrapper (Expr t) (d ::> tp) utp
a) Maybe (Assignment IndexLit (d ::> tp))
mcidx Assignment (Expr t) (d ::> tp)
idx
      ExprBuilder t st fs
-> ExprSymFn t (ctx ::> d) r
-> Assignment (Expr t) (ctx ::> d)
-> IO (Expr t r)
forall t (st :: Type -> Type) fs (args :: Ctx BaseType)
       (ret :: BaseType).
ExprBuilder t st fs
-> ExprSymFn t args ret
-> Assignment (Expr t) args
-> IO (Expr t ret)
betaReduce ExprBuilder t st fs
sym ExprSymFn t (ctx ::> d) r
f (Assignment (Expr t) (ctx ::> d) -> IO (Expr t r))
-> IO (Assignment (Expr t) (ctx ::> d)) -> IO (Expr t r)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (x :: BaseType).
 ArrayResultWrapper (Expr t) (idx ::> itp) x -> IO (Expr t x))
-> Assignment
     (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
-> IO (Assignment (Expr t) (ctx ::> d))
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC forall (utp :: BaseType).
ArrayResultWrapper (Expr t) (d ::> tp) utp -> IO (Expr t utp)
forall (x :: BaseType).
ArrayResultWrapper (Expr t) (idx ::> itp) x -> IO (Expr t x)
eval Assignment (ArrayResultWrapper (Expr t) (idx ::> itp)) (ctx ::> d)
args
    -- Create select index.
  | Bool
otherwise = do
    case Expr t (BaseArrayType (d ::> tp) range)
-> BaseTypeRepr (BaseArrayType (d ::> tp) range)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType Expr t (BaseArrayType (d ::> tp) range)
arr0 of
      BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_ BaseTypeRepr xs
range ->
        ExprBuilder t st fs -> App (Expr t) xs -> IO (Expr t xs)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym (BaseTypeRepr xs
-> Expr t (BaseArrayType (d ::> tp) xs)
-> Assignment (Expr t) (d ::> tp)
-> App (Expr t) xs
forall (b :: BaseType) (e :: BaseType -> Type) (i :: Ctx BaseType)
       (tp :: BaseType).
BaseTypeRepr b
-> e (BaseArrayType (i ::> tp) b)
-> Assignment e (i ::> tp)
-> App e b
SelectArray BaseTypeRepr xs
range Expr t (BaseArrayType (d ::> tp) range)
Expr t (BaseArrayType (d ::> tp) xs)
arr0 Assignment (Expr t) (d ::> tp)
idx)

----------------------------------------------------------------------
-- Expression builder instances

-- | Evaluate a weighted sum of integer values.
intSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SR.SemiRingInteger -> IO (IntegerExpr t)
intSum :: ExprBuilder t st fs
-> WeightedSum (Expr t) SemiRingInteger -> IO (IntegerExpr t)
intSum ExprBuilder t st fs
sym WeightedSum (Expr t) SemiRingInteger
s = ExprBuilder t st fs
-> WeightedSum (Expr t) SemiRingInteger
-> IO (Expr t (SemiRingBase SemiRingInteger))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym WeightedSum (Expr t) SemiRingInteger
s

-- | Evaluate a weighted sum of real values.
realSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SR.SemiRingReal -> IO (RealExpr t)
realSum :: ExprBuilder t st fs
-> WeightedSum (Expr t) SemiRingReal -> IO (RealExpr t)
realSum ExprBuilder t st fs
sym WeightedSum (Expr t) SemiRingReal
s = ExprBuilder t st fs
-> WeightedSum (Expr t) SemiRingReal
-> IO (Expr t (SemiRingBase SemiRingReal))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym WeightedSum (Expr t) SemiRingReal
s

bvSum :: ExprBuilder t st fs -> WeightedSum (Expr t) (SR.SemiRingBV flv w) -> IO (BVExpr t w)
bvSum :: ExprBuilder t st fs
-> WeightedSum (Expr t) (SemiRingBV flv w) -> IO (BVExpr t w)
bvSum ExprBuilder t st fs
sym WeightedSum (Expr t) (SemiRingBV flv w)
s = ExprBuilder t st fs
-> WeightedSum (Expr t) (SemiRingBV flv w)
-> IO (Expr t (SemiRingBase (SemiRingBV flv w)))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym WeightedSum (Expr t) (SemiRingBV flv w)
s

conjPred :: ExprBuilder t st fs -> BoolMap (Expr t) -> IO (BoolExpr t)
conjPred :: ExprBuilder t st fs -> BoolMap (Expr t) -> IO (BoolExpr t)
conjPred ExprBuilder t st fs
sym BoolMap (Expr t)
bm =
  case BoolMap (Expr t) -> BoolMapView (Expr t)
forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
BM.viewBoolMap BoolMap (Expr t)
bm of
    BoolMapView (Expr t)
BoolMapUnit     -> BoolExpr t -> IO (BoolExpr t)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BoolExpr t -> IO (BoolExpr t)) -> BoolExpr t -> IO (BoolExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> Pred (ExprBuilder t st fs)
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred ExprBuilder t st fs
sym
    BoolMapView (Expr t)
BoolMapDualUnit -> BoolExpr t -> IO (BoolExpr t)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BoolExpr t -> IO (BoolExpr t)) -> BoolExpr t -> IO (BoolExpr t)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs -> Pred (ExprBuilder t st fs)
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred ExprBuilder t st fs
sym
    BoolMapTerms ((BoolExpr t
x,Polarity
p):|[]) ->
      case Polarity
p of
        Polarity
Positive -> BoolExpr t -> IO (BoolExpr t)
forall (m :: Type -> Type) a. Monad m => a -> m a
return BoolExpr t
x
        Polarity
Negative -> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred ExprBuilder t st fs
sym Pred (ExprBuilder t st fs)
BoolExpr t
x
    BoolMapView (Expr t)
_ -> ExprBuilder t st fs -> App (Expr t) BaseBoolType -> IO (BoolExpr t)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym (App (Expr t) BaseBoolType -> IO (BoolExpr t))
-> App (Expr t) BaseBoolType -> IO (BoolExpr t)
forall a b. (a -> b) -> a -> b
$ BoolMap (Expr t) -> App (Expr t) BaseBoolType
forall (e :: BaseType -> Type). BoolMap e -> App e BaseBoolType
ConjPred BoolMap (Expr t)
bm

bvUnary :: (1 <= w) => ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w)
bvUnary :: ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w)
bvUnary ExprBuilder t st fs
sym UnaryBV (BoolExpr t) w
u
  -- BGS: We probably don't need to re-truncate the result, but
  -- until we refactor UnaryBV to use BV w instead of integer,
  -- that'll have to wait.
  | Just Integer
v <-  UnaryBV (BoolExpr t) w -> Maybe Integer
forall (p :: BaseType -> Type) (w :: Nat).
IsExpr p =>
UnaryBV (p BaseBoolType) w -> Maybe Integer
UnaryBV.asConstant UnaryBV (BoolExpr t) w
u = ExprBuilder t st fs
-> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit ExprBuilder t st fs
sym NatRepr w
w (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
v)
  | Bool
otherwise = ExprBuilder t st fs
-> App (Expr t) (BaseBVType w) -> IO (BVExpr t w)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym (UnaryBV (BoolExpr t) w -> App (Expr t) (BaseBVType w)
forall (n :: Nat) (e :: BaseType -> Type).
(1 <= n) =>
UnaryBV (e BaseBoolType) n -> App e (BaseBVType n)
BVUnaryTerm UnaryBV (BoolExpr t) w
u)
  where w :: NatRepr w
w = UnaryBV (BoolExpr t) w -> NatRepr w
forall p (n :: Nat). UnaryBV p n -> NatRepr n
UnaryBV.width UnaryBV (BoolExpr t) w
u

asUnaryBV :: (?unaryThreshold :: Int)
          => ExprBuilder t st fs
          -> BVExpr t n
          -> Maybe (UnaryBV (BoolExpr t) n)
asUnaryBV :: ExprBuilder t st fs -> BVExpr t n -> Maybe (UnaryBV (BoolExpr t) n)
asUnaryBV ExprBuilder t st fs
sym BVExpr t n
e
  | Just (BVUnaryTerm UnaryBV (BoolExpr t) n
u) <- BVExpr t n -> Maybe (App (Expr t) (BaseBVType n))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp BVExpr t n
e = UnaryBV (BoolExpr t) n -> Maybe (UnaryBV (BoolExpr t) n)
forall a. a -> Maybe a
Just UnaryBV (BoolExpr t) n
u
  | ?unaryThreshold::Int
Int
?unaryThreshold Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Maybe (UnaryBV (BoolExpr t) n)
forall a. Maybe a
Nothing
  | SemiRingLiteral (SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
w) Coefficient sr
v ProgramLoc
_ <- BVExpr t n
e = UnaryBV (BoolExpr t) n -> Maybe (UnaryBV (BoolExpr t) n)
forall a. a -> Maybe a
Just (UnaryBV (BoolExpr t) n -> Maybe (UnaryBV (BoolExpr t) n))
-> UnaryBV (BoolExpr t) n -> Maybe (UnaryBV (BoolExpr t) n)
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs
-> NatRepr w -> Integer -> UnaryBV (Pred (ExprBuilder t st fs)) w
forall sym (n :: Nat).
IsExprBuilder sym =>
sym -> NatRepr n -> Integer -> UnaryBV (Pred sym) n
UnaryBV.constant ExprBuilder t st fs
sym NatRepr w
w (BV n -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV n
Coefficient sr
v)
  | Bool
otherwise = Maybe (UnaryBV (BoolExpr t) n)
forall a. Maybe a
Nothing

-- | This create a unary bitvector representing if the size is not too large.
sbTryUnaryTerm :: (1 <= w, ?unaryThreshold :: Int)
               => ExprBuilder t st fs
               -> Maybe (IO (UnaryBV (BoolExpr t) w))
               -> IO (BVExpr t w)
               -> IO (BVExpr t w)
sbTryUnaryTerm :: ExprBuilder t st fs
-> Maybe (IO (UnaryBV (BoolExpr t) w))
-> IO (BVExpr t w)
-> IO (BVExpr t w)
sbTryUnaryTerm ExprBuilder t st fs
_sym Maybe (IO (UnaryBV (BoolExpr t) w))
Nothing IO (BVExpr t w)
fallback = IO (BVExpr t w)
fallback
sbTryUnaryTerm ExprBuilder t st fs
sym (Just IO (UnaryBV (BoolExpr t) w)
mku) IO (BVExpr t w)
fallback =
  do UnaryBV (BoolExpr t) w
u <- IO (UnaryBV (BoolExpr t) w)
mku
     if UnaryBV (BoolExpr t) w -> Int
forall p (n :: Nat). UnaryBV p n -> Int
UnaryBV.size UnaryBV (BoolExpr t) w
u Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ?unaryThreshold::Int
Int
?unaryThreshold then
       ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w)
forall (w :: Nat) t (st :: Type -> Type) fs.
(1 <= w) =>
ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w)
bvUnary ExprBuilder t st fs
sym UnaryBV (BoolExpr t) w
u
     else
       IO (BVExpr t w)
fallback

semiRingProd ::
  ExprBuilder t st fs ->
  SemiRingProduct (Expr t) sr ->
  IO (Expr t (SR.SemiRingBase sr))
semiRingProd :: ExprBuilder t st fs
-> SemiRingProduct (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingProd ExprBuilder t st fs
sym SemiRingProduct (Expr t) sr
pd
  | SemiRingProduct (Expr t) sr -> Bool
forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> Bool
WSum.nullProd SemiRingProduct (Expr t) sr
pd = ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
semiRingLit ExprBuilder t st fs
sym (SemiRingProduct (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WSum.prodRepr SemiRingProduct (Expr t) sr
pd) (SemiRingRepr sr -> Coefficient sr
forall (sr :: SemiRing). SemiRingRepr sr -> Coefficient sr
SR.one (SemiRingProduct (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WSum.prodRepr SemiRingProduct (Expr t) sr
pd))
  | Just Expr t (SemiRingBase sr)
v <- SemiRingProduct (Expr t) sr -> Maybe (Expr t (SemiRingBase sr))
forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> Maybe (f (SemiRingBase sr))
WSum.asProdVar SemiRingProduct (Expr t) sr
pd = Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t (SemiRingBase sr)
v
  | Bool
otherwise = ExprBuilder t st fs
-> App (Expr t) (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym (App (Expr t) (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr)))
-> App (Expr t) (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall a b. (a -> b) -> a -> b
$ SemiRingProduct (Expr t) sr -> App (Expr t) (SemiRingBase sr)
forall (e :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct e sr -> App e (SemiRingBase sr)
SemiRingProd SemiRingProduct (Expr t) sr
pd

semiRingSum ::
  ExprBuilder t st fs ->
  WeightedSum (Expr t) sr ->
  IO (Expr t (SR.SemiRingBase sr))
semiRingSum :: ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym WeightedSum (Expr t) sr
s
    | Just Coefficient sr
c <- WeightedSum (Expr t) sr -> Maybe (Coefficient sr)
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> Maybe (Coefficient sr)
WSum.asConstant WeightedSum (Expr t) sr
s = ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
semiRingLit ExprBuilder t st fs
sym (WeightedSum (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> SemiRingRepr sr
WSum.sumRepr WeightedSum (Expr t) sr
s) Coefficient sr
c
    | Just Expr t (SemiRingBase sr)
r <- WeightedSum (Expr t) sr -> Maybe (Expr t (SemiRingBase sr))
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> Maybe (f (SemiRingBase sr))
WSum.asVar WeightedSum (Expr t) sr
s      = Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t (SemiRingBase sr)
r
    | Bool
otherwise                   = ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
sum' ExprBuilder t st fs
sym WeightedSum (Expr t) sr
s

sum' ::
  ExprBuilder t st fs ->
  WeightedSum (Expr t) sr ->
  IO (Expr t (SR.SemiRingBase sr))
sum' :: ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
sum' ExprBuilder t st fs
sym WeightedSum (Expr t) sr
s = ExprBuilder t st fs
-> App (Expr t) (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym (App (Expr t) (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr)))
-> App (Expr t) (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall a b. (a -> b) -> a -> b
$ WeightedSum (Expr t) sr -> App (Expr t) (SemiRingBase sr)
forall (e :: BaseType -> Type) (sr :: SemiRing).
WeightedSum e sr -> App e (SemiRingBase sr)
SemiRingSum WeightedSum (Expr t) sr
s
{-# INLINE sum' #-}

scalarMul ::
   ExprBuilder t st fs ->
   SR.SemiRingRepr sr ->
   SR.Coefficient sr ->
   Expr t (SR.SemiRingBase sr) ->
   IO (Expr t (SR.SemiRingBase sr))
scalarMul :: ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
scalarMul ExprBuilder t st fs
sym SemiRingRepr sr
sr Coefficient sr
c Expr t (SemiRingBase sr)
x
  | SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
forall (sr :: SemiRing).
SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
SR.eq SemiRingRepr sr
sr (SemiRingRepr sr -> Coefficient sr
forall (sr :: SemiRing). SemiRingRepr sr -> Coefficient sr
SR.zero SemiRingRepr sr
sr) Coefficient sr
c = ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
semiRingLit ExprBuilder t st fs
sym SemiRingRepr sr
sr (SemiRingRepr sr -> Coefficient sr
forall (sr :: SemiRing). SemiRingRepr sr -> Coefficient sr
SR.zero SemiRingRepr sr
sr)
  | SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
forall (sr :: SemiRing).
SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
SR.eq SemiRingRepr sr
sr (SemiRingRepr sr -> Coefficient sr
forall (sr :: SemiRing). SemiRingRepr sr -> Coefficient sr
SR.one SemiRingRepr sr
sr)  Coefficient sr
c = Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t (SemiRingBase sr)
x
  | Just Coefficient sr
r <- SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
asSemiRingLit SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x =
    ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
semiRingLit ExprBuilder t st fs
sym SemiRingRepr sr
sr (SemiRingRepr sr
-> Coefficient sr -> Coefficient sr -> Coefficient sr
forall (sr :: SemiRing).
SemiRingRepr sr
-> Coefficient sr -> Coefficient sr -> Coefficient sr
SR.mul SemiRingRepr sr
sr Coefficient sr
c Coefficient sr
r)
  | Just WeightedSum (Expr t) sr
s <- SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (WeightedSum (Expr t) sr)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (WeightedSum (Expr t) sr)
asSemiRingSum SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x =
    ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
sum' ExprBuilder t st fs
sym (SemiRingRepr sr
-> Coefficient sr
-> WeightedSum (Expr t) sr
-> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr
-> Coefficient sr -> WeightedSum f sr -> WeightedSum f sr
WSum.scale SemiRingRepr sr
sr Coefficient sr
c WeightedSum (Expr t) sr
s)
  | Bool
otherwise =
    ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
sum' ExprBuilder t st fs
sym (SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr
-> Coefficient sr -> f (SemiRingBase sr) -> WeightedSum f sr
WSum.scaledVar SemiRingRepr sr
sr Coefficient sr
c Expr t (SemiRingBase sr)
x)

semiRingIte ::
  ExprBuilder t st fs ->
  SR.SemiRingRepr sr ->
  Expr t BaseBoolType ->
  Expr t (SR.SemiRingBase sr) ->
  Expr t (SR.SemiRingBase sr) ->
  IO (Expr t (SR.SemiRingBase sr))
semiRingIte :: ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t BaseBoolType
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingIte ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t BaseBoolType
c Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y
    -- evaluate as constants
  | Just Bool
True  <- Expr t BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Expr t BaseBoolType
c = Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t (SemiRingBase sr)
x
  | Just Bool
False <- Expr t BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Expr t BaseBoolType
c = Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t (SemiRingBase sr)
y

    -- reduce negations
  | Just (NotPred Expr t BaseBoolType
c') <- Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t BaseBoolType
c
  = ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t BaseBoolType
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t BaseBoolType
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingIte ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t BaseBoolType
c' Expr t (SemiRingBase sr)
y Expr t (SemiRingBase sr)
x

    -- remove the ite if the then and else cases are the same
  | Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr) -> Expr t (SemiRingBase sr) -> Bool
forall a. Eq a => a -> a -> Bool
== Expr t (SemiRingBase sr)
y = Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t (SemiRingBase sr)
x

    -- Try to extract common sum information.
  | (WeightedSum (Expr t) sr
z, WeightedSum (Expr t) sr
x',WeightedSum (Expr t) sr
y') <- WeightedSum (Expr t) sr
-> WeightedSum (Expr t) sr
-> (WeightedSum (Expr t) sr, WeightedSum (Expr t) sr,
    WeightedSum (Expr t) sr)
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
WeightedSum f sr
-> WeightedSum f sr
-> (WeightedSum f sr, WeightedSum f sr, WeightedSum f sr)
WSum.extractCommon (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
forall t (sr :: SemiRing).
HashableF (Expr t) =>
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x) (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
forall t (sr :: SemiRing).
HashableF (Expr t) =>
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum SemiRingRepr sr
sr Expr t (SemiRingBase sr)
y)
  , Bool -> Bool
not (SemiRingRepr sr -> WeightedSum (Expr t) sr -> Bool
forall (sr :: SemiRing) (f :: BaseType -> Type).
SemiRingRepr sr -> WeightedSum f sr -> Bool
WSum.isZero SemiRingRepr sr
sr WeightedSum (Expr t) sr
z) = do
    Expr t (SemiRingBase sr)
xr <- ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym WeightedSum (Expr t) sr
x'
    Expr t (SemiRingBase sr)
yr <- ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym WeightedSum (Expr t) sr
y'
    let sz :: Integer
sz = Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Expr t (SemiRingBase sr) -> Integer
forall t (tp :: BaseType). Expr t tp -> Integer
iteSize Expr t (SemiRingBase sr)
xr Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Expr t (SemiRingBase sr) -> Integer
forall t (tp :: BaseType). Expr t tp -> Integer
iteSize Expr t (SemiRingBase sr)
yr
    Expr t (SemiRingBase sr)
r <- ExprBuilder t st fs
-> App (Expr t) (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym (BaseTypeRepr (SemiRingBase sr)
-> Integer
-> Expr t BaseBoolType
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> App (Expr t) (SemiRingBase sr)
forall (tp :: BaseType) (e :: BaseType -> Type).
BaseTypeRepr tp
-> Integer -> e BaseBoolType -> e tp -> e tp -> App e tp
BaseIte (SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
forall (sr :: SemiRing).
SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
SR.semiRingBase SemiRingRepr sr
sr) Integer
sz Expr t BaseBoolType
c Expr t (SemiRingBase sr)
xr Expr t (SemiRingBase sr)
yr)
    ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym (WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr)))
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall a b. (a -> b) -> a -> b
$! SemiRingRepr sr
-> WeightedSum (Expr t) sr
-> Expr t (SemiRingBase sr)
-> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr
-> WeightedSum f sr -> f (SemiRingBase sr) -> WeightedSum f sr
WSum.addVar SemiRingRepr sr
sr WeightedSum (Expr t) sr
z Expr t (SemiRingBase sr)
r

    -- final fallback, create the ite term
  | Bool
otherwise =
      let sz :: Integer
sz = Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Expr t (SemiRingBase sr) -> Integer
forall t (tp :: BaseType). Expr t tp -> Integer
iteSize Expr t (SemiRingBase sr)
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Expr t (SemiRingBase sr) -> Integer
forall t (tp :: BaseType). Expr t tp -> Integer
iteSize Expr t (SemiRingBase sr)
y in
      ExprBuilder t st fs
-> App (Expr t) (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym (BaseTypeRepr (SemiRingBase sr)
-> Integer
-> Expr t BaseBoolType
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> App (Expr t) (SemiRingBase sr)
forall (tp :: BaseType) (e :: BaseType -> Type).
BaseTypeRepr tp
-> Integer -> e BaseBoolType -> e tp -> e tp -> App e tp
BaseIte (SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
forall (sr :: SemiRing).
SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
SR.semiRingBase SemiRingRepr sr
sr) Integer
sz Expr t BaseBoolType
c Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y)


mkIte ::
  ExprBuilder t st fs ->
  Expr t BaseBoolType ->
  Expr t bt ->
  Expr t bt ->
  IO (Expr t bt)
mkIte :: ExprBuilder t st fs
-> Expr t BaseBoolType -> Expr t bt -> Expr t bt -> IO (Expr t bt)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
c Expr t bt
x Expr t bt
y
    -- evaluate as constants
  | Just Bool
True  <- Expr t BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Expr t BaseBoolType
c = Expr t bt -> IO (Expr t bt)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t bt
x
  | Just Bool
False <- Expr t BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Expr t BaseBoolType
c = Expr t bt -> IO (Expr t bt)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t bt
y

    -- reduce negations
  | Just (NotPred Expr t BaseBoolType
c') <- Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t BaseBoolType
c
  = ExprBuilder t st fs
-> Expr t BaseBoolType -> Expr t bt -> Expr t bt -> IO (Expr t bt)
forall t (st :: Type -> Type) fs (bt :: BaseType).
ExprBuilder t st fs
-> Expr t BaseBoolType -> Expr t bt -> Expr t bt -> IO (Expr t bt)
mkIte ExprBuilder t st fs
sym Expr t BaseBoolType
c' Expr t bt
y Expr t bt
x

    -- remove the ite if the then and else cases are the same
  | Expr t bt
x Expr t bt -> Expr t bt -> Bool
forall a. Eq a => a -> a -> Bool
== Expr t bt
y = Expr t bt -> IO (Expr t bt)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t bt
x

  | Bool
otherwise =
      let sz :: Integer
sz = Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Expr t bt -> Integer
forall t (tp :: BaseType). Expr t tp -> Integer
iteSize Expr t bt
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Expr t bt -> Integer
forall t (tp :: BaseType). Expr t tp -> Integer
iteSize Expr t bt
y in
      ExprBuilder t st fs -> App (Expr t) bt -> IO (Expr t bt)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym (BaseTypeRepr bt
-> Integer
-> Expr t BaseBoolType
-> Expr t bt
-> Expr t bt
-> App (Expr t) bt
forall (tp :: BaseType) (e :: BaseType -> Type).
BaseTypeRepr tp
-> Integer -> e BaseBoolType -> e tp -> e tp -> App e tp
BaseIte (Expr t bt -> BaseTypeRepr bt
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType Expr t bt
x) Integer
sz Expr t BaseBoolType
c Expr t bt
x Expr t bt
y)

semiRingLe ::
  ExprBuilder t st fs ->
  SR.OrderedSemiRingRepr sr ->
  (Expr t (SR.SemiRingBase sr) -> Expr t (SR.SemiRingBase sr) -> IO (Expr t BaseBoolType))
      {- ^ recursive call for simplifications -} ->
  Expr t (SR.SemiRingBase sr) ->
  Expr t (SR.SemiRingBase sr) ->
  IO (Expr t BaseBoolType)
semiRingLe :: ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> (Expr t (SemiRingBase sr)
    -> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType))
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t BaseBoolType)
semiRingLe ExprBuilder t st fs
sym OrderedSemiRingRepr sr
osr Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType)
rec Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y
      -- Check for syntactic equality.
    | Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr) -> Expr t (SemiRingBase sr) -> Bool
forall a. Eq a => a -> a -> Bool
== Expr t (SemiRingBase sr)
y = Expr t BaseBoolType -> IO (Expr t BaseBoolType)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExprBuilder t st fs -> Pred (ExprBuilder t st fs)
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred ExprBuilder t st fs
sym)

      -- Strength reductions on a non-linear constraint to piecewise linear.
    | Just Coefficient sr
c <- SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
asSemiRingLit SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x
    , SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
forall (sr :: SemiRing).
SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
SR.eq SemiRingRepr sr
sr Coefficient sr
c (SemiRingRepr sr -> Coefficient sr
forall (sr :: SemiRing). SemiRingRepr sr -> Coefficient sr
SR.zero SemiRingRepr sr
sr)
    , Just (SemiRingProd SemiRingProduct (Expr t) sr
pd) <- Expr t (SemiRingBase sr) -> Maybe (App (Expr t) (SemiRingBase sr))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (SemiRingBase sr)
y
    , Just sr :~: sr
Refl <- SemiRingRepr sr -> SemiRingRepr sr -> Maybe (sr :~: sr)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SemiRingRepr sr
sr (SemiRingProduct (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WSum.prodRepr SemiRingProduct (Expr t) sr
pd)
    = ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> SemiRingProduct (Expr t) sr
-> IO (Expr t BaseBoolType)
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> SemiRingProduct (Expr t) sr
-> IO (Expr t BaseBoolType)
prodNonneg ExprBuilder t st fs
sym OrderedSemiRingRepr sr
osr SemiRingProduct (Expr t) sr
SemiRingProduct (Expr t) sr
pd

      -- Another strength reduction
    | Just Coefficient sr
c <- SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
asSemiRingLit SemiRingRepr sr
sr Expr t (SemiRingBase sr)
y
    , SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
forall (sr :: SemiRing).
SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
SR.eq SemiRingRepr sr
sr Coefficient sr
c (SemiRingRepr sr -> Coefficient sr
forall (sr :: SemiRing). SemiRingRepr sr -> Coefficient sr
SR.zero SemiRingRepr sr
sr)
    , Just (SemiRingProd SemiRingProduct (Expr t) sr
pd) <- Expr t (SemiRingBase sr) -> Maybe (App (Expr t) (SemiRingBase sr))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (SemiRingBase sr)
x
    , Just sr :~: sr
Refl <- SemiRingRepr sr -> SemiRingRepr sr -> Maybe (sr :~: sr)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SemiRingRepr sr
sr (SemiRingProduct (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WSum.prodRepr SemiRingProduct (Expr t) sr
pd)
    = ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> SemiRingProduct (Expr t) sr
-> IO (Expr t BaseBoolType)
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> SemiRingProduct (Expr t) sr
-> IO (Expr t BaseBoolType)
prodNonpos ExprBuilder t st fs
sym OrderedSemiRingRepr sr
osr SemiRingProduct (Expr t) sr
SemiRingProduct (Expr t) sr
pd

      -- Push some comparisons under if/then/else
    | SemiRingLiteral SemiRingRepr sr
_ Coefficient sr
_ ProgramLoc
_ <- Expr t (SemiRingBase sr)
x
    , Just (BaseIte BaseTypeRepr (SemiRingBase sr)
_ Integer
_ Expr t BaseBoolType
c Expr t (SemiRingBase sr)
a Expr t (SemiRingBase sr)
b) <- Expr t (SemiRingBase sr) -> Maybe (App (Expr t) (SemiRingBase sr))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (SemiRingBase sr)
Expr t (SemiRingBase sr)
y
    = IO (IO (Expr t BaseBoolType)) -> IO (Expr t BaseBoolType)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sym Pred (ExprBuilder t st fs)
Expr t BaseBoolType
c (Expr t BaseBoolType
 -> Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType)
-> IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType)
rec Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
Expr t (SemiRingBase sr)
a IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType) -> IO (IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType)
rec Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
Expr t (SemiRingBase sr)
b)

      -- Push some comparisons under if/then/else
    | Just (BaseIte BaseTypeRepr (SemiRingBase sr)
tp Integer
_ Expr t BaseBoolType
c Expr t (SemiRingBase sr)
a Expr t (SemiRingBase sr)
b) <- Expr t (SemiRingBase sr) -> Maybe (App (Expr t) (SemiRingBase sr))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (SemiRingBase sr)
x
    , SemiRingLiteral SemiRingRepr sr
_ Coefficient sr
_ ProgramLoc
_ <- Expr t (SemiRingBase sr)
y
    , Just SemiRingBase sr :~: SemiRingBase sr
Refl <- BaseTypeRepr (SemiRingBase sr)
-> BaseTypeRepr (SemiRingBase sr)
-> Maybe (SemiRingBase sr :~: SemiRingBase sr)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BaseTypeRepr (SemiRingBase sr)
tp (SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
forall (sr :: SemiRing).
SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
SR.semiRingBase SemiRingRepr sr
sr)
    = IO (IO (Expr t BaseBoolType)) -> IO (Expr t BaseBoolType)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sym Pred (ExprBuilder t st fs)
Expr t BaseBoolType
c (Expr t BaseBoolType
 -> Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType)
-> IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType)
rec Expr t (SemiRingBase sr)
a Expr t (SemiRingBase sr)
y IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType) -> IO (IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType)
rec Expr t (SemiRingBase sr)
b Expr t (SemiRingBase sr)
y)

      -- Try to extract common sum information.
    | (WeightedSum (Expr t) sr
z, WeightedSum (Expr t) sr
x',WeightedSum (Expr t) sr
y') <- WeightedSum (Expr t) sr
-> WeightedSum (Expr t) sr
-> (WeightedSum (Expr t) sr, WeightedSum (Expr t) sr,
    WeightedSum (Expr t) sr)
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
WeightedSum f sr
-> WeightedSum f sr
-> (WeightedSum f sr, WeightedSum f sr, WeightedSum f sr)
WSum.extractCommon (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
forall t (sr :: SemiRing).
HashableF (Expr t) =>
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x) (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
forall t (sr :: SemiRing).
HashableF (Expr t) =>
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum SemiRingRepr sr
sr Expr t (SemiRingBase sr)
y)
    , Bool -> Bool
not (SemiRingRepr sr -> WeightedSum (Expr t) sr -> Bool
forall (sr :: SemiRing) (f :: BaseType -> Type).
SemiRingRepr sr -> WeightedSum f sr -> Bool
WSum.isZero SemiRingRepr sr
sr WeightedSum (Expr t) sr
z) = do
      Expr t (SemiRingBase sr)
xr <- ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym WeightedSum (Expr t) sr
x'
      Expr t (SemiRingBase sr)
yr <- ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym WeightedSum (Expr t) sr
y'
      Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType)
rec Expr t (SemiRingBase sr)
xr Expr t (SemiRingBase sr)
yr

      -- Default case
    | Bool
otherwise = ExprBuilder t st fs
-> App (Expr t) BaseBoolType -> IO (Expr t BaseBoolType)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym (App (Expr t) BaseBoolType -> IO (Expr t BaseBoolType))
-> App (Expr t) BaseBoolType -> IO (Expr t BaseBoolType)
forall a b. (a -> b) -> a -> b
$ OrderedSemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> App (Expr t) BaseBoolType
forall (sr :: SemiRing) (e :: BaseType -> Type).
OrderedSemiRingRepr sr
-> e (SemiRingBase sr) -> e (SemiRingBase sr) -> App e BaseBoolType
SemiRingLe OrderedSemiRingRepr sr
osr Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y

 where sr :: SemiRingRepr sr
sr = OrderedSemiRingRepr sr -> SemiRingRepr sr
forall (sr :: SemiRing). OrderedSemiRingRepr sr -> SemiRingRepr sr
SR.orderedSemiRing OrderedSemiRingRepr sr
osr


semiRingEq ::
  ExprBuilder t st fs ->
  SR.SemiRingRepr sr ->
  (Expr t (SR.SemiRingBase sr) -> Expr t (SR.SemiRingBase sr) -> IO (Expr t BaseBoolType))
    {- ^ recursive call for simplifications -} ->
  Expr t (SR.SemiRingBase sr) ->
  Expr t (SR.SemiRingBase sr) ->
  IO (Expr t BaseBoolType)
semiRingEq :: ExprBuilder t st fs
-> SemiRingRepr sr
-> (Expr t (SemiRingBase sr)
    -> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType))
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t BaseBoolType)
semiRingEq ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType)
rec Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y
  -- Check for syntactic equality.
  | Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr) -> Expr t (SemiRingBase sr) -> Bool
forall a. Eq a => a -> a -> Bool
== Expr t (SemiRingBase sr)
y = Expr t BaseBoolType -> IO (Expr t BaseBoolType)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExprBuilder t st fs -> Pred (ExprBuilder t st fs)
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred ExprBuilder t st fs
sym)

    -- Push some equalities under if/then/else
  | SemiRingLiteral SemiRingRepr sr
_ Coefficient sr
_ ProgramLoc
_ <- Expr t (SemiRingBase sr)
x
  , Just (BaseIte BaseTypeRepr (SemiRingBase sr)
_ Integer
_ Expr t BaseBoolType
c Expr t (SemiRingBase sr)
a Expr t (SemiRingBase sr)
b) <- Expr t (SemiRingBase sr) -> Maybe (App (Expr t) (SemiRingBase sr))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (SemiRingBase sr)
Expr t (SemiRingBase sr)
y
  = IO (IO (Expr t BaseBoolType)) -> IO (Expr t BaseBoolType)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sym Pred (ExprBuilder t st fs)
Expr t BaseBoolType
c (Expr t BaseBoolType
 -> Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType)
-> IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType)
rec Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
Expr t (SemiRingBase sr)
a IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType) -> IO (IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType)
rec Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
Expr t (SemiRingBase sr)
b)

    -- Push some equalities under if/then/else
  | Just (BaseIte BaseTypeRepr (SemiRingBase sr)
_ Integer
_ Expr t BaseBoolType
c Expr t (SemiRingBase sr)
a Expr t (SemiRingBase sr)
b) <- Expr t (SemiRingBase sr) -> Maybe (App (Expr t) (SemiRingBase sr))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (SemiRingBase sr)
x
  , SemiRingLiteral SemiRingRepr sr
_ Coefficient sr
_ ProgramLoc
_ <- Expr t (SemiRingBase sr)
y
  = IO (IO (Expr t BaseBoolType)) -> IO (Expr t BaseBoolType)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sym Pred (ExprBuilder t st fs)
Expr t BaseBoolType
c (Expr t BaseBoolType
 -> Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType)
-> IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType)
rec Expr t (SemiRingBase sr)
a Expr t (SemiRingBase sr)
y IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType) -> IO (IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> IO (Expr t BaseBoolType)
rec Expr t (SemiRingBase sr)
b Expr t (SemiRingBase sr)
y)

  | (WeightedSum (Expr t) sr
z, WeightedSum (Expr t) sr
x',WeightedSum (Expr t) sr
y') <- WeightedSum (Expr t) sr
-> WeightedSum (Expr t) sr
-> (WeightedSum (Expr t) sr, WeightedSum (Expr t) sr,
    WeightedSum (Expr t) sr)
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
WeightedSum f sr
-> WeightedSum f sr
-> (WeightedSum f sr, WeightedSum f sr, WeightedSum f sr)
WSum.extractCommon (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
forall t (sr :: SemiRing).
HashableF (Expr t) =>
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x) (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
forall t (sr :: SemiRing).
HashableF (Expr t) =>
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum SemiRingRepr sr
sr Expr t (SemiRingBase sr)
y)
  , Bool -> Bool
not (SemiRingRepr sr -> WeightedSum (Expr t) sr -> Bool
forall (sr :: SemiRing) (f :: BaseType -> Type).
SemiRingRepr sr -> WeightedSum f sr -> Bool
WSum.isZero SemiRingRepr sr
sr WeightedSum (Expr t) sr
z) =
    case (WeightedSum (Expr t) sr -> Maybe (Coefficient sr)
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> Maybe (Coefficient sr)
WSum.asConstant WeightedSum (Expr t) sr
x', WeightedSum (Expr t) sr -> Maybe (Coefficient sr)
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> Maybe (Coefficient sr)
WSum.asConstant WeightedSum (Expr t) sr
y') of
      (Just Coefficient sr
a, Just Coefficient sr
b) -> Expr t BaseBoolType -> IO (Expr t BaseBoolType)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> Expr t BaseBoolType -> IO (Expr t BaseBoolType)
forall a b. (a -> b) -> a -> b
$! ExprBuilder t st fs -> Bool -> Pred (ExprBuilder t st fs)
forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
backendPred ExprBuilder t st fs
sym (SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
forall (sr :: SemiRing).
SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
SR.eq SemiRingRepr sr
sr Coefficient sr
a Coefficient sr
b)
      (Maybe (Coefficient sr), Maybe (Coefficient sr))
_ -> do Expr t (SemiRingBase sr)
xr <- ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym WeightedSum (Expr t) sr
x'
              Expr t (SemiRingBase sr)
yr <- ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym WeightedSum (Expr t) sr
y'
              ExprBuilder t st fs
-> App (Expr t) BaseBoolType -> IO (Expr t BaseBoolType)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym (App (Expr t) BaseBoolType -> IO (Expr t BaseBoolType))
-> App (Expr t) BaseBoolType -> IO (Expr t BaseBoolType)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> App (Expr t) BaseBoolType
forall (tp :: BaseType) (e :: BaseType -> Type).
BaseTypeRepr tp -> e tp -> e tp -> App e BaseBoolType
BaseEq (SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
forall (sr :: SemiRing).
SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
SR.semiRingBase SemiRingRepr sr
sr) (Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> Expr t (SemiRingBase sr)
forall a. Ord a => a -> a -> a
min Expr t (SemiRingBase sr)
xr Expr t (SemiRingBase sr)
yr) (Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> Expr t (SemiRingBase sr)
forall a. Ord a => a -> a -> a
max Expr t (SemiRingBase sr)
xr Expr t (SemiRingBase sr)
yr)

  | Bool
otherwise =
    ExprBuilder t st fs
-> App (Expr t) BaseBoolType -> IO (Expr t BaseBoolType)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sym (App (Expr t) BaseBoolType -> IO (Expr t BaseBoolType))
-> App (Expr t) BaseBoolType -> IO (Expr t BaseBoolType)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> App (Expr t) BaseBoolType
forall (tp :: BaseType) (e :: BaseType -> Type).
BaseTypeRepr tp -> e tp -> e tp -> App e BaseBoolType
BaseEq (SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
forall (sr :: SemiRing).
SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
SR.semiRingBase SemiRingRepr sr
sr) (Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> Expr t (SemiRingBase sr)
forall a. Ord a => a -> a -> a
min Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y) (Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr) -> Expr t (SemiRingBase sr)
forall a. Ord a => a -> a -> a
max Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y)

semiRingAdd ::
  forall t st fs sr.
  ExprBuilder t st fs ->
  SR.SemiRingRepr sr ->
  Expr t (SR.SemiRingBase sr) ->
  Expr t (SR.SemiRingBase sr) ->
  IO (Expr t (SR.SemiRingBase sr))
semiRingAdd :: ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingAdd ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y =
    case (SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
forall (sr :: SemiRing) t.
SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
viewSemiRing SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x, SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
forall (sr :: SemiRing) t.
SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
viewSemiRing SemiRingRepr sr
sr Expr t (SemiRingBase sr)
y) of
      (SR_Constant Coefficient sr
c, SemiRingView t sr
_) | SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
forall (sr :: SemiRing).
SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
SR.eq SemiRingRepr sr
sr Coefficient sr
c (SemiRingRepr sr -> Coefficient sr
forall (sr :: SemiRing). SemiRingRepr sr -> Coefficient sr
SR.zero SemiRingRepr sr
sr) -> Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t (SemiRingBase sr)
y
      (SemiRingView t sr
_, SR_Constant Coefficient sr
c) | SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
forall (sr :: SemiRing).
SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
SR.eq SemiRingRepr sr
sr Coefficient sr
c (SemiRingRepr sr -> Coefficient sr
forall (sr :: SemiRing). SemiRingRepr sr -> Coefficient sr
SR.zero SemiRingRepr sr
sr) -> Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t (SemiRingBase sr)
x

      (SR_Constant Coefficient sr
xc, SR_Constant Coefficient sr
yc) ->
        ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
semiRingLit ExprBuilder t st fs
sym SemiRingRepr sr
sr (SemiRingRepr sr
-> Coefficient sr -> Coefficient sr -> Coefficient sr
forall (sr :: SemiRing).
SemiRingRepr sr
-> Coefficient sr -> Coefficient sr -> Coefficient sr
SR.add SemiRingRepr sr
sr Coefficient sr
xc Coefficient sr
yc)

      (SR_Constant Coefficient sr
xc, SR_Sum WeightedSum (Expr t) sr
ys) ->
        ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
sum' ExprBuilder t st fs
sym (SemiRingRepr sr
-> WeightedSum (Expr t) sr
-> Coefficient sr
-> WeightedSum (Expr t) sr
forall (sr :: SemiRing) (f :: BaseType -> Type).
SemiRingRepr sr
-> WeightedSum f sr -> Coefficient sr -> WeightedSum f sr
WSum.addConstant SemiRingRepr sr
sr WeightedSum (Expr t) sr
ys Coefficient sr
xc)
      (SR_Sum WeightedSum (Expr t) sr
xs, SR_Constant Coefficient sr
yc) ->
        ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
sum' ExprBuilder t st fs
sym (SemiRingRepr sr
-> WeightedSum (Expr t) sr
-> Coefficient sr
-> WeightedSum (Expr t) sr
forall (sr :: SemiRing) (f :: BaseType -> Type).
SemiRingRepr sr
-> WeightedSum f sr -> Coefficient sr -> WeightedSum f sr
WSum.addConstant SemiRingRepr sr
sr WeightedSum (Expr t) sr
xs Coefficient sr
yc)

      (SR_Constant Coefficient sr
xc, SemiRingView t sr
_)
        | Just (BaseIte BaseTypeRepr (SemiRingBase sr)
_ Integer
_ Expr t BaseBoolType
cond Expr t (SemiRingBase sr)
a Expr t (SemiRingBase sr)
b) <- Expr t (SemiRingBase sr) -> Maybe (App (Expr t) (SemiRingBase sr))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (SemiRingBase sr)
y
        , Expr t (SemiRingBase sr) -> Bool
isConstantSemiRingExpr Expr t (SemiRingBase sr)
a Bool -> Bool -> Bool
|| Expr t (SemiRingBase sr) -> Bool
isConstantSemiRingExpr Expr t (SemiRingBase sr)
b -> do
            Expr t (SemiRingBase sr)
xa <- ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingAdd ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
a
            Expr t (SemiRingBase sr)
xb <- ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingAdd ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
b
            ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t BaseBoolType
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t BaseBoolType
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingIte ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t BaseBoolType
cond Expr t (SemiRingBase sr)
xa Expr t (SemiRingBase sr)
xb
        | Bool
otherwise ->
            ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
sum' ExprBuilder t st fs
sym (SemiRingRepr sr
-> WeightedSum (Expr t) sr
-> Coefficient sr
-> WeightedSum (Expr t) sr
forall (sr :: SemiRing) (f :: BaseType -> Type).
SemiRingRepr sr
-> WeightedSum f sr -> Coefficient sr -> WeightedSum f sr
WSum.addConstant SemiRingRepr sr
sr (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr -> f (SemiRingBase sr) -> WeightedSum f sr
WSum.var SemiRingRepr sr
sr Expr t (SemiRingBase sr)
y) Coefficient sr
xc)

      (SemiRingView t sr
_, SR_Constant Coefficient sr
yc)
        | Just (BaseIte BaseTypeRepr (SemiRingBase sr)
_ Integer
_ Expr t BaseBoolType
cond Expr t (SemiRingBase sr)
a Expr t (SemiRingBase sr)
b) <- Expr t (SemiRingBase sr) -> Maybe (App (Expr t) (SemiRingBase sr))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (SemiRingBase sr)
x
        , Expr t (SemiRingBase sr) -> Bool
isConstantSemiRingExpr Expr t (SemiRingBase sr)
a Bool -> Bool -> Bool
|| Expr t (SemiRingBase sr) -> Bool
isConstantSemiRingExpr Expr t (SemiRingBase sr)
b -> do
            Expr t (SemiRingBase sr)
ay <- ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingAdd ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t (SemiRingBase sr)
a Expr t (SemiRingBase sr)
y
            Expr t (SemiRingBase sr)
by <- ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingAdd ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t (SemiRingBase sr)
b Expr t (SemiRingBase sr)
y
            ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t BaseBoolType
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t BaseBoolType
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingIte ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t BaseBoolType
cond Expr t (SemiRingBase sr)
ay Expr t (SemiRingBase sr)
by
        | Bool
otherwise ->
            ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
sum' ExprBuilder t st fs
sym (SemiRingRepr sr
-> WeightedSum (Expr t) sr
-> Coefficient sr
-> WeightedSum (Expr t) sr
forall (sr :: SemiRing) (f :: BaseType -> Type).
SemiRingRepr sr
-> WeightedSum f sr -> Coefficient sr -> WeightedSum f sr
WSum.addConstant SemiRingRepr sr
sr (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr -> f (SemiRingBase sr) -> WeightedSum f sr
WSum.var SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x) Coefficient sr
yc)

      (SR_Sum WeightedSum (Expr t) sr
xs, SR_Sum WeightedSum (Expr t) sr
ys) -> ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym (SemiRingRepr sr
-> WeightedSum (Expr t) sr
-> WeightedSum (Expr t) sr
-> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr
-> WeightedSum f sr -> WeightedSum f sr -> WeightedSum f sr
WSum.add SemiRingRepr sr
sr WeightedSum (Expr t) sr
xs WeightedSum (Expr t) sr
ys)
      (SR_Sum WeightedSum (Expr t) sr
xs, SemiRingView t sr
_)         -> ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym (SemiRingRepr sr
-> WeightedSum (Expr t) sr
-> Expr t (SemiRingBase sr)
-> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr
-> WeightedSum f sr -> f (SemiRingBase sr) -> WeightedSum f sr
WSum.addVar SemiRingRepr sr
sr WeightedSum (Expr t) sr
xs Expr t (SemiRingBase sr)
y)
      (SemiRingView t sr
_ , SR_Sum WeightedSum (Expr t) sr
ys)        -> ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym (SemiRingRepr sr
-> WeightedSum (Expr t) sr
-> Expr t (SemiRingBase sr)
-> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr
-> WeightedSum f sr -> f (SemiRingBase sr) -> WeightedSum f sr
WSum.addVar SemiRingRepr sr
sr WeightedSum (Expr t) sr
ys Expr t (SemiRingBase sr)
x)
      (SemiRingView t sr, SemiRingView t sr)
_                      -> ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> WeightedSum (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingSum ExprBuilder t st fs
sym (SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr
-> f (SemiRingBase sr) -> f (SemiRingBase sr) -> WeightedSum f sr
WSum.addVars SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y)
  where isConstantSemiRingExpr :: Expr t (SR.SemiRingBase sr) -> Bool
        isConstantSemiRingExpr :: Expr t (SemiRingBase sr) -> Bool
isConstantSemiRingExpr (SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
forall (sr :: SemiRing) t.
SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
viewSemiRing SemiRingRepr sr
sr -> SR_Constant Coefficient sr
_) = Bool
True
        isConstantSemiRingExpr Expr t (SemiRingBase sr)
_ = Bool
False

semiRingMul ::
  ExprBuilder t st fs ->
  SR.SemiRingRepr sr ->
  Expr t (SR.SemiRingBase sr) ->
  Expr t (SR.SemiRingBase sr) ->
  IO (Expr t (SR.SemiRingBase sr))
semiRingMul :: ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingMul ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y =
  case (SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
forall (sr :: SemiRing) t.
SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
viewSemiRing SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x, SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
forall (sr :: SemiRing) t.
SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
viewSemiRing SemiRingRepr sr
sr Expr t (SemiRingBase sr)
y) of
    (SR_Constant Coefficient sr
c, SemiRingView t sr
_) -> ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
scalarMul ExprBuilder t st fs
sym SemiRingRepr sr
sr Coefficient sr
c Expr t (SemiRingBase sr)
y
    (SemiRingView t sr
_, SR_Constant Coefficient sr
c) -> ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
scalarMul ExprBuilder t st fs
sym SemiRingRepr sr
sr Coefficient sr
c Expr t (SemiRingBase sr)
x

    (SR_Sum (WeightedSum (Expr t) sr
-> Maybe (Coefficient sr, Expr t (SemiRingBase sr), Coefficient sr)
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr
-> Maybe (Coefficient sr, f (SemiRingBase sr), Coefficient sr)
WSum.asAffineVar -> Just (Coefficient sr
c,Expr t (SemiRingBase sr)
x',Coefficient sr
o)), SemiRingView t sr
_) ->
      do Expr t (SemiRingBase sr)
cxy <- ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
scalarMul ExprBuilder t st fs
sym SemiRingRepr sr
sr Coefficient sr
c (Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr)))
-> IO (Expr t (SemiRingBase sr)) -> IO (Expr t (SemiRingBase sr))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingMul ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x' Expr t (SemiRingBase sr)
y
         Expr t (SemiRingBase sr)
oy  <- ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
scalarMul ExprBuilder t st fs
sym SemiRingRepr sr
sr Coefficient sr
o Expr t (SemiRingBase sr)
y
         ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingAdd ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t (SemiRingBase sr)
cxy Expr t (SemiRingBase sr)
oy

    (SemiRingView t sr
_, SR_Sum (WeightedSum (Expr t) sr
-> Maybe (Coefficient sr, Expr t (SemiRingBase sr), Coefficient sr)
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr
-> Maybe (Coefficient sr, f (SemiRingBase sr), Coefficient sr)
WSum.asAffineVar -> Just (Coefficient sr
c,Expr t (SemiRingBase sr)
y',Coefficient sr
o))) ->
      do Expr t (SemiRingBase sr)
cxy <- ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
scalarMul ExprBuilder t st fs
sym SemiRingRepr sr
sr Coefficient sr
c (Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr)))
-> IO (Expr t (SemiRingBase sr)) -> IO (Expr t (SemiRingBase sr))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingMul ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
y'
         Expr t (SemiRingBase sr)
ox  <- ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
scalarMul ExprBuilder t st fs
sym SemiRingRepr sr
sr Coefficient sr
o Expr t (SemiRingBase sr)
x
         ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
semiRingAdd ExprBuilder t st fs
sym SemiRingRepr sr
sr Expr t (SemiRingBase sr)
cxy Expr t (SemiRingBase sr)
ox

    (SR_Prod SemiRingProduct (Expr t) sr
px, SR_Prod SemiRingProduct (Expr t) sr
py) -> ExprBuilder t st fs
-> SemiRingProduct (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingProduct (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingProd ExprBuilder t st fs
sym (SemiRingProduct (Expr t) sr
-> SemiRingProduct (Expr t) sr -> SemiRingProduct (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingProduct f sr
-> SemiRingProduct f sr -> SemiRingProduct f sr
WSum.prodMul SemiRingProduct (Expr t) sr
px SemiRingProduct (Expr t) sr
py)
    (SR_Prod SemiRingProduct (Expr t) sr
px, SemiRingView t sr
_)          -> ExprBuilder t st fs
-> SemiRingProduct (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingProduct (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingProd ExprBuilder t st fs
sym (SemiRingProduct (Expr t) sr
-> SemiRingProduct (Expr t) sr -> SemiRingProduct (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingProduct f sr
-> SemiRingProduct f sr -> SemiRingProduct f sr
WSum.prodMul SemiRingProduct (Expr t) sr
px (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> SemiRingProduct (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr -> f (SemiRingBase sr) -> SemiRingProduct f sr
WSum.prodVar SemiRingRepr sr
sr Expr t (SemiRingBase sr)
y))
    (SemiRingView t sr
_, SR_Prod SemiRingProduct (Expr t) sr
py)          -> ExprBuilder t st fs
-> SemiRingProduct (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingProduct (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingProd ExprBuilder t st fs
sym (SemiRingProduct (Expr t) sr
-> SemiRingProduct (Expr t) sr -> SemiRingProduct (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingProduct f sr
-> SemiRingProduct f sr -> SemiRingProduct f sr
WSum.prodMul (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> SemiRingProduct (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr -> f (SemiRingBase sr) -> SemiRingProduct f sr
WSum.prodVar SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x) SemiRingProduct (Expr t) sr
py)
    (SemiRingView t sr, SemiRingView t sr)
_                        -> ExprBuilder t st fs
-> SemiRingProduct (Expr t) sr -> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingProduct (Expr t) sr -> IO (Expr t (SemiRingBase sr))
semiRingProd ExprBuilder t st fs
sym (SemiRingProduct (Expr t) sr
-> SemiRingProduct (Expr t) sr -> SemiRingProduct (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingProduct f sr
-> SemiRingProduct f sr -> SemiRingProduct f sr
WSum.prodMul (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> SemiRingProduct (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr -> f (SemiRingBase sr) -> SemiRingProduct f sr
WSum.prodVar SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x) (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> SemiRingProduct (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr -> f (SemiRingBase sr) -> SemiRingProduct f sr
WSum.prodVar SemiRingRepr sr
sr Expr t (SemiRingBase sr)
y))


prodNonneg ::
  ExprBuilder t st fs ->
  SR.OrderedSemiRingRepr sr ->
  WSum.SemiRingProduct (Expr t) sr ->
  IO (Expr t BaseBoolType)
prodNonneg :: ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> SemiRingProduct (Expr t) sr
-> IO (Expr t BaseBoolType)
prodNonneg ExprBuilder t st fs
sym OrderedSemiRingRepr sr
osr SemiRingProduct (Expr t) sr
pd =
  do let sr :: SemiRingRepr sr
sr = OrderedSemiRingRepr sr -> SemiRingRepr sr
forall (sr :: SemiRing). OrderedSemiRingRepr sr -> SemiRingRepr sr
SR.orderedSemiRing OrderedSemiRingRepr sr
osr
     Expr t (SemiRingBase sr)
zero <- ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
semiRingLit ExprBuilder t st fs
sym SemiRingRepr sr
sr (SemiRingRepr sr -> Coefficient sr
forall (sr :: SemiRing). SemiRingRepr sr -> Coefficient sr
SR.zero SemiRingRepr sr
sr)
     (Expr t BaseBoolType, Expr t BaseBoolType) -> Expr t BaseBoolType
forall a b. (a, b) -> a
fst ((Expr t BaseBoolType, Expr t BaseBoolType) -> Expr t BaseBoolType)
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
-> IO (Expr t BaseBoolType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> SemiRingProduct (Expr t) sr
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> SemiRingProduct (Expr t) sr
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
computeNonnegNonpos ExprBuilder t st fs
sym OrderedSemiRingRepr sr
osr Expr t (SemiRingBase sr)
zero SemiRingProduct (Expr t) sr
pd

prodNonpos ::
  ExprBuilder t st fs ->
  SR.OrderedSemiRingRepr sr ->
  WSum.SemiRingProduct (Expr t) sr ->
  IO (Expr t BaseBoolType)
prodNonpos :: ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> SemiRingProduct (Expr t) sr
-> IO (Expr t BaseBoolType)
prodNonpos ExprBuilder t st fs
sym OrderedSemiRingRepr sr
osr SemiRingProduct (Expr t) sr
pd =
  do let sr :: SemiRingRepr sr
sr = OrderedSemiRingRepr sr -> SemiRingRepr sr
forall (sr :: SemiRing). OrderedSemiRingRepr sr -> SemiRingRepr sr
SR.orderedSemiRing OrderedSemiRingRepr sr
osr
     Expr t (SemiRingBase sr)
zero <- ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> IO (Expr t (SemiRingBase sr))
semiRingLit ExprBuilder t st fs
sym SemiRingRepr sr
sr (SemiRingRepr sr -> Coefficient sr
forall (sr :: SemiRing). SemiRingRepr sr -> Coefficient sr
SR.zero SemiRingRepr sr
sr)
     (Expr t BaseBoolType, Expr t BaseBoolType) -> Expr t BaseBoolType
forall a b. (a, b) -> b
snd ((Expr t BaseBoolType, Expr t BaseBoolType) -> Expr t BaseBoolType)
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
-> IO (Expr t BaseBoolType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> SemiRingProduct (Expr t) sr
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> SemiRingProduct (Expr t) sr
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
computeNonnegNonpos ExprBuilder t st fs
sym OrderedSemiRingRepr sr
osr Expr t (SemiRingBase sr)
zero SemiRingProduct (Expr t) sr
pd

computeNonnegNonpos ::
  ExprBuilder t st fs ->
  SR.OrderedSemiRingRepr sr ->
  Expr t (SR.SemiRingBase sr) {- zero element -} ->
  WSum.SemiRingProduct (Expr t) sr ->
  IO (Expr t BaseBoolType, Expr t BaseBoolType)
computeNonnegNonpos :: ExprBuilder t st fs
-> OrderedSemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> SemiRingProduct (Expr t) sr
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
computeNonnegNonpos ExprBuilder t st fs
sym OrderedSemiRingRepr sr
osr Expr t (SemiRingBase sr)
zero SemiRingProduct (Expr t) sr
pd =
   (Expr t BaseBoolType, Expr t BaseBoolType)
-> Maybe (Expr t BaseBoolType, Expr t BaseBoolType)
-> (Expr t BaseBoolType, Expr t BaseBoolType)
forall a. a -> Maybe a -> a
fromMaybe (ExprBuilder t st fs -> Pred (ExprBuilder t st fs)
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred ExprBuilder t st fs
sym, ExprBuilder t st fs -> Pred (ExprBuilder t st fs)
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred ExprBuilder t st fs
sym) (Maybe (Expr t BaseBoolType, Expr t BaseBoolType)
 -> (Expr t BaseBoolType, Expr t BaseBoolType))
-> IO (Maybe (Expr t BaseBoolType, Expr t BaseBoolType))
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Expr t BaseBoolType, Expr t BaseBoolType)
 -> (Expr t BaseBoolType, Expr t BaseBoolType)
 -> IO (Expr t BaseBoolType, Expr t BaseBoolType))
-> (Expr t (SemiRingBase sr)
    -> IO (Expr t BaseBoolType, Expr t BaseBoolType))
-> SemiRingProduct (Expr t) sr
-> IO (Maybe (Expr t BaseBoolType, Expr t BaseBoolType))
forall (m :: Type -> Type) r (f :: BaseType -> Type)
       (sr :: SemiRing).
Monad m =>
(r -> r -> m r)
-> (f (SemiRingBase sr) -> m r)
-> SemiRingProduct f sr
-> m (Maybe r)
WSum.prodEvalM (Expr t BaseBoolType, Expr t BaseBoolType)
-> (Expr t BaseBoolType, Expr t BaseBoolType)
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
merge Expr t (SemiRingBase sr)
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
single SemiRingProduct (Expr t) sr
pd
 where

 single :: Expr t (SemiRingBase sr)
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
single Expr t (SemiRingBase sr)
x = (,) (Expr t BaseBoolType
 -> Expr t BaseBoolType
 -> (Expr t BaseBoolType, Expr t BaseBoolType))
-> IO (Expr t BaseBoolType)
-> IO
     (Expr t BaseBoolType -> (Expr t BaseBoolType, Expr t BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> (forall (w :: Nat).
    (1 <= w) =>
    ExprBuilder t st fs
    -> UnaryBV (Pred (ExprBuilder t st fs)) w
    -> IO (SymExpr (ExprBuilder t st fs) (BaseBVType w)))
-> App (SymExpr (ExprBuilder t st fs)) BaseBoolType
-> IO (Pred (ExprBuilder t st fs))
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> UnaryBV (Pred sym) w -> IO (SymExpr sym (BaseBVType w)))
-> App (SymExpr sym) tp
-> IO (SymExpr sym tp)
reduceApp ExprBuilder t st fs
sym forall (w :: Nat).
(1 <= w) =>
ExprBuilder t st fs
-> UnaryBV (Pred (ExprBuilder t st fs)) w
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType w))
forall (w :: Nat) t (st :: Type -> Type) fs.
(1 <= w) =>
ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w)
bvUnary (OrderedSemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> App (Expr t) BaseBoolType
forall (sr :: SemiRing) (e :: BaseType -> Type).
OrderedSemiRingRepr sr
-> e (SemiRingBase sr) -> e (SemiRingBase sr) -> App e BaseBoolType
SemiRingLe OrderedSemiRingRepr sr
osr Expr t (SemiRingBase sr)
zero Expr t (SemiRingBase sr)
x) -- nonnegative
                IO
  (Expr t BaseBoolType -> (Expr t BaseBoolType, Expr t BaseBoolType))
-> IO (Expr t BaseBoolType)
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ExprBuilder t st fs
-> (forall (w :: Nat).
    (1 <= w) =>
    ExprBuilder t st fs
    -> UnaryBV (Pred (ExprBuilder t st fs)) w
    -> IO (SymExpr (ExprBuilder t st fs) (BaseBVType w)))
-> App (SymExpr (ExprBuilder t st fs)) BaseBoolType
-> IO (Pred (ExprBuilder t st fs))
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> UnaryBV (Pred sym) w -> IO (SymExpr sym (BaseBVType w)))
-> App (SymExpr sym) tp
-> IO (SymExpr sym tp)
reduceApp ExprBuilder t st fs
sym forall (w :: Nat).
(1 <= w) =>
ExprBuilder t st fs
-> UnaryBV (Pred (ExprBuilder t st fs)) w
-> IO (SymExpr (ExprBuilder t st fs) (BaseBVType w))
forall (w :: Nat) t (st :: Type -> Type) fs.
(1 <= w) =>
ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w)
bvUnary (OrderedSemiRingRepr sr
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> App (Expr t) BaseBoolType
forall (sr :: SemiRing) (e :: BaseType -> Type).
OrderedSemiRingRepr sr
-> e (SemiRingBase sr) -> e (SemiRingBase sr) -> App e BaseBoolType
SemiRingLe OrderedSemiRingRepr sr
osr Expr t (SemiRingBase sr)
x Expr t (SemiRingBase sr)
zero) -- nonpositive

 merge :: (Expr t BaseBoolType, Expr t BaseBoolType)
-> (Expr t BaseBoolType, Expr t BaseBoolType)
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
merge (Expr t BaseBoolType
nn1, Expr t BaseBoolType
np1) (Expr t BaseBoolType
nn2, Expr t BaseBoolType
np2) =
   do Expr t BaseBoolType
nn <- IO (IO (Expr t BaseBoolType)) -> IO (Expr t BaseBoolType)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred ExprBuilder t st fs
sym (Expr t BaseBoolType
 -> Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType)
-> IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred ExprBuilder t st fs
sym Pred (ExprBuilder t st fs)
Expr t BaseBoolType
nn1 Pred (ExprBuilder t st fs)
Expr t BaseBoolType
nn2 IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType) -> IO (IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred ExprBuilder t st fs
sym Pred (ExprBuilder t st fs)
Expr t BaseBoolType
np1 Pred (ExprBuilder t st fs)
Expr t BaseBoolType
np2)
      Expr t BaseBoolType
np <- IO (IO (Expr t BaseBoolType)) -> IO (Expr t BaseBoolType)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred ExprBuilder t st fs
sym (Expr t BaseBoolType
 -> Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType)
-> IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred ExprBuilder t st fs
sym Pred (ExprBuilder t st fs)
Expr t BaseBoolType
nn1 Pred (ExprBuilder t st fs)
Expr t BaseBoolType
np2 IO (Expr t BaseBoolType -> IO (Expr t BaseBoolType))
-> IO (Expr t BaseBoolType) -> IO (IO (Expr t BaseBoolType))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> Pred (ExprBuilder t st fs)
-> IO (Pred (ExprBuilder t st fs))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred ExprBuilder t st fs
sym Pred (ExprBuilder t st fs)
Expr t BaseBoolType
np1 Pred (ExprBuilder t st fs)
Expr t BaseBoolType
nn2)
      (Expr t BaseBoolType, Expr t BaseBoolType)
-> IO (Expr t BaseBoolType, Expr t BaseBoolType)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr t BaseBoolType
nn, Expr t BaseBoolType
np)



arrayResultIdxType :: BaseTypeRepr (BaseArrayType (idx ::> itp) d)
                   -> Ctx.Assignment BaseTypeRepr (idx ::> itp)
arrayResultIdxType :: BaseTypeRepr (BaseArrayType (idx ::> itp) d)
-> Assignment BaseTypeRepr (idx ::> itp)
arrayResultIdxType (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idx BaseTypeRepr xs
_) = Assignment BaseTypeRepr (idx ::> itp)
Assignment BaseTypeRepr (idx ::> tp)
idx

-- | This decomposes A ExprBuilder array expression into a set of indices that
-- have been updated, and an underlying index.
data ArrayMapView i f tp
   = ArrayMapView { ArrayMapView i f tp -> ArrayUpdateMap f i tp
_arrayMapViewIndices :: !(AUM.ArrayUpdateMap f i tp)
                  , ArrayMapView i f tp -> f (BaseArrayType i tp)
_arrayMapViewExpr    :: !(f (BaseArrayType i tp))
                  }

-- | Construct an 'ArrayMapView' for an element.
viewArrayMap :: Expr t (BaseArrayType i tp)
             -> ArrayMapView i (Expr t) tp
viewArrayMap :: Expr t (BaseArrayType i tp) -> ArrayMapView i (Expr t) tp
viewArrayMap  Expr t (BaseArrayType i tp)
x
  | Just (ArrayMap Assignment BaseTypeRepr (i ::> itp)
_ BaseTypeRepr tp
_ ArrayUpdateMap (Expr t) (i ::> itp) tp
m Expr t (BaseArrayType (i ::> itp) tp)
c) <- Expr t (BaseArrayType i tp)
-> Maybe (App (Expr t) (BaseArrayType i tp))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t (BaseArrayType i tp)
x = ArrayUpdateMap (Expr t) (i ::> itp) tp
-> Expr t (BaseArrayType (i ::> itp) tp)
-> ArrayMapView (i ::> itp) (Expr t) tp
forall (i :: Ctx BaseType) (f :: BaseType -> Type)
       (tp :: BaseType).
ArrayUpdateMap f i tp
-> f (BaseArrayType i tp) -> ArrayMapView i f tp
ArrayMapView ArrayUpdateMap (Expr t) (i ::> itp) tp
m Expr t (BaseArrayType (i ::> itp) tp)
c
  | Bool
otherwise = ArrayUpdateMap (Expr t) i tp
-> Expr t (BaseArrayType i tp) -> ArrayMapView i (Expr t) tp
forall (i :: Ctx BaseType) (f :: BaseType -> Type)
       (tp :: BaseType).
ArrayUpdateMap f i tp
-> f (BaseArrayType i tp) -> ArrayMapView i f tp
ArrayMapView ArrayUpdateMap (Expr t) i tp
forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
ArrayUpdateMap e ctx tp
AUM.empty Expr t (BaseArrayType i tp)
x

-- | Construct an 'ArrayMapView' for an element.
underlyingArrayMapExpr :: ArrayResultWrapper (Expr t) i tp
                      -> ArrayResultWrapper (Expr t) i tp
underlyingArrayMapExpr :: ArrayResultWrapper (Expr t) i tp
-> ArrayResultWrapper (Expr t) i tp
underlyingArrayMapExpr ArrayResultWrapper (Expr t) i tp
x
  | Just (ArrayMap Assignment BaseTypeRepr (i ::> itp)
_ BaseTypeRepr tp
_ ArrayUpdateMap (Expr t) (i ::> itp) tp
_ Expr t (BaseArrayType (i ::> itp) tp)
c) <- Expr t (BaseArrayType i tp)
-> Maybe (App (Expr t) (BaseArrayType i tp))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp (ArrayResultWrapper (Expr t) i tp -> Expr t (BaseArrayType i tp)
forall (f :: BaseType -> Type) (idx :: Ctx BaseType)
       (tp :: BaseType).
ArrayResultWrapper f idx tp -> f (BaseArrayType idx tp)
unwrapArrayResult ArrayResultWrapper (Expr t) i tp
x) = Expr t (BaseArrayType (i ::> itp) tp)
-> ArrayResultWrapper (Expr t) (i ::> itp) tp
forall (f :: BaseType -> Type) (idx :: Ctx BaseType)
       (tp :: BaseType).
f (BaseArrayType idx tp) -> ArrayResultWrapper f idx tp
ArrayResultWrapper Expr t (BaseArrayType (i ::> itp) tp)
c
  | Bool
otherwise = ArrayResultWrapper (Expr t) i tp
x

-- | Return set of addresss in assignment that are written to by at least one expr
concreteArrayEntries :: forall t i ctx
                     .  Ctx.Assignment (ArrayResultWrapper (Expr t) i) ctx
                     -> Set (Ctx.Assignment IndexLit i)
concreteArrayEntries :: Assignment (ArrayResultWrapper (Expr t) i) ctx
-> Set (Assignment IndexLit i)
concreteArrayEntries = (forall (x :: BaseType).
 Set (Assignment IndexLit i)
 -> ArrayResultWrapper (Expr t) i x -> Set (Assignment IndexLit i))
-> Set (Assignment IndexLit i)
-> Assignment (ArrayResultWrapper (Expr t) i) ctx
-> Set (Assignment IndexLit i)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). b -> f x -> b)
-> forall (x :: l). b -> t f x -> b
foldlFC' forall (x :: BaseType).
Set (Assignment IndexLit i)
-> ArrayResultWrapper (Expr t) i x -> Set (Assignment IndexLit i)
f Set (Assignment IndexLit i)
forall a. Set a
Set.empty
  where f :: Set (Ctx.Assignment IndexLit i)
          -> ArrayResultWrapper (Expr t) i tp
          -> Set (Ctx.Assignment IndexLit i)
        f :: Set (Assignment IndexLit i)
-> ArrayResultWrapper (Expr t) i tp -> Set (Assignment IndexLit i)
f Set (Assignment IndexLit i)
s ArrayResultWrapper (Expr t) i tp
e
          | Just (ArrayMap Assignment BaseTypeRepr (i ::> itp)
_ BaseTypeRepr tp
_ ArrayUpdateMap (Expr t) (i ::> itp) tp
m Expr t (BaseArrayType (i ::> itp) tp)
_) <- Expr t (BaseArrayType i tp)
-> Maybe (App (Expr t) (BaseArrayType i tp))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp (ArrayResultWrapper (Expr t) i tp -> Expr t (BaseArrayType i tp)
forall (f :: BaseType -> Type) (idx :: Ctx BaseType)
       (tp :: BaseType).
ArrayResultWrapper f idx tp -> f (BaseArrayType idx tp)
unwrapArrayResult  ArrayResultWrapper (Expr t) i tp
e) =
            Set (Assignment IndexLit i)
-> Set (Assignment IndexLit i) -> Set (Assignment IndexLit i)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Assignment IndexLit i)
s (ArrayUpdateMap (Expr t) (i ::> itp) tp
-> Set (Assignment IndexLit (i ::> itp))
forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
ArrayUpdateMap e ctx tp -> Set (Assignment IndexLit ctx)
AUM.keysSet ArrayUpdateMap (Expr t) (i ::> itp) tp
m)
          | Bool
otherwise = Set (Assignment IndexLit i)
s



data IntLit tp = (tp ~ BaseIntegerType) => IntLit Integer

asIntBounds :: Ctx.Assignment (Expr t) idx -> Maybe (Ctx.Assignment IntLit idx)
asIntBounds :: Assignment (Expr t) idx -> Maybe (Assignment IntLit idx)
asIntBounds = (forall (x :: BaseType). Expr t x -> Maybe (IntLit x))
-> forall (x :: Ctx BaseType).
   Assignment (Expr t) x -> Maybe (Assignment IntLit x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC forall t (tp :: BaseType). Expr t tp -> Maybe (IntLit tp)
forall (x :: BaseType). Expr t x -> Maybe (IntLit x)
f
  where f :: Expr t tp -> Maybe (IntLit tp)
        f :: Expr t tp -> Maybe (IntLit tp)
f (SemiRingLiteral SemiRingRepr sr
SR.SemiRingIntegerRepr Coefficient sr
n ProgramLoc
_) = IntLit tp -> Maybe (IntLit tp)
forall a. a -> Maybe a
Just (Integer -> IntLit tp
forall (tp :: BaseType).
(tp ~ BaseIntegerType) =>
Integer -> IntLit tp
IntLit Integer
Coefficient sr
n)
        f Expr t tp
_ = Maybe (IntLit tp)
forall a. Maybe a
Nothing

foldBoundLeM :: (r -> Integer -> IO r) -> r -> Integer -> IO r
foldBoundLeM :: (r -> Integer -> IO r) -> r -> Integer -> IO r
foldBoundLeM r -> Integer -> IO r
f r
r Integer
n
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 = r -> IO r
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure r
r
  | Bool
otherwise =
      do r
r' <- (r -> Integer -> IO r) -> r -> Integer -> IO r
forall r. (r -> Integer -> IO r) -> r -> Integer -> IO r
foldBoundLeM r -> Integer -> IO r
f r
r (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)
         r -> Integer -> IO r
f r
r' Integer
n

foldIndicesInRangeBounds :: forall sym idx r
                         .  IsExprBuilder sym
                         => sym
                         -> (r -> Ctx.Assignment (SymExpr sym) idx -> IO r)
                         -> r
                         -> Ctx.Assignment IntLit idx
                         -> IO r
foldIndicesInRangeBounds :: sym
-> (r -> Assignment (SymExpr sym) idx -> IO r)
-> r
-> Assignment IntLit idx
-> IO r
foldIndicesInRangeBounds sym
sym r -> Assignment (SymExpr sym) idx -> IO r
f0 r
a0 Assignment IntLit idx
bnds0 = do
  case Assignment IntLit idx
bnds0 of
    Assignment IntLit idx
Ctx.Empty -> r -> Assignment (SymExpr sym) idx -> IO r
f0 r
a0 Assignment (SymExpr sym) idx
forall k (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty
    Assignment IntLit ctx
bnds Ctx.:> IntLit Integer
b -> sym
-> (r -> Assignment (SymExpr sym) ctx -> IO r)
-> r
-> Assignment IntLit ctx
-> IO r
forall sym (idx :: Ctx BaseType) r.
IsExprBuilder sym =>
sym
-> (r -> Assignment (SymExpr sym) idx -> IO r)
-> r
-> Assignment IntLit idx
-> IO r
foldIndicesInRangeBounds sym
sym ((r -> Assignment (SymExpr sym) (ctx ::> BaseIntegerType) -> IO r)
-> r -> Assignment (SymExpr sym) ctx -> IO r
forall (idx0 :: Ctx BaseType).
(r -> Assignment (SymExpr sym) (idx0 ::> BaseIntegerType) -> IO r)
-> r -> Assignment (SymExpr sym) idx0 -> IO r
g r -> Assignment (SymExpr sym) idx -> IO r
r -> Assignment (SymExpr sym) (ctx ::> BaseIntegerType) -> IO r
f0) r
a0 Assignment IntLit ctx
bnds
      where g :: (r -> Ctx.Assignment (SymExpr sym) (idx0 ::> BaseIntegerType) -> IO r)
              -> r
              -> Ctx.Assignment (SymExpr sym) idx0
              -> IO r
            g :: (r -> Assignment (SymExpr sym) (idx0 ::> BaseIntegerType) -> IO r)
-> r -> Assignment (SymExpr sym) idx0 -> IO r
g r -> Assignment (SymExpr sym) (idx0 ::> BaseIntegerType) -> IO r
f r
a Assignment (SymExpr sym) idx0
i = (r -> Integer -> IO r) -> r -> Integer -> IO r
forall r. (r -> Integer -> IO r) -> r -> Integer -> IO r
foldBoundLeM ((r -> Assignment (SymExpr sym) (idx0 ::> BaseIntegerType) -> IO r)
-> Assignment (SymExpr sym) idx0 -> r -> Integer -> IO r
forall (idx0 :: Ctx BaseType).
(r -> Assignment (SymExpr sym) (idx0 ::> BaseIntegerType) -> IO r)
-> Assignment (SymExpr sym) idx0 -> r -> Integer -> IO r
h r -> Assignment (SymExpr sym) (idx0 ::> BaseIntegerType) -> IO r
f Assignment (SymExpr sym) idx0
i) r
a Integer
b

            h :: (r -> Ctx.Assignment (SymExpr sym) (idx0 ::> BaseIntegerType) -> IO r)
              -> Ctx.Assignment (SymExpr sym) idx0
              -> r
              -> Integer
              -> IO r
            h :: (r -> Assignment (SymExpr sym) (idx0 ::> BaseIntegerType) -> IO r)
-> Assignment (SymExpr sym) idx0 -> r -> Integer -> IO r
h r -> Assignment (SymExpr sym) (idx0 ::> BaseIntegerType) -> IO r
f Assignment (SymExpr sym) idx0
i r
a Integer
j = do
              SymExpr sym BaseIntegerType
je <- sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
j
              r -> Assignment (SymExpr sym) (idx0 ::> BaseIntegerType) -> IO r
f r
a (Assignment (SymExpr sym) idx0
i Assignment (SymExpr sym) idx0
-> SymExpr sym BaseIntegerType
-> Assignment (SymExpr sym) (idx0 ::> BaseIntegerType)
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> SymExpr sym BaseIntegerType
je)

-- | Examine the list of terms, and determine if any one of them
--   appears in the given @BoolMap@ with the same polarity.
checkAbsorption ::
  BoolMap (Expr t) ->
  [(BoolExpr t, Polarity)] ->
  Bool
checkAbsorption :: BoolMap (Expr t) -> [(BoolExpr t, Polarity)] -> Bool
checkAbsorption BoolMap (Expr t)
_bm [] = Bool
False
checkAbsorption BoolMap (Expr t)
bm ((BoolExpr t
x,Polarity
p):[(BoolExpr t, Polarity)]
_)
  | Just Polarity
p' <- BoolMap (Expr t) -> BoolExpr t -> Maybe Polarity
forall (f :: BaseType -> Type).
OrdF f =>
BoolMap f -> f BaseBoolType -> Maybe Polarity
BM.contains BoolMap (Expr t)
bm BoolExpr t
x, Polarity
p Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
p' = Bool
True
checkAbsorption BoolMap (Expr t)
bm ((BoolExpr t, Polarity)
_:[(BoolExpr t, Polarity)]
xs) = BoolMap (Expr t) -> [(BoolExpr t, Polarity)] -> Bool
forall t. BoolMap (Expr t) -> [(BoolExpr t, Polarity)] -> Bool
checkAbsorption BoolMap (Expr t)
bm [(BoolExpr t, Polarity)]
xs

-- | If @tryAndAbsorption x y@ returns @True@, that means that @y@
-- implies @x@, so that the conjunction @x AND y = y@. A @False@
-- result gives no information.
tryAndAbsorption ::
  BoolExpr