-- 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.1.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]

-- | Method used to get the value of a constant component. It doesn't
--   require an implementation if you don't use constant components.
getConstValue :: SynthComponent comp spec a => comp a -> a

-- | Method used to by the synthesis procedure to set the value of a
--   constant component. It doesn't require an implementation if you don't
--   use constant components.
putConstValue :: SynthComponent comp spec a => comp a -> a -> comp a

-- | 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 -> a -> SimpleComponent a
[simpleName] :: SimpleComponent a -> String
[simpleSpec] :: SimpleComponent a -> SimpleSpec a
[simpleVal] :: SimpleComponent a -> a
mkSimpleComp :: String -> SimpleSpec a -> SimpleComponent 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
const :: SimpleComponent a
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
bNand :: 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))

-- | Returns <a>True</a> if the component is a <b>constant</b> one.
--   Constant components have zero inputs (their <a>specArity</a>
--   &lt;math&gt; ).
isConstantComponent :: forall a comp spec. (SynthSpec spec a, SynthComponent comp spec a) => comp a -> Bool

-- | 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 :: (Show a, 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. It also
--   doesn't support constant components. 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)

-- | Special version of <a>createProgramVarsWith</a> for constant
--   components. A constant component is a component having
--   <a>specArity</a> &lt;math&gt;. The original paper slightly touches
--   this topic in the last paragraph of section 7. This function always
--   uses existential quantification and only operates on constant
--   components. The <a>Program</a> returned from this function contains
--   <a>undefined</a> values for <a>programIOs</a> and non-constant
--   <a>programInstructions</a>. The user is expected to call
--   <a>createProgramVarsWith</a> later and then use
--   <a>combineProgramVars</a> to merge two results.
createConstantVars :: forall a comp spec. (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => [comp a] -> Symbolic (Program (SBV a) (comp a))

-- | Given a <a>Program</a> of constant-only components and a
--   <a>Program</a> of non-constant components, combine them into a single
--   <a>Program</a>.
combineProgramVars :: forall a comp spec. (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => Program (SBV a) (comp a) -> Program (SBV a) (comp a) -> Program (SBV a) (comp a)

-- | Smart version of <a>getValue</a> for <a>Instruction</a>. For each
--   component it gets solutions for location variable, effectively turning
--   'Instruction SLocation (comp a)' into 'Instruction Location (comp a)'.
--   For constant components it additionaly fills 'comp a' part of the
--   structure with its returning value.
instructionGetValue :: forall a comp spec m. (SymVal a, SynthSpec spec a, SynthComponent comp spec a) => Instruction SLocation (comp a) -> Instruction (SBV a) (comp a) -> Query (Instruction Location (comp a))
instance GHC.Show.Show a => GHC.Show.Show (Data.SBV.Program.STuple a)


-- | These examples can from GHCi by importing this module. To get a
--   human-readable pseudocode for the solution use
--   
--   <pre>
--   ghci&gt; Right res &lt;- someExample
--   ghci&gt; putStrLn $ writePseudocode res
--   </pre>
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)))

-- | Reimplement arbitrary boolean formula with only NAND components.
--   Example usage:
--   
--   <pre>
--   nandifyExample 2 (SimpleSpec 2 $ [i1, i2] o -&gt; o .== (i1 .&amp;&amp; i2))
--   </pre>
nandifyExample :: Int -> SimpleSpec Bool -> IO (Either SynthesisError (Program Location (SimpleComponent Bool)))