Data.SBV.Program.Types

Documentation

module Data.Biapplicative

module Data.Bifoldable

module Data.Bitraversable

type Location = Word64

Type used to represent a value from the set of location variables \(l_x \in L\).

type SLocation = SWord64

Symbolic Location.

class SynthSpec s a where

Class for a program or a component specification \(φ(\vec I, O)\). Type variable a stands for function's domain type.

Methods

specArity :: s a -> Word

Number of inputs the specification function takes.

specFunc

Arguments

:: s a

-> [SBV a]

Input variables. The list should be of specArity size.

-> SBV a

Output variable.

-> SBool

An equation that relates input variables to the output one. The equation is build up either using (.==) or in a "tabular" way using multiple (.=>) expressions. See definitions from the Data.SBV.Program.SimpleLibrary module for examples.

Instances

SynthSpec SimpleSpec a

Defined in Data.SBV.Program.Types

Methods

specArity :: SimpleSpec a -> Word

specFunc :: SimpleSpec a -> [SBV a] -> SBV a -> SBool

class SynthSpec spec a => SynthComponent comp spec a | comp -> spec where

A class for a library component.

Minimal complete definition

compSpec

Methods

compName :: comp a -> String

Component name (optional). Used for naming SBV variables and when rendering the resulting program.

compSpec :: comp a -> spec a

Component's specification.

extraLocConstrs :: comp a -> [[SLocation] -> SLocation -> SBool]

Optional constraints to set on location variables \(l_x \in L\).

Instances

SynthComponent SimpleComponent SimpleSpec a

Defined in Data.SBV.Program.Types

Methods

compName :: SimpleComponent a -> String

compSpec :: SimpleComponent a -> SimpleSpec a

extraLocConstrs :: SimpleComponent a -> [[SLocation] -> SLocation -> SBool]

data SimpleSpec a

A simplest specification datatype possible. Type variable a stands for function's domain type.

Constructors

SimpleSpec

Fields

• simpleArity :: Word
• simpleFunc :: [SBV a] -> SBV a -> SBool

Instances

SynthSpec SimpleSpec a

Defined in Data.SBV.Program.Types

Methods

specArity :: SimpleSpec a -> Word

specFunc :: SimpleSpec a -> [SBV a] -> SBV a -> SBool

SynthComponent SimpleComponent SimpleSpec a

Defined in Data.SBV.Program.Types

Methods

compName :: SimpleComponent a -> String

compSpec :: SimpleComponent a -> SimpleSpec a

extraLocConstrs :: SimpleComponent a -> [[SLocation] -> SLocation -> SBool]

data SimpleComponent a

A simplest library component datatype possible.

Constructors

SimpleComponent

Fields

• simpleName :: String
• simpleSpec :: SimpleSpec a

Instances

SynthComponent SimpleComponent SimpleSpec a

Defined in Data.SBV.Program.Types

Methods

compName :: SimpleComponent a -> String

compSpec :: SimpleComponent a -> SimpleSpec a

extraLocConstrs :: SimpleComponent a -> [[SLocation] -> SLocation -> SBool]

Show (SimpleComponent spec)

Defined in Data.SBV.Program.Types

Methods

showsPrec :: Int -> SimpleComponent spec -> ShowS

show :: SimpleComponent spec -> String

showList :: [SimpleComponent spec] -> ShowS

data SynthesisError

Possible failure reasons during synthesis operation.

Constructors

ErrorUnsat

ErrorUnknown String

ErrorZeroResultsRequested

ErrorSeedingFailed

Instances

Show SynthesisError

Defined in Data.SBV.Program.Types

Methods

showsPrec :: Int -> SynthesisError -> ShowS

show :: SynthesisError -> String

showList :: [SynthesisError] -> ShowS

data IOs l

A datatype holding inputs and output of something. Usual types for l are Location and SLocation.

Constructors

IOs

Fields

• _ins :: [l]
• _out :: l

Instances

Foldable IOs

Defined in Data.SBV.Program.Types

Methods

fold :: Monoid m => IOs m -> m

foldMap :: Monoid m => (a -> m) -> IOs a -> m

foldMap' :: Monoid m => (a -> m) -> IOs a -> m

foldr :: (a -> b -> b) -> b -> IOs a -> b

foldr' :: (a -> b -> b) -> b -> IOs a -> b

foldl :: (b -> a -> b) -> b -> IOs a -> b

foldl' :: (b -> a -> b) -> b -> IOs a -> b

foldr1 :: (a -> a -> a) -> IOs a -> a

