--
-- | This module implements an algorithm described in the
-- "Component-based Synthesis Applied to Bitvector Programs" paper.
--
-- https://www.microsoft.com/en-us/research/wp-content/uploads/2010/02/bv.pdf
--
-- 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 'SynthSpec' class.
-- The library is a list of 'SynthComponent' instances.
--
-- There are three entry points to this module: 'standardExAllProcedure', 'refinedExAllProcedure' and 'exAllProcedure'.
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RecordWildCards #-}

module Data.SBV.Program (
  -- * Definitions for specification and component classes and the resulting data type
  module Data.SBV.Program.Types,
  -- * Predefined components library
  module Data.SBV.Program.SimpleLibrary,
  -- * Various utility functions
  module Data.SBV.Program.Utils,

  -- * Package entry points #entry#

  standardExAllProcedure,
  refinedExAllProcedure,
  exAllProcedure,

  -- * Auxiliary functions that make up synthesis procedures #aux#

  createProgramLocs,
  constrainLocs,
  createProgramVarsWith,
  createVarsConstraints,
  )
where

import Control.Monad
import Control.Monad.IO.Class
import Data.Either
import Data.Foldable
import Data.List
import Data.Maybe
import Data.Ord (comparing)
import Data.Traversable (for)
import Data.SBV hiding (STuple)
import Data.SBV.Control

import Data.SBV.Program.SimpleLibrary
import Data.SBV.Program.Types
import Data.SBV.Program.Utils

import Text.Pretty.Simple (pPrint)


-- | Represents a failed run in 'standardExAllProcedure'. Corresponds to
-- __program variable__ \(S\) in the paper.
data STuple a = STuple {
    forall a. STuple a -> IOs a
s_ios :: IOs a,
    forall a. STuple a -> [IOs a]
s_comps :: [IOs a]
  }
  deriving Int -> STuple a -> ShowS
forall a. Show a => Int -> STuple a -> ShowS
forall a. Show a => [STuple a] -> ShowS
forall a. Show a => STuple a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [STuple a] -> ShowS
$cshowList :: forall a. Show a => [STuple a] -> ShowS
show :: STuple a -> String
$cshow :: forall a. Show a => STuple a -> String
showsPrec :: Int -> STuple a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> STuple a -> ShowS
Show


-- | An implementation of __StandardExAllSolver__ 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) =>
    -- | Component library
       [comp a]
    -- | Specification of program being synthesized
    -> spec a
    -> IO (Either SynthesisError (Program Location (comp a)))
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)))
standardExAllProcedure [comp a]
library spec a
spec = do
  -- generate a seed for S
  Maybe (IOs a)
mbRes <- forall a comp (spec :: * -> *).
(SymVal a, SynthSpec spec a) =>
spec a -> IO (Maybe (IOs a))
sampleSpec spec a
spec
  case Maybe (IOs a)
mbRes of
      Maybe (IOs a)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left SynthesisError
ErrorSeedingFailed
      Just IOs a
i0 -> do
        String -> IO ()
putStrLn String
"Seeding done, result:"
        forall a. Show a => a -> IO ()
print IOs a
i0
        forall {spec :: * -> *} {t} {spec :: * -> *} {spec :: * -> *}.
(SynthComponent comp spec a, Show t, Num t,
 SynthComponent comp spec a, SynthComponent comp spec a) =>
t
-> [STuple a]
-> IO (Either SynthesisError (Program Location (comp a)))
go Integer
1 [forall a. IOs a -> [IOs a] -> STuple a
STuple (IOs a
i0 :: IOs a) []]
  where
    n :: Word
n = forall i a. Num i => [a] -> i
genericLength [comp a]
library
    numInputs :: Word
numInputs = forall (s :: * -> *) a. SynthSpec s a => s a -> Word
specArity spec a
spec
    m :: Word
m = Word
n forall a. Num a => a -> a -> a
+ Word
numInputs
    go :: t
-> [STuple a]
-> IO (Either SynthesisError (Program Location (comp a)))
go t
step [STuple a]
s = do
      String -> IO ()
putStrLn String
"============="
      String -> IO ()
putStrLn String
"Synthesizing with s = "
      forall (m :: * -> *) a. (MonadIO m, Show a) => a -> m ()
pPrint [STuple a]
s
      -- Finite synthesis part
      Either SynthesisError (Program Location (comp a))
r <- forall a. Symbolic a -> IO a
runSMT forall a b. (a -> b) -> a -> b
$ do
        Program (SBV Location) (comp a)
