grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Internal.IR.SymPrim

Description

 
Synopsis

Documentation

class (SupportedPrim arg, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => UnaryOp tag arg t | tag arg -> t where Source #

Methods

partialEvalUnary :: (Typeable tag, Typeable t) => tag -> Term arg -> Term t Source #

pformatUnary :: tag -> Term arg -> String Source #

class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => BinaryOp tag arg1 arg2 t | tag arg1 arg2 -> t where Source #

Methods

partialEvalBinary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term t Source #

pformatBinary :: tag -> Term arg1 -> Term arg2 -> String Source #

class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim arg3, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => TernaryOp tag arg1 arg2 arg3 t | tag arg1 arg2 arg3 -> t where Source #

Methods

partialEvalTernary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t Source #

pformatTernary :: tag -> Term arg1 -> Term arg2 -> Term arg3 -> String Source #

data Term t where Source #

Constructors

ConTerm :: SupportedPrim t => !Id -> !t -> Term t 
SymTerm :: SupportedPrim t => !Id -> !(TypedSymbol t) -> Term t 
UnaryTerm :: UnaryOp tag arg t => !Id -> !tag -> !(Term arg) -> Term t 
BinaryTerm :: BinaryOp tag arg1 arg2 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> Term t 
TernaryTerm :: TernaryOp tag arg1 arg2 arg3 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> !(Term arg3) -> Term t 
NotTerm :: !Id -> !(Term Bool) -> Term Bool 
OrTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool 
AndTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool 
EqvTerm :: SupportedPrim t => !Id -> !(Term t) -> !(Term t) -> Term Bool 
ITETerm :: SupportedPrim t => !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t 
AddNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> !(Term t) -> Term t 
UMinusNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> Term t 
TimesNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> !(Term t) -> Term t 
AbsNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> Term t 
SignumNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> Term t 
LTNumTerm :: (SupportedPrim t, Num t, Ord t) => !Id -> !(Term t) -> !(Term t) -> Term Bool 
LENumTerm :: (SupportedPrim t, Num t, Ord t) => !Id -> !(Term t) -> !(Term t) -> Term Bool 
AndBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !(Term t) -> Term t 
OrBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !(Term t) -> Term t 
XorBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !(Term t) -> Term t 
ComplementBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> Term t 
ShiftBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !Int -> Term t 
RotateBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !Int -> Term t 
BVConcatTerm :: (SupportedPrim (bv a), SupportedPrim (bv b), SupportedPrim (bv (a + b)), KnownNat a, KnownNat b, 1 <= a, 1 <= b, SizedBV bv) => !Id -> !(Term (bv a)) -> !(Term (bv b)) -> Term (bv (a + b)) 
BVSelectTerm :: (SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n, SizedBV bv) => !Id -> !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv n)) -> Term (bv w) 
BVExtendTerm :: (SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l, KnownNat r, 1 <= l, l <= r, SizedBV bv) => !Id -> !Bool -> !(TypeRep r) -> !(Term (bv l)) -> Term (bv r) 
TabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => !Id -> Term (a =-> b) -> Term a -> Term b 
GeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => !Id -> Term (a --> b) -> Term a -> Term b 
DivIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
ModIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
QuotIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
RemIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
DivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
ModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
QuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 
RemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t 

Instances

