grisette 0.4.0.0 → 0.4.1.0

raw patch · 6 files changed

+163/−26 lines, 6 filesdep ~sbvPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: sbv

API changes (from Hackage documentation)

Files

• CHANGELOG.md +7/−0
• README.md +1/−1
• grisette.cabal +1/−1
• src/Grisette/Core.hs +9/−1
• src/Grisette/Core/Data/Class/CEGISSolver.hs +118/−2
• test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs +27/−21

@@ -5,6 +5,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.4.1.0] -- 2024-01-10++### Added++- Added `cegisForAll` interfaces. ([#165])(https://github.com/lsrcz/grisette/pull/165)+ ## [0.4.0.0] -- 2024-01-08  ### Added@@ -125,6 +131,7 @@  - Initial release for Grisette. +[0.4.1.0]: https://github.com/lsrcz/grisette/compare/v0.4.1.0...v0.4.0.0 [0.4.0.0]: https://github.com/lsrcz/grisette/compare/v0.4.0.0...v0.3.1.0 [0.3.1.1]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...v0.3.1.1 [0.3.1.0]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...v0.3.1.0

@@ -47,7 +47,7 @@ ```cabal library   ...-  build-depends: grisette >= 0.4 < 0.5+  build-depends: grisette >= 0.4.1 < 0.5 ```  #### Quick start template with `stack new`

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           grisette-version:        0.4.0.0+version:        0.4.1.0 synopsis:       Symbolic evaluation as a library description:    Grisette is a reusable symbolic evaluation library for Haskell. By                 translating programs into constraints, Grisette can help the development of

@@ -964,9 +964,9 @@      -- ** CEGIS interfaces with pre/post conditions     CEGISCondition (..),-    cegisMultiInputs,     cegisPostCond,     cegisPrePost,+    cegisMultiInputs,     cegis,     cegisExcept,     cegisExceptStdVC,@@ -974,6 +974,10 @@     cegisExceptMultiInputs,     cegisExceptStdVCMultiInputs,     cegisExceptVCMultiInputs,+    cegisForAll,+    cegisForAllExcept,+    cegisForAllExceptStdVC,+    cegisForAllExceptVC,      -- ** Symbolic constant extraction @@ -1087,6 +1091,10 @@     cegisExceptStdVCMultiInputs,     cegisExceptVC,     cegisExceptVCMultiInputs,+    cegisForAll,+    cegisForAllExcept,+    cegisForAllExceptStdVC,+    cegisForAllExceptVC,     cegisMultiInputs,     cegisPostCond,     cegisPrePost,