progLocs <- forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a] -> Word -> Symbolic (Program (SBV Location) (comp a))
createProgramLocs [comp a]
library Word
numInputs

        forall (spec :: * -> *) a (comp :: * -> *).
(SynthSpec spec a, SynthComponent comp spec a) =>
Word -> Word -> Program (SBV Location) (comp a) -> Symbolic ()
constrainLocs Word
m Word
numInputs Program (SBV Location) (comp a)
progLocs

        -- Unlike 'exAllProcedure' we call 'createProgramVarsWith' here multiple times
        -- Since we aren't using forall quantifier, we have to create variables
        -- for each STuple item in s.
        [Program (SBV a) (comp a)]
manyProgVars <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [STuple a]
s forall a b. (a -> b) -> a -> b
$ \(STuple {[IOs a]
IOs a
s_comps :: [IOs a]
s_ios :: IOs a
s_comps :: forall a. STuple a -> [IOs a]
s_ios :: forall a. STuple a -> IOs a
..}) -> do
          let numInputs :: Word
numInputs = forall i a. Num i => [a] -> i
genericLength forall a b. (a -> b) -> a -> b
$ forall l. IOs l -> [l]
_ins IOs a
s_ios
          Program (SBV a) (comp a)
progVars <- 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))
createProgramVarsWith forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists [comp a]
library Word
numInputs

          -- pin input/output variables (members of I and O sets) to values from S
          forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. SymVal a => a -> SBV a
literal IOs a
s_ios forall a. EqSymbolic a => a -> a -> SBool
.== forall l a. Program l a -> IOs l
programIOs Program (SBV a) (comp a)
progVars
          -- on the first run we don't have values for component locations (members of T set in the paper)
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IOs a]
s_comps) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. SymVal a => a -> SBV a
literal) [IOs a]
s_comps forall a. EqSymbolic a => a -> a -> SBool
.== forall a b. (a -> b) -> [a] -> [b]
map forall l a. Instruction l a -> IOs l
instructionIOs (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV a) (comp a)
progVars)

          forall (m :: * -> *) a. Monad m => a -> m a
return Program (SBV a) (comp a)
progVars

        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Program (SBV a) (comp a)]
manyProgVars forall a b. (a -> b) -> a -> b
$ \Program (SBV a) (comp a)
progVars -> do
          let (IOs [SBV a]
inputVars SBV a
outputVar) = forall l a. Program l a -> IOs l
programIOs Program (SBV a) (comp a)
progVars
              (SBool
psi_conn, SBool
phi_lib) = forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
Program (SBV Location) (comp a)
-> Program (SBV a) (comp a) -> (SBool, SBool)
createVarsConstraints Program (SBV Location) (comp a)
progLocs Program (SBV a) (comp a)
progVars
          forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (SBool
phi_lib SBool -> SBool -> SBool
.&& SBool
psi_conn) SBool -> SBool -> SBool
.=> forall (s :: * -> *) a.
SynthSpec s a =>
s a -> [SBV a] -> SBV a -> SBool
specFunc spec a
spec [SBV a]
inputVars SBV a
outputVar

        forall a. Query a -> Symbolic a
query forall a b. (a -> b) -> a -> b
$ do
          CheckSatResult
r <- Query CheckSatResult
checkSat
          case CheckSatResult
r of
            CheckSatResult
Sat -> do
              IOs Location
solution <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. SymVal a => SBV a -> Query a
getValue (forall l a. Program l a -> IOs l
programIOs Program (SBV Location) (comp a)
progLocs)
              [Instruction Location (comp a)]
componentLocVals <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM forall a. SymVal a => SBV a -> Query a
getValue forall (f :: * -> *) a. Applicative f => a -> f a
pure) (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV Location) (comp a)
progLocs)
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (forall l a. IOs l -> [Instruction l a] -> Program l a
Program IOs Location
solution [Instruction Location (comp a)]
componentLocVals)
            CheckSatResult
Unsat -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left SynthesisError
ErrorUnsat
            CheckSatResult
Unk -> forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> SynthesisError
ErrorUnknown forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Query SMTReasonUnknown
getUnknownReason
      -- Verification part
      -- At this stage the 'currL' program represents a solution that is known to
      -- work for all values from S. We now check if this solution works for all
      -- values possible.
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for Either SynthesisError (Program Location (comp a))
r forall a b. (a -> b) -> a -> b
$ \Program Location (comp a)
currL -> forall a. Symbolic a -> IO a
runSMT forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
          String -> IO ()
putStrLn String
"Synthesis step done, current solution:"
          String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
