-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Component-based program synthesis using SBV
--   
--   Given a library of available componen functions, synthesize a program
--   implementing a specification.
@package sbv-program
@version 1.0.0.0

module Data.SBV.Program.Types

-- | Type used to represent a value from the <b>set of location
--   variables</b> &lt;math&gt;.
type Location = Word64

-- | Symbolic <a>Location</a>.
type SLocation = SWord64

-- | Class for a program or a component <b>specification</b> &lt;math&gt;.
--   Type variable <tt>a</tt> stands for function's domain type.
class SynthSpec s a

-- | Number of inputs the specification function takes.
specArity :: SynthSpec s a => s a -> Word

-- | An equation that relates input variables to the output one. The
--   equation is build up either using <a>(.==)</a> or in a "tabular" way
--   using multiple <a>(.=&gt;)</a> expressions. See definitions from the
--   Data.SBV.Program.SimpleLibrary module for examples.
specFunc :: SynthSpec s a => s a -> [SBV a] -> SBV a -> SBool

-- | A class for a <b>library component</b>.
class SynthSpec spec a => SynthComponent comp spec a | comp -> spec

-- | Component name (optional). Used for naming SBV variables and when
--   rendering the resulting program.
compName :: SynthComponent comp spec a => comp a -> String

-- | Component's <b>specification</b>.
compSpec :: SynthComponent comp spec a => comp a -> spec a

-- | Optional constraints to set on <b>location variables</b> &lt;math&gt;.
extraLocConstrs :: SynthComponent comp spec a => comp a -> [[SLocation] -> SLocation -> SBool]

-- | A simplest <b>specification</b> datatype possible. Type variable
--   <tt>a</tt> stands for function's domain type.
data SimpleSpec a
SimpleSpec :: Word -> ([SBV a] -> SBV a -> SBool) -> SimpleSpec a
[simpleArity] :: SimpleSpec a -> Word
[simpleFunc] :: SimpleSpec a -> [SBV a] -> SBV a -> SBool

-- | A simplest <b>library component</b> datatype possible.
data SimpleComponent a
SimpleComponent :: String -> SimpleSpec a -> SimpleComponent a
[simpleName] :: SimpleComponent a -> String
[simpleSpec] :: SimpleComponent a -> SimpleSpec a

-- | Possible failure reasons during synthesis operation.
data SynthesisError
ErrorUnsat :: SynthesisError
ErrorUnknown :: String -> SynthesisError
ErrorZeroResultsRequested :: SynthesisError
ErrorSeedingFailed :: SynthesisError

-- | A datatype holding inputs and output of something. Usual types for
--   <tt>l</tt> are <a>Location</a> and <a>SLocation</a>.
data IOs l
IOs :: [l] -> l -> IOs l
[_ins] :: IOs l -> [l]
[_out] :: IOs l -> l

-- | A datatype that holds a <a>SynthComponent</a> with inputs and output
--   locations.
data Instruction l a
Instruction :: IOs l -> a -> Instruction l a
[instructionIOs] :: Instruction l a -> IOs l
[instructionComponent] :: Instruction l a -> a

-- | A datatype that unites program instructions with <a>IOs</a> of the
--   program itself.
data Program l a
Program :: IOs l -> [Instruction l a] -> Program l a
[programIOs] :: Program l a -> IOs l
[programInstructions] :: Program l a -> [Instruction l a]

-- | Extract all locations from the program as a list, including locations
--   of instructions.
toIOsList :: Program l a -> [l]

-- | Sorts program's instructions by their output location.
sortInstructions :: Ord l => Program l a -> Program l a

-- | A <a>Program</a> converted into a tree-like structure.
data ProgramTree a
InstructionNode :: a -> [ProgramTree a] -> ProgramTree a
InputLeaf :: Location -> ProgramTree a

-- | Create a <a>ProgramTree</a> for a given <a>Program</a> by resolving
--   its <a>Location</a>s. This function effectively performs dead code
--   elimination.
buildProgramTree :: Program Location a -> ProgramTree a

