| Copyright | (c) Sirui Lu 2021-2024 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Grisette.SymPrim
Description
Synopsis
- data IntN (n :: Nat)
- data WordN (n :: Nat)
- data SomeBV bv where
- data BitwidthMismatch = BitwidthMismatch
- pattern SomeIntN :: () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN
- type SomeIntN = SomeBV IntN
- pattern SomeWordN :: () => (KnownNat n, 1 <= n) => WordN n -> SomeWordN
- type SomeWordN = SomeBV WordN
- data a =-> b = TabularFun {
- funcTable :: [(a, b)]
- defaultFuncValue :: b
- data a --> b
- (-->) :: (SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedSymbol ca -> sb -> ca --> cb
- unsafeSomeBV :: forall bv. Int -> (forall proxy n. (KnownNat n, 1 <= n) => proxy n -> bv n) -> SomeBV bv
- unarySomeBV :: forall bv r. (forall n. (KnownNat n, 1 <= n) => bv n -> r) -> SomeBV bv -> r
- unarySomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> SomeBV bv -> SomeBV bv
- binSomeBV :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> SomeBV bv -> SomeBV bv -> r
- binSomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> SomeBV bv -> SomeBV bv -> SomeBV bv
- binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
- binSomeBVSafe :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, Mergeable r) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) -> SomeBV bv -> SomeBV bv -> m r
- binSomeBVSafeR1 :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
- binSomeBVSafeR2 :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
- conBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv
- conBVView :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV bv -> Maybe (SomeBV cbv)
- pattern ConBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv
- symBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Symbol -> SomeBV bv
- ssymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> SomeBV bv
- isymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> Int -> SomeBV bv
- arbitraryBV :: forall bv. (forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n)) => Int -> Gen (SomeBV bv)
- class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t, SupportedPrimConstraint t, SBVRep t) => SupportedPrim t
- class SupportedPrim con => SymRep con where
- type SymType con
- class ConRep sym where
- type ConType sym
- class (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) => LinkedRep con sym | con -> sym, sym -> con
- newtype SymBool = SymBool (Term Bool)
- newtype SymInteger = SymInteger (Term Integer)
- newtype SymWordN (n :: Nat) = SymWordN {
- underlyingWordNTerm :: Term (WordN n)
- newtype SymIntN (n :: Nat) = SymIntN {
- underlyingIntNTerm :: Term (IntN n)
- type SomeSymIntN = SomeBV SymIntN
- type SomeSymWordN = SomeBV SymWordN
- pattern SomeSymIntN :: () => (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN
- pattern SomeSymWordN :: () => (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN
- data sa =~> sb where
- data sa -~> sb where
- data TypedSymbol t where
- TypedSymbol :: SupportedPrim t => {..} -> TypedSymbol t
- symSize :: forall con sym. LinkedRep con sym => sym -> Int
- symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int
- class AllSyms a where
- allSymsSize :: AllSyms a => a -> Int
- newtype SymbolSet = SymbolSet {}
- newtype Model = Model {}
- data ModelValuePair t = (TypedSymbol t) ::= t
- data ModelSymPair ct st where
- (:=) :: LinkedRep ct st => st -> ct -> ModelSymPair ct st
Symbolic type implementation
Extended types
Symbolic signed bit vectors.
Instances
data WordN (n :: Nat) Source #
Symbolic unsigned bit vectors.
Instances
Non-indexed bitvectors.
Instances
data BitwidthMismatch Source #
Constructors
| BitwidthMismatch |
Instances
pattern SomeIntN :: () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN Source #
Pattern synonym for SomeBV with concrete signed bitvectors.
pattern SomeWordN :: () => (KnownNat n, 1 <= n) => WordN n -> SomeWordN Source #
Pattern synonym for SomeBV with concrete unsigned bitvectors.
data a =-> b infixr 0 Source #
Functions as a table. Use the # operator to apply the function.
>>>:set -XTypeOperators>>>let f = TabularFun [(1, 2), (3, 4)] 0 :: Int =-> Int>>>f # 12>>>f # 20>>>f # 34
Constructors
| TabularFun | |
Fields
| |
Instances
data a --> b infixr 0 Source #
General symbolic function type. Use the # operator to apply the function.
Note that this function should be applied to symbolic values only. It is by
itself already a symbolic value, but can be considered partially concrete
as the function body is specified. Use -~>
for uninterpreted general symbolic functions.
The result would be partially evaluated.
>>>:set -XOverloadedStrings>>>:set -XTypeOperators>>>let f = ("x" :: TypedSymbol Integer) --> ("x" + 1 + "y" :: SymInteger) :: Integer --> Integer>>>f # 1 -- 1 has the type SymInteger(+ 2 y)>>>f # "a" -- "a" has the type SymInteger(+ 1 (+ a y))
Instances
(-->) :: (SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedSymbol ca -> sb -> ca --> cb infixr 0 Source #
Construction of general symbolic functions.
>>>f = "a" --> "a" + 1 :: Integer --> Integer>>>f\(a:ARG :: Integer) -> (+ 1 a:ARG)
This general symbolic function needs to be applied to symbolic values: >>> f # ("a" :: SymInteger) (+ 1 a)
unsafeSomeBV :: forall bv. Int -> (forall proxy n. (KnownNat n, 1 <= n) => proxy n -> bv n) -> SomeBV bv Source #
Construct a SomeBV with a given run-time bitwidth and a polymorphic
value for the underlying bitvector.
unarySomeBV :: forall bv r. (forall n. (KnownNat n, 1 <= n) => bv n -> r) -> SomeBV bv -> r Source #
Lift a unary operation on sized bitvectors that returns anything to
SomeBV.
unarySomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> SomeBV bv -> SomeBV bv Source #
binSomeBV :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> SomeBV bv -> SomeBV bv -> r Source #
Lift a binary operation on sized bitvectors that returns anything to
SomeBV. Crash if the bitwidths do not match.
binSomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> SomeBV bv -> SomeBV bv -> SomeBV bv Source #
binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv) Source #
binSomeBVSafe :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, Mergeable r) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) -> SomeBV bv -> SomeBV bv -> m r Source #
Lift a binary operation on sized bitvectors that returns anything wrapped
with ExceptT to SomeBV. If the bitwidths do not match, throw an
BitwidthMismatch error to the monadic context.
binSomeBVSafeR1 :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source #
Lift a binary operation on sized bitvectors that returns a bitvector
wrapped with ExceptT to SomeBV. The result will also be wrapped with
SomeBV.
If the bitwidths do not match, throw an BitwidthMismatch error to the
monadic context.
binSomeBVSafeR2 :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv) Source #
Lift a binary operation on sized bitvectors that returns two bitvectors
wrapped with ExceptT to SomeBV. The results will also be wrapped with
SomeBV.
If the bitwidths do not match, throw an BitwidthMismatch error to the
monadic context.
conBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv Source #
conBVView :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV bv -> Maybe (SomeBV cbv) Source #
pattern ConBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv Source #
symBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Symbol -> SomeBV bv Source #
ssymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> SomeBV bv Source #
isymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> Int -> SomeBV bv Source #
arbitraryBV :: forall bv. (forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n)) => Int -> Gen (SomeBV bv) Source #
Generate an arbitrary SomeBV with a given run-time bitwidth.
Symbolic types
class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t, SupportedPrimConstraint t, SBVRep t) => SupportedPrim t Source #
Indicates that a type is supported and can be represented as a symbolic term.
Minimal complete definition
defaultValue, pevalITETerm, pevalEqTerm, conSBVTerm, symSBVName, symSBVTerm, parseSMTModelResult
Instances
class SupportedPrim con => SymRep con Source #
Type family to resolve the symbolic type associated with a concrete type.
Instances
| SymRep Integer Source # | |
Defined in Grisette.Internal.SymPrim.SymInteger | |
| SymRep Bool Source # | |
Defined in Grisette.Internal.SymPrim.SymBool | |
| (KnownNat n, 1 <= n) => SymRep (IntN n) Source # | |
Defined in Grisette.Internal.SymPrim.SymBV | |
| (KnownNat n, 1 <= n) => SymRep (WordN n) Source # | |
Defined in Grisette.Internal.SymPrim.SymBV | |
| (SymRep ca, SymRep cb, SupportedPrim (ca --> cb)) => SymRep (ca --> cb) Source # | |
Defined in Grisette.Internal.SymPrim.SymGeneralFun | |
| (SymRep a, SymRep b, SupportedPrim (a =-> b)) => SymRep (a =-> b) Source # | |
Defined in Grisette.Internal.SymPrim.SymTabularFun | |
Type family to resolve the concrete type associated with a symbolic type.
Instances
| ConRep SymBool Source # | |
Defined in Grisette.Internal.SymPrim.SymBool | |
| ConRep SymInteger Source # | |
Defined in Grisette.Internal.SymPrim.SymInteger Associated Types type ConType SymInteger Source # | |
| (KnownNat n, 1 <= n) => ConRep (SymIntN n) Source # | |
Defined in Grisette.Internal.SymPrim.SymBV | |
| (KnownNat n, 1 <= n) => ConRep (SymWordN n) Source # | |
Defined in Grisette.Internal.SymPrim.SymBV | |
| (ConRep a, ConRep b) => ConRep (a -~> b) Source # | |
Defined in Grisette.Internal.SymPrim.SymGeneralFun | |
| (ConRep a, ConRep b) => ConRep (a =~> b) Source # | |
Defined in Grisette.Internal.SymPrim.SymTabularFun | |
class (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) => LinkedRep con sym | con -> sym, sym -> con Source #
One-to-one mapping between symbolic types and concrete types.
Minimal complete definition
Instances
| LinkedRep Integer SymInteger Source # | |
Defined in Grisette.Internal.SymPrim.SymInteger Methods underlyingTerm :: SymInteger -> Term Integer Source # | |
| LinkedRep Bool SymBool Source # | |
| (KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source # | |
| (KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source # | |
| (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim ca, SupportedPrim cb, SupportedPrim (ca --> cb)) => LinkedRep (ca --> cb) (sa -~> sb) Source # | |
| (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => LinkedRep (ca =-> cb) (sa =~> sb) Source # | |
Symbolic Boolean type.
>>>:set -XOverloadedStrings>>>"a" :: SymBoola>>>"a" .&& "b" :: SymBool(&& a b)
More symbolic operations are available. Please refer to the documentation for the type class instances.
Instances
newtype SymInteger Source #
Symbolic (unbounded, mathematical) integer type.
>>>"a" + 1 :: SymInteger(+ 1 a)
More symbolic operations are available. Please refer to the documentation for the type class instances.
Constructors
| SymInteger (Term Integer) |
Instances
newtype SymWordN (n :: Nat) Source #
Symbolic unsigned bit vector type. Indexed with the bit width. Signedness affects the semantics of the operations, including comparison/extension, etc.
>>>:set -XOverloadedStrings -XDataKinds -XBinaryLiterals>>>"a" + 5 :: SymWordN 5(+ 0b00101 a)>>>sizedBVConcat (con 0b101 :: SymWordN 3) (con 0b110 :: SymWordN 3)0b101110>>>sizedBVExt (Proxy @6) (con 0b101 :: SymWordN 3)0b000101>>>(8 :: SymWordN 4) .< (7 :: SymWordN 4)false
More symbolic operations are available. Please refer to the documentation for the type class instances.
Constructors
| SymWordN | |
Fields
| |
Instances
newtype SymIntN (n :: Nat) Source #
Symbolic signed bit vector type. Indexed with the bit width. Signedness affects the semantics of the operations, including comparison/extension, etc.
>>>:set -XOverloadedStrings -XDataKinds -XBinaryLiterals>>>"a" + 5 :: SymIntN 5(+ 0b00101 a)>>>sizedBVConcat (con 0b101 :: SymIntN 3) (con 0b110 :: SymIntN 3)0b101110>>>sizedBVExt (Proxy @6) (con 0b101 :: SymIntN 3)0b111101>>>(8 :: SymIntN 4) .< (7 :: SymIntN 4)true
More symbolic operations are available. Please refer to the documentation for the type class instances.
Constructors
| SymIntN | |
Fields
| |
Instances
type SomeSymWordN = SomeBV SymWordN Source #
Type synonym for SomeBV with symbolic unsigned bitvectors.
pattern SomeSymIntN :: () => (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN Source #
Pattern synonym for SomeBV with symbolic signed bitvectors.
pattern SomeSymWordN :: () => (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN Source #
Pattern synonym for SomeBV with symbolic unsigned bitvectors.
data sa =~> sb where infixr 0 Source #
Symbolic tabular function type.
>>>:set -XTypeOperators -XOverloadedStrings>>>f' = "f" :: SymInteger =~> SymInteger>>>f = (f' #)>>>f 1(apply f 1)
>>>f' = con (TabularFun [(1, 2), (2, 3)] 4) :: SymInteger =~> SymInteger>>>f = (f' #)>>>f 12>>>f 23>>>f 34>>>f "b"(ite (= b 1) 2 (ite (= b 2) 3 4))
Instances
data sa -~> sb where infixr 0 Source #
Symbolic general function type.
>>>:set -XTypeOperators -XOverloadedStrings>>>f' = "f" :: SymInteger -~> SymInteger>>>f = (f' #)>>>f 1(apply f 1)
>>>f' = con ("a" --> "a" + 1) :: SymInteger -~> SymInteger>>>f'\(a:ARG :: Integer) -> (+ 1 a:ARG)>>>f = (f' #)>>>f 12>>>f 23>>>f 34>>>f "b"(+ 1 b)
Instances
data TypedSymbol t where Source #
A typed symbol is a symbol that is associated with a type. Note that the same symbol bodies with different types are considered different symbols and can coexist in a term.
Simple symbols can be created with the OverloadedStrings extension:
>>>:set -XOverloadedStrings>>>"a" :: TypedSymbol Boola :: Bool
Constructors
| TypedSymbol | |
Fields
| |
Instances
symSize :: forall con sym. LinkedRep con sym => sym -> Int Source #
Get the size of a symbolic term. Duplicate sub-terms are counted for only once.
>>>symSize (1 :: SymInteger)1>>>symSize ("a" :: SymInteger)1>>>symSize ("a" + 1 :: SymInteger)3>>>symSize (("a" + 1) * ("a" + 1) :: SymInteger)4
symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int Source #
Get the sum of the sizes of a list of symbolic terms. Duplicate sub-terms are counted for only once.
>>>symsSize [1, "a" :: SymInteger, "a" + 1 :: SymInteger]3
class AllSyms a where Source #
Extract all symbolic primitive values that are represented as SMT terms.
Note: This type class can be derived for algebraic data types. You may
need the DerivingVia and DerivingStrategies extenstions.
data X = ... deriving Generic deriving AllSyms via (Default X)
Methods
allSymsS :: a -> [SomeSym] -> [SomeSym] Source #
Convert a value to a list of symbolic primitive values. It should prepend to an existing list of symbolic primitive values.
allSyms :: a -> [SomeSym] Source #
Specialized allSymsS that prepends to an empty list.
Instances
allSymsSize :: AllSyms a => a -> Int Source #
Get the total size of symbolic terms in a value. Duplicate sub-terms are counted for only once.
>>>allSymsSize ("a" :: SymInteger, "a" + "b" :: SymInteger, ("a" + "b") * "c" :: SymInteger)5
Symbolic constant sets and models
Symbolic constant set.
Constructors
| SymbolSet | |
Fields | |
Instances
Model returned by the solver.
Constructors
| Model | |
Fields | |
Instances
data ModelValuePair t Source #
A type used for building a model by hand.
>>>buildModel ("x" ::= (1 :: Integer), "y" ::= True) :: ModelModel {x -> 1 :: Integer, y -> True :: Bool}
Constructors
| (TypedSymbol t) ::= t |
Instances
| Show t => Show (ModelValuePair t) Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Model Methods showsPrec :: Int -> ModelValuePair t -> ShowS # show :: ModelValuePair t -> String # showList :: [ModelValuePair t] -> ShowS # | |
| ModelRep (ModelValuePair t) Model Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildModel :: ModelValuePair t -> Model Source # | |
data ModelSymPair ct st where Source #
A pair of a symbolic constant and its value. This is used to build a model from a list of symbolic constants and their values.
>>>buildModel ("a" := (1 :: Integer), "b" := True) :: ModelModel {a -> 1 :: Integer, b -> True :: Bool}
Constructors
| (:=) :: LinkedRep ct st => st -> ct -> ModelSymPair ct st |
Instances
| ModelRep (ModelSymPair ct st) Model Source # | |
Defined in Grisette.Internal.SymPrim.ModelRep Methods buildModel :: ModelSymPair ct st -> Model Source # | |