Program Location (comp a) -> String
writePseudocode Program Location (comp a)
currL

        Program (SBV Location) (comp a)
progLocs <- forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a] -> Word -> Symbolic (Program (SBV Location) (comp a))
createProgramLocs [comp a]
library Word
numInputs

        -- In the verification part we pin location variables L
        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (forall a. SymVal a => a -> SBV a
literal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall l a. Program l a -> IOs l
programIOs Program Location (comp a)
currL) forall a. EqSymbolic a => a -> a -> SBool
.== forall l a. Program l a -> IOs l
programIOs Program (SBV Location) (comp a)
progLocs
        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
sAnd forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Location
x SBV Location
y -> forall a. SymVal a => a -> SBV a
literal Location
x forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
y) (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall b c a. (b -> c) -> (a -> b) -> a -> c
.forall l a. Instruction l a -> IOs l
instructionIOs) (forall l a. Program l a -> [Instruction l a]
programInstructions Program Location (comp a)
currL)) (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall b c a. (b -> c) -> (a -> b) -> a -> c
.forall l a. Instruction l a -> IOs l
instructionIOs) (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV Location) (comp a)
progLocs))

        Program (SBV a) (comp a)
progVars <- 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))
createProgramVarsWith forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists [comp a]
library Word
numInputs

        let Program (IOs [SBV a]
inputVars SBV a
outputVar) [Instruction (SBV a) (comp a)]
componentVars = Program (SBV a) (comp a)
progVars
            (SBool
psi_conn, SBool
phi_lib) = forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
Program (SBV Location) (comp a)
-> Program (SBV a) (comp a) -> (SBool, SBool)
createVarsConstraints Program (SBV Location) (comp a)
progLocs Program (SBV a) (comp a)
progVars

        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot forall a b. (a -> b) -> a -> b
$ (SBool
phi_lib SBool -> SBool -> SBool
.&& SBool
psi_conn) SBool -> SBool -> SBool
.=> forall (s :: * -> *) a.
SynthSpec s a =>
s a -> [SBV a] -> SBV a -> SBool
specFunc spec a
spec [SBV a]
inputVars SBV a
outputVar

        forall a. Query a -> Symbolic a
query forall a b. (a -> b) -> a -> b
$ do
          CheckSatResult
r <- Query CheckSatResult
checkSat
          forall a. IO a -> Query a
io forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Verification step done"
          case CheckSatResult
r of
            CheckSatResult
Unsat -> do
              forall a. IO a -> Query a
io forall a b. (a -> b) -> a -> b
$ do
                String -> IO ()
putStrLn String
"============="
                String -> IO ()
putStrLn (String
"Solution found after " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
step forall a. [a] -> [a] -> [a]
++ String
" iterations")
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Program Location (comp a)
currL
            CheckSatResult
Sat -> do
              forall a. IO a -> Query a
io forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Solution does not work for all inputs"
              [a]
inputVals <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. SymVal a => SBV a -> Query a
getValue [SBV a]
inputVars
              a
outputVal <- forall a. SymVal a => SBV a -> Query a
getValue SBV a
outputVar
              [IOs a]
componentVals <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. SymVal a => SBV a -> Query a
getValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l a. Instruction l a -> IOs l
instructionIOs) [Instruction (SBV a) (comp a)]
componentVars
              forall a. IO a -> Query a
io forall a b. (a -> b) -> a -> b
$ t
-> [STuple a]
-> IO (Either SynthesisError (Program Location (comp a)))
go (t
step forall a. Num a => a -> a -> a
+ t
1) forall a b. (a -> b) -> a -> b
$ forall a. IOs a -> [IOs a] -> STuple a
STuple (forall l. [l] -> l -> IOs l
IOs [a]
inputVals a
outputVal) [IOs a]
componentVals forall a. a -> [a] -> [a]
: [STuple a]
s


-- | An implementation of __RefinedExAllSolver__ presented in section 6.2 of the paper.
-- This is an improved version of 'standardExAllProcedure'. It only keeps input
-- values \(|\vec I|\) in \(S\) and uses different synthesis constraints on __synthesis__
-- and __verification__ steps.
refinedExAllProcedure :: forall a comp spec .
  (SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
    -- | Component library
       [comp a]
    -- | Specification of program being synthesized
    -> spec a
    -> IO (Either SynthesisError (Program Location (comp a)))
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)))
refinedExAllProcedure [comp a]
library spec a
spec = do
  Maybe (IOs a)
mbRes <- forall a comp (spec :: * -> *).
(SymVal a, SynthSpec spec a) =>
spec a -> IO (Maybe (IOs a))
sampleSpec spec a
spec
  case Maybe (IOs a)
