Simplify

registerSMTFunction -> registerFunction
registerSMTType -> registerType

CHANGES.md

@@ -27,11 +27,13 @@
   * [BACKWARDS COMPATIBILITY] Data.SBV no longer exports the class SatModel, which is more directed
     towards internal SBV purposes. If you need it, you can now import it from Data.SBV.Internals.
 
-  * [BACKWARDS COMPATIBILITY] Added 'registerSMTFunction' which comes in handy for telling SBV about functions
+  * [BACKWARDS COMPATIBILITY] Added 'registerFunction' which comes in handy for telling SBV about functions
     that are used in query mode. This is typically not necessary as SBV will register them automatically, but
     there are certain scenarios where explicit control is needed. This function also generalizes the old
     'registerUISMTFunction', which was a special case of this function and is now removed.
 
+  * [BACKWARDS COMPATIBILITY] The function 'registerSMTType' is renamed to 'registerType'.
+
 ### Version 11.0, 2024-11-06
 
   * [BACKWARDS COMPATIBILITY] SBV now handles arrays in a much more uniform way, unifying

Data/SBV.hs

@@ -312,7 +312,7 @@ module Data.SBV (
   , mkUninterpretedSort
 
   -- * Stopping unrolling: Defined functions
-  , SMTDefinable(..), registerSMTType
+  , SMTDefinable(..), registerType
 
   -- * Special relations
   -- $specialRels

Data/SBV/Core/Data.hs

@@ -64,7 +64,7 @@ module Data.SBV.Core.Data
  , QueryState(..), QueryT(..), SMTProblem(..), Constraint(..), Lambda(..), Forall(..), Exists(..), ExistsUnique(..), ForallN(..), ExistsN(..)
  , QuantifiedBool(..), EqSymbolic(..), QNot(..), Skolemize(SkolemsTo, skolemize, taggedSkolemize)
  , bvExtract, (#), bvDrop, bvTake
- , registerSMTType
+ , registerType
  ) where
 
 import GHC.TypeLits (KnownNat, Nat, Symbol, KnownSymbol, symbolVal, AppendSymbol, type (+), type (-), type (<=), natVal)
@@ -558,12 +558,12 @@ class SolverContext m where
    setLogic     = setOption . SetLogic
    setInfo    k = setOption . SetInfo k
 
--- | Register a kind with the solver. Like 'registerUISMTFunction', this is typically not necessary
--- since SBV will register kinds as it encounters them automatically. But there are cases
+-- | Register a type with the solver. Like 'registerFunction', This is typically not necessary
+-- since SBV will register types as it encounters them automatically. But there are cases
 -- where doing this can explicitly can come handy, typically in query contexts.
-registerSMTType :: forall a m. (MonadIO m, SolverContext m, HasKind a) => Proxy a -> m ()
-registerSMTType _ = do st <- contextState
-                       liftIO $ registerKind st (kindOf (Proxy @a))
+registerType :: forall a m. (MonadIO m, SolverContext m, HasKind a) => Proxy a -> m ()
+registerType _ = do st <- contextState
+                    liftIO $ registerKind st (kindOf (Proxy @a))
 
 -- | A class representing what can be returned from a symbolic computation.
 class Outputtable a where

Data/SBV/Core/Model.hs

@@ -2423,13 +2423,12 @@ class SMTDefinable a where
   -- 'smtFunction' return a monadic result, please get in touch!
   smtFunction :: Lambda Symbolic a => String -> a -> a
 
-  -- | Register an smt defined function. This function is typically not needed as SBV will register
-  -- the function automatically upon first use. However, there are scenarios (in particular query contexts)
-  -- where the definition isn't used before query-mode starts, and SBV does not (for historical reasons)
+  -- | Register a function. This function is typically not needed as SBV will register functions used
+  -- automatically upon first use. However, there are scenarios (in particular query contexts)
+  -- where the definition isn't used before query-mode starts, and SBV (for historical reasons)
   -- requires functions to be known before query-mode starts executing. In such cases, use this function
-  -- to register them with the system. This is similar to 'Data.SBV.Control.registerUISMTFunction', but for
-  -- defined functions, as opposed to uninterpreted functions.
-  registerSMTFunction :: a -> Symbolic ()
+  -- to register them with the system.
+  registerFunction :: a -> Symbolic ()
 
   -- | Uninterpret a value, i.e., add this value as a completely undefined value/function that
   -- the solver is free to instantiate to satisfy other constraints.
@@ -2492,12 +2491,12 @@ class SMTDefinable a where
   cgUninterpret       nm code v = sbvDefineValue nm Nothing   $ UICodeC (v, code)
   sym                           = uninterpret
 
-  default registerSMTFunction :: forall b c. (a ~ (SBV b -> c), SymVal b, SMTDefinable c) => a -> Symbolic ()
-  registerSMTFunction f = do let k = kindOf (Proxy @b)
-                             st <- symbolicEnv
-                             v <- liftIO $ internalVariable st k
-                             let b = SBV $ SVal k $ Right $ cache (const (pure v))
-                             registerSMTFunction $ f b
+  default registerFunction :: forall b c. (a ~ (SBV b -> c), SymVal b, SMTDefinable c) => a -> Symbolic ()
+  registerFunction f = do let k = kindOf (Proxy @b)
+                          st <- symbolicEnv
+                          v <- liftIO $ internalVariable st k
+                          let b = SBV $ SVal k $ Right $ cache (const (pure v))
+                          registerFunction $ f b
 
 -- | Kind of uninterpretation
 data UIKind a = UIFree  Bool                            -- ^ completely uninterpreted. If Bool is true, then this is curried.
@@ -2531,7 +2530,7 @@ instance (SymVal a, HasKind a) => SMTDefinable (SBV a) where
                                          , show s
                                          ]
 
