grisette-0.1.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

data FunArg Source #

Constructors

FunArg 

Instances

Instances details
Generic FunArg Source # 
Instance details

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

Associated Types

type Rep FunArg :: Type -> Type #

Methods

from :: FunArg -> Rep FunArg x #

to :: Rep FunArg x -> FunArg #

Show FunArg Source # 
Instance details

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

NFData FunArg Source # 
Instance details

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

Methods

rnf :: FunArg -> () #

Eq FunArg Source # 
Instance details

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

Methods

(==) :: FunArg -> FunArg -> Bool #

(/=) :: FunArg -> FunArg -> Bool #

Ord FunArg Source # 
Instance details

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

Hashable FunArg Source # 
Instance details

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

Methods

hashWithSalt :: Int -> FunArg -> Int #

hash :: FunArg -> Int #

Lift FunArg Source # 
Instance details

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

Methods

lift :: Quote m => FunArg -> m Exp #

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

type Rep FunArg Source # 
Instance details

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

type Rep FunArg = D1 ('MetaData "FunArg" "Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'False) (C1 ('MetaCons "FunArg" 'PrefixI 'False) (U1 :: Type -> Type))

newtype Sym a Source #

Symbolic primitive type.

Symbolic Boolean, integer, and bit vector types are supported.

>>> :set -XOverloadedStrings
>>> "a" :: Sym Bool
a
>>> "a" &&~ "b" :: Sym Bool
(&& a b)
>>> "i" + 1 :: Sym Integer
(+ 1 i)

For more symbolic operations, please refer to the documentation of the grisette-core package.

Grisette also supports uninterpreted functions. You can use the --> (general function) or =-> (tabular function) types to define uninterpreted functions. The following code shows the examples

>>> :set -XTypeOperators
>>> let ftab = "ftab" :: Sym (Integer =-> Integer)
>>> ftab # "x"
(apply ftab x)
>>> solve (UnboundedReasoning z3) (ftab # 1 ==~ 2 &&~ ftab # 2 ==~ 3 &&~ ftab # 3 ==~ 4)
Right (Model {
  ftab ->
    TabularFun {funcTable = [(3,4),(2,3)], defaultFuncValue = 2}
      :: (=->) Integer Integer
}) -- possible result (reformatted)
>>> let fgen = "fgen" :: Sym (Integer --> Integer)
>>> fgen # "x"
(apply fgen x)
>>> solve (UnboundedReasoning z3) (fgen # 1 ==~ 2 &&~ fgen # 2 ==~ 3 &&~ fgen # 3 ==~ 4)
Right (Model {
  fgen ->
    \(arg@0:FuncArg :: Integer) ->
      (ite (= arg@0:FuncArg 2) 3 (ite (= arg@0:FuncArg 3) 4 2))
        :: (-->) Integer Integer
}) -- possible result (reformatted)

Constructors

Sym 

Fields

Instances

Instances details
SupportedPrim a => GenSym () (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (Sym a)) Source #

SupportedPrim a => GenSymSimple () (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (Sym a) Source #

SupportedPrim a => Solvable a (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: a -> Sym a Source #

conView :: Sym a -> Maybe a Source #

ssym :: String -> Sym a Source #

isym :: String -> Int -> Sym a Source #

sinfosym :: (Typeable a0, Ord a0, Lift a0, NFData a0, Show a0, Hashable a0) => String -> a0 -> Sym a Source #

iinfosym :: (Typeable a0, Ord a0, Lift a0, NFData a0, Show a0, Hashable a0) => String -> Int -> a0 -> Sym a Source #

ToSym Int16 (Sym (IntN 16)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int16 -> Sym (IntN 16) Source #

ToSym Int32 (Sym (IntN 32)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int32 -> Sym (IntN 32) Source #

ToSym Int64 (Sym (IntN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int64 -> Sym (IntN 64) Source #

ToSym Int8 (Sym (IntN 8)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int8 -> Sym (IntN 8) Source #

ToSym Word16 (Sym (WordN 16)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word16 -> Sym (WordN 16) Source #

ToSym Word32 (Sym (WordN 32)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word32 -> Sym (WordN 32) Source #

ToSym Word64 (Sym (WordN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word64 -> Sym (WordN 64) Source #

ToSym Word8 (Sym (WordN 8)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word8 -> Sym (WordN 8) Source #

ToSym Int (Sym (IntN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int -> Sym (IntN 64) Source #

ToSym Word (Sym (WordN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word -> Sym (WordN 64) Source #

SupportedPrim a => ToSym a (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: a -> Sym a Source #

Lift (Sym a :: Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

lift :: Quote m => Sym a -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => Sym a -> Code m (Sym a) #

SupportedPrim (IntN n) => Bits (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(.&.) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

(.|.) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

xor :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

complement :: Sym (IntN n) -> Sym (IntN n) #

shift :: Sym (IntN n) -> Int -> Sym (IntN n) #

rotate :: Sym (IntN n) -> Int -> Sym (IntN n) #

zeroBits :: Sym (IntN n) #

bit :: Int -> Sym (IntN n) #

setBit :: Sym (IntN n) -> Int -> Sym (IntN n) #

clearBit :: Sym (IntN n) -> Int -> Sym (IntN n) #

complementBit :: Sym (IntN n) -> Int -> Sym (IntN n) #

testBit :: Sym (IntN n) -> Int -> Bool #

bitSizeMaybe :: Sym (IntN n) -> Maybe Int #

bitSize :: Sym (IntN n) -> Int #

isSigned :: Sym (IntN n) -> Bool #

shiftL :: Sym (IntN n) -> Int -> Sym (IntN n) #

unsafeShiftL :: Sym (IntN n) -> Int -> Sym (IntN n) #

shiftR :: Sym (IntN n) -> Int -> Sym (IntN n) #

unsafeShiftR :: Sym (IntN n) -> Int -> Sym (IntN n) #

rotateL :: Sym (IntN n) -> Int -> Sym (IntN n) #

rotateR :: Sym (IntN n) -> Int -> Sym (IntN n) #

popCount :: Sym (IntN n) -> Int #

SupportedPrim (WordN n) => Bits (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(.&.) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

(.|.) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

xor :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

complement :: Sym (WordN n) -> Sym (WordN n) #

shift :: Sym (WordN n) -> Int -> Sym (WordN n) #

rotate :: Sym (WordN n) -> Int -> Sym (WordN n) #

zeroBits :: Sym (WordN n) #

bit :: Int -> Sym (WordN n) #

setBit :: Sym (WordN n) -> Int -> Sym (WordN n) #

clearBit :: Sym (WordN n) -> Int -> Sym (WordN n) #

complementBit :: Sym (WordN n) -> Int -> Sym (WordN n) #

testBit :: Sym (WordN n) -> Int -> Bool #

bitSizeMaybe :: Sym (WordN n) -> Maybe Int #

bitSize :: Sym (WordN n) -> Int #

isSigned :: Sym (WordN n) -> Bool #

shiftL :: Sym (WordN n) -> Int -> Sym (WordN n) #

unsafeShiftL :: Sym (WordN n) -> Int -> Sym (WordN n) #

shiftR :: Sym (WordN n) -> Int -> Sym (WordN n) #

unsafeShiftR :: Sym (WordN n) -> Int -> Sym (WordN n) #

rotateL :: Sym (WordN n) -> Int -> Sym (WordN n) #

rotateR :: Sym (WordN n) -> Int -> Sym (WordN n) #

popCount :: Sym (WordN n) -> Int #

SupportedPrim t => IsString (Sym t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

fromString :: String -> Sym t #

Generic (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Rep (Sym a) :: Type -> Type #

Methods

from :: Sym a -> Rep (Sym a) x #

to :: Rep (Sym a) x -> Sym a #

SupportedPrim (IntN n) => Num (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(+) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

(-) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

(*) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

negate :: Sym (IntN n) -> Sym (IntN n) #

abs :: Sym (IntN n) -> Sym (IntN n) #

signum :: Sym (IntN n) -> Sym (IntN n) #

fromInteger :: Integer -> Sym (IntN n) #

SupportedPrim (WordN n) => Num (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(+) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

(-) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

(*) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

negate :: Sym (WordN n) -> Sym (WordN n) #

abs :: Sym (WordN n) -> Sym (WordN n) #

signum :: Sym (WordN n) -> Sym (WordN n) #

fromInteger :: Integer -> Sym (WordN n) #

Num (Sym Integer) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim a => Show (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

showsPrec :: Int -> Sym a -> ShowS #

show :: Sym a -> String #

showList :: [Sym a] -> ShowS #

NFData (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

rnf :: Sym a -> () #

SupportedPrim a => Eq (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(==) :: Sym a -> Sym a -> Bool #

(/=) :: Sym a -> Sym a -> Bool #

SupportedPrim a => ITEOp (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

Methods

ites :: SymBool -> Sym a -> Sym a -> Sym a Source #

LogicalOp (Sym Bool) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SupportedPrim (IntN n) => SEq (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(==~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(/=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

SupportedPrim (WordN n) => SEq (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(==~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(/=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

SupportedPrim Integer => SEq (Sym Integer) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim Bool => SEq (Sym Bool) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymBoolOp (Sym Bool) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim a => EvaluateSym (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

evaluateSym :: Bool -> Model -> Sym a -> Sym a Source #

SupportedPrim a => ExtractSymbolics (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SignedDivMod (Sym Integer) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymIntegerOp (Sym Integer) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim a => Mergeable (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

SupportedPrim (IntN n) => SOrd (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(<=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(>~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(>=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

symCompare :: Sym (IntN n) -> Sym (IntN n) -> UnionM Ordering Source #

SupportedPrim (WordN n) => SOrd (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(<=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(>~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(>=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

symCompare :: Sym (WordN n) -> Sym (WordN n) -> UnionM Ordering Source #

SupportedPrim Integer => SOrd (Sym Integer) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SOrd (Sym Bool) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim a => SimpleMergeable (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> Sym a -> Sym a -> Sym a Source #

SubstituteSym (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Sym a -> Sym a Source #

SupportedPrim a => Hashable (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

hashWithSalt :: Int -> Sym a -> Int #

hash :: Sym a -> Int #

ToCon (Sym (IntN 8)) Int8 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 8) -> Maybe Int8 Source #

ToCon (Sym (IntN 16)) Int16 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 16) -> Maybe Int16 Source #

ToCon (Sym (IntN 32)) Int32 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 32) -> Maybe Int32 Source #

ToCon (Sym (IntN 64)) Int64 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 64) -> Maybe Int64 Source #

ToCon (Sym (IntN 64)) Int Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 64) -> Maybe Int Source #

ToCon (Sym (WordN 8)) Word8 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 8) -> Maybe Word8 Source #

ToCon (Sym (WordN 16)) Word16 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 16) -> Maybe Word16 Source #

ToCon (Sym (WordN 32)) Word32 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 32) -> Maybe Word32 Source #

ToCon (Sym (WordN 64)) Word64 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 64) -> Maybe Word64 Source #

ToCon (Sym (WordN 64)) Word Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 64) -> Maybe Word Source #

SupportedPrim a => ToCon (Sym a) a Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym a -> Maybe a Source #

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (IntN ow)) ix w (Sym (IntN w)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvselect :: proxy ix -> proxy w -> Sym (IntN ow) -> Sym (IntN w) Source #

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (WordN ow)) ix w (Sym (WordN w)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvselect :: proxy ix -> proxy w -> Sym (WordN ow) -> Sym (WordN w) Source #

(KnownNat w, KnownNat w', 1 <= w, 1 <= w', w <= w', (w + 1) <= w', 1 <= (w' - w), KnownNat (w' - w)) => BVExtend (Sym (IntN w)) w' (Sym (IntN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvzeroExtend :: proxy w' -> Sym (IntN w) -> Sym (IntN w') Source #

bvsignExtend :: proxy w' -> Sym (IntN w) -> Sym (IntN w') Source #

bvextend :: proxy w' -> Sym (IntN w) -> Sym (IntN w') Source #

(KnownNat w, KnownNat w', 1 <= w, 1 <= w', (w + 1) <= w', w <= w', 1 <= (w' - w), KnownNat (w' - w)) => BVExtend (Sym (WordN w)) w' (Sym (WordN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvzeroExtend :: proxy w' -> Sym (WordN w) -> Sym (WordN w') Source #

bvsignExtend :: proxy w' -> Sym (WordN w) -> Sym (WordN w') Source #

bvextend :: proxy w' -> Sym (WordN w) -> Sym (WordN w') Source #

SupportedPrim a => GenSym (Sym a) (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Sym a -> m (UnionM (Sym a)) Source #

SupportedPrim a => GenSymSimple (Sym a) (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => Sym a -> m (Sym a) Source #

SupportedPrim a => ToCon (Sym a) (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym a -> Maybe (Sym a) Source #

SupportedPrim a => ToSym (Sym a) (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Sym a -> Sym a Source #

(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') => BVConcat (Sym (IntN n)) (Sym (IntN w)) (Sym (IntN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvconcat :: Sym (IntN n) -> Sym (IntN w) -> Sym (IntN w') Source #

(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') => BVConcat (Sym (WordN n)) (Sym (WordN w)) (Sym (WordN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvconcat :: Sym (WordN n) -> Sym (WordN w) -> Sym (WordN w') Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Arg (a -~> b) Source #

type Ret (a -~> b) Source #

Methods

(#) :: (a -~> b) -> Arg (a -~> b) -> Ret (a -~> b) Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Arg (a =~> b) Source #

type Ret (a =~> b) Source #

Methods

(#) :: (a =~> b) -> Arg (a =~> b) -> Ret (a =~> b) Source #

type Rep (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Rep (Sym a) = D1 ('MetaData "Sym" "Grisette.IR.SymPrim.Data.SymPrim" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'True) (C1 ('MetaCons "Sym" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term a))))
type Arg (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Arg (a -~> b) = Sym a
type Arg (a =~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Arg (a =~> b) = Sym a
type Ret (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Ret (a -~> b) = Sym b
type Ret (a =~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Ret (a =~> b) = Sym b

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 c), KnownNat a, KnownNat b, KnownNat c, BVConcat (bv a) (bv b) (bv c)) => !Id -> !(Term (bv a)) -> !(Term (bv b)) -> Term (bv c) 
BVSelectTerm :: (SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a, KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) => !Id -> !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv a)) -> Term (bv w) 
BVExtendTerm :: (SupportedPrim (bv a), SupportedPrim (bv b), KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b)) => !Id -> !Bool -> !(TypeRep n) -> !(Term (bv a)) -> Term (bv b) 
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 
DivIntegerTerm :: !Id -> Term Integer -> Term Integer -> Term Integer 
ModIntegerTerm :: !Id -> Term Integer -> Term Integer -> Term Integer 

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 #