mbRes of
    Maybe (IOs a)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left SynthesisError
ErrorSeedingFailed
    Just IOs a
r -> forall {spec :: * -> *} {t} {spec :: * -> *} {spec :: * -> *}.
(SynthComponent comp spec a, Num t, SynthComponent comp spec a,
 SynthComponent comp spec a) =>
t
-> [[a]] -> IO (Either SynthesisError (Program Location (comp a)))
go Integer
1 ([forall l. IOs l -> [l]
_ins IOs a
r] :: [[a]])
  where
    n :: Word
n = forall i a. Num i => [a] -> i
genericLength [comp a]
library
    numInputs :: Word
numInputs = forall (s :: * -> *) a. SynthSpec s a => s a -> Word
specArity spec a
spec
    m :: Word
m = Word
n forall a. Num a => a -> a -> a
+ Word
numInputs
    go :: t
-> [[a]] -> IO (Either SynthesisError (Program Location (comp a)))
go t
step [[a]]
s = do
      -- Finite synthesis part
      Either SynthesisError (Program Location (comp a))
r <- forall a. Symbolic a -> IO a
runSMT forall a b. (a -> b) -> a -> b
$ do
        Program (SBV Location) (comp a)
progLocs <- forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a] -> Word -> Symbolic (Program (SBV Location) (comp a))
createProgramLocs [comp a]
library Word
numInputs

        forall (spec :: * -> *) a (comp :: * -> *).
(SynthSpec spec a, SynthComponent comp spec a) =>
Word -> Word -> Program (SBV Location) (comp a) -> Symbolic ()
constrainLocs Word
m Word
numInputs Program (SBV Location) (comp a)
progLocs

        -- Unlike 'exAllProcedure' here we call 'createProgramVarsWith' multiple times
        -- Since we aren't using forall quantifier, we have to create variables
        -- for each I vector in s.
        [Program (SBV a) (comp a)]
manyProgVars <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [[a]]
s forall a b. (a -> b) -> a -> b
$ \[a]
inputVars_s -> do
          let numInputs :: Word
numInputs = forall i a. Num i => [a] -> i
genericLength [a]
inputVars_s
          Program (SBV a) (comp a)
progVars <- 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))
createProgramVarsWith forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists [comp a]
library Word
numInputs

          -- pin input variables (members of I set) to values from S
          forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. SymVal a => a -> SBV a
literal [a]
inputVars_s forall a. EqSymbolic a => a -> a -> SBool
.== forall l. IOs l -> [l]
_ins (forall l a. Program l a -> IOs l
programIOs Program (SBV a) (comp a)
progVars)

          forall (m :: * -> *) a. Monad m => a -> m a
return Program (SBV a) (comp a)
progVars

        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Program (SBV a) (comp a)]
manyProgVars forall a b. (a -> b) -> a -> b
$ \Program (SBV a) (comp a)
progVars -> do
          let (IOs [SBV a]
inputVars SBV a
outputVar) = forall l a. Program l a -> IOs l
programIOs Program (SBV a) (comp a)
progVars
              (SBool
psi_conn, SBool
phi_lib) = forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
Program (SBV Location) (comp a)
-> Program (SBV a) (comp a) -> (SBool, SBool)
createVarsConstraints Program (SBV Location) (comp a)
progLocs Program (SBV a) (comp a)
progVars
          forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (SBool
phi_lib SBool -> SBool -> SBool
.&& SBool
psi_conn) SBool -> SBool -> SBool
.&& forall (s :: * -> *) a.
SynthSpec s a =>
s a -> [SBV a] -> SBV a -> SBool
specFunc spec a
spec [SBV a]
inputVars SBV a
outputVar

        forall a. Query a -> Symbolic a
query forall a b. (a -> b) -> a -> b
$ do
          CheckSatResult
r <- Query CheckSatResult
checkSat
          case CheckSatResult
r of
            CheckSatResult
Sat -> forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse forall a. SymVal a => SBV a -> Query a
getValue forall (f :: * -> *) a. Applicative f => a -> f a
pure Program (SBV Location) (comp a)
progLocs
            CheckSatResult
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left SynthesisError
ErrorUnsat
      -- Verification part
      -- At this stage the 'currL' program represents a solution that is known to
      -- work for all values from S. We now check if this solution works for all
      -- values possible.
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for Either SynthesisError (Program Location (comp a))
r forall a b. (a -> b) -> a -> b
$ \Program Location (comp a)
currL -> forall a. Symbolic a -> IO a
runSMT forall a b. (a -> b) -> a -> b
$ do
        Program (SBV Location) (comp a)