-  registerSMTFunction x = constrain $ x .== x
+  registerFunction x = constrain $ x .== x
 
   sbvDefineValue nm mbArgs uiKind
      | Just v <- retrieveConstCode uiKind
@@ -2933,15 +2932,15 @@ mkUncurried (UICodeC a) = UICodeC a
 instance (SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV c, SBV b) -> SBV a) where
   sbv2smt fn = defs2smt $ \p -> fn p .== fn p
 
-  registerSMTFunction = registerSMTFunction . curry
+  registerFunction = registerFunction . curry
 
   sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry <$> mkUncurried uiKind) in uncurry f
 
 -- Uncurried functions of three arguments
 instance (SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV d, SBV c, SBV b) -> SBV a) where
   sbv2smt fn = defs2smt $ \p -> fn p .== fn p
 
-  registerSMTFunction fn = registerSMTFunction $ \a b c -> fn (a, b, c)
+  registerFunction fn = registerFunction $ \a b c -> fn (a, b, c)
 
   sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (uc3 <$> mkUncurried uiKind) in \(arg0, arg1, arg2) -> f arg0 arg1 arg2
     where uc3 fn a b c = fn (a, b, c)
@@ -2951,7 +2950,7 @@ instance (SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a)
             => SMTDefinable ((SBV e, SBV d, SBV c, SBV b) -> SBV a) where
   sbv2smt fn = defs2smt $ \p -> fn p .== fn p
 
-  registerSMTFunction fn = registerSMTFunction $ \a b c d -> fn (a, b, c, d)
+  registerFunction fn = registerFunction $ \a b c d -> fn (a, b, c, d)
 
   sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (uc4 <$> mkUncurried uiKind) in \(arg0, arg1, arg2, arg3) -> f arg0 arg1 arg2 arg3
     where uc4 fn a b c d = fn (a, b, c, d)
@@ -2961,7 +2960,7 @@ instance (SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a)
             => SMTDefinable ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
   sbv2smt fn = defs2smt $ \p -> fn p .== fn p
 
-  registerSMTFunction fn = registerSMTFunction $ \a b c d e -> fn (a, b, c, d, e)
+  registerFunction fn = registerFunction $ \a b c d e -> fn (a, b, c, d, e)
 
   sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (uc5 <$> mkUncurried uiKind) in \(arg0, arg1, arg2, arg3, arg4) -> f arg0 arg1 arg2 arg3 arg4
     where uc5 fn a b c d e = fn (a, b, c, d, e)