-- | Create a <a>ProgramTree</a> for each unused output in the
--   <a>Program</a>
buildForestResult :: Program Location a -> [ProgramTree a]
instance GHC.Show.Show Data.SBV.Program.Types.SynthesisError
instance GHC.Base.Functor Data.SBV.Program.Types.IOs
instance GHC.Classes.Ord l => GHC.Classes.Ord (Data.SBV.Program.Types.IOs l)
instance GHC.Classes.Eq l => GHC.Classes.Eq (Data.SBV.Program.Types.IOs l)
instance GHC.Show.Show l => GHC.Show.Show (Data.SBV.Program.Types.IOs l)
instance (GHC.Classes.Ord l, GHC.Classes.Ord a) => GHC.Classes.Ord (Data.SBV.Program.Types.Instruction l a)
instance (GHC.Classes.Eq l, GHC.Classes.Eq a) => GHC.Classes.Eq (Data.SBV.Program.Types.Instruction l a)
instance (GHC.Show.Show l, GHC.Show.Show a) => GHC.Show.Show (Data.SBV.Program.Types.Instruction l a)
instance (GHC.Classes.Ord l, GHC.Classes.Ord a) => GHC.Classes.Ord (Data.SBV.Program.Types.Program l a)
instance (GHC.Classes.Eq l, GHC.Classes.Eq a) => GHC.Classes.Eq (Data.SBV.Program.Types.Program l a)
instance (GHC.Show.Show l, GHC.Show.Show a) => GHC.Show.Show (Data.SBV.Program.Types.Program l a)
instance GHC.Base.Functor Data.SBV.Program.Types.ProgramTree
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.SBV.Program.Types.ProgramTree a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.SBV.Program.Types.ProgramTree a)
instance GHC.Show.Show a => GHC.Show.Show (Data.SBV.Program.Types.ProgramTree a)
instance Data.Foldable.Foldable Data.SBV.Program.Types.ProgramTree
instance Data.Bifunctor.Bifunctor Data.SBV.Program.Types.Program
instance Data.Bitraversable.Bitraversable Data.SBV.Program.Types.Program
instance Data.Bifoldable.Bifoldable Data.SBV.Program.Types.Program
instance Data.Bifunctor.Bifunctor Data.SBV.Program.Types.Instruction
instance Data.Bitraversable.Bitraversable Data.SBV.Program.Types.Instruction
instance Data.Bifoldable.Bifoldable Data.SBV.Program.Types.Instruction
instance Data.Foldable.Foldable Data.SBV.Program.Types.IOs
instance Data.Traversable.Traversable Data.SBV.Program.Types.IOs
instance Data.SBV.Core.Model.EqSymbolic l => Data.SBV.Core.Model.EqSymbolic (Data.SBV.Program.Types.IOs l)
instance Data.SBV.Program.Types.SynthComponent Data.SBV.Program.Types.SimpleComponent Data.SBV.Program.Types.SimpleSpec a
instance GHC.Show.Show (Data.SBV.Program.Types.SimpleComponent spec)
instance Data.SBV.Program.Types.SynthSpec Data.SBV.Program.Types.SimpleSpec a

module Data.SBV.Program.SimpleLibrary
inc :: (SymVal a, Ord a, Num a) => SimpleComponent a
dec :: (SymVal a, Ord a, Num a) => SimpleComponent a
add :: (SymVal a, Ord a, Num a) => SimpleComponent a
sub :: (SymVal a, Ord a, Num a) => SimpleComponent a
mul :: (SymVal a, Ord a, Num a) => SimpleComponent a
and :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a
or :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a
not :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a
bXor :: SimpleComponent Bool

-- | Logical equivalence implemented in "tabular" style
bEquiv :: SimpleComponent Bool

module Data.SBV.Program.Utils

-- | Given a <a>SynthSpec</a> tries to generate a set of input/output
--   values that satisfy the specification. Uses solver under the hood.
sampleSpec :: forall a comp spec. (SymVal a, SynthSpec spec a) => spec a -> IO (Maybe (IOs a))

-- | Creates sanitized variable name suitable for SBV.
mkVarName :: String -> Bool -> Bool -> Word -> String

-- | Shortcut for the more general <a>mkVarName</a> function.
mkInputLocName :: String -> Word -> String

-- | Shortcut for the more general <a>mkVarName</a> function.
mkOutputLocName :: String -> String

-- | Shortcut for the more general <a>mkVarName</a> function.
mkInputVarName :: String -> Word -> String

-- | Shortcut for the more general <a>mkVarName</a> function.
mkOutputVarName :: String -> String

-- | Renders the solution in SSA style.
writePseudocode :: SynthComponent comp spec a => Program Location (comp a) -> String


