| Copyright | (c) Sirui Lu 2021-2023 |
|---|---|
| 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.Internal.IR.SymPrim
Description
Synopsis
- data FunArg = FunArg
- newtype Sym a = Sym {
- underlyingTerm :: Term a
- 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
- partialEvalUnary :: (Typeable tag, Typeable t) => tag -> Term arg -> Term t
- pformatUnary :: tag -> Term arg -> String
- 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
- partialEvalBinary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term t
- pformatBinary :: tag -> Term arg1 -> Term arg2 -> String
- 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
- data Term t where
- 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
- showUntyped :: TypedSymbol t -> String
- withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a
- data SomeTypedSymbol where
- SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol
- someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol
- evaluateTerm :: forall a. SupportedPrim a => Bool -> Model -> Term a -> Term a
- introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a
- data SomeTerm where
- SomeTerm :: forall a. SupportedPrim a => Term a -> SomeTerm
- class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where
- type PrimConstraint t :: Constraint
- withPrim :: proxy t -> (PrimConstraint t => a) -> a
- termCache :: Cache (Term t)
- pformatCon :: t -> String
- pformatSym :: TypedSymbol t -> String
- defaultValue :: t
- defaultValueDynamic :: proxy t -> ModelValue
- castTerm :: forall a b. Typeable b => Term a -> Maybe (Term b)
- identity :: Term t -> Id
- identityWithTypeRep :: forall t. Term t -> (TypeRep, Id)
- pformat :: forall t. SupportedPrim t => Term t -> String
- constructUnary :: forall tag arg t. (SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t, Show tag) => tag -> Term arg -> Term t
- 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
- 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
- conTerm :: (SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) => t -> Term t
- symTerm :: forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
- ssymTerm :: (SupportedPrim t, Typeable t) => String -> Term t
- isymTerm :: (SupportedPrim t, Typeable t) => String -> Int -> Term t
- sinfosymTerm :: (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> Term t
- iinfosymTerm :: (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> Term t
- termSize :: Term a -> Int
- termsSize :: [Term a] -> Int
- extractSymbolicsTerm :: SupportedPrim a => Term a -> HashSet SomeTypedSymbol
- trueTerm :: Term Bool
- falseTerm :: Term Bool
- pattern BoolConTerm :: Bool -> Term a
- pattern TrueTerm :: Term a
- pattern FalseTerm :: Term a
- pattern BoolTerm :: Term Bool -> Term a
- pevalNotTerm :: Term Bool -> Term Bool
- pevalEqvTerm :: forall a. SupportedPrim a => Term a -> Term a -> Term Bool
- pevalNotEqvTerm :: SupportedPrim a => Term a -> Term a -> Term Bool
- pevalOrTerm :: Term Bool -> Term Bool -> Term Bool
- pevalAndTerm :: Term Bool -> Term Bool -> Term Bool
- pevalITETerm :: forall a. SupportedPrim a => Term Bool -> Term a -> Term a -> Term a
- pevalImplyTerm :: Term Bool -> Term Bool -> Term Bool
- pevalXorTerm :: Term Bool -> Term Bool -> Term Bool
- unaryUnfoldOnce :: forall a b. (Typeable a, SupportedPrim b) => PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
- binaryUnfoldOnce :: forall a b c. (Typeable a, Typeable b, SupportedPrim c) => PartialRuleBinary a b c -> TotalRuleBinary a b c -> TotalRuleBinary a b c
- pattern UnaryTermPatt :: forall a b tag. (Typeable tag, Typeable b) => tag -> Term b -> Term a
- pattern BinaryTermPatt :: forall a b c tag. (Typeable tag, Typeable b, Typeable c) => tag -> Term b -> Term c -> Term a
- 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
- type PartialFun a b = a -> Maybe b
- type PartialRuleUnary a b = PartialFun (Term a) (Term b)
- type TotalRuleUnary a b = Term a -> Term b
- type PartialRuleBinary a b c = Term a -> PartialFun (Term b) (Term c)
- type TotalRuleBinary a b c = Term a -> Term b -> Term c
- totalize :: PartialFun a b -> (a -> b) -> a -> b
- totalize2 :: (a -> PartialFun b c) -> (a -> b -> c) -> a -> b -> c
- class UnaryPartialStrategy tag a b | tag a -> b where
- extractor :: tag -> Term a -> Maybe a
- constantHandler :: tag -> a -> Maybe (Term b)
- nonConstantHandler :: tag -> Term a -> Maybe (Term b)
- unaryPartial :: forall tag a b. UnaryPartialStrategy tag a b => tag -> PartialRuleUnary a b
- class BinaryCommPartialStrategy tag a c | tag a -> c where
- singleConstantHandler :: tag -> a -> Term a -> Maybe (Term c)
- class BinaryPartialStrategy tag a b c | tag a b -> c where
- extractora :: tag -> Term a -> Maybe a
- extractorb :: tag -> Term b -> Maybe b
- allConstantHandler :: tag -> a -> b -> Maybe (Term c)
- leftConstantHandler :: tag -> a -> Term b -> Maybe (Term c)
- rightConstantHandler :: tag -> Term a -> b -> Maybe (Term c)
- nonBinaryConstantHandler :: tag -> Term a -> Term b -> Maybe (Term c)
- binaryPartial :: forall tag a b c. BinaryPartialStrategy tag a b c => tag -> PartialRuleBinary a b c
- pattern NumConTerm :: forall b a. (Num b, Typeable b) => b -> Term a
- pattern NumOrdConTerm :: forall b a. (Num b, Ord b, Typeable b) => b -> Term a
- pevalAddNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
- pevalMinusNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a -> Term a
- pevalUMinusNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a
- pevalAbsNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a
- pevalSignumNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a
- pevalTimesNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
- pevalLtNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
- pevalLeNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
- pevalGtNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
- pevalGeNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
- pevalTabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> Term b
- pevalGeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> Term b
- pevalDivIntegerTerm :: Term Integer -> Term Integer -> Term Integer
- pevalModIntegerTerm :: Term Integer -> Term Integer -> Term Integer
Documentation
Constructors
| FunArg |
Symbolic primitive type.
Symbolic Boolean, integer, and bit vector types are supported.
>>>:set -XOverloadedStrings>>>"a" :: Sym Boola>>>"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
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 #
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 #
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 #
Constructors
Instances
showUntyped :: TypedSymbol t -> String Source #
withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a Source #
data SomeTypedSymbol where Source #
Constructors
| SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol |
Instances
someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol Source #
evaluateTerm :: forall a. SupportedPrim a => Bool -> Model -> Term a -> Term a Source #
introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a 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
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
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 #
symTerm :: forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t Source #
sinfosymTerm :: (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> Term t Source #
iinfosymTerm :: (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> Term t Source #
extractSymbolicsTerm :: SupportedPrim a => Term a -> HashSet SomeTypedSymbol Source #
pattern BoolConTerm :: Bool -> Term a Source #
pevalEqvTerm :: forall a. SupportedPrim a => Term a -> Term a -> Term Bool Source #
pevalNotEqvTerm :: SupportedPrim a => Term a -> Term a -> Term Bool Source #
pevalITETerm :: forall a. SupportedPrim a => Term Bool -> Term a -> Term a -> Term a Source #
unaryUnfoldOnce :: forall a b. (Typeable a, SupportedPrim b) => PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b Source #
binaryUnfoldOnce :: forall a b c. (Typeable a, Typeable b, SupportedPrim c) => PartialRuleBinary a b c -> TotalRuleBinary a b c -> TotalRuleBinary a b c 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 PartialRuleUnary a b = PartialFun (Term a) (Term b) Source #
type TotalRuleUnary a b = Term a -> Term b Source #
type PartialRuleBinary a b c = Term a -> PartialFun (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 #
unaryPartial :: forall tag a b. UnaryPartialStrategy tag a b => tag -> PartialRuleUnary a b Source #
class BinaryCommPartialStrategy tag a c | tag a -> c where Source #
class BinaryPartialStrategy tag a b c | tag a b -> c where Source #
Minimal complete definition
extractora, extractorb, allConstantHandler, nonBinaryConstantHandler
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 #
pevalAddNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a Source #
pevalMinusNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a -> Term a Source #
pevalUMinusNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a Source #
pevalAbsNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a Source #
pevalSignumNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a Source #
pevalTimesNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a Source #
pevalLtNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool Source #
pevalLeNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool Source #
pevalGtNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool Source #
pevalGeNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool Source #
pevalTabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> Term b Source #
pevalGeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> Term b Source #