diff --git a/sbv-program.cabal b/sbv-program.cabal --- a/sbv-program.cabal +++ b/sbv-program.cabal @@ -1,7 +1,7 @@ cabal-version: >= 1.10 name: sbv-program -version: 1.0.0.0 +version: 1.1.0.0 category: SMT, Symbolic Computation, Bit vectors, Formal Methods synopsis: Component-based program synthesis using SBV description: Given a library of available componen functions, synthesize a program implementing a specification. @@ -31,10 +31,10 @@ src build-depends: base < 5 - , bifunctors - , containers - , pretty-simple - , sbv + , bifunctors >= 5.5.13 && < 5.6 + , containers >= 0.6.5 && < 0.7 + , pretty-simple >= 4.1.2 && < 4.2 + , sbv >= 9.0 && < 9.1 default-extensions: RecordWildCards default-language: Haskell2010 diff --git a/src/Data/SBV/Program.hs b/src/Data/SBV/Program.hs --- a/src/Data/SBV/Program.hs +++ b/src/Data/SBV/Program.hs @@ -35,6 +35,12 @@ constrainLocs, createProgramVarsWith, createVarsConstraints, + + -- * Constant components handling #constants# + + createConstantVars, + combineProgramVars, + instructionGetValue ) where @@ -69,7 +75,8 @@ -- 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. +-- 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 @@ -183,25 +190,37 @@ mbRes <- sampleSpec spec case mbRes of Nothing -> return $ Left ErrorSeedingFailed - Just r -> go 1 ([_ins r] :: [[a]]) + Just r -> go ([_ins r] :: [[a]]) where n = genericLength library numInputs = specArity spec m = n + numInputs - go step s = do + go s = do -- Finite synthesis part r <- runSMT $ do progLocs <- createProgramLocs library numInputs constrainLocs m numInputs progLocs - -- Unlike 'exAllProcedure' here we call 'createProgramVarsWith' multiple times + -- 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. + progConsts <- createConstantVars 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. manyProgVars <- forM s $ \inputVars_s -> do let numInputs = genericLength inputVars_s - progVars <- createProgramVarsWith sbvExists library numInputs + progVars0 <- createProgramVarsWith sbvExists library 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 = combineProgramVars progConsts progVars0 + -- pin input variables (members of I set) to values from S constrain $ fmap literal inputVars_s .== _ins (programIOs progVars) @@ -215,21 +234,45 @@ query $ do r <- checkSat case r of - Sat -> Right <$> bitraverse getValue pure progLocs + 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. + inputLocVals <- mapM getValue (_ins $ programIOs progLocs) + outputLocVal <- getValue (_out $ programIOs 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. + componentLocVals <- zipWithM instructionGetValue (programInstructions progLocs) (programInstructions progConsts) + constantVals <- mapM (getValue . _out . instructionIOs) (filter (isConstantComponent . instructionComponent) (programInstructions progConsts)) + + let currL = Program (IOs inputLocVals outputLocVal) componentLocVals + return $ Right (currL, constantVals) _ -> return $ Left 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. - fmap join $ for r $ \currL -> runSMT $ do + fmap join $ for r $ \(currL, constantVals) -> runSMT $ do progLocs <- createProgramLocs library numInputs -- In the verification part we pin location variables L constrain $ (literal <$> programIOs currL) .== programIOs progLocs constrain $ sAnd $ zipWith (\x y -> literal x .== y) (concatMap (toList .instructionIOs) (programInstructions currL)) (concatMap (toList .instructionIOs) (programInstructions progLocs)) - progVars <- createProgramVarsWith sbvExists library numInputs + -- For constant components we also pin their return values. + progConsts <- createConstantVars library + constrain $ + map (_out . instructionIOs) (filter (isConstantComponent . instructionComponent) (programInstructions progConsts)) + .== + map literal constantVals + -- We want to find at least one set of inputs that doesn't work for our + -- current design, hence existential quantification. + progVars0 <- createProgramVarsWith sbvExists library numInputs + let progVars = combineProgramVars progConsts progVars0 + let (Program (IOs inputVars outputVar) componentVars) = progVars (psi_conn, phi_lib) = createVarsConstraints progLocs progVars @@ -238,12 +281,14 @@ query $ do r <- checkSat case r of + -- We were unable to find any counterexamples, which means that + -- our design works for all inputs. Return it. Unsat -> return $ Right 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. Sat -> do inputVals <- mapM getValue inputVars - outputVal <- getValue outputVar - componentVals <- mapM (traverse getValue . instructionIOs) componentVars - io $ go (step + 1) $ inputVals : s + io $ go $ inputVals : 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 @@ -268,7 +313,10 @@ constrainLocs m numInputs progLocs - progVars <- createProgramVarsWith sbvForall library numInputs + -- Not part of the original paper. See comments for the similar call in 'refinedExAllProcedure'. + progConsts <- createConstantVars library + progVars0 <- createProgramVarsWith sbvForall library numInputs + let progVars = combineProgramVars progConsts progVars0 let (Program (IOs inputVars outputVar) _) = progVars (psi_conn, phi_lib) = createVarsConstraints progLocs progVars @@ -281,8 +329,9 @@ Sat -> do inputLocVals <- mapM getValue (_ins $ programIOs progLocs) outputLocVal <- getValue (_out $ programIOs progLocs) - componentLocVals <- traverse (bimapM getValue pure) (programInstructions progLocs) - return $ Right $ Program (IOs inputLocVals outputLocVal) (sortOn (_out . instructionIOs) componentLocVals) + -- Careful solution extraction. See comments for the similar call in 'refinedExAllProcedure'. + componentLocVals <- zipWithM instructionGetValue (programInstructions progLocs) (programInstructions progConsts) + return $ Right $ Program (IOs inputLocVals outputLocVal) componentLocVals Unsat -> return $ Left ErrorUnsat Unk -> do reason <- getUnknownReason @@ -385,3 +434,63 @@ phi_lib = sAnd $ flip map (programInstructions progVars) $ \(Instruction (IOs inputVars outputVar) comp) -> specFunc (compSpec comp) inputVars 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 library = do + componentVars <- forM library $ \comp -> do + if isConstantComponent comp + then do + compOutputVar <- sbvExists $ mkOutputVarName $ compName comp + return $ Instruction (IOs [] compOutputVar) comp + else return $ Instruction undefined comp + + return $ Program undefined 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 lhProgram rhProgram = Program (programIOs rhProgram) $ + zipWith selectInstruction (programInstructions lhProgram) (programInstructions rhProgram) + where + selectInstruction lhInst rhInst = + if specArity (compSpec $ instructionComponent lhInst) == 0 + then lhInst + else 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 instLocs instVars = do + locVals <- traverse getValue (instructionIOs instLocs) + comp <- let comp = instructionComponent instLocs + in if isConstantComponent comp + then do + constValue <- getValue $ _out $ instructionIOs instVars + return $ putConstValue comp constValue + else + return comp + return $ Instruction locVals comp diff --git a/src/Data/SBV/Program/Examples.hs b/src/Data/SBV/Program/Examples.hs --- a/src/Data/SBV/Program/Examples.hs +++ b/src/Data/SBV/Program/Examples.hs @@ -1,10 +1,20 @@ +-- +-- | These examples can from GHCi by importing this module. +-- To get a human-readable pseudocode for the solution use +-- +-- @ +-- ghci> Right res <- someExample +-- ghci> putStrLn $ writePseudocode res +-- @ module Data.SBV.Program.Examples( -- * Reset most significant set bit paperRunningExampleSpec, paperRunningExample, -- * Quadratic equation quadEquExampleSpec, - quadEquExample + quadEquExample, + -- * Transform boolean formula into NAND-only expression + nandifyExample ) where import Data.List @@ -24,7 +34,7 @@ paperRunningExample = refinedExAllProcedure [Lib.and, Lib.dec] paperRunningExampleSpec --- | Synthesizes a formula for the quadratic equation \(x^2 - 2*x + 1 = 0\) +-- | Synthesizes a formula for the quadratic equation \(x^2 - 2x + 1 = 0\) quadEquExampleSpec :: SimpleSpec Int32 quadEquExampleSpec = SimpleSpec 1 $ \[i] o -> sAnd [ i .== 1 .=> o .== 0, @@ -32,3 +42,17 @@ ] quadEquExample = refinedExAllProcedure [Lib.mul, Lib.add, Lib.sub, Lib.inc] quadEquExampleSpec + +-- | Reimplement arbitrary boolean formula with only NAND components. +-- Example usage: +-- +-- @ +-- nandifyExample 2 (SimpleSpec 2 $ \[i1, i2] o -> o .== (i1 .&& i2)) +-- @ +nandifyExample :: + Int -- ^ Amount of NAND components available + -> SimpleSpec Bool -- ^ Specification of the desired function + -> IO (Either SynthesisError (Program Location (SimpleComponent Bool))) +nandifyExample size = refinedExAllProcedure library + where + library = [Lib.const, Lib.const] ++ replicate size Lib.bNand diff --git a/src/Data/SBV/Program/SimpleLibrary.hs b/src/Data/SBV/Program/SimpleLibrary.hs --- a/src/Data/SBV/Program/SimpleLibrary.hs +++ b/src/Data/SBV/Program/SimpleLibrary.hs @@ -1,4 +1,6 @@ module Data.SBV.Program.SimpleLibrary( + Data.SBV.Program.SimpleLibrary.const, + -- * Arithmetic components inc, dec, @@ -13,6 +15,7 @@ -- * Logic components bXor, + bNand, bEquiv ) where @@ -21,36 +24,44 @@ import Data.SBV.Program.Types +const = mkSimpleComp "const" $ SimpleSpec 0 $ \[] o -> sTrue + + inc :: (SymVal a, Ord a, Num a) => SimpleComponent a -inc = SimpleComponent "inc" $ SimpleSpec 1 $ \[i] o -> o .== (i+1) +inc = mkSimpleComp "inc" $ SimpleSpec 1 $ \[i] o -> o .== (i+1) dec :: (SymVal a, Ord a, Num a) => SimpleComponent a -dec = SimpleComponent "dec" $ SimpleSpec 1 $ \[i] o -> o .== (i-1) +dec = mkSimpleComp "dec" $ SimpleSpec 1 $ \[i] o -> o .== (i-1) add :: (SymVal a, Ord a, Num a) => SimpleComponent a -add = SimpleComponent "add" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 + i2) +add = mkSimpleComp "add" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 + i2) sub :: (SymVal a, Ord a, Num a) => SimpleComponent a -sub = SimpleComponent "sub" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 - i2) +sub = mkSimpleComp "sub" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 - i2) mul :: (SymVal a, Ord a, Num a) => SimpleComponent a -mul = SimpleComponent "mul" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 * i2) +mul = mkSimpleComp "mul" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 * i2) and :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a -and = SimpleComponent "and" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 .&. i2) +and = mkSimpleComp "and" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 .&. i2) or :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a -or = SimpleComponent "or" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 .|. i2) +or = mkSimpleComp "or" $ SimpleSpec 2 $ \[i1,i2] o -> o .== (i1 .|. i2) not :: (SymVal a, Ord a, Num a, Bits a) => SimpleComponent a -not = SimpleComponent "not" $ SimpleSpec 1 $ \[i1] o -> o .== complement i1 +not = mkSimpleComp "not" $ SimpleSpec 1 $ \[i1] o -> o .== complement i1 -bXor = SimpleComponent "bXor" $ SimpleSpec 2 $ \[i1,i2] o -> o .== i1 .<+> i2 +bXor :: SimpleComponent Bool +bXor = mkSimpleComp "bXor" $ SimpleSpec 2 $ \[i1,i2] o -> o .== i1 .<+> i2 +bNand :: SimpleComponent Bool +bNand = mkSimpleComp "bNand" $ SimpleSpec 2 $ \[i1,i2] o -> o .== sNot (i1 .&& i2) + -- | Logical equivalence implemented in "tabular" style -bEquiv = SimpleComponent "bEquiv" $ SimpleSpec 2 $ \[i1,i2] o -> sAnd [ +bEquiv :: SimpleComponent Bool +bEquiv = mkSimpleComp "bEquiv" $ SimpleSpec 2 $ \[i1,i2] o -> sAnd [ sNot i1 .&& sNot i2 .=> o, i1 .&& sNot i2 .=> sNot o, sNot i1 .&& i2 .=> sNot o, diff --git a/src/Data/SBV/Program/Types.hs b/src/Data/SBV/Program/Types.hs --- a/src/Data/SBV/Program/Types.hs +++ b/src/Data/SBV/Program/Types.hs @@ -15,6 +15,7 @@ SimpleSpec(..), SimpleComponent(..), + mkSimpleComp, SynthesisError(..), @@ -70,10 +71,18 @@ compSpec :: comp a -> spec a -- | Optional constraints to set on __location variables__ \(l_x \in L\). extraLocConstrs :: comp a -> [[SLocation] -> SLocation -> SBool] + -- | Method used to get the value of a constant component. It doesn't require + -- an implementation if you don't use constant components. + getConstValue :: comp a -> a + -- | Method used to by the synthesis procedure to set the value of a constant + -- component. It doesn't require an implementation if you don't use constant + -- components. + putConstValue :: comp a -> a -> comp a compName = const "" extraLocConstrs = const [] - + getConstValue = const undefined + putConstValue = const -- | A simplest __specification__ datatype possible. Type variable 'a' stands -- for function's domain type. @@ -90,12 +99,21 @@ data SimpleComponent a = SimpleComponent { simpleName :: String , simpleSpec :: SimpleSpec a + , simpleVal :: a } +mkSimpleComp name spec = SimpleComponent { + simpleName = name + , simpleSpec = spec + , simpleVal = undefined + } + instance SynthComponent SimpleComponent SimpleSpec a where compName = simpleName compSpec = simpleSpec extraLocConstrs = const [] + getConstValue = simpleVal + putConstValue comp c = comp { simpleVal = c } instance Show (SimpleComponent spec) where show = compName diff --git a/src/Data/SBV/Program/Utils.hs b/src/Data/SBV/Program/Utils.hs --- a/src/Data/SBV/Program/Utils.hs +++ b/src/Data/SBV/Program/Utils.hs @@ -4,6 +4,8 @@ module Data.SBV.Program.Utils ( sampleSpec, + isConstantComponent, + mkVarName, mkInputLocName, mkOutputLocName, @@ -35,6 +37,13 @@ _ -> pure Nothing +-- | Returns 'True' if the component is a __constant__ one. Constant components +-- have zero inputs (their 'specArity' \(=0\) ). +isConstantComponent :: forall a comp spec . (SynthSpec spec a, SynthComponent comp spec a) => + comp a + -> Bool +isConstantComponent comp = specArity (compSpec comp) == 0 + -- | Creates sanitized variable name suitable for SBV. mkVarName :: String -- ^ Base name, which can be an empty string, in which case \"UnnamedComponent\" value will be used. -> Bool -- ^ Setting 'isLocation' to 'True' will append \"Loc\" to the name. @@ -57,7 +66,7 @@ -- | Renders the solution in SSA style. -writePseudocode :: SynthComponent comp spec a => Program Location (comp a) -> String +writePseudocode :: (Show a, SynthComponent comp spec a) => Program Location (comp a) -> String writePseudocode prog = unlines (header : body ++ ret) where prog' = sortInstructions prog @@ -72,7 +81,8 @@ " = ", compName comp, " ", - intercalate ", " $ map writeArg _ins + intercalate ", " $ map writeArg _ins, + if isConstantComponent comp then show $ getConstValue comp else "" ] ret = ["\treturn " ++ writeArg (_out $ programIOs prog')] writeArg loc = '%' : show loc diff --git a/test/SmokeTest.hs b/test/SmokeTest.hs --- a/test/SmokeTest.hs +++ b/test/SmokeTest.hs @@ -31,6 +31,24 @@ assert $ solutionCorrect (toIOsList $ sortInstructions r) _ -> error "refinedExAllProcedure" + putStrLn "===== refinedExAllProcedure with constant ======" + r <- refinedExAllProcedure [Lib.and, Lib.const, sub] paperRunningExampleSpec + case r of + Right r -> do + let code = writePseudocode r + putStrLn code + assert $ "const 1" `isInfixOf` code + Left e -> error $ show e + + putStrLn "===== exAllProcedure with constant ======" + r <- exAllProcedure [Lib.and, Lib.const, sub] paperRunningExampleSpec + case r of + Right r -> do + let code = writePseudocode r + putStrLn code + assert $ "const 1" `isInfixOf` code + Left e -> error $ show e + solutionCorrect s = [0,2] `isPrefixOf` s && ([1,0,2] `isSuffixOf` s || [0,1,2] `isSuffixOf` s) assert cond = unless cond (error "assertion failed")