@@ -2971,7 +2970,7 @@ instance (SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a,
             => SMTDefinable ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
   sbv2smt fn = defs2smt $ \p -> fn p .== fn p
 
-  registerSMTFunction fn = registerSMTFunction $ \a b c d e f -> fn (a, b, c, d, e, f)
+  registerFunction fn = registerFunction $ \a b c d e f -> fn (a, b, c, d, e, f)
 
   sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (uc6 <$> mkUncurried uiKind) in \(arg0, arg1, arg2, arg3, arg4, arg5) -> f arg0 arg1 arg2 arg3 arg4 arg5
     where uc6 fn a b c d e f = fn (a, b, c, d, e, f)
@@ -2981,7 +2980,7 @@ instance (SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b,
             => SMTDefinable ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
   sbv2smt fn = defs2smt $ \p -> fn p .== fn p
 
-  registerSMTFunction fn = registerSMTFunction $ \a b c d e f g -> fn (a, b, c, d, e, f, g)
+  registerFunction fn = registerFunction $ \a b c d e f g -> fn (a, b, c, d, e, f, g)
 
   sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (uc7 <$> mkUncurried uiKind) in \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6
     where uc7 fn a b c d e f g = fn (a, b, c, d, e, f, g)
@@ -2991,7 +2990,7 @@ instance (SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c,
             => SMTDefinable ((SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
   sbv2smt fn = defs2smt $ \p -> fn p .== fn p
 
-  registerSMTFunction fn = registerSMTFunction $ \a b c d e f g h -> fn (a, b, c, d, e, f, g, h)
+  registerFunction fn = registerFunction $ \a b c d e f g h -> fn (a, b, c, d, e, f, g, h)
 
   sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (uc8 <$> mkUncurried uiKind) in \(arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7
     where uc8 fn a b c d e f g h = fn (a, b, c, d, e, f, g, h)
@@ -3001,7 +3000,7 @@ instance (SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d,
             => SMTDefinable ((SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
   sbv2smt fn = defs2smt $ \p -> fn p .== fn p
 
-  registerSMTFunction fn = registerSMTFunction $ \a b c d e f g h i -> fn (a, b, c, d, e, f, g, h, i)
+  registerFunction fn = registerFunction $ \a b c d e f g h i -> fn (a, b, c, d, e, f, g, h, i)
 
   sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (uc9 <$> mkUncurried uiKind) in \(arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8
     where uc9 fn a b c d e f g h i = fn (a, b, c, d, e, f, g, h, i)
@@ -3011,7 +3010,7 @@ instance (SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e,
             => SMTDefinable ((SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
   sbv2smt fn = defs2smt $ \p -> fn p .== fn p
 
-  registerSMTFunction fn = registerSMTFunction $ \a b c d e f g h i j -> fn (a, b, c, d, e, f, g, h, i, j)
+  registerFunction fn = registerFunction $ \a b c d e f g h i j -> fn (a, b, c, d, e, f, g, h, i, j)
 
   sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (uc10 <$> mkUncurried uiKind) in \(arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9
     where uc10 fn a b c d e f g h i j = fn (a, b, c, d, e, f, g, h, i, j)
@@ -3021,7 +3020,7 @@ instance (SymVal l, SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f,
             => SMTDefinable ((SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
   sbv2smt fn = defs2smt $ \p -> fn p .== fn p
 
-  registerSMTFunction fn = registerSMTFunction $ \a b c d e f g h i j k -> fn (a, b, c, d, e, f, g, h, i, j, k)
+  registerFunction fn = registerFunction $ \a b c d e f g h i j k -> fn (a, b, c, d, e, f, g, h, i, j, k)
 
   sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (uc11 <$> mkUncurried uiKind) in \(arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10
     where uc11 fn a b c d e f g h i j k = fn (a, b, c, d, e, f, g, h, i, j, k)
@@ -3031,7 +3030,7 @@ instance (SymVal m, SymVal l, SymVal k, SymVal j, SymVal i, SymVal h, SymVal g,
             => SMTDefinable ((SBV m, SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
   sbv2smt fn = defs2smt $ \p -> fn p .== fn p
 
-  registerSMTFunction fn = registerSMTFunction $ \a b c d e f g h i j k l -> fn (a, b, c, d, e, f, g, h, i, j, k, l)
+  registerFunction fn = registerFunction $ \a b c d e f g h i j k l -> fn (a, b, c, d, e, f, g, h, i, j, k, l)
 
   sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (uc12 <$> mkUncurried uiKind) in \(arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10 arg11
     where uc12 fn a b c d e f g h i j k l = fn (a, b, c, d, e, f, g, h, i, j, k, l)

Data/SBV/Core/Symbolic.hs

@@ -1398,8 +1398,7 @@ newUninterpreted st (nm, mbArgNames) t uiCode
                                                        , "  Name: " ++ nm
                                                        , "  Type: " ++ show t
                                                        , ""
-                                                       , "You should use these functions at least once the query part starts"
-                                                       , "and then use them in the query section as usual."
+                                                       , "You should explicitly register these functions by calling registerFunction before starting the query section."
                                                        ]
                                      pure True
                       UICgC c  -> -- No need to record the code in interactive mode: CodeGen doesn't use interactive

Documentation/SBV/Examples/Puzzles/HexPuzzle.hs

@@ -86,7 +86,7 @@ next b g = ite (readArray g b .== sBlack) g
 -- | Iteratively search at increasing depths of button-presses to see if we can
 -- transform from the initial board position to a final board position.
 search :: [Color] -> [Color] -> IO ()
-search initial final = runSMT $ do registerSMTType (Proxy @SColor)
+search initial final = runSMT $ do registerType (Proxy @SColor)
                                    let emptyGrid = lambdaArray (const sBlack)
                                        initGrid  = foldr (\(i, c) a -> writeArray a (literal i) (literal c)) emptyGrid (zip [1..] initial)
                                    query $ loop (0 :: Int) initGrid []

SBVTestSuite/TestSuite/Basics/UISat.hs

@@ -44,15 +44,15 @@ q2 = uninterpret "q2"
 
 test1 :: ConstraintSet
 test1 = do setLogic Logic_ALL
-           registerSMTFunction q1
+           registerFunction q1
 
 test2 :: ConstraintSet
 test2 = do setLogic Logic_ALL
-           registerSMTFunction q2
+           registerFunction q2
 
 test3 :: ConstraintSet
 test3 = do setLogic Logic_ALL
-           registerSMTFunction q1
-           registerSMTFunction q2
+           registerFunction q1
+           registerFunction q2
 
 {- HLint ignore module "Reduce duplication" -}

SBVTestSuite/TestSuite/Queries/UISatEx.hs

@@ -47,7 +47,7 @@ testQuery2 rf = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=J
   where qCore = do core
                    let q6 :: SInteger -> SBool
                        q6 = uninterpret "q6"
-                   registerSMTFunction q6
+                   registerFunction q6
                    query $ do ensureSat
                               qv1 <- getFunction q1
                               qv2 <- getFunction q2
@@ -79,7 +79,7 @@ core = do x <- sInteger_
           constrain $ q1 (-3) .== 9
           constrain $ q1 x    .== x+1
 
-          registerSMTFunction q2 -- Not really necessary, but testing it doesn't break anything
+          registerFunction q2 -- Not really necessary, but testing it doesn't break anything
           constrain $ q2 sTrue 3   .== 5
           constrain $ q2 sFalse 7  .== 6
           constrain $ q2 sFalse 12 .== 3

SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs

@@ -62,7 +62,7 @@ thingMerge = uninterpret "thingMerge"
 p1 :: Symbolic SBool
 p1 = do constrain $ \(Forall x) -> thingCompare x x
         constrain $ \(Forall k1) (Forall k2) -> k1 ./= thingMerge k1 k2
-        registerSMTFunction thingMerge
+        registerFunction thingMerge
         k1 <- free_
         k2 <- free_
         return $ k1 .== k2 .=> thingCompare k1 k2