From a4d2cde370ee38be79cca19f0a92dc7f0285a75c Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Tue, 10 Sep 2024 14:35:41 -0700
Subject: [PATCH] add solver config to KD config

---
 Data/SBV/Tools/KDKernel.hs       |  9 ++++++---
 Data/SBV/Tools/KDUtils.hs        |  7 ++++++-
 Data/SBV/Tools/KnuckleDragger.hs | 17 +++++++++++------
 3 files changed, 23 insertions(+), 10 deletions(-)

diff --git a/Data/SBV/Tools/KDKernel.hs b/Data/SBV/Tools/KDKernel.hs
index da19b7914..ed8b676ce 100644
--- a/Data/SBV/Tools/KDKernel.hs
+++ b/Data/SBV/Tools/KDKernel.hs
@@ -27,7 +27,8 @@ module Data.SBV.Tools.KDKernel (
        , sorry
        ) where
 
-import Control.Monad.Trans (liftIO)
+import Control.Monad.Trans  (liftIO)
+import Control.Monad.Reader (ask)
 
 import Data.List (intercalate, sort, nub)
 
@@ -156,7 +157,8 @@ lemmaGen cfg what nms inputProp by = do
 
 -- | Prove a given statement, using auxiliaries as helpers. Using the default solver.
 lemma :: Proposition a => String -> a -> [Proven] -> KD Proven
-lemma = lemmaWith defaultSMTCfg
+lemma nm f by = do KDConfig{kdSolverConfig} <- ask
+                   lemmaWith kdSolverConfig nm f by
 
 -- | Prove a given statement, using auxiliaries as helpers. Using the given solver.
 lemmaWith :: Proposition a => SMTConfig -> String -> a -> [Proven] -> KD Proven
@@ -164,7 +166,8 @@ 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.
 theorem :: Proposition a => String -> a -> [Proven] -> KD Proven
-theorem = theoremWith defaultSMTCfg
+theorem nm f by = do KDConfig{kdSolverConfig} <- ask
+                     theoremWith kdSolverConfig nm f by
 
 -- | Prove a given statement, using auxiliaries as helpers. Essentially the same as 'lemmaWith', except for the name.
 theoremWith :: Proposition a => SMTConfig -> String -> a -> [Proven] -> KD Proven
diff --git a/Data/SBV/Tools/KDUtils.hs b/Data/SBV/Tools/KDUtils.hs
index 225e8887f..ac159d217 100644
--- a/Data/SBV/Tools/KDUtils.hs
+++ b/Data/SBV/Tools/KDUtils.hs
@@ -27,13 +27,18 @@ import Control.Monad.Trans  (MonadIO(liftIO))
 import Data.List (intercalate)
 import System.IO (hFlush, stdout)
 
+import Data.SBV.Core.Symbolic  (SMTConfig)
+import Data.SBV.Provers.Prover (defaultSMTCfg)
+
 -- | Keeping track of KD options/state
-data KDConfig = KDConfig { kdRibbonLength :: Int   -- ^ Lenght of the line as we print the proof
+data KDConfig = KDConfig { kdRibbonLength :: Int        -- ^ Lenght of the line as we print the proof
+                         , kdSolverConfig :: SMTConfig  -- ^ The backend solver to use
                          }
 
 -- | Default KD-config
 defaultKDConfig :: KDConfig
 defaultKDConfig = KDConfig { kdRibbonLength = 40
+                           , kdSolverConfig = defaultSMTCfg
                            }
 
 -- | Monad for running KnuckleDragger proofs in.
diff --git a/Data/SBV/Tools/KnuckleDragger.hs b/Data/SBV/Tools/KnuckleDragger.hs
index 3d3f62eaf..d69b59442 100644
--- a/Data/SBV/Tools/KnuckleDragger.hs
+++ b/Data/SBV/Tools/KnuckleDragger.hs
@@ -16,11 +16,12 @@
 {-# LANGUAGE ConstraintKinds            #-}
 {-# LANGUAGE DataKinds                  #-}
 {-# LANGUAGE DerivingStrategies         #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses      #-}
-{-# LANGUAGE FunctionalDependencies     #-}
 {-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE FunctionalDependencies     #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE NamedFieldPuns             #-}
 {-# LANGUAGE TypeAbstractions           #-}
 
 {-# OPTIONS_GHC -Wall -Werror #-}
@@ -50,7 +51,8 @@ import Data.SBV
 import Data.SBV.Tools.KDKernel
 import Data.SBV.Tools.KDUtils
 
-import Control.Monad(when)
+import Control.Monad        (when)
+import Control.Monad.Reader (ask)
 
 -- | A class for doing equational reasoning style chained proofs. Use 'chainLemma' to prove a given theorem
 -- as a sequence of equalities, each step following from the previous.
@@ -87,8 +89,11 @@ class ChainLemma steps step | steps -> step where
   makeSteps :: steps -> [step]
   makeInter :: steps -> step -> step -> SBool
 
-  chainLemma   = chainLemmaWith   defaultSMTCfg
-  chainTheorem = chainTheoremWith defaultSMTCfg
+  chainLemma nm p steps by = do KDConfig{kdSolverConfig} <- ask
+                                chainLemmaWith kdSolverConfig nm p steps by
+
+  chainTheorem nm p steps by = do KDConfig{kdSolverConfig} <- ask
+                                  chainTheoremWith kdSolverConfig nm p steps by
 
   chainLemmaWith   = chainGeneric False
   chainTheoremWith = chainGeneric True