progLocs <- forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a] -> Word -> Symbolic (Program (SBV Location) (comp a))
createProgramLocs [comp a]
library Word
numInputs

        -- In the verification part we pin location variables L
        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (forall a. SymVal a => a -> SBV a
literal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall l a. Program l a -> IOs l
programIOs Program Location (comp a)
currL) forall a. EqSymbolic a => a -> a -> SBool
.== forall l a. Program l a -> IOs l
programIOs Program (SBV Location) (comp a)
progLocs
        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
sAnd forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Location
x SBV Location
y -> forall a. SymVal a => a -> SBV a
literal Location
x forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
y) (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall b c a. (b -> c) -> (a -> b) -> a -> c
.forall l a. Instruction l a -> IOs l
instructionIOs) (forall l a. Program l a -> [Instruction l a]
programInstructions Program Location (comp a)
currL)) (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall b c a. (b -> c) -> (a -> b) -> a -> c
.forall l a. Instruction l a -> IOs l
instructionIOs) (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV Location) (comp a)
progLocs))

        Program (SBV a) (comp a)
progVars <- 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))
createProgramVarsWith forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists [comp a]
library Word
numInputs

        let (Program (IOs [SBV a]
inputVars SBV a
outputVar) [Instruction (SBV a) (comp a)]
componentVars) = Program (SBV a) (comp a)
progVars
            (SBool
psi_conn, SBool
phi_lib) = forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
Program (SBV Location) (comp a)
-> Program (SBV a) (comp a) -> (SBool, SBool)
createVarsConstraints Program (SBV Location) (comp a)
progLocs Program (SBV a) (comp a)
progVars

        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (SBool
phi_lib SBool -> SBool -> SBool
.&& SBool
psi_conn) SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (forall (s :: * -> *) a.
SynthSpec s a =>
s a -> [SBV a] -> SBV a -> SBool
specFunc spec a
spec [SBV a]
inputVars SBV a
outputVar)

        forall a. Query a -> Symbolic a
query forall a b. (a -> b) -> a -> b
$ do
          CheckSatResult
r <- Query CheckSatResult
checkSat
          case CheckSatResult
r of
            CheckSatResult
Unsat -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Program Location (comp a)
currL
            CheckSatResult
Sat -> do
              [a]
inputVals <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. SymVal a => SBV a -> Query a
getValue [SBV a]
inputVars
              a
outputVal <- forall a. SymVal a => SBV a -> Query a
getValue SBV a
outputVar
              [IOs a]
componentVals <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. SymVal a => SBV a -> Query a
getValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l a. Instruction l a -> IOs l
instructionIOs) [Instruction (SBV a) (comp a)]
componentVars
              forall a. IO a -> Query a
io forall a b. (a -> b) -> a -> b
$ t
-> [[a]] -> IO (Either SynthesisError (Program Location (comp a)))
go (t
step forall a. Num a => a -> a -> a
+ t
1) forall a b. (a -> b) -> a -> b
$ [a]
inputVals forall a. a -> [a] -> [a]
: [[a]]
s

-- | This procedure is not part of the paper. It uses forall quantification directly
-- when creating variables from the \(T\) 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) =>
    -- | Component library
       [comp a]
    -- | Specification of program being synthesized
    -> spec a
    -> IO (Either SynthesisError (Program Location (comp a)))
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)))
exAllProcedure [comp a]
library spec a
spec =
  -- run SBV with 'allowQuantifiedQueries' to silence warnings about entering
  -- 'query' mode in presence of universally quantified variables
  forall a. SMTConfig -> Symbolic a -> IO a
runSMTWith (SMTConfig
defaultSMTCfg {allowQuantifiedQueries :: Bool
allowQuantifiedQueries = Bool
True}) forall a b. (a -> b) -> a -> b
$ do
    let n :: Word
n = forall i a. Num i => [a] -> i
genericLength [comp a]
library
        numInputs :: Word
numInputs = forall (s :: * -> *) a. SynthSpec s a => s a -> Word
specArity spec a
spec
        m :: Word
m = Word
n forall a. Num a => a -> a -> a
+ Word
numInputs

    Program (SBV Location) (comp a)
progLocs <- forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a] -> Word -> Symbolic (Program (SBV Location) (comp a))
createProgramLocs [comp a]
library Word
numInputs

    forall (spec :: * -> *) a (comp :: * -> *).
