Copyright	(c) Sirui Lu 2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	None
Language	Haskell2010

Grisette.Internal.Unified.Class.UnifiedSolvable

Description

Synopsis

class UnifiedSolvable (mode :: EvalModeTag) a con | a -> mode con, con mode -> a where
- withBaseSolvable :: (If (IsConMode mode) (a ~ con) (Solvable con a) => r) -> r
con :: forall (mode :: EvalModeTag) a con. (DecideEvalMode mode, UnifiedSolvable mode a con) => con -> a
pattern Con :: forall (mode :: EvalModeTag) a con. (DecideEvalMode mode, UnifiedSolvable mode a con) => con -> a
conView :: forall (mode :: EvalModeTag) a con. (DecideEvalMode mode, UnifiedSolvable mode a con) => a -> Maybe con

Documentation

class UnifiedSolvable (mode :: EvalModeTag) a con | a -> mode con, con mode -> a where Source #

A class that provides the ability to extract/wrap the concrete value from/into a symbolic value.

Methods

withBaseSolvable :: (If (IsConMode mode) (a ~ con) (Solvable con a) => r) -> r Source #

Instances

Instances details

UnifiedSolvable 'C AlgReal AlgReal Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'C) (AlgReal ~ AlgReal) (Solvable AlgReal AlgReal) => r) -> r Source #
UnifiedSolvable 'C Integer Integer Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'C) (Integer ~ Integer) (Solvable Integer Integer) => r) -> r Source #
UnifiedSolvable 'C Bool Bool Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'C) (Bool ~ Bool) (Solvable Bool Bool) => r) -> r Source #
UnifiedSolvable 'S SymAlgReal AlgReal Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'S) (SymAlgReal ~ AlgReal) (Solvable AlgReal SymAlgReal) => r) -> r Source #
UnifiedSolvable 'S SymBool Bool Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'S) (SymBool ~ Bool) (Solvable Bool SymBool) => r) -> r Source #
UnifiedSolvable 'S SymInteger Integer Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'S) (SymInteger ~ Integer) (Solvable Integer SymInteger) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedSolvable 'C (IntN n) (IntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'C) (IntN n ~ IntN n) (Solvable (IntN n) (IntN n)) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedSolvable 'C (WordN n) (WordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'C) (WordN n ~ WordN n) (Solvable (WordN n) (WordN n)) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedSolvable 'S (SymIntN n) (IntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'S) (SymIntN n ~ IntN n) (Solvable (IntN n) (SymIntN n)) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedSolvable 'S (SymWordN n) (WordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'S) (SymWordN n ~ WordN n) (Solvable (WordN n) (SymWordN n)) => r) -> r Source #
ValidFP eb sb => UnifiedSolvable 'C (FP eb sb) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'C) (FP eb sb ~ FP eb sb) (Solvable (FP eb sb) (FP eb sb)) => r) -> r Source #
ValidFP eb sb => UnifiedSolvable 'S (SymFP eb sb) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'S) (SymFP eb sb ~ FP eb sb) (Solvable (FP eb sb) (SymFP eb sb)) => r) -> r Source #

con :: forall (mode :: EvalModeTag) a con. (DecideEvalMode mode, UnifiedSolvable mode a con) => con -> a Source #

Wrap a concrete value in a symbolic value.

>>> con True :: Bool
True

>>> con True :: SymBool
true

pattern Con :: forall (mode :: EvalModeTag) a con. (DecideEvalMode mode, UnifiedSolvable mode a con) => con -> a Source #

A pattern synonym for extracting the concrete value from a symbolic value.

>>> case con True :: SymBool of Con v -> v
True

>>> case ssym "a" :: SymBool of Con v -> Just v; _ -> Nothing
Nothing

conView :: forall (mode :: EvalModeTag) a con. (DecideEvalMode mode, UnifiedSolvable mode a con) => a -> Maybe con Source #

Extract the concrete value from a symbolic value.

>>> conView (con True :: SymBool)
Just True

>>> conView (ssym "a" :: SymBool)
Nothing

>>> conView True
Just True