foldl1 :: (a -> a -> a) -> IOs a -> a

toList :: IOs a -> [a]

null :: IOs a -> Bool

length :: IOs a -> Int

elem :: Eq a => a -> IOs a -> Bool

maximum :: Ord a => IOs a -> a

minimum :: Ord a => IOs a -> a

sum :: Num a => IOs a -> a

product :: Num a => IOs a -> a

Traversable IOs

Defined in Data.SBV.Program.Types

Methods

traverse :: Applicative f => (a -> f b) -> IOs a -> f (IOs b)

sequenceA :: Applicative f => IOs (f a) -> f (IOs a)

mapM :: Monad m => (a -> m b) -> IOs a -> m (IOs b)

sequence :: Monad m => IOs (m a) -> m (IOs a)

Functor IOs

Defined in Data.SBV.Program.Types

Methods

fmap :: (a -> b) -> IOs a -> IOs b

(<$) :: a -> IOs b -> IOs a

Show l => Show (IOs l)

Defined in Data.SBV.Program.Types

Methods

showsPrec :: Int -> IOs l -> ShowS

show :: IOs l -> String

showList :: [IOs l] -> ShowS

Eq l => Eq (IOs l)

Defined in Data.SBV.Program.Types

Methods

(==) :: IOs l -> IOs l -> Bool

(/=) :: IOs l -> IOs l -> Bool

Ord l => Ord (IOs l)

Defined in Data.SBV.Program.Types

Methods

compare :: IOs l -> IOs l -> Ordering

(<) :: IOs l -> IOs l -> Bool

(<=) :: IOs l -> IOs l -> Bool

(>) :: IOs l -> IOs l -> Bool

(>=) :: IOs l -> IOs l -> Bool

max :: IOs l -> IOs l -> IOs l

min :: IOs l -> IOs l -> IOs l

EqSymbolic l => EqSymbolic (IOs l)

Defined in Data.SBV.Program.Types

Methods

(.==) :: IOs l -> IOs l -> SBool

(./=) :: IOs l -> IOs l -> SBool

(.===) :: IOs l -> IOs l -> SBool

(./==) :: IOs l -> IOs l -> SBool

distinct :: [IOs l] -> SBool

distinctExcept :: [IOs l] -> [IOs l] -> SBool

allEqual :: [IOs l] -> SBool

sElem :: IOs l -> [IOs l] -> SBool

sNotElem :: IOs l -> [IOs l] -> SBool

data Instruction l a

A datatype that holds a SynthComponent with inputs and output locations.

Constructors

Instruction

Fields

• instructionIOs :: IOs l
• instructionComponent :: a

Instances

Bifoldable Instruction

Defined in Data.SBV.Program.Types

Methods

bifold :: Monoid m => Instruction m m -> m

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Instruction a b -> m

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Instruction a b -> c

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Instruction a b -> c

Bifunctor Instruction

Defined in Data.SBV.Program.Types

Methods

bimap :: (a -> b) -> (c -> d) -> Instruction a c -> Instruction b d

first :: (a -> b) -> Instruction a c -> Instruction b c

second :: (b -> c) -> Instruction a b -> Instruction a c

Bitraversable Instruction

Defined in Data.SBV.Program.Types

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Instruction a b -> f (Instruction c d)

(Show l, Show a) => Show (Instruction l a)

Defined in Data.SBV.Program.Types

Methods

showsPrec :: Int -> Instruction l a -> ShowS

show :: Instruction l a -> String

showList :: [Instruction l a] -> ShowS

(Eq l, Eq a) => Eq (Instruction l a)

Defined in Data.SBV.Program.Types

Methods

(==) :: Instruction l a -> Instruction l a -> Bool

(/=) :: Instruction l a -> Instruction l a -> Bool

(Ord l, Ord a) => Ord (Instruction l a)

Defined in Data.SBV.Program.Types

Methods

compare :: Instruction l a -> Instruction l a -> Ordering

(<) :: Instruction l a -> Instruction l a -> Bool

(<=) :: Instruction l a -> Instruction l a -> Bool

(>) :: Instruction l a -> Instruction l a -> Bool

(>=) :: Instruction l a -> Instruction l a -> Bool

max :: Instruction l a -> Instruction l a -> Instruction l a

min :: Instruction l a -> Instruction l a -> Instruction l a

data Program l a

A datatype that unites program instructions with IOs of the program itself.

Constructors

Program

Fields

• programIOs :: IOs l
• programInstructions :: [Instruction l a]

Instances