(SynthSpec spec a, SynthComponent comp spec a) =>
Word -> Word -> Program (SBV Location) (comp a) -> Symbolic ()
constrainLocs Word
m Word
numInputs Program (SBV Location) (comp a)
progLocs

    Program (SBV a) (comp a)
progVars <- 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))
createProgramVarsWith forall a. SymVal a => String -> Symbolic (SBV a)
sbvForall [comp a]
library Word
numInputs

    let (Program (IOs [SBV a]
inputVars SBV a
outputVar) [Instruction (SBV a) (comp a)]
_) = Program (SBV a) (comp a)
progVars
        (SBool
psi_conn, SBool
phi_lib) = forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
Program (SBV Location) (comp a)
-> Program (SBV a) (comp a) -> (SBool, SBool)
createVarsConstraints Program (SBV Location) (comp a)
progLocs Program (SBV a) (comp a)
progVars

    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (SBool
phi_lib SBool -> SBool -> SBool
.&& SBool
psi_conn) SBool -> SBool -> SBool
.=> forall (s :: * -> *) a.
SynthSpec s a =>
s a -> [SBV a] -> SBV a -> SBool
specFunc spec a
spec [SBV a]
inputVars SBV a
outputVar

    forall a. Query a -> Symbolic a
query forall a b. (a -> b) -> a -> b
$ do
      CheckSatResult
r <- Query CheckSatResult
checkSat
      case CheckSatResult
r of
        CheckSatResult
Sat -> do
          [Location]
inputLocVals <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. SymVal a => SBV a -> Query a
getValue (forall l. IOs l -> [l]
_ins forall a b. (a -> b) -> a -> b
$ forall l a. Program l a -> IOs l
programIOs Program (SBV Location) (comp a)
progLocs)
          Location
outputLocVal <- forall a. SymVal a => SBV a -> Query a
getValue (forall l. IOs l -> l
_out forall a b. (a -> b) -> a -> b
$ forall l a. Program l a -> IOs l
programIOs Program (SBV Location) (comp a)
progLocs)
          [Instruction Location (comp a)]
componentLocVals <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM forall a. SymVal a => SBV a -> Query a
getValue forall (f :: * -> *) a. Applicative f => a -> f a
pure) (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV Location) (comp a)
progLocs)
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall l a. IOs l -> [Instruction l a] -> Program l a
Program (forall l. [l] -> l -> IOs l
IOs [Location]
inputLocVals Location
outputLocVal) (forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (forall l. IOs l -> l
_out forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l a. Instruction l a -> IOs l
instructionIOs) [Instruction Location (comp a)]
componentLocVals)
        CheckSatResult
Unsat -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left SynthesisError
ErrorUnsat
        CheckSatResult
Unk -> do
          SMTReasonUnknown
reason <- Query SMTReasonUnknown
getUnknownReason
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String -> SynthesisError
ErrorUnknown forall a b. (a -> b) -> a -> b
$ String
"Unknown: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SMTReasonUnknown
reason


-- | First step of each synthesis procedure. Given a library of components and
-- a number of program's inputs, it creates existentially quantified
-- __location variables__ (members of set \(L\) 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))
createProgramLocs :: forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a] -> Word -> Symbolic (Program (SBV Location) (comp a))
createProgramLocs [comp a]
library Word
numInputs = do
  [SBV Location]
inputLocs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists forall a b. (a -> b) -> a -> b
$ forall i a. Integral i => i -> [a] -> [a]
genericTake Word
numInputs [String
"InputLoc" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
i | Integer
i <- [Integer
1..]] :: Symbolic [SLocation]
  SBV Location
outputLoc <- forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists String
"OutputLoc" :: Symbolic SLocation

  [Instruction (SBV Location) (comp a)]
componentsWithLocs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [comp a]
library forall a b. (a -> b) -> a -> b
$ \comp a
component -> do
    let n' :: Word
n' = forall (s :: * -> *) a. SynthSpec s a => s a -> Word
specArity forall a b. (a -> b) -> a -> b
$ forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> spec a
compSpec comp a
component
    [SBV Location]
compInputLocs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists forall a b. (a -> b) -> a -> b
$ forall i a. Integral i => i -> [a] -> [a]
genericTake Word
n' [String -> Word -> String
mkInputLocName (forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> String
compName comp a
component) Word
i | Word
i <- [Word
1..]]
    SBV Location
