Language.Hasmtlib.Variable

This module provides the class Variable which lets you create symbolical values of a data-type.

A generic default implementation with GVariable is possible.

Example

data V3 a = V3 a a a deriving Generic
instance Codec a => Codec (V3 a)
instance Equatable a => Codec (V3 a)

problem :: MonadSMT s m => StateT s m (V3 (Expr RealSort))
problem = do
  let constantV3 = encode $ V3 7 69 42
  symbolicV3 <- variable @(V3 (Expr RealSort))
  assert $ symbolicV3 /== constantV3
  return symbolicV3

Class

class Variable a where

Construct a variable datum of a data-type by creating variables for all its fields.

You can derive an instance of this class if your type is Generic and has exactly one constructor.

Minimal complete definition

Nothing

Methods

variable :: MonadSMT s m => m a

default variable :: (MonadSMT s m, Generic a, GVariable (Rep a)) => m a

Instances

Variable ()

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m ()

Variable a => Variable (Identity a)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (Identity a)

Variable a => Variable (First a)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (First a)

Variable a => Variable (Last a)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (Last a)

Variable a => Variable (Dual a)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (Dual a)

Variable a => Variable (Product a)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (Product a)

Variable a => Variable (Sum a)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (Sum a)

KnownSMTSort t => Variable (Expr t)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (Expr t)

Variable a => Variable (Maybe a)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (Maybe a)

Variable b => Variable (Either a b)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (Either a b)

(Variable a, Variable b) => Variable (a, b)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (a, b)

Variable m => Variable (Const m a)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m0 => m0 (Const m a)

Variable (f a) => Variable (Alt f a)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (Alt f a)

(Variable a, Variable b, Variable c) => Variable (a, b, c)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (a, b, c)

(Variable a, Variable b, Variable c, Variable d) => Variable (a, b, c, d)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (a, b, c, d)

Variable (f (g a)) => Variable (Compose f g a)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (Compose f g a)

(Variable a, Variable b, Variable c, Variable d, Variable e) => Variable (a, b, c, d, e)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (a, b, c, d, e)

(Variable a, Variable b, Variable c, Variable d, Variable e, Variable f) => Variable (a, b, c, d, e, f)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (a, b, c, d, e, f)

(Variable a, Variable b, Variable c, Variable d, Variable e, Variable f, Variable g) => Variable (a, b, c, d, e, f, g)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (a, b, c, d, e, f, g)

(Variable a, Variable b, Variable c, Variable d, Variable e, Variable f, Variable g, Variable h) => Variable (a, b, c, d, e, f, g, h)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (a, b, c, d, e, f, g, h)

Other functions

variable' :: forall s m a. (MonadSMT s m, Variable a) => Proxy a -> m a

Wrapper for variable which takes a Proxy

Generics

class GVariable f where

Methods

gvariable :: MonadSMT s m => m (f a)

Instances

GVariable (U1 :: k -> Type)

Defined in Language.Hasmtlib.Variable

Methods

gvariable :: forall s m (a :: k0). MonadSMT s m => m (U1 a)

(GVariable f, GVariable g) => GVariable (f :*: g :: k -> Type)

Defined in Language.Hasmtlib.Variable

Methods

gvariable :: forall s m (a :: k0). MonadSMT s m => m ((f :*: g) a)

Variable a => GVariable (K1 i a :: k -> Type)

Defined in Language.Hasmtlib.Variable

Methods

gvariable :: forall s m (a0 :: k0). MonadSMT s m => m (K1 i a a0)

GVariable f => GVariable (M1 i c f :: k -> Type)

Defined in Language.Hasmtlib.Variable

Methods

gvariable :: forall s m (a :: k0). MonadSMT s m => m (M1 i c f a)