Instances details
Lift (Term t :: Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

lift :: Quote m => Term t -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => Term t -> Code m (Term t) #

Show (Term ty) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

showsPrec :: Int -> Term ty -> ShowS #

show :: Term ty -> String #

showList :: [Term ty] -> ShowS #

NFData (Term a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

rnf :: Term a -> () #

SupportedPrim t => Eq (Term t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

(==) :: Term t -> Term t -> Bool #

(/=) :: Term t -> Term t -> Bool #

SupportedPrim t => Eq (Description (Term t)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

(==) :: Description (Term t) -> Description (Term t) -> Bool #

(/=) :: Description (Term t) -> Description (Term t) -> Bool #

SupportedPrim t => Hashable (Term t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

hashWithSalt :: Int -> Term t -> Int #

hash :: Term t -> Int #

SupportedPrim t => Hashable (Description (Term t)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

hashWithSalt :: Int -> Description (Term t) -> Int #

hash :: Description (Term t) -> Int #

SupportedPrim t => Interned (Term t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

data Description (Term t) #

type Uninterned (Term t) #

Methods

describe :: Uninterned (Term t) -> Description (Term t) #

identify :: Id -> Uninterned (Term t) -> Term t #

seedIdentity :: p (Term t) -> Id #

cacheWidth :: p (Term t) -> Int #

modifyAdvice :: IO (Term t) -> IO (Term t) #

cache :: Cache (Term t) #

data Description (Term t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

data Description (Term t) where
type Uninterned (Term t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

type Uninterned (Term t) = UTerm t

evaluateTerm :: forall a. SupportedPrim a => Bool -> Model -> Term a -> Term a Source #

introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a Source #

data SomeTerm where Source #

Constructors

SomeTerm :: forall a. SupportedPrim a => Term a -> SomeTerm 

class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where Source #

Indicates that a type is supported and can be represented as a symbolic term.

Minimal complete definition

defaultValue

Associated Types

type PrimConstraint t :: Constraint Source #

type PrimConstraint t = ()

Methods

withPrim :: proxy t -> (PrimConstraint t => a) -> a Source #

default withPrim :: PrimConstraint t => proxy t -> (PrimConstraint t => a) -> a Source #

termCache :: Cache (Term t) Source #

pformatCon :: t -> String Source #

default pformatCon :: Show t => t -> String Source #

pformatSym :: TypedSymbol t -> String Source #

defaultValue :: t Source #

defaultValueDynamic :: proxy t -> ModelValue Source #

Instances

Instances details
SupportedPrim Integer Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint Integer Source #

SupportedPrim Bool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint Bool Source #

(KnownNat w, 1 <= w) => SupportedPrim (IntN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (IntN w) Source #

(KnownNat w, 1 <= w) => SupportedPrim (WordN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (WordN w) Source #

(SupportedPrim a, SupportedPrim b) => SupportedPrim (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (a --> b) Source #

Methods

withPrim :: proxy (a --> b) -> (PrimConstraint (a --> b) => a0) -> a0 Source #

termCache :: Cache (Term (a --> b)) Source #

pformatCon :: (a --> b) -> String Source #

pformatSym :: TypedSymbol (a --> b) -> String Source #

defaultValue :: a --> b Source #

defaultValueDynamic :: proxy (a --> b) -> ModelValue Source #

(SupportedPrim a, SupportedPrim b) => SupportedPrim (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Associated Types

type PrimConstraint (a =-> b) Source #

Methods

withPrim :: proxy (a =-> b) -> (PrimConstraint (a =-> b) => a0) -> a0 Source #

termCache :: Cache (Term (a =-> b)) Source #

pformatCon :: (a =-> b) -> String Source #

pformatSym :: TypedSymbol (a =-> b) -> String Source #

defaultValue :: a =-> b Source #

defaultValueDynamic :: proxy (a =-> b) -> ModelValue Source #

castTerm :: forall a b. Typeable b => Term a -> Maybe (Term b) Source #

identityWithTypeRep :: forall t. Term t -> (TypeRep, Id) Source #

pformat :: forall t. SupportedPrim t => Term t -> String Source #

constructUnary :: forall tag arg t. (SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t, Show tag) => tag -> Term arg -> Term t Source #

constructBinary :: forall tag arg1 arg2 t. (SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term t Source #

constructTernary :: forall tag arg1 arg2 arg3 t. (SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t Source #

conTerm :: (SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) => t -> Term t Source #

symTerm :: forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t Source #

pattern BoolConTerm :: Bool -> Term a Source #

pattern TrueTerm :: Term a Source #

pattern FalseTerm :: Term a Source #

pattern BoolTerm :: Term Bool -> Term a Source #

pevalEqvTerm :: forall a. SupportedPrim a => Term a -> Term a -> Term Bool Source #

pevalITETerm :: forall a. SupportedPrim a => Term Bool -> Term a -> Term a -> Term a Source #

pattern UnaryTermPatt :: forall a b tag. (Typeable tag, Typeable b) => tag -> Term b -> Term a Source #

pattern BinaryTermPatt :: forall a b c tag. (Typeable tag, Typeable b, Typeable c) => tag -> Term b -> Term c -> Term a Source #

pattern TernaryTermPatt :: forall a b c d tag. (Typeable tag, Typeable b, Typeable c, Typeable d) => tag -> Term b -> Term c -> Term d -> Term a Source #

type PartialFun a b = a -> Maybe b Source #

type TotalRuleUnary a b = Term a -> Term b Source #

type PartialRuleBinary a b c = Term a -> PartialFun (Term b) (Term c) Source #

type TotalRuleBinary a b c = Term a -> Term b -> Term c Source #

totalize :: PartialFun a b -> (a -> b) -> a -> b Source #

totalize2 :: (a -> PartialFun b c) -> (a -> b -> c) -> a -> b -> c Source #

class UnaryPartialStrategy tag a b | tag a -> b where Source #

Methods

extractor :: tag -> Term a -> Maybe a Source #

constantHandler :: tag -> a -> Maybe (Term b) Source #

nonConstantHandler :: tag -> Term a -> Maybe (Term b) Source #

unaryPartial :: forall tag a b. UnaryPartialStrategy tag a b => tag -> PartialRuleUnary a b Source #

class BinaryCommPartialStrategy tag a c | tag a -> c where Source #

Methods

singleConstantHandler :: tag -> a -> Term a -> Maybe (Term c) Source #

class BinaryPartialStrategy tag a b c | tag a b -> c where Source #

Methods

extractora :: tag -> Term a -> Maybe a Source #

extractorb :: tag -> Term b -> Maybe b Source #

allConstantHandler :: tag -> a -> b -> Maybe (Term c) Source #

leftConstantHandler :: tag -> a -> Term b -> Maybe (Term c) Source #

default leftConstantHandler :: (a ~ b, BinaryCommPartialStrategy tag a c) => tag -> a -> Term b -> Maybe (Term c) Source #

rightConstantHandler :: tag -> Term a -> b -> Maybe (Term c) Source #

default rightConstantHandler :: (a ~ b, BinaryCommPartialStrategy tag a c) => tag -> Term a -> b -> Maybe (Term c) Source #

nonBinaryConstantHandler :: tag -> Term a -> Term b -> Maybe (Term c) Source #

binaryPartial :: forall tag a b c. BinaryPartialStrategy tag a b c => tag -> PartialRuleBinary a b c Source #

pattern NumConTerm :: forall b a. (Num b, Typeable b) => b -> Term a Source #

pattern NumOrdConTerm :: forall b a. (Num b, Ord b, Typeable b) => b -> Term a Source #

pevalAddNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a Source #

pevalTimesNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a Source #