From ccee2eb384aeb831356394d2257d2a41682947e0 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Sun, 22 Sep 2024 22:14:12 -0700 Subject: [PATCH] Get rid of KDConfig --- Data/SBV/Core/Symbolic.hs | 1 + Data/SBV/Provers/Prover.hs | 1 + Data/SBV/Tools/KDKernel.hs | 22 +++++------- Data/SBV/Tools/KDUtils.hs | 36 ++++--------------- Data/SBV/Tools/KnuckleDragger.hs | 8 ++--- .../SBV/Examples/KnuckleDragger/CaseSplit.hs | 4 +-- 6 files changed, 23 insertions(+), 49 deletions(-) diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs index 2271850db..31aeaccf9 100644 --- a/Data/SBV/Core/Symbolic.hs +++ b/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 diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs index 0e14515df..1ed458280 100644 --- a/Data/SBV/Provers/Prover.hs +++ b/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 diff --git a/Data/SBV/Tools/KDKernel.hs b/Data/SBV/Tools/KDKernel.hs index 575a1f252..e68feab8a 100644 --- a/Data/SBV/Tools/KDKernel.hs +++ b/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 diff --git a/Data/SBV/Tools/KDUtils.hs b/Data/SBV/Tools/KDUtils.hs index 9616d14d9..d5631f8ee 100644 --- a/Data/SBV/Tools/KDUtils.hs +++ b/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 diff --git a/Data/SBV/Tools/KnuckleDragger.hs b/Data/SBV/Tools/KnuckleDragger.hs index 06850d729..e6d2a99fa 100644 --- a/Data/SBV/Tools/KnuckleDragger.hs +++ b/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 diff --git a/Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs b/Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs index 237335211..dd46013e2 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs +++ b/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@. --