sbv-program 1.0.0.0 → 1.1.0.0

raw patch · 7 files changed

+224/−34 lines, 7 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• sbv-program.cabal +5/−5
• src/Data/SBV/Program.hs +123/−14
• src/Data/SBV/Program/Examples.hs +26/−2
• src/Data/SBV/Program/SimpleLibrary.hs +21/−10
• src/Data/SBV/Program/Types.hs +19/−1
• src/Data/SBV/Program/Utils.hs +12/−2
• test/SmokeTest.hs +18/−0

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

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

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

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

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

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

@@ -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")