From 5097f8baa1a66f680ecf9bb4591ad3b5bea64369 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Wed, 6 Nov 2024 07:23:13 -0800 Subject: [PATCH] Move Queriable class to Data.SBV makes imports simpler --- Data/SBV.hs | 55 ++++++++++++++++--- Data/SBV/Control.hs | 45 +-------------- Documentation/SBV/Examples/ProofTools/BMC.hs | 1 - .../SBV/Examples/ProofTools/Fibonacci.hs | 1 - .../SBV/Examples/ProofTools/Strengthen.hs | 1 - Documentation/SBV/Examples/ProofTools/Sum.hs | 1 - Documentation/SBV/Examples/Puzzles/DieHard.hs | 1 - .../Examples/WeakestPreconditions/Append.hs | 4 +- .../Examples/WeakestPreconditions/Basics.hs | 2 - .../SBV/Examples/WeakestPreconditions/Fib.hs | 2 - .../SBV/Examples/WeakestPreconditions/GCD.hs | 2 - .../Examples/WeakestPreconditions/IntDiv.hs | 2 - .../Examples/WeakestPreconditions/IntSqrt.hs | 2 - .../Examples/WeakestPreconditions/Length.hs | 4 +- .../SBV/Examples/WeakestPreconditions/Sum.hs | 2 - 15 files changed, 50 insertions(+), 75 deletions(-) diff --git a/Data/SBV.hs b/Data/SBV.hs index fe6a4a383..92625070d 100644 --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -145,13 +145,15 @@ -- get in touch if there is a solver you'd like to see included. ----------------------------------------------------------------------------- -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -421,6 +423,9 @@ module Data.SBV ( , isConcrete, isSymbolic, isConcretely, mkSymVal , MonadSymbolic(..), Symbolic, SymbolicT, label, output, runSMT, runSMTWith + -- * Queriable values + , Queriable(..), freshVar, freshVar_, getValue + -- * Module exports -- $moduleExportIntro @@ -430,7 +435,8 @@ module Data.SBV ( , module Data.Ratio ) where -import Control.Monad (when) +import Control.Monad (when) +import Control.Monad.Trans (MonadIO) import Data.SBV.Core.AlgReals import Data.SBV.Core.Data hiding (free, free_, mkFreeVars, @@ -488,11 +494,14 @@ import Data.Ratio import Data.Word import Data.SBV.SMT.Utils (SBVException(..)) + import Data.SBV.Control.Types (SMTReasonUnknown(..), Logic(..)) +import Data.SBV.Control.Utils (getValue, freshVar, freshVar_) import qualified Data.SBV.Utils.CrackNum as CN import Data.Proxy (Proxy(..)) +import Data.Kind (Type) import GHC.TypeLits (KnownNat, type (<=), type (+), type (-)) import Prelude hiding((+), (-)) -- to avoid the haddock ambiguity @@ -1752,4 +1761,34 @@ optIndependentWith config p = do _ -> error $ "An independent optimization call resulted in a bad result:" ++ "\n" ++ show res +-- | An queriable value: Mapping between concrete/symbolic values. If your type is traversable and simply embeds +-- symbolic equivalents for one type, then you can simply define 'create'. (Which is the most common case.) +class Queriable m a where + type QueryResult a :: Type + + -- | ^ Create a new symbolic value of type @a@ + create :: QueryT m a + + -- | ^ Extract the current value in a SAT context + project :: a -> QueryT m (QueryResult a) + + -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other + -- via the 'QueryT' monad transformer. + embed :: QueryResult a -> QueryT m a + + default project :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => a -> QueryT m (QueryResult a) + project = mapM getValue + + default embed :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => QueryResult a -> QueryT m a + embed = pure . fmap literal + {-# MINIMAL create #-} + +-- | Generic 'Queriable' instance for 'SymVal' values +instance {-# OVERLAPPABLE #-} (MonadIO m, SymVal a) => Queriable m (SBV a) where + type QueryResult (SBV a) = a + + create = freshVar_ + project = getValue + embed = return . literal + {- HLint ignore module "Use import/export shortcut" -} diff --git a/Data/SBV/Control.hs b/Data/SBV/Control.hs index 4f53b6e60..476acb6d4 100644 --- a/Data/SBV/Control.hs +++ b/Data/SBV/Control.hs @@ -9,20 +9,13 @@ -- Control sublanguage for interacting with SMT solvers. ----------------------------------------------------------------------------- -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DefaultSignatures #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} - {-# OPTIONS_GHC -Wall -Werror #-} module Data.SBV.Control ( -- $queryIntro -- * User queries - ExtractIO(..), MonadQuery(..), Queriable(..), Query, query + ExtractIO(..), MonadQuery(..), Query, query -- * Create a fresh variable , freshVar_, freshVar @@ -88,46 +81,10 @@ import Data.SBV.Control.Utils (registerUISMTFunction, registerSMTType) import qualified Data.SBV.Control.Utils as Trans -import Data.SBV.Core.Data (SymVal, SBV, literal) - -import Control.Monad.Trans (MonadIO) -import Data.Kind (Type) - - -- | Run a custom query query :: Query a -> Symbolic a query = Trans.executeQuery QueryExternal --- | An queriable value: Mapping between concrete/symbolic values. If your type is traversable and simply embeds --- symbolic equivalents for one type, then you can simply define 'create'. (Which is the most common case.) -class Queriable m a where - type QueryResult a :: Type - - -- | ^ Create a new symbolic value of type @a@ - create :: QueryT m a - - -- | ^ Extract the current value in a SAT context - project :: a -> QueryT m (QueryResult a) - - -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other - -- via the 'QueryT' monad transformer. - embed :: QueryResult a -> QueryT m a - - default project :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => a -> QueryT m (QueryResult a) - project = mapM getValue - - default embed :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => QueryResult a -> QueryT m a - embed = pure . fmap literal - {-# MINIMAL create #-} - --- | Generic 'Queriable' instance for 'SymVal' values -instance {-# OVERLAPPABLE #-} (MonadIO m, SymVal a) => Queriable m (SBV a) where - type QueryResult (SBV a) = a - - create = freshVar_ - project = getValue - embed = return . literal - {- $queryIntro In certain cases, the user might want to take over the communication with the solver, programmatically querying the engine and issuing commands accordingly. Queries can be extremely powerful as diff --git a/Documentation/SBV/Examples/ProofTools/BMC.hs b/Documentation/SBV/Examples/ProofTools/BMC.hs index b57f42687..abb440e78 100644 --- a/Documentation/SBV/Examples/ProofTools/BMC.hs +++ b/Documentation/SBV/Examples/ProofTools/BMC.hs @@ -30,7 +30,6 @@ module Documentation.SBV.Examples.ProofTools.BMC where import Data.SBV import Data.SBV.Tools.BMC -import Data.SBV.Control -- * System state diff --git a/Documentation/SBV/Examples/ProofTools/Fibonacci.hs b/Documentation/SBV/Examples/ProofTools/Fibonacci.hs index a0349a6b2..5e92ee79c 100644 --- a/Documentation/SBV/Examples/ProofTools/Fibonacci.hs +++ b/Documentation/SBV/Examples/ProofTools/Fibonacci.hs @@ -34,7 +34,6 @@ module Documentation.SBV.Examples.ProofTools.Fibonacci where import Data.SBV import Data.SBV.Tools.Induction -import Data.SBV.Control -- * System state diff --git a/Documentation/SBV/Examples/ProofTools/Strengthen.hs b/Documentation/SBV/Examples/ProofTools/Strengthen.hs index 5abe95cfb..022e541d1 100644 --- a/Documentation/SBV/Examples/ProofTools/Strengthen.hs +++ b/Documentation/SBV/Examples/ProofTools/Strengthen.hs @@ -41,7 +41,6 @@ module Documentation.SBV.Examples.ProofTools.Strengthen where import Data.SBV import Data.SBV.Tools.Induction -import Data.SBV.Control -- * System state diff --git a/Documentation/SBV/Examples/ProofTools/Sum.hs b/Documentation/SBV/Examples/ProofTools/Sum.hs index b4e81701b..1df9b4bb0 100644 --- a/Documentation/SBV/Examples/ProofTools/Sum.hs +++ b/Documentation/SBV/Examples/ProofTools/Sum.hs @@ -33,7 +33,6 @@ module Documentation.SBV.Examples.ProofTools.Sum where import Data.SBV import Data.SBV.Tools.Induction -import Data.SBV.Control -- * System state diff --git a/Documentation/SBV/Examples/Puzzles/DieHard.hs b/Documentation/SBV/Examples/Puzzles/DieHard.hs index 5812dc61a..b3ace0f03 100644 --- a/Documentation/SBV/Examples/Puzzles/DieHard.hs +++ b/Documentation/SBV/Examples/Puzzles/DieHard.hs @@ -26,7 +26,6 @@ module Documentation.SBV.Examples.Puzzles.DieHard where import Data.SBV -import Data.SBV.Control import Data.SBV.Tools.BMC -- | Possible actions diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Append.hs b/Documentation/SBV/Examples/WeakestPreconditions/Append.hs index 5bfc7042b..127175081 100644 --- a/Documentation/SBV/Examples/WeakestPreconditions/Append.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Append.hs @@ -25,7 +25,7 @@ module Documentation.SBV.Examples.WeakestPreconditions.Append where import Data.SBV -import Data.SBV.Control +import Data.SBV.Tools.WeakestPreconditions import Prelude hiding ((++)) import qualified Prelude as P @@ -33,8 +33,6 @@ import qualified Prelude as P import Data.SBV.List ((++)) import qualified Data.SBV.List as L -import Data.SBV.Tools.WeakestPreconditions - import GHC.Generics (Generic) -- * Program state diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs b/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs index e930385ab..338343091 100644 --- a/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs @@ -25,8 +25,6 @@ module Documentation.SBV.Examples.WeakestPreconditions.Basics where import Data.SBV -import Data.SBV.Control - import Data.SBV.Tools.WeakestPreconditions import GHC.Generics (Generic) diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs index 004654bd0..13000afa1 100644 --- a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs @@ -26,8 +26,6 @@ module Documentation.SBV.Examples.WeakestPreconditions.Fib where import Data.SBV -import Data.SBV.Control - import Data.SBV.Tools.WeakestPreconditions import GHC.Generics (Generic) diff --git a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs index 93b137b11..bb80f2c19 100644 --- a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs @@ -28,8 +28,6 @@ module Documentation.SBV.Examples.WeakestPreconditions.GCD where import Data.SBV -import Data.SBV.Control - import Data.SBV.Tools.WeakestPreconditions import GHC.Generics (Generic) diff --git a/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs b/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs index 9567ad171..d2f48e919 100644 --- a/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs @@ -24,8 +24,6 @@ module Documentation.SBV.Examples.WeakestPreconditions.IntDiv where import Data.SBV -import Data.SBV.Control - import Data.SBV.Tools.WeakestPreconditions import GHC.Generics (Generic) diff --git a/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs b/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs index 62f023de8..52f5e4b66 100644 --- a/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs @@ -26,8 +26,6 @@ module Documentation.SBV.Examples.WeakestPreconditions.IntSqrt where import Data.SBV -import Data.SBV.Control - import Data.SBV.Tools.WeakestPreconditions import GHC.Generics (Generic) diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Length.hs b/Documentation/SBV/Examples/WeakestPreconditions/Length.hs index a7c9e7910..95d8e7a9a 100644 --- a/Documentation/SBV/Examples/WeakestPreconditions/Length.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Length.hs @@ -23,12 +23,10 @@ module Documentation.SBV.Examples.WeakestPreconditions.Length where import Data.SBV -import Data.SBV.Control +import Data.SBV.Tools.WeakestPreconditions import qualified Data.SBV.List as L -import Data.SBV.Tools.WeakestPreconditions - import GHC.Generics (Generic) -- * Program state diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs index c4c49da37..35b3f2fc1 100644 --- a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs @@ -25,8 +25,6 @@ module Documentation.SBV.Examples.WeakestPreconditions.Sum where import Data.SBV -import Data.SBV.Control - import Data.SBV.Tools.WeakestPreconditions import GHC.Generics (Generic)