Bifoldable Program

Defined in Data.SBV.Program.Types

Methods

bifold :: Monoid m => Program m m -> m

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Program a b -> m

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Program a b -> c

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Program a b -> c

Bifunctor Program

Defined in Data.SBV.Program.Types

Methods

bimap :: (a -> b) -> (c -> d) -> Program a c -> Program b d

first :: (a -> b) -> Program a c -> Program b c

second :: (b -> c) -> Program a b -> Program a c

Bitraversable Program

Defined in Data.SBV.Program.Types

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Program a b -> f (Program c d)

(Show l, Show a) => Show (Program l a)

Defined in Data.SBV.Program.Types

Methods

showsPrec :: Int -> Program l a -> ShowS

show :: Program l a -> String

showList :: [Program l a] -> ShowS

(Eq l, Eq a) => Eq (Program l a)

Defined in Data.SBV.Program.Types

Methods

(==) :: Program l a -> Program l a -> Bool

(/=) :: Program l a -> Program l a -> Bool

(Ord l, Ord a) => Ord (Program l a)

Defined in Data.SBV.Program.Types

Methods

compare :: Program l a -> Program l a -> Ordering

(<) :: Program l a -> Program l a -> Bool

(<=) :: Program l a -> Program l a -> Bool

(>) :: Program l a -> Program l a -> Bool

(>=) :: Program l a -> Program l a -> Bool

max :: Program l a -> Program l a -> Program l a

min :: Program l a -> Program l a -> Program l a

toIOsList :: Program l a -> [l]

Extract all locations from the program as a list, including locations of instructions.

sortInstructions :: Ord l => Program l a -> Program l a

Sorts program's instructions by their output location.

data ProgramTree a

A Program converted into a tree-like structure.

Constructors

InstructionNode a [ProgramTree a]

InputLeaf Location

Instances

Foldable ProgramTree

Defined in Data.SBV.Program.Types

Methods

fold :: Monoid m => ProgramTree m -> m

foldMap :: Monoid m => (a -> m) -> ProgramTree a -> m

foldMap' :: Monoid m => (a -> m) -> ProgramTree a -> m

foldr :: (a -> b -> b) -> b -> ProgramTree a -> b

foldr' :: (a -> b -> b) -> b -> ProgramTree a -> b

foldl :: (b -> a -> b) -> b -> ProgramTree a -> b

foldl' :: (b -> a -> b) -> b -> ProgramTree a -> b

foldr1 :: (a -> a -> a) -> ProgramTree a -> a

foldl1 :: (a -> a -> a) -> ProgramTree a -> a

toList :: ProgramTree a -> [a]

null :: ProgramTree a -> Bool

length :: ProgramTree a -> Int

elem :: Eq a => a -> ProgramTree a -> Bool

maximum :: Ord a => ProgramTree a -> a

minimum :: Ord a => ProgramTree a -> a

sum :: Num a => ProgramTree a -> a

product :: Num a => ProgramTree a -> a

Functor ProgramTree

Defined in Data.SBV.Program.Types

Methods

fmap :: (a -> b) -> ProgramTree a -> ProgramTree b

(<$) :: a -> ProgramTree b -> ProgramTree a

Show a => Show (ProgramTree a)

Defined in Data.SBV.Program.Types

Methods

showsPrec :: Int -> ProgramTree a -> ShowS

show :: ProgramTree a -> String

showList :: [ProgramTree a] -> ShowS

Eq a => Eq (ProgramTree a)

Defined in Data.SBV.Program.Types

Methods

(==) :: ProgramTree a -> ProgramTree a -> Bool

(/=) :: ProgramTree a -> ProgramTree a -> Bool

Ord a => Ord (ProgramTree a)

Defined in Data.SBV.Program.Types

Methods

compare :: ProgramTree a -> ProgramTree a -> Ordering

(<) :: ProgramTree a -> ProgramTree a -> Bool

(<=) :: ProgramTree a -> ProgramTree a -> Bool

(>) :: ProgramTree a -> ProgramTree a -> Bool

(>=) :: ProgramTree a -> ProgramTree a -> Bool

max :: ProgramTree a -> ProgramTree a -> ProgramTree a

min :: ProgramTree a -> ProgramTree a -> ProgramTree a

buildProgramTree :: Program Location a -> ProgramTree a

Create a ProgramTree for a given Program by resolving its Locations. This function effectively performs dead code elimination.

buildForestResult :: Program Location a -> [ProgramTree a]

Create a ProgramTree for each unused output in the Program