-- | This module implements an algorithm described in the "Component-based
--   Synthesis Applied to Bitvector Programs" paper.
--   
--   
--   <a>https://www.microsoft.com/en-us/research/wp-content/uploads/2010/02/bv.pdf</a>
--   
--   Given a program specification along with a library of available
--   components it synthesizes an actual program using an off-the-shelf
--   SMT-solver.
--   
--   The specification is an arbitrary datatype that is an instance of the
--   <a>SynthSpec</a> class. The library is a list of <a>SynthComponent</a>
--   instances.
--   
--   There are three entry points to this module:
--   <a>standardExAllProcedure</a>, <a>refinedExAllProcedure</a> and
--   <a>exAllProcedure</a>.
module Data.SBV.Program

-- | An implementation of <b>StandardExAllSolver</b> presented in section
--   6.1 of the paper. As stated in the paper, this implementation boils
--   down to exhaustive enumeration of possible solutions, and as such
--   isn't effective. It can be used to better understand how the synthesis
--   procedure works and provides a lot of debugging output. Do not use
--   this procedure for solving real problems.
standardExAllProcedure :: forall a comp spec. (SymVal a, Show a, SynthSpec spec a, SynthComponent comp spec a) => [comp a] -> spec a -> IO (Either SynthesisError (Program Location (comp a)))

-- | An implementation of <b>RefinedExAllSolver</b> presented in section
--   6.2 of the paper. This is an improved version of
--   <a>standardExAllProcedure</a>. It only keeps input values &lt;math&gt;
--   in &lt;math&gt; and uses different synthesis constraints on
--   <b>synthesis</b> and <b>verification</b> steps.
refinedExAllProcedure :: forall a comp spec. (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => [comp a] -> spec a -> IO (Either SynthesisError (Program Location (comp a)))

-- | This procedure is not part of the paper. It uses forall quantification
--   directly when creating variables from the &lt;math&gt; set. As
--   consequence it requires an SMT-solver than can handle foralls (for
--   instance, Z3). This procedure is the easiest to understand.
exAllProcedure :: forall a comp spec. (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => [comp a] -> spec a -> IO (Either SynthesisError (Program Location (comp a)))

-- | First step of each synthesis procedure. Given a library of components
--   and a number of program's inputs, it creates existentially quantified
--   <b>location variables</b> (members of set &lt;math&gt; in the paper)
--   for each component and for the program itself.
createProgramLocs :: forall a comp spec. (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => [comp a] -> Word -> Symbolic (Program SLocation (comp a))

-- | Second step of each synthesis procedure. It applies constraints on
--   <b>location variables</b> from section 5 of the original paper. These
--   constraints include <b>well-formedness constraint</b> &lt;math&gt;,
--   <b>acyclicity constraint</b> &lt;math&gt; and <b>consistency
--   constraint</b> &lt;math&gt;. Constraints are not returned from this
--   function, but are applied immediately. Section 5 of the paper also
--   talks about <b>connectivity constraint</b> &lt;math&gt;, which is not
--   created here.
constrainLocs :: (SynthSpec spec a, SynthComponent comp spec a) => Word -> Word -> Program SLocation (comp a) -> Symbolic ()

-- | Third step of the synthesis process. It creates variables that
--   represent actual inputs/outputs values (members of the set
--   &lt;math&gt; in the paper). This function resembles
--   <a>createProgramLocs</a>, but unlike it allows creating both
--   existentially and universally quantified variables. Standard and
--   Refined procedures pass <a>sbvExists</a> to create existentially
--   quantified variables, while <a>exAllProcedure</a> uses
--   <a>sbvForall</a>.
createProgramVarsWith :: forall a comp spec. (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => (String -> Symbolic (SBV a)) -> [comp a] -> Word -> Symbolic (Program (SBV a) (comp a))

-- | Last building block of the synthesis process. This function creates
--   &lt;math&gt; and &lt;math&gt; constraints and return them.
createVarsConstraints :: SynthComponent comp spec a => Program SLocation (comp a) -> Program (SBV a) (comp a) -> (SBool, SBool)
instance GHC.Show.Show a => GHC.Show.Show (Data.SBV.Program.STuple a)

module Data.SBV.Program.Examples

-- | A running example from the original paper. The function should reset
--   the least significant set bit of a 8-byte word: &gt;&gt;&gt; 0001 0010
--   -&gt; 0000 0010
paperRunningExampleSpec :: SimpleSpec Word8
paperRunningExample :: IO (Either SynthesisError (Program Location (SimpleComponent Word8)))

-- | Synthesizes a formula for the quadratic equation &lt;math&gt;
quadEquExampleSpec :: SimpleSpec Int32
quadEquExample :: IO (Either SynthesisError (Program Location (SimpleComponent Int32)))