compOutputLoc <- forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists forall a b. (a -> b) -> a -> b
$ ShowS
mkOutputLocName forall a b. (a -> b) -> a -> b
$ forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> String
compName comp a
component
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall l a. IOs l -> a -> Instruction l a
Instruction (forall l. [l] -> l -> IOs l
IOs [SBV Location]
compInputLocs SBV Location
compOutputLoc) comp a
component :: Symbolic (Instruction SLocation (comp a))

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall l a. IOs l -> [Instruction l a] -> Program l a
Program (forall l. [l] -> l -> IOs l
IOs [SBV Location]
inputLocs SBV Location
outputLoc) [Instruction (SBV Location) (comp a)]
componentsWithLocs


-- | Second step of each synthesis procedure. It applies constraints on
-- __location variables__ from section 5 of the original paper. These constraints
-- include __well-formedness constraint__ \(ψ_{wfp}\), __acyclicity constraint__
-- \(ψ_{acyc}\) and __consistency constraint__ \(ψ_{cons}\). Constraints are not
-- returned from this function, but are applied immediately. Section 5 of the
-- paper also talks about __connectivity constraint__ \(ψ_{conn}\), which is
-- not created here.
constrainLocs :: (SynthSpec spec a, SynthComponent comp spec a) =>
  -- | The \(M\) constant from the paper, which equals to \(N + |\vec I|\), where
  -- __N__ is the size of the library.
     Word
  -- | Number of program inputs \(|\vec I|\).
  -> Word
  -> Program SLocation (comp a) -> Symbolic ()
constrainLocs :: forall (spec :: * -> *) a (comp :: * -> *).
(SynthSpec spec a, SynthComponent comp spec a) =>
Word -> Word -> Program (SBV Location) (comp a) -> Symbolic ()
constrainLocs Word
m Word
numInputs (Program {[Instruction (SBV Location) (comp a)]
IOs (SBV Location)
programInstructions :: [Instruction (SBV Location) (comp a)]
programIOs :: IOs (SBV Location)
programInstructions :: forall l a. Program l a -> [Instruction l a]
programIOs :: forall l a. Program l a -> IOs l
..}) = do
  -- program inputs are assigned locations from 0 to numInputs
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [Location
0..] (forall l. IOs l -> [l]
_ins IOs (SBV Location)
programIOs)) forall a b. (a -> b) -> a -> b
$ \(Location
i, SBV Location
inputLoc) -> do
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV Location
inputLoc forall a. EqSymbolic a => a -> a -> SBool
.== forall a. SymVal a => a -> SBV a
literal Location
i
  -- program output location should not be greater than the number of instructions
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall l. IOs l -> l
_out IOs (SBV Location)
programIOs forall a. OrdSymbolic a => a -> a -> SBool
.< forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
m

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Instruction (SBV Location) (comp a)]
programInstructions forall a b. (a -> b) -> a -> b
$ \(Instruction (IOs [SBV Location]
compInputLocs SBV Location
compOutputLoc) comp a
comp) -> do
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SBV Location]
compInputLocs forall a b. (a -> b) -> a -> b
$ \SBV Location
inputLoc -> do
      -- psi_wfp for component inputs
      forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV Location
inputLoc forall a. OrdSymbolic a => a -> a -> SBool
.>= forall a. SymVal a => a -> SBV a
literal Location
0
      forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV Location
inputLoc forall a. OrdSymbolic a => a -> a -> SBool
.<= forall a. SymVal a => a -> SBV a
literal (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Word
mforall a. Num a => a -> a -> a
-Word
1)
      -- psi_acyc
      forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV Location
inputLoc forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Location
compOutputLoc

    -- psi_wfp for component outputs
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV Location
compOutputLoc forall a. OrdSymbolic a => a -> a -> SBool
.>= forall a. SymVal a => a -> SBV a
literal (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
numInputs)
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV Location
compOutputLoc forall a. OrdSymbolic a => a -> a -> SBool
.<= forall a. SymVal a => a -> SBV a
literal (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ Word
mforall a. Num a => a -> a -> a
-Word
1)

    -- extra constraints supplied by user
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> [[SBV Location] -> SBV Location -> SBool]
extraLocConstrs comp a
comp) forall a b. (a -> b) -> a -> b
$ \[SBV Location] -> SBV Location -> SBool
extraConstr ->
      forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ [SBV Location] -> SBV Location -> SBool
extraConstr [SBV Location]
compInputLocs SBV Location
compOutputLoc

  -- psi_cons
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall a. EqSymbolic a => [a] -> SBool
distinct forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall l. IOs l -> l
_out forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l a. Instruction l a -> IOs l
instructionIOs) [Instruction (SBV Location) (comp a)]
programInstructions