@@ -33,9 +33,9 @@      -- * CEGIS interfaces with pre/post conditions     CEGISCondition (..),-    cegisMultiInputs,     cegisPostCond,     cegisPrePost,+    cegisMultiInputs,     cegis,     cegisExcept,     cegisExceptStdVC,@@ -43,6 +43,10 @@     cegisExceptMultiInputs,     cegisExceptStdVCMultiInputs,     cegisExceptVCMultiInputs,+    cegisForAll,+    cegisForAllExcept,+    cegisForAllExceptStdVC,+    cegisForAllExceptVC,   ) where @@ -275,7 +279,7 @@ -- >>> :set -XOverloadedStrings -- >>> let [x,c] = ["x","c"] :: [SymInteger] -- >>> cegis (precise z3) x (\x -> cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2))--- ([...],CEGISSuccess (Model {c -> -1 :: Integer}))+-- (...,CEGISSuccess (Model {c -> -1 :: Integer})) cegis ::   ( ConfigurableSolver config handle,     EvaluateSym inputs,@@ -496,3 +500,115 @@   (inputs -> t) ->   IO ([inputs], CEGISResult SolvingFailure) cegisExceptStdVC config inputs = cegisExceptVC config inputs return++-- |+-- CEGIS with a single symbolic input to represent a set of inputs.+--+-- The following example tries to find the value of @c@ such that for all+-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ clause is used to make+-- the solution unique.+--+-- >>> :set -XOverloadedStrings+-- >>> let [x,c] = ["x","c"] :: [SymInteger]+-- >>> cegisForAll (precise z3) x $ cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2)+-- (...,CEGISSuccess (Model {c -> -1 :: Integer}))+cegisForAll ::+  ( ExtractSymbolics forallInput,+    ConfigurableSolver config handle+  ) =>+  config ->+  -- | A symbolic value. All the symbolic constants in the value are treated as+  -- for-all variables.+  forallInput ->+  CEGISCondition ->+  -- | First output are the counter-examples for all the for-all variables, and+  -- the second output is the model for all other variables if CEGIS succeeds.+  IO ([Model], CEGISResult SolvingFailure)+cegisForAll config input (CEGISCondition pre post) = do+  (models, result) <- genericCEGIS config phi synthConstr () verifier+  let exactResult = case result of+        CEGISSuccess model -> CEGISSuccess $ exceptFor forallSymbols model+        _ -> result+  return (models, exactResult)+  where+    phi = pre .&& post+    negphi = pre .&& symNot post+    forallSymbols = extractSymbolics input+    synthConstr _ model = return $ evaluateSym False model phi+    verifier () candidate = do+      let evaluated =+            evaluateSym False (exceptFor forallSymbols candidate) negphi+      r <- solve config evaluated+      case r of+        Left Unsat -> return ((), CEGISVerifierNoCex)+        Left err -> return ((), CEGISVerifierException err)+        Right model ->+          return ((), CEGISVerifierFoundCex $ exact forallSymbols model)++-- |+-- CEGIS for symbolic programs with error handling, with a forall variable.+--+-- See 'cegisForAll' and 'cegisExcept'.+cegisForAllExcept ::+  ( UnionWithExcept t u e v,+    UnionPrjOp u,+    Functor u,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    ConfigurableSolver config handle,+    SEq inputs+  ) =>+  config ->+  inputs ->+  (Either e v -> CEGISCondition) ->+  t ->+  IO ([Model], CEGISResult SolvingFailure)+cegisForAllExcept config inputs f v =+  cegisForAll config inputs $ simpleMerge $ f <$> extractUnionExcept v++-- |+-- CEGIS for symbolic programs with error handling, with a forall variable.+--+-- See 'cegisForAll' and 'cegisExceptVC'.+cegisForAllExceptVC ::+  ( UnionWithExcept t u e v,+    UnionPrjOp u,+    Monad u,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    ConfigurableSolver config handle,+    SEq inputs+  ) =>+  config ->+  inputs ->+  (Either e v -> u (Either VerificationConditions ())) ->+  t ->+  IO ([Model], CEGISResult SolvingFailure)+cegisForAllExceptVC config inputs f v = do+  cegisForAll config inputs $+    simpleMerge $+      ( \case+          Left AssumptionViolation -> cegisPrePost (con False) (con True)+          Left AssertionViolation -> cegisPostCond (con False)+          _ -> cegisPostCond (con True)+      )+        <$> (extractUnionExcept v >>= f)++-- |+-- CEGIS for symbolic programs with error handling, with a forall variable.+--+-- See 'cegisForAll' and 'cegisExceptStdVC'.+cegisForAllExceptStdVC ::+  ( UnionWithExcept t u VerificationConditions (),+    UnionPrjOp u,+    Monad u,+    EvaluateSym inputs,+    ExtractSymbolics inputs,+    ConfigurableSolver config handle,+    SEq inputs+  ) =>+  config ->+  inputs ->+  t ->+  IO ([Model], CEGISResult SolvingFailure)+cegisForAllExceptStdVC config inputs = cegisForAllExceptVC config inputs return

@@ -7,7 +7,7 @@  module Grisette.Backend.SBV.Data.SMT.CEGISTests (cegisTests) where -import Control.Monad.Except (ExceptT, runExceptT)+import Control.Monad.Except (ExceptT) import Data.Proxy (Proxy (Proxy)) import qualified Data.SBV as SBV import Data.String (IsString (fromString))@@ -24,6 +24,7 @@   ( CEGISResult (CEGISSuccess),     cegis,     cegisExceptVC,+    cegisForAllExceptVC,     cegisMultiInputs,     cegisPostCond,   )@@ -64,30 +65,35 @@   (a -> [SymBool]) ->   Assertion testCegis config shouldSuccess inputs bs = do-  x <--    cegisExceptVC-      config-      (inputs, "internal" :: SymInteger)-      return-      ( \(cexInputs, internal) ->-          runExceptT $ buildFormula internal (bs cexInputs)-      )-  case x of+  cegisExceptVCResult <-+    cegisExceptVC config (inputs, "internal" :: SymInteger) return $+      \(cexInputs, internal) -> buildFormula internal (bs cexInputs)+  case cegisExceptVCResult of     (_, CEGISSuccess m) -> do       shouldSuccess @=? True-      verify (bs inputs)-      where-        verify [] = return ()-        verify (v : vs) = do-          y <- solve config (evaluateSym False m $ symNot v)-          case y of-            Left _ -> do-              verify vs-            Right _ ->-              assertFailure $-                "Failed to verify " ++ show v ++ " with the model " ++ show m+      verify "cegisExceptVC" m (bs inputs)     _ -> shouldSuccess @=? False+  cegisForAllExceptVCResult <-+    cegisForAllExceptVC config (inputs, "internal" :: SymInteger) return $+      buildFormula "internal" (bs inputs)+  case cegisForAllExceptVCResult of+    (_, CEGISSuccess m) -> do+      shouldSuccess @=? True+      verify "cegisForAllExceptVC" m (bs inputs)+    _ -> shouldSuccess @=? False   where+    verify _ _ [] = return ()+    verify funName m (v : vs) = do+      y <- solve config (evaluateSym False m $ symNot v)+      case y of+        Left _ -> verify funName m vs+        Right _ ->+          assertFailure $+            funName+              ++ ": Failed to verify "+              ++ show v+              ++ " with the model "+              ++ show m     buildFormula internal l = do       symAssume (internal .>= 0)       go l 0