--
-- | 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,

  -- * Constant components handling #constants#

  createConstantVars,
  combineProgramVars,
  instructionGetValue
  )
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. 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) =>
    -- | 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 a (comp :: * -> *) (spec :: * -> *).
(Show 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 :: * -> *} {spec :: * -> *} {spec :: * -> *}
       {spec :: * -> *} {spec :: * -> *}.
(SynthComponent comp spec a, SynthComponent comp spec a,
 SynthComponent comp spec a, SynthComponent comp spec a,
 SynthComponent comp spec a) =>
[[a]] -> IO (Either SynthesisError (Program Location (comp a)))
go ([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 :: [[a]] -> IO (Either SynthesisError (Program Location (comp a)))
go [[a]]
s = do
      -- Finite synthesis part
      Either SynthesisError (Program Location (comp a), [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

        -- Not part of the original paper.
        -- Here we create existentially quantified variables for constant components.
        -- These variables represent actual value that the component returns.
        -- The returned 'Program' is filled with 'undefined' values for non-constant
        -- components.
        Program (SBV a) (comp a)
progConsts <- forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a] -> Symbolic (Program (SBV a) (comp a))
createConstantVars [comp a]
library

        -- 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)
progVars0 <- 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

          -- Not part of the original paper.
          -- Combine variables of constant components with variable of non-constant ones.
          -- The resulting program will not contain 'undefined' values anymore.
          let progVars :: Program (SBV a) (comp a)
progVars = 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)
combineProgramVars Program (SBV a) (comp a)
progConsts Program (SBV a) (comp a)
progVars0

          -- 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 -> do
              -- We could've just call 'bimapM getValue pure' to get all solutions
              -- at once, but in presence of constant components we have to do
              -- a bit more manual work.
              [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)
              -- Carefully extract solutions for component location vars.
              -- The 'instructionGetValue' function selectively calls 'getValue'
              -- either on left-hand 'Program' or right-hand 'Program' depending
              -- on component's constness.
              [Instruction Location (comp a)]
componentLocVals <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM forall a (comp :: * -> *) (spec :: * -> *) m.
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
Instruction (SBV Location) (comp a)
-> Instruction (SBV a) (comp a)
-> Query (Instruction Location (comp a))
instructionGetValue (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV Location) (comp a)
progLocs) (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV a) (comp a)
progConsts)
              [a]
constantVals <- 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 b c a. (b -> c) -> (a -> b) -> a -> c
. 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) (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a (comp :: * -> *) (spec :: * -> *).
(SynthSpec spec a, SynthComponent comp spec a) =>
comp a -> Bool
isConstantComponent forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l a. Instruction l a -> a
instructionComponent) (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV a) (comp a)
progConsts))

              let currL :: Program Location (comp a)
currL = forall l a. IOs l -> [Instruction l a] -> Program l a
Program (forall l. [l] -> l -> IOs l
IOs [Location]
inputLocVals Location
outputLocVal) [Instruction Location (comp a)]
componentLocVals
              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, [a]
constantVals)
            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), [a])
r forall a b. (a -> b) -> a -> b
$ \(Program Location (comp a)
currL, [a]
constantVals) -> 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))

        -- For constant components we also pin their return values.
        Program (SBV a) (comp a)
progConsts <- forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a] -> Symbolic (Program (SBV a) (comp a))
createConstantVars [comp a]
library
        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain 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) (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a (comp :: * -> *) (spec :: * -> *).
(SynthSpec spec a, SynthComponent comp spec a) =>
comp a -> Bool
isConstantComponent forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l a. Instruction l a -> a
instructionComponent) (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV a) (comp a)
progConsts))
          forall a. EqSymbolic a => a -> a -> SBool
.==
          forall a b. (a -> b) -> [a] -> [b]
map forall a. SymVal a => a -> SBV a
literal [a]
constantVals

        -- We want to find at least one set of inputs that doesn't work for our
        -- current design, hence existential quantification.
        Program (SBV a) (comp a)
progVars0 <- 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 progVars :: Program (SBV a) (comp a)
progVars = 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)
combineProgramVars Program (SBV a) (comp a)
progConsts Program (SBV a) (comp a)
progVars0

        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
            -- We were unable to find any counterexamples, which means that
            -- our design works for all inputs. Return it.
            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
            -- We found a set of input assignments that makes our design return
            -- wrong values. Add this set to 's' and go to the next iteration.
            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
              forall a. IO a -> Query a
io forall a b. (a -> b) -> a -> b
$ [[a]] -> IO (Either SynthesisError (Program Location (comp a)))
go 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

    -- Not part of the original paper. See comments for the similar call in 'refinedExAllProcedure'.
    Program (SBV a) (comp a)
progConsts <- forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a] -> Symbolic (Program (SBV a) (comp a))
createConstantVars [comp a]
library
    Program (SBV a) (comp a)
progVars0 <- 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 progVars :: Program (SBV a) (comp a)
progVars = 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)
combineProgramVars Program (SBV a) (comp a)
progConsts Program (SBV a) (comp a)
progVars0

    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)
          -- Careful solution extraction. See comments for the similar call in 'refinedExAllProcedure'.
          [Instruction Location (comp a)]
componentLocVals <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM forall a (comp :: * -> *) (spec :: * -> *) m.
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
Instruction (SBV Location) (comp a)
-> Instruction (SBV a) (comp a)
-> Query (Instruction Location (comp a))
instructionGetValue (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV Location) (comp a)
progLocs) (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV a) (comp a)
progConsts)
          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) [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


-- | Special version of 'createProgramVarsWith' for constant components.
-- A constant component is a component having 'specArity' \(=0\). 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 'Program' returned from this function contains
-- 'undefined' values for 'programIOs' and non-constant 'programInstructions'.
-- The user is expected to call 'createProgramVarsWith' later and then use
-- 'combineProgramVars' to merge two results.
createConstantVars :: forall a comp spec . (SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
  -- | Component library.
     [comp a]
  -> Symbolic (Program (SBV a) (comp a))
createConstantVars :: forall a (comp :: * -> *) (spec :: * -> *).
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
[comp a] -> Symbolic (Program (SBV a) (comp a))
createConstantVars [comp a]
library = do
  [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
    if forall a (comp :: * -> *) (spec :: * -> *).
(SynthSpec spec a, SynthComponent comp spec a) =>
comp a -> Bool
isConstantComponent comp a
comp
      then do
         SBV a
compOutputVar <- forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists 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
compOutputVar) comp a
comp
      else 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 a. HasCallStack => a
undefined 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 a. HasCallStack => a
undefined [Instruction (SBV a) (comp a)]
componentVars


-- | Given a 'Program' of constant-only components and a 'Program' of non-constant
-- components, combine them into a single 'Program'.
combineProgramVars :: forall a comp spec . (SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
  -- | The result of 'createConstantVars'
     Program (SBV a) (comp a)
  -- | The result of 'createProgramVarsWith'
  -> Program (SBV a) (comp a)
  -> Program (SBV a) (comp 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)
combineProgramVars Program (SBV a) (comp a)
lhProgram Program (SBV a) (comp a)
rhProgram = forall l a. IOs l -> [Instruction l a] -> Program l a
Program (forall l a. Program l a -> IOs l
programIOs Program (SBV a) (comp a)
rhProgram) forall a b. (a -> b) -> a -> b
$
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {s :: * -> *} {a} {comp :: * -> *} {l}.
SynthComponent comp s a =>
Instruction l (comp a)
-> Instruction l (comp a) -> Instruction l (comp a)
selectInstruction (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV a) (comp a)
lhProgram) (forall l a. Program l a -> [Instruction l a]
programInstructions Program (SBV a) (comp a)
rhProgram)
  where
    selectInstruction :: Instruction l (comp a)
-> Instruction l (comp a) -> Instruction l (comp a)
selectInstruction Instruction l (comp a)
lhInst Instruction l (comp a)
rhInst =
      if forall (s :: * -> *) a. SynthSpec s a => s a -> Word
specArity (forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> spec a
compSpec forall a b. (a -> b) -> a -> b
$ forall l a. Instruction l a -> a
instructionComponent Instruction l (comp a)
lhInst) forall a. Eq a => a -> a -> Bool
== Word
0
        then Instruction l (comp a)
lhInst
        else Instruction l (comp a)
rhInst


-- | Smart version of 'getValue' for 'Instruction'.
-- 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))
instructionGetValue :: forall a (comp :: * -> *) (spec :: * -> *) m.
(SymVal a, SynthSpec spec a, SynthComponent comp spec a) =>
Instruction (SBV Location) (comp a)
-> Instruction (SBV a) (comp a)
-> Query (Instruction Location (comp a))
instructionGetValue Instruction (SBV Location) (comp a)
instLocs Instruction (SBV a) (comp a)
instVars = do
  IOs Location
locVals <- 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 l a. Instruction l a -> IOs l
instructionIOs Instruction (SBV Location) (comp a)
instLocs)
  comp a
comp <- let comp :: comp a
comp = forall l a. Instruction l a -> a
instructionComponent Instruction (SBV Location) (comp a)
instLocs
          in if forall a (comp :: * -> *) (spec :: * -> *).
(SynthSpec spec a, SynthComponent comp spec a) =>
comp a -> Bool
isConstantComponent comp a
comp
            then do
              a
constValue <- forall a. SymVal a => SBV a -> Query a
getValue forall a b. (a -> b) -> a -> b
$ forall l. IOs l -> l
_out forall a b. (a -> b) -> a -> b
$ forall l a. Instruction l a -> IOs l
instructionIOs Instruction (SBV a) (comp a)
instVars
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (comp :: * -> *) (spec :: * -> *) a.
SynthComponent comp spec a =>
comp a -> a -> comp a
putConstValue comp a
comp a
constValue
            else
              forall (m :: * -> *) a. Monad m => a -> m a
return 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 IOs Location
locVals comp a
comp