-- | Third step of the synthesis process. It creates variables that represent
-- actual inputs/outputs values (members of the set \(T\) in the paper). This
-- function resembles 'createProgramLocs', but unlike it allows creating both existentially
-- and universally quantified variables. Standard and Refined procedures pass
-- 'sbvExists' to create existentially quantified variables, while 'exAllProcedure'
-- uses 'sbvForall'.
createProgramVarsWith :: forall a comp spec . (SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
  -- | Variable creation function. Either 'sbvExists' or 'sbvForall'.
     (String -> Symbolic (SBV a))
  -- | Component library.
  -> [comp a]
  -- | Number of program inputs \(|\vec I|\).
  -> Word
  -> Symbolic (Program (SBV a) (comp 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))
createProgramVarsWith String -> Symbolic (SBV a)
sbvMakeFunc [comp a]
library Word
numInputs = do
  [SBV a]
inputVars <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> Symbolic (SBV a)
sbvMakeFunc forall a b. (a -> b) -> a -> b
$ forall i a. Integral i => i -> [a] -> [a]
genericTake Word
numInputs [String
"Input" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
i | Integer
i <- [Integer
1..]]
  SBV a
outputVar <- String -> Symbolic (SBV a)
sbvMakeFunc String
"Output"

  [Instruction (SBV a) (comp a)]
componentVars <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [comp a]
library forall a b. (a -> b) -> a -> b
$ \comp a
comp -> do
    let n' :: Word
n' = forall (s :: * -> *) a. SynthSpec s a => s a -> Word
specArity forall a b. (a -> b) -> a -> b
$ forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> spec a
compSpec comp a
comp
    [SBV a]
compInputVars <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> Symbolic (SBV a)
sbvMakeFunc forall a b. (a -> b) -> a -> b
$ forall i a. Integral i => i -> [a] -> [a]
genericTake Word
n' [String -> Word -> String
mkInputVarName (forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> String
compName comp a
comp) Word
i | Word
i <- [Word
1..]]
    SBV a
compOutputVar <- String -> Symbolic (SBV a)
sbvMakeFunc forall a b. (a -> b) -> a -> b
$ ShowS
mkOutputVarName forall a b. (a -> b) -> a -> b
$ forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> String
compName comp a
comp
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall l a. IOs l -> a -> Instruction l a
Instruction (forall l. [l] -> l -> IOs l
IOs [SBV a]
compInputVars SBV a
compOutputVar) comp a
comp

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall l a. IOs l -> [Instruction l a] -> Program l a
Program (forall l. [l] -> l -> IOs l
IOs [SBV a]
inputVars SBV a
outputVar) [Instruction (SBV a) (comp a)]
componentVars


-- | Last building block of the synthesis process. This function creates
-- \(ψ_{conn}\) and \(φ_{lib}\) constraints and return them.
createVarsConstraints :: SynthComponent comp spec a => Program SLocation (comp a) -> Program (SBV a) (comp a) -> (SBool, SBool)
createVarsConstraints :: forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
Program (SBV Location) (comp a)
-> Program (SBV a) (comp a) -> (SBool, SBool)
createVarsConstraints Program (SBV Location) (comp a)
progLocs Program (SBV a) (comp a)
progVars = (SBool
psi_conn, SBool
phi_lib)
  where
    allVarsWithLocs :: [(SBV a, SBV Location)]
allVarsWithLocs = forall a b. [a] -> [b] -> [(a, b)]
zip (forall l a. Program l a -> [l]
toIOsList Program (SBV a) (comp a)
progVars) (forall l a. Program l a -> [l]
toIOsList Program (SBV Location) (comp a)
progLocs)
    psi_conn :: SBool
psi_conn = [SBool] -> SBool
sAnd [(SBV Location
xLoc forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
yLoc) SBool -> SBool -> SBool
.=> (SBV a
x forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
y) | (SBV a
x, SBV Location
xLoc) <- [(SBV a, SBV Location)]
allVarsWithLocs, (SBV a
y, SBV Location
yLoc) <- [(SBV a, SBV Location)]
allVarsWithLocs]
    phi_lib :: SBool
phi_lib = [SBool] -> SBool
sAnd forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> [a] -> [b]
map (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV a) (comp a)
progVars) forall a b. (a -> b) -> a -> b
$
        \(Instruction (IOs [SBV a]
inputVars SBV a
outputVar) comp a
comp) -> forall (s :: * -> *) a.
SynthSpec s a =>
s a -> [SBV a] -> SBV a -> SBool
specFunc (forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> spec a
compSpec comp a
comp) [SBV a]
inputVars SBV a
outputVar