Merge branch 'master' into insertionSort

Data/SBV/Core/Symbolic.hs

@@ -2273,6 +2273,7 @@ data SMTConfig = SMTConfig {
        , solverSetOptions            :: [SMTOption]         -- ^ Options to set as we start the solver
        , ignoreExitCode              :: Bool                -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.
        , redirectVerbose             :: Maybe FilePath      -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied.
+       , kdRibbonLength              :: Int                 -- ^ Line length for KD proofs
        }
 
 -- | Ignore internal names and those the user told us to

Data/SBV/Provers/Prover.hs

@@ -106,6 +106,7 @@ mkConfig s smtVersion startOpts = SMTConfig { verbose                     = Fals
                                             , solverSetOptions            = startOpts
                                             , ignoreExitCode              = False
                                             , redirectVerbose             = Nothing
+                                            , kdRibbonLength              = 40
                                             }
 
 -- | If supported, this makes all output go to stdout, which works better with SBV

Data/SBV/Tools/KDKernel.hs

@@ -33,6 +33,7 @@ import Data.List (intercalate, sort, nub)
 
 import Data.SBV
 import Data.SBV.Core.Data (Constraint)
+
 import Data.SBV.Tools.KDUtils
 
 import qualified Data.SBV.List as SL
@@ -109,16 +110,11 @@ sorry = Proof { rootOfTrust = Self
         p (Forall (x :: SBool)) = label "SORRY: KnuckleDragger, proof uses \"sorry\"" x
 
 -- | Helper to generate lemma/theorem statements.
-lemmaGen :: Proposition a => KDConfig -> String -> [String] -> a -> [Proof] -> KD Proof
-lemmaGen cfg what nms inputProp by = do
-    tab <- start (kdVerbose cfg) what nms
-
-    let underlyingSolver = kdSolverConfig cfg
-        solver           = underlyingSolver{ verbose   = verbose   underlyingSolver || kdVerbose cfg
-                                           , extraArgs = extraArgs underlyingSolver ++ kdExtraSolverArgs cfg
-                                           }
+lemmaGen :: Proposition a => SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
+lemmaGen cfg@SMTConfig{verbose} what nms inputProp by = do
+    tab <- start verbose what nms
 
-        nm = intercalate "." nms
+    let nm = intercalate "." nms
 
         -- What to do if all goes well
         good = do finish ("Q.E.D." ++ modulo) tab
@@ -150,7 +146,7 @@ lemmaGen cfg what nms inputProp by = do
                            -- way our counter-example will be more likely to be relevant
                            -- to the proposition we're currently proving. (Hopefully.)
                            -- Remember that we first have to negate, and then skolemize!
-                           SatResult res <- satWith solver $ do
+                           SatResult res <- satWith cfg $ do
                                                mapM_ constrain [getProof | Proof{isUserAxiom, getProof} <- by, isUserAxiom] :: Symbolic ()
                                                pure $ skolemize (qNot inputProp)
 
@@ -162,7 +158,7 @@ lemmaGen cfg what nms inputProp by = do
                                print r
                                error "Failed"
 
-    pRes <- liftIO $ proveWith solver $ do
+    pRes <- liftIO $ proveWith cfg $ do
                 mapM_ (constrain . getProof) by :: Symbolic ()
                 pure $ skolemize (quantifiedBool inputProp)
 
@@ -180,7 +176,7 @@ lemma nm f by = do cfg <- ask
                    lemmaWith cfg nm f by
 
 -- | Prove a given statement, using auxiliaries as helpers. Using the given solver.
-lemmaWith :: Proposition a => KDConfig -> String -> a -> [Proof] -> KD Proof
+lemmaWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof
 lemmaWith cfg nm = lemmaGen cfg "Lemma" [nm]
 
 -- | Prove a given statement, using auxiliaries as helpers. Essentially the same as 'lemma', except for the name, using the default solver.
@@ -189,7 +185,7 @@ theorem nm f by = do cfg <- ask
                      theoremWith cfg nm f by
 
 -- | Prove a given statement, using auxiliaries as helpers. Essentially the same as 'lemmaWith', except for the name.
-theoremWith :: Proposition a => KDConfig -> String -> a -> [Proof] -> KD Proof
+theoremWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof
 theoremWith cfg nm = lemmaGen cfg "Theorem" [nm]
 
 -- | Given a predicate, return an induction principle for it. Typically, we only have one viable

Data/SBV/Tools/KDUtils.hs

@@ -18,7 +18,6 @@
 module Data.SBV.Tools.KDUtils (
          KD, runKD, runKDWith
        , start, finish
-       , KDConfig(..), defaultKDConfig, z3KD, cvc5KD
        ) where
 
 import Control.Monad.Reader (ReaderT, runReaderT, ask, MonadReader)
@@ -28,41 +27,18 @@ import Data.List (intercalate)
 import System.IO (hFlush, stdout)
 
 import Data.SBV.Core.Symbolic  (SMTConfig)
-import Data.SBV.Provers.Prover (defaultSMTCfg, z3, cvc5)
-
--- | Keeping track of KD options/state
-data KDConfig = KDConfig { kdRibbonLength    :: Int        -- ^ Lenght of the line as we print the proof
-                         , kdVerbose         :: Bool       -- ^ Run verbose
-                         , kdExtraSolverArgs :: [String]   -- ^ Extra command line arguments to pass to the solver
-                         , kdSolverConfig    :: SMTConfig  -- ^ The backend solver to use
-                         }
-
--- | Default KD-config uses the default SBV config (which is z3)
-defaultKDConfig :: KDConfig
-defaultKDConfig = KDConfig { kdRibbonLength    = 40
-                           , kdVerbose         = False
-                           , kdExtraSolverArgs = []
-                           , kdSolverConfig    = defaultSMTCfg
-                           }
-
--- | Run KD proof with z3 configuration.
-z3KD :: KDConfig
-z3KD = defaultKDConfig{kdSolverConfig = z3}
-
--- | Run KD proof with z3 configuration.
-cvc5KD :: KDConfig
-cvc5KD = defaultKDConfig{kdSolverConfig = cvc5}
+import Data.SBV.Provers.Prover (defaultSMTCfg, SMTConfig(..))
 
 -- | Monad for running KnuckleDragger proofs in.
-newtype KD a = KD (ReaderT KDConfig IO a)
-            deriving newtype (Applicative, Functor, Monad, MonadIO, MonadReader KDConfig, MonadFail)
+newtype KD a = KD (ReaderT SMTConfig IO a)
+            deriving newtype (Applicative, Functor, Monad, MonadIO, MonadReader SMTConfig, MonadFail)
 
 -- | Run a KD proof, using the default configuration.
 runKD :: KD a -> IO a
-runKD = runKDWith defaultKDConfig
+runKD = runKDWith defaultSMTCfg
 
 -- | Run a KD proof, using the given configuration.
-runKDWith :: KDConfig -> KD a -> IO a
+runKDWith :: SMTConfig -> KD a -> IO a
 runKDWith cfg (KD f) = runReaderT f cfg
 
 -- | Start a proof. We return the number of characters we printed, so the finisher can align the result.
@@ -77,5 +53,5 @@ start newLine what nms = liftIO $ do putStr $ line ++ if newLine then "\n" else
 
 -- | Finish a proof. First argument is what we got from the call of 'start' above.
 finish :: String -> Int -> KD ()
-finish what skip = do KDConfig{kdRibbonLength} <- ask
+finish what skip = do SMTConfig{kdRibbonLength} <- ask
                       liftIO $ putStrLn $ replicate (kdRibbonLength - skip) ' ' ++ what

Data/SBV/Tools/KnuckleDragger.hs

@@ -42,7 +42,7 @@ module Data.SBV.Tools.KnuckleDragger (
        -- * Faking proofs
        , sorry
        -- * Running KnuckleDragger proofs
-       , KD, runKD, runKDWith, KDConfig(..), defaultKDConfig, z3KD, cvc5KD
+       , KD, runKD, runKDWith
        ) where
 
 import Control.Monad.Trans (liftIO)
@@ -84,10 +84,10 @@ class ChainLemma steps step | steps -> step where
   chainTheorem :: Proposition a => String -> a -> steps -> [Proof] -> KD Proof
 
   -- | Prove a property via a series of equality steps, using the given solver.
-  chainLemmaWith :: Proposition a => KDConfig -> String -> a -> steps -> [Proof] -> KD Proof
+  chainLemmaWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
 
   -- | Same as chainLemmaWith, except tagged as Theorem
-  chainTheoremWith :: Proposition a => KDConfig -> String -> a -> steps -> [Proof] -> KD Proof
+  chainTheoremWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
 
   -- | Internal, shouldn't be needed outside the library
   makeSteps :: steps -> [step]
@@ -102,7 +102,7 @@ class ChainLemma steps step | steps -> step where
   chainLemmaWith   = chainGeneric False
   chainTheoremWith = chainGeneric True
 
-  chainGeneric :: Proposition a => Bool -> KDConfig -> String -> a -> steps -> [Proof] -> KD Proof
+  chainGeneric :: Proposition a => Bool -> SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
   chainGeneric taggedTheorem cfg nm result steps base = do
         liftIO $ putStrLn $ "Chain: " ++ nm
         let proofSteps = makeSteps steps

Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs

@@ -23,8 +23,8 @@ import Data.SBV.Tools.KnuckleDragger
 
 -- | The default settings for z3 have trouble running this proof out-of-the-box.
 -- We have to pass auto_config=false to z3!
-z3NoAutoConfig :: KDConfig
-z3NoAutoConfig = z3KD{kdExtraSolverArgs = ["auto_config=false"]}
+z3NoAutoConfig :: SMTConfig
+z3NoAutoConfig = z3{extraArgs = ["auto_config=false"]}
 
 -- | Prove that @2n^2 + n + 1@ is not divisible by @3@.
 --