sbv-14.4: Data/SBV/Core/Model.hs
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Core.Model
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Instance declarations for our symbolic world
-----------------------------------------------------------------------------
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -Werror -Wno-orphans #-}
module Data.SBV.Core.Model (
Mergeable(..), Equality(..), EqSymbolic(..), OrdSymbolic(..)
, Zero(..), MeasureOf, Measure(..), MeasureHelper(..)
, ContractOf, smtFunction, smtFunctionWithMeasure, smtFunctionWithContract, smtProductiveFunction, smtFunctionNoTermination
, checkMutualGroup
, SDivisible(..), SMTDefinable(..), QSaturate, qSaturateSavingObservables
, Metric(..), minimize, maximize, assertWithPenalty, SIntegral, SFiniteBits(..)
, ite, iteLazy, sFromIntegral, sShiftLeft, sShiftRight, sRotateLeft, sBarrelRotateLeft, sRotateRight, sBarrelRotateRight, sSignedShiftArithRight, (.^)
, some
, oneIf, genVar, genVar_
, pbAtMost, pbAtLeast, pbExactly, pbLe, pbGe, pbEq, pbMutexed, pbStronglyMutexed
, sBool, sBool_, sBools, sWord8, sWord8_, sWord8s, sWord16, sWord16_, sWord16s, sWord32, sWord32_, sWord32s
, sWord64, sWord64_, sWord64s, sInt8, sInt8_, sInt8s, sInt16, sInt16_, sInt16s, sInt32, sInt32_, sInt32s, sInt64, sInt64_
, sInt64s, sInteger, sInteger_, sIntegers, sReal, sReal_, sReals, sFloat, sFloat_, sFloats, sDouble, sDouble_, sDoubles
, sWord, sWord_, sWords, sInt, sInt_, sInts
, sFPHalf, sFPHalf_, sFPHalfs, sFPBFloat, sFPBFloat_, sFPBFloats, sFPSingle, sFPSingle_, sFPSingles, sFPDouble, sFPDouble_, sFPDoubles, sFPQuad, sFPQuad_, sFPQuads, sArray, sArray_, sArrays
, sFloatingPoint, sFloatingPoint_, sFloatingPoints
, sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero
, sRNE, sRNA, sRTP, sRTN, sRTZ
, sChar, sChar_, sChars, sString, sString_, sStrings, sList, sList_, sLists
, sRational, sRational_, sRationals
, SymTuple, sTuple, sTuple_, sTuples
, sSet, sSet_, sSets
, sEDivMod, sEDiv, sEMod
, sDivides
, solve
, slet
, sRealToSInteger, sRealToSIntegerTruncate, label, observe, observeIf, sObserve
, sAssert
, liftQRem, liftDMod, symbolicMergeWithKind
, genLiteral, genFromCV, genMkSymVar
, zeroExtend, signExtend
, sbvQuickCheck
, readArray, writeArray, constArray, freeArray, lambdaArray, listArray
, FromSized, ToSized, FromSizedBV(..), ToSizedBV(..)
, smtHOFunction, smtHOFunctionWithMeasure, Closure(..)
)
where
import Control.Applicative (ZipList(ZipList))
import Control.Monad (when, unless, mplus, replicateM)
import Control.Monad.IO.Class (MonadIO, liftIO)
import qualified Control.Exception as C
import GHC.Generics (M1(..), U1(..), (:*:)(..), K1(..))
import qualified GHC.Generics as G
import GHC.Stack
import GHC.TypeLits hiding(SChar)
import Data.Array (Array, Ix, elems, bounds, rangeSize)
import qualified Data.Array as DA (listArray)
import Data.Bifunctor (first)
import Data.Bits (Bits(..))
import Data.Int (Int8, Int16, Int32, Int64)
import Data.Kind (Type, Constraint)
import Data.List (genericLength, genericIndex, genericTake, unzip4, unzip5, unzip6, unzip7
, intercalate, dropWhileEnd, isPrefixOf, partition, nubBy
#if !MIN_VERSION_base(4,20,0)
, foldl'
#endif
)
import Data.Maybe (fromMaybe, mapMaybe, isJust)
import Data.String (IsString(..))
import Data.Word (Word8, Word16, Word32, Word64)
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NE
import qualified Data.Set as Set
import qualified Data.Graph as DG
import Data.Proxy
import Data.Dynamic (fromDynamic, toDyn, Typeable)
import Test.QuickCheck (Testable(..), Arbitrary(..))
import qualified Test.QuickCheck.Test as QC (isSuccess)
import qualified Test.QuickCheck as QC (quickCheckResult, counterexample)
import qualified Test.QuickCheck.Monadic as QC (monadicIO, run, assert, pre, monitor)
import qualified Data.Foldable as F (toList, for_)
import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq
import qualified Data.Text as T
import Data.SBV.Core.AlgReals
import Data.SBV.Core.Sized
import Data.SBV.Core.SizedFloats
import Data.SBV.Core.Data hiding (Constraint)
import Data.SBV.Core.Symbolic
import Data.SBV.Core.Operations
import Data.SBV.Core.Kind
import Data.SBV.Lambda
import Data.SBV.Utils.ExtractIO (ExtractIO)
import Data.SBV.Provers.Prover (defaultSMTCfg, SafeResult(..), defs2smt, prove, proveWith)
import Data.SBV.SMT.SMT (ThmResult(..), showModel)
import Data.SBV.SMT.Utils (debug)
import Data.SBV.Utils.Numeric (fpIsEqualObjectH)
import Data.IORef (readIORef, writeIORef, modifyIORef')
import System.Mem.StableName (makeStableName, hashStableName)
import Data.SBV.Utils.Lib
import Data.Char
import System.FilePath (dropExtension, takeExtension)
-- Symbolic-Word class instances
import Crypto.Hash.SHA512 (hash)
import qualified Data.ByteString.Base16 as B
import qualified Data.ByteString.Char8 as BC
-- | Generate a variable, named
genVar :: MonadSymbolic m => VarContext -> Kind -> String -> m (SBV a)
genVar q k = mkSymSBV q k . Just
-- | Generate an unnamed variable
genVar_ :: MonadSymbolic m => VarContext -> Kind -> m (SBV a)
genVar_ q k = mkSymSBV q k Nothing
-- | Generate a finite constant bitvector
genLiteral :: Integral a => Kind -> a -> SBV b
genLiteral k = SBV . SVal k . Left . mkConstCV k
-- | Convert a constant to an integral value
genFromCV :: Integral a => CV -> a
genFromCV (CV _ (CInteger x)) = fromInteger x
genFromCV c = error $ "genFromCV: Unsupported non-integral value: " ++ show c
-- | Generalization of 'Data.SBV.genMkSymVar'
genMkSymVar :: MonadSymbolic m => Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar k mbq Nothing = genVar_ mbq k
genMkSymVar k mbq (Just s) = genVar mbq k s
instance SymVal Bool where
mkSymVal = genMkSymVar KBool
literal = SBV . svBool
fromCV = cvToBool
instance SymVal Word8 where
mkSymVal = genMkSymVar (KBounded False 8)
literal = genLiteral (KBounded False 8)
fromCV = genFromCV
instance SymVal Int8 where
mkSymVal = genMkSymVar (KBounded True 8)
literal = genLiteral (KBounded True 8)
fromCV = genFromCV
instance SymVal Word16 where
mkSymVal = genMkSymVar (KBounded False 16)
literal = genLiteral (KBounded False 16)
fromCV = genFromCV
instance SymVal Int16 where
mkSymVal = genMkSymVar (KBounded True 16)
literal = genLiteral (KBounded True 16)
fromCV = genFromCV
instance SymVal Word32 where
mkSymVal = genMkSymVar (KBounded False 32)
literal = genLiteral (KBounded False 32)
fromCV = genFromCV
instance SymVal Int32 where
mkSymVal = genMkSymVar (KBounded True 32)
literal = genLiteral (KBounded True 32)
fromCV = genFromCV
instance SymVal Word64 where
mkSymVal = genMkSymVar (KBounded False 64)
literal = genLiteral (KBounded False 64)
fromCV = genFromCV
instance SymVal Int64 where
mkSymVal = genMkSymVar (KBounded True 64)
literal = genLiteral (KBounded True 64)
fromCV = genFromCV
instance SymVal Integer where
mkSymVal = genMkSymVar KUnbounded
literal = SBV . SVal KUnbounded . Left . mkConstCV KUnbounded
fromCV = genFromCV
minMaxBound = Nothing
instance SymVal Rational where
mkSymVal = genMkSymVar KRational
literal = SBV . SVal KRational . Left . CV KRational . CRational
fromCV (CV _ (CRational r)) = r
fromCV c = error $ "SymVal.Rational: Unexpected non-rational value: " ++ show c
minMaxBound = Nothing
instance SymVal AlgReal where
mkSymVal = genMkSymVar KReal
literal = SBV . SVal KReal . Left . CV KReal . CAlgReal
fromCV (CV _ (CAlgReal a)) = a
fromCV c = error $ "SymVal.AlgReal: Unexpected non-real value: " ++ show c
minMaxBound = Nothing
-- AlgReal needs its own definition of isConcretely
-- to make sure we avoid using unimplementable Haskell functions
isConcretely (SBV (SVal KReal (Left (CV KReal (CAlgReal v))))) p
| isExactRational v = p v
isConcretely _ _ = False
instance SymVal Float where
mkSymVal = genMkSymVar KFloat
literal = SBV . SVal KFloat . Left . CV KFloat . CFloat
fromCV (CV _ (CFloat a)) = a
fromCV c = error $ "SymVal.Float: Unexpected non-float value: " ++ show c
minMaxBound = Nothing
-- For Float, we conservatively return 'False' for isConcretely. The reason is that
-- this function is used for optimizations when only one of the argument is concrete,
-- and in the presence of NaN's it would be incorrect to do any optimization
isConcretely _ _ = False
instance SymVal Double where
mkSymVal = genMkSymVar KDouble
literal = SBV . SVal KDouble . Left . CV KDouble . CDouble
fromCV (CV _ (CDouble a)) = a
fromCV c = error $ "SymVal.Double: Unexpected non-double value: " ++ show c
minMaxBound = Nothing
-- For Double, we conservatively return 'False' for isConcretely. The reason is that
-- this function is used for optimizations when only one of the argument is concrete,
-- and in the presence of NaN's it would be incorrect to do any optimization
isConcretely _ _ = False
instance SymVal RoundingMode where
literal = SBV . svRoundingMode
fromCV c =
case cvAsRoundingMode c of
Just mode -> mode
Nothing -> error $ "SymVal.RoundingMode: Unexpected non-rounding mode value: " ++ show c
-- | Symbolic variant of 'RoundNearestTiesToEven'
sRoundNearestTiesToEven :: SRoundingMode
sRoundNearestTiesToEven = literal RoundNearestTiesToEven
-- | Symbolic variant of 'RoundNearestTiesToAway'
sRoundNearestTiesToAway :: SRoundingMode
sRoundNearestTiesToAway = literal RoundNearestTiesToAway
-- | Symbolic variant of 'RoundTowardPositive'
sRoundTowardPositive :: SRoundingMode
sRoundTowardPositive = literal RoundTowardPositive
-- | Symbolic variant of 'RoundTowardNegative'
sRoundTowardNegative :: SRoundingMode
sRoundTowardNegative = literal RoundTowardNegative
-- | Symbolic variant of 'RoundTowardZero'
sRoundTowardZero :: SRoundingMode
sRoundTowardZero = literal RoundTowardZero
-- | Alias for 'sRoundNearestTiesToEven'
sRNE :: SRoundingMode
sRNE = sRoundNearestTiesToEven
-- | Alias for 'sRoundNearestTiesToAway'
sRNA :: SRoundingMode
sRNA = sRoundNearestTiesToAway
-- | Alias for 'sRoundTowardPositive'
sRTP :: SRoundingMode
sRTP = sRoundTowardPositive
-- | Alias for 'sRoundTowardNegative'
sRTN :: SRoundingMode
sRTN = sRoundTowardNegative
-- | Alias for 'sRoundTowardZero'
sRTZ :: SRoundingMode
sRTZ = sRoundTowardZero
instance SymVal Char where
mkSymVal = genMkSymVar KChar
literal c = SBV . SVal KChar . Left . CV KChar $ CChar c
fromCV (CV _ (CChar a)) = a
fromCV c = error $ "SymVal.String: Unexpected non-char value: " ++ show c
instance SymVal a => SymVal [a] where
mkSymVal
| isKString @[a] undefined = genMkSymVar KString
| True = genMkSymVar (KList (kindOf (Proxy @a)))
literal as
| isKString @[a] undefined = case fromDynamic (toDyn as) of
Just s -> SBV . SVal KString . Left . CV KString . CString $ s
Nothing -> error "SString: Cannot construct literal string!"
| True = let k = KList (kindOf (Proxy @a))
in SBV $ SVal k $ Left $ CV k $ CList $ map toCV as
fromCV (CV _ (CString a)) = fromMaybe (error "SString: Cannot extract a literal string!")
(fromDynamic (toDyn a))
fromCV (CV _ (CList a)) = fromCV . CV (kindOf (Proxy @a)) <$> a
fromCV c = error $ "SymVal.fromCV: Unexpected non-list value: " ++ show c
minMaxBound = Nothing
instance ValidFloat eb sb => HasKind (FloatingPoint eb sb) where
kindOf _ = KFP (intOfProxy (Proxy @eb)) (intOfProxy (Proxy @sb))
instance ValidFloat eb sb => SymVal (FloatingPoint eb sb) where
mkSymVal = genMkSymVar (KFP (intOfProxy (Proxy @eb)) (intOfProxy (Proxy @sb)))
literal (FloatingPoint r) = let k = KFP (intOfProxy (Proxy @eb)) (intOfProxy (Proxy @sb))
in SBV $ SVal k $ Left $ CV k (CFP r)
fromCV (CV _ (CFP r)) = FloatingPoint r
fromCV c = error $ "SymVal.FPR: Unexpected non-arbitrary-precision value: " ++ show c
minMaxBound = Nothing
-- | 'SymVal' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SymVal (WordN n) where
literal x = genLiteral (kindOf x) x
mkSymVal = genMkSymVar (kindOf (undefined :: WordN n))
fromCV = genFromCV
-- | 'SymVal' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SymVal (IntN n) where
literal x = genLiteral (kindOf x) x
mkSymVal = genMkSymVar (kindOf (undefined :: IntN n))
fromCV = genFromCV
toCV :: SymVal a => a -> CVal
toCV a = case literal a of
SBV (SVal _ (Left cv)) -> cvVal cv
_ -> error "SymVal.toCV: Impossible happened, couldn't produce a concrete value"
mkCVTup :: Int -> Kind -> [CVal] -> SBV a
mkCVTup i k@(KTuple ks) cs
| lks == lcs && lks == i
= SBV $ SVal k $ Left $ CV k $ CTuple cs
| True
= error $ "SymVal.mkCVTup: Impossible happened. Malformed tuple received: " ++ show (i, k)
where lks = length ks
lcs = length cs
mkCVTup i k _
= error $ "SymVal.mkCVTup: Impossible happened. Non-tuple received: " ++ show (i, k)
fromCVTup :: Int -> CV -> [CV]
fromCVTup i inp@(CV (KTuple ks) (CTuple cs))
| lks == lcs && lks == i
= zipWith CV ks cs
| True
= error $ "SymVal.fromCTup: Impossible happened. Malformed tuple received: " ++ show (i, inp)
where lks = length ks
lcs = length cs
fromCVTup i inp = error $ "SymVal.fromCVTup: Impossible happened. Non-tuple received: " ++ show (i, inp)
instance (HasKind a, HasKind b, SymVal a, SymVal b) => SymVal (ArrayModel a b) where
mkSymVal = genMkSymVar (KArray (kindOf (Proxy @a)) (kindOf (Proxy @b)))
-- If the table has duplicate entries for keys, then the first one takes precedence.
-- That is, [(a, v1), (a, v2)] is equivalent to [(a, v1)]. The best way to think about
-- this is as a "stack" of writes. [(a, v1), (a, v2)] means we first "wrote" v2 at
-- a, and then wrote v1 at the same address; so the first write of v2 got overwritten.
literal (ArrayModel tbl def) = SBV . SVal knd . Left . CV knd $ CArray $ ArrayModel [(toCV k, toCV v) | (k, v) <- tbl] (toCV def)
where knd = kindOf (Proxy @(ArrayModel a b))
fromCV (CV (KArray k1 k2) (CArray (ArrayModel assocs def))) = ArrayModel [(fromCV (CV k1 a), fromCV (CV k2 b)) | (a, b) <- assocs]
(fromCV (CV k2 def))
fromCV bad = error $ "SymVal.fromCV (SArray): Malformed array received: " ++ show bad
minMaxBound = Nothing
instance (Arbitrary a, Arbitrary b) => Arbitrary (ArrayModel a b) where
arbitrary = ArrayModel <$> arbitrary <*> arbitrary
instance (Ord a, SymVal a) => SymVal (RCSet a) where
mkSymVal = genMkSymVar (kindOf (Proxy @(RCSet a)))
literal eur = SBV $ SVal k $ Left $ CV k $ CSet $ dir $ Set.map toCV s
where (dir, s) = case eur of
RegularSet x -> (RegularSet, x)
ComplementSet x -> (ComplementSet, x)
k = kindOf (Proxy @(RCSet a))
fromCV (CV (KSet a) (CSet (RegularSet s))) = RegularSet $ Set.map (fromCV . CV a) s
fromCV (CV (KSet a) (CSet (ComplementSet s))) = ComplementSet $ Set.map (fromCV . CV a) s
fromCV bad = error $ "SymVal.fromCV (Set): Malformed set received: " ++ show bad
minMaxBound = Nothing
-- | SymVal for 0-tuple (i.e., unit)
instance SymVal () where
mkSymVal = genMkSymVar (KTuple [])
literal () = mkCVTup 0 (kindOf (Proxy @())) []
fromCV cv = fromCVTup 0 cv `seq` ()
-- | SymVal for 2-tuples
instance (SymVal a, SymVal b) => SymVal (a, b) where
mkSymVal = genMkSymVar (kindOf (Proxy @(a, b)))
literal (v1, v2) = mkCVTup 2 (kindOf (Proxy @(a, b))) [toCV v1, toCV v2]
fromCV cv = case fromCVTup 2 cv of
[v1, v2] -> (fromCV v1, fromCV v2)
res -> error $ "Data.SBV.SymVal-Tuple2: Unexpected result: " ++ show res
minMaxBound = Nothing
-- | SymVal for 3-tuples
instance (SymVal a, SymVal b, SymVal c) => SymVal (a, b, c) where
mkSymVal = genMkSymVar (kindOf (Proxy @(a, b, c)))
literal (v1, v2, v3) = mkCVTup 3 (kindOf (Proxy @(a, b, c))) [toCV v1, toCV v2, toCV v3]
fromCV cv = case fromCVTup 3 cv of
[v1, v2, v3] -> (fromCV v1, fromCV v2, fromCV v3)
res -> error $ "Data.SBV.SymVal-Tuple3: Unexpected result: " ++ show res
minMaxBound = Nothing
-- | SymVal for 4-tuples
instance (SymVal a, SymVal b, SymVal c, SymVal d) => SymVal (a, b, c, d) where
mkSymVal = genMkSymVar (kindOf (Proxy @(a, b, c, d)))
literal (v1, v2, v3, v4) = mkCVTup 4 (kindOf (Proxy @(a, b, c, d))) [toCV v1, toCV v2, toCV v3, toCV v4]
fromCV cv = case fromCVTup 4 cv of
[v1, v2, v3, v4] -> (fromCV v1, fromCV v2, fromCV v3, fromCV v4)
res -> error $ "Data.SBV.SymVal-Tuple4: Unexpected result: " ++ show res
minMaxBound = Nothing
-- | SymVal for 5-tuples
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e) => SymVal (a, b, c, d, e) where
mkSymVal = genMkSymVar (kindOf (Proxy @(a, b, c, d, e)))
literal (v1, v2, v3, v4, v5) = mkCVTup 5 (kindOf (Proxy @(a, b, c, d, e))) [toCV v1, toCV v2, toCV v3, toCV v4, toCV v5]
fromCV cv = case fromCVTup 5 cv of
[v1, v2, v3, v4, v5] -> (fromCV v1, fromCV v2, fromCV v3, fromCV v4, fromCV v5)
res -> error $ "Data.SBV.SymVal-Tuple5: Unexpected result: " ++ show res
minMaxBound = Nothing
-- | SymVal for 6-tuples
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f) => SymVal (a, b, c, d, e, f) where
mkSymVal = genMkSymVar (kindOf (Proxy @(a, b, c, d, e, f)))
literal (v1, v2, v3, v4, v5, v6) = mkCVTup 6 (kindOf (Proxy @(a, b, c, d, e, f))) [toCV v1, toCV v2, toCV v3, toCV v4, toCV v5, toCV v6]
fromCV cv = case fromCVTup 6 cv of
[v1, v2, v3, v4, v5, v6] -> (fromCV v1, fromCV v2, fromCV v3, fromCV v4, fromCV v5, fromCV v6)
res -> error $ "Data.SBV.SymVal-Tuple6: Unexpected result: " ++ show res
minMaxBound = Nothing
-- | SymVal for 7-tuples
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g) => SymVal (a, b, c, d, e, f, g) where
mkSymVal = genMkSymVar (kindOf (Proxy @(a, b, c, d, e, f, g)))
literal (v1, v2, v3, v4, v5, v6, v7) = mkCVTup 7 (kindOf (Proxy @(a, b, c, d, e, f, g))) [toCV v1, toCV v2, toCV v3, toCV v4, toCV v5, toCV v6, toCV v7]
fromCV cv = case fromCVTup 7 cv of
[v1, v2, v3, v4, v5, v6, v7] -> (fromCV v1, fromCV v2, fromCV v3, fromCV v4, fromCV v5, fromCV v6, fromCV v7)
res -> error $ "Data.SBV.SymVal-Tuple7: Unexpected result: " ++ show res
minMaxBound = Nothing
-- | SymVal for 8-tuples
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h) => SymVal (a, b, c, d, e, f, g, h) where
mkSymVal = genMkSymVar (kindOf (Proxy @(a, b, c, d, e, f, g, h)))
literal (v1, v2, v3, v4, v5, v6, v7, v8) = mkCVTup 8 (kindOf (Proxy @(a, b, c, d, e, f, g, h))) [toCV v1, toCV v2, toCV v3, toCV v4, toCV v5, toCV v6, toCV v7, toCV v8]
fromCV cv = case fromCVTup 8 cv of
[v1, v2, v3, v4, v5, v6, v7, v8] -> (fromCV v1, fromCV v2, fromCV v3, fromCV v4, fromCV v5, fromCV v6, fromCV v7, fromCV v8)
res -> error $ "Data.SBV.SymVal-Tuple8: Unexpected result: " ++ show res
minMaxBound = Nothing
instance IsString SString where
fromString = literal
------------------------------------------------------------------------------------
-- * Smart constructors for creating symbolic values. These are not strictly
-- necessary, as they are mere aliases for 'symbolic' and 'symbolics', but
-- they nonetheless make programming easier.
------------------------------------------------------------------------------------
-- | Generalization of 'Data.SBV.sBool'
sBool :: MonadSymbolic m => String -> m SBool
sBool = symbolic
-- | Generalization of 'Data.SBV.sBool_'
sBool_ :: MonadSymbolic m => m SBool
sBool_ = free_
-- | Generalization of 'Data.SBV.sBools'
sBools :: MonadSymbolic m => [String] -> m [SBool]
sBools = symbolics
-- | Generalization of 'Data.SBV.sWord8'
sWord8 :: MonadSymbolic m => String -> m SWord8
sWord8 = symbolic
-- | Generalization of 'Data.SBV.sWord8_'
sWord8_ :: MonadSymbolic m => m SWord8
sWord8_ = free_
-- | Generalization of 'Data.SBV.sWord8s'
sWord8s :: MonadSymbolic m => [String] -> m [SWord8]
sWord8s = symbolics
-- | Generalization of 'Data.SBV.sWord16'
sWord16 :: MonadSymbolic m => String -> m SWord16
sWord16 = symbolic
-- | Generalization of 'Data.SBV.sWord16_'
sWord16_ :: MonadSymbolic m => m SWord16
sWord16_ = free_
-- | Generalization of 'Data.SBV.sWord16s'
sWord16s :: MonadSymbolic m => [String] -> m [SWord16]
sWord16s = symbolics
-- | Generalization of 'Data.SBV.sWord32'
sWord32 :: MonadSymbolic m => String -> m SWord32
sWord32 = symbolic
-- | Generalization of 'Data.SBV.sWord32_'
sWord32_ :: MonadSymbolic m => m SWord32
sWord32_ = free_
-- | Generalization of 'Data.SBV.sWord32s'
sWord32s :: MonadSymbolic m => [String] -> m [SWord32]
sWord32s = symbolics
-- | Generalization of 'Data.SBV.sWord64'
sWord64 :: MonadSymbolic m => String -> m SWord64
sWord64 = symbolic
-- | Generalization of 'Data.SBV.sWord64_'
sWord64_ :: MonadSymbolic m => m SWord64
sWord64_ = free_
-- | Generalization of 'Data.SBV.sWord64s'
sWord64s :: MonadSymbolic m => [String] -> m [SWord64]
sWord64s = symbolics
-- | Generalization of 'Data.SBV.sInt8'
sInt8 :: MonadSymbolic m => String -> m SInt8
sInt8 = symbolic
-- | Generalization of 'Data.SBV.sInt8_'
sInt8_ :: MonadSymbolic m => m SInt8
sInt8_ = free_
-- | Generalization of 'Data.SBV.sInt8s'
sInt8s :: MonadSymbolic m => [String] -> m [SInt8]
sInt8s = symbolics
-- | Generalization of 'Data.SBV.sInt16'
sInt16 :: MonadSymbolic m => String -> m SInt16
sInt16 = symbolic
-- | Generalization of 'Data.SBV.sInt16_'
sInt16_ :: MonadSymbolic m => m SInt16
sInt16_ = free_
-- | Generalization of 'Data.SBV.sInt16s'
sInt16s :: MonadSymbolic m => [String] -> m [SInt16]
sInt16s = symbolics
-- | Generalization of 'Data.SBV.sInt32'
sInt32 :: MonadSymbolic m => String -> m SInt32
sInt32 = symbolic
-- | Generalization of 'Data.SBV.sInt32_'
sInt32_ :: MonadSymbolic m => m SInt32
sInt32_ = free_
-- | Generalization of 'Data.SBV.sInt32s'
sInt32s :: MonadSymbolic m => [String] -> m [SInt32]
sInt32s = symbolics
-- | Generalization of 'Data.SBV.sInt64'
sInt64 :: MonadSymbolic m => String -> m SInt64
sInt64 = symbolic
-- | Generalization of 'Data.SBV.sInt64_'
sInt64_ :: MonadSymbolic m => m SInt64
sInt64_ = free_
-- | Generalization of 'Data.SBV.sInt64s'
sInt64s :: MonadSymbolic m => [String] -> m [SInt64]
sInt64s = symbolics
-- | Generalization of 'Data.SBV.sInteger'
sInteger:: MonadSymbolic m => String -> m SInteger
sInteger = symbolic
-- | Generalization of 'Data.SBV.sInteger_'
sInteger_:: MonadSymbolic m => m SInteger
sInteger_ = free_
-- | Generalization of 'Data.SBV.sIntegers'
sIntegers :: MonadSymbolic m => [String] -> m [SInteger]
sIntegers = symbolics
-- | Generalization of 'Data.SBV.sReal'
sReal:: MonadSymbolic m => String -> m SReal
sReal = symbolic
-- | Generalization of 'Data.SBV.sReal_'
sReal_:: MonadSymbolic m => m SReal
sReal_ = free_
-- | Generalization of 'Data.SBV.sReals'
sReals :: MonadSymbolic m => [String] -> m [SReal]
sReals = symbolics
-- | Generalization of 'Data.SBV.sFloat'
sFloat :: MonadSymbolic m => String -> m SFloat
sFloat = symbolic
-- | Generalization of 'Data.SBV.sFloat_'
sFloat_ :: MonadSymbolic m => m SFloat
sFloat_ = free_
-- | Generalization of 'Data.SBV.sFloats'
sFloats :: MonadSymbolic m => [String] -> m [SFloat]
sFloats = symbolics
-- | Generalization of 'Data.SBV.sDouble'
sDouble :: MonadSymbolic m => String -> m SDouble
sDouble = symbolic
-- | Generalization of 'Data.SBV.sDouble_'
sDouble_ :: MonadSymbolic m => m SDouble
sDouble_ = free_
-- | Generalization of 'Data.SBV.sDoubles'
sDoubles :: MonadSymbolic m => [String] -> m [SDouble]
sDoubles = symbolics
-- | Generalization of 'Data.SBV.sFPHalf'
sFPHalf :: String -> Symbolic SFPHalf
sFPHalf = symbolic
-- | Generalization of 'Data.SBV.sFPHalf_'
sFPHalf_ :: Symbolic SFPHalf
sFPHalf_ = free_
-- | Generalization of 'Data.SBV.sFPHalfs'
sFPHalfs :: [String] -> Symbolic [SFPHalf]
sFPHalfs = symbolics
-- | Generalization of 'Data.SBV.sFPBFloat'
sFPBFloat :: String -> Symbolic SFPBFloat
sFPBFloat = symbolic
-- | Generalization of 'Data.SBV.sFPBFloat_'
sFPBFloat_ :: Symbolic SFPBFloat
sFPBFloat_ = free_
-- | Generalization of 'Data.SBV.sFPBFloats'
sFPBFloats :: [String] -> Symbolic [SFPBFloat]
sFPBFloats = symbolics
-- | Generalization of 'Data.SBV.sFPSingle'
sFPSingle :: String -> Symbolic SFPSingle
sFPSingle = symbolic
-- | Generalization of 'Data.SBV.sFPSingle_'
sFPSingle_ :: Symbolic SFPSingle
sFPSingle_ = free_
-- | Generalization of 'Data.SBV.sFPSingles'
sFPSingles :: [String] -> Symbolic [SFPSingle]
sFPSingles = symbolics
-- | Generalization of 'Data.SBV.sFPDouble'
sFPDouble :: String -> Symbolic SFPDouble
sFPDouble = symbolic
-- | Generalization of 'Data.SBV.sFPDouble_'
sFPDouble_ :: Symbolic SFPDouble
sFPDouble_ = free_
-- | Generalization of 'Data.SBV.sFPDoubles'
sFPDoubles :: [String] -> Symbolic [SFPDouble]
sFPDoubles = symbolics
-- | Generalization of 'Data.SBV.sFPQuad'
sFPQuad :: String -> Symbolic SFPQuad
sFPQuad = symbolic
-- | Generalization of 'Data.SBV.sFPQuad_'
sFPQuad_ :: Symbolic SFPQuad
sFPQuad_ = free_
-- | Generalization of 'Data.SBV.sFPQuads'
sFPQuads :: [String] -> Symbolic [SFPQuad]
sFPQuads = symbolics
-- | Generalization of 'Data.SBV.sFloatingPoint'
sFloatingPoint :: ValidFloat eb sb => String -> Symbolic (SFloatingPoint eb sb)
sFloatingPoint = symbolic
-- | Generalization of 'Data.SBV.sFloatingPoint_'
sFloatingPoint_ :: ValidFloat eb sb => Symbolic (SFloatingPoint eb sb)
sFloatingPoint_ = free_
-- | Generalization of 'Data.SBV.sFloatingPoints'
sFloatingPoints :: ValidFloat eb sb => [String] -> Symbolic [SFloatingPoint eb sb]
sFloatingPoints = symbolics
-- | Generalization of 'Data.SBV.sWord'
sWord :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SWord n)
sWord = symbolic
-- | Generalization of 'Data.SBV.sWord_'
sWord_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SWord n)
sWord_ = free_
-- | Generalization of 'Data.SBV.sWord64s'
sWords :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SWord n]
sWords = symbolics
-- | Generalization of 'Data.SBV.sInt'
sInt :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SInt n)
sInt = symbolic
-- | Generalization of 'Data.SBV.sInt_'
sInt_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SInt n)
sInt_ = free_
-- | Generalization of 'Data.SBV.sInts'
sInts :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SInt n]
sInts = symbolics
-- | Generalization of 'Data.SBV.sChar'
sChar :: MonadSymbolic m => String -> m SChar
sChar = symbolic
-- | Generalization of 'Data.SBV.sChar_'
sChar_ :: MonadSymbolic m => m SChar
sChar_ = free_
-- | Generalization of 'Data.SBV.sChars'
sChars :: MonadSymbolic m => [String] -> m [SChar]
sChars = symbolics
-- | Generalization of 'Data.SBV.sString'
sString :: MonadSymbolic m => String -> m SString
sString = symbolic
-- | Generalization of 'Data.SBV.sString_'
sString_ :: MonadSymbolic m => m SString
sString_ = free_
-- | Generalization of 'Data.SBV.sStrings'
sStrings :: MonadSymbolic m => [String] -> m [SString]
sStrings = symbolics
-- | Generalization of 'Data.SBV.sList'
sList :: (SymVal a, MonadSymbolic m) => String -> m (SList a)
sList = symbolic
-- | Generalization of 'Data.SBV.sList_'
sList_ :: (SymVal a, MonadSymbolic m) => m (SList a)
sList_ = free_
-- | Generalization of 'Data.SBV.sLists'
sLists :: (SymVal a, MonadSymbolic m) => [String] -> m [SList a]
sLists = symbolics
-- | Generalization of 'Data.SBV.sAray'
sArray :: (SymVal a, SymVal b, MonadSymbolic m) => String -> m (SArray a b)
sArray = symbolic
-- | Generalization of 'Data.SBV.sList_'
sArray_ :: (SymVal a, SymVal b, MonadSymbolic m) => m (SArray a b)
sArray_ = free_
-- | Generalization of 'Data.SBV.sLists'
sArrays :: (SymVal a, SymVal b, MonadSymbolic m) => [String] -> m [SArray a b]
sArrays = symbolics
-- | Identify tuple like things. Note that there are no methods, just instances to control type inference
class SymTuple a
instance SymTuple ()
instance SymTuple (a, b)
instance SymTuple (a, b, c)
instance SymTuple (a, b, c, d)
instance SymTuple (a, b, c, d, e)
instance SymTuple (a, b, c, d, e, f)
instance SymTuple (a, b, c, d, e, f, g)
instance SymTuple (a, b, c, d, e, f, g, h)
-- | Generalization of 'Data.SBV.sTuple'
sTuple :: (SymTuple tup, SymVal tup, MonadSymbolic m) => String -> m (SBV tup)
sTuple = symbolic
-- | Generalization of 'Data.SBV.sTuple_'
sTuple_ :: (SymTuple tup, SymVal tup, MonadSymbolic m) => m (SBV tup)
sTuple_ = free_
-- | Generalization of 'Data.SBV.sTuples'
sTuples :: (SymTuple tup, SymVal tup, MonadSymbolic m) => [String] -> m [SBV tup]
sTuples = symbolics
-- | Generalization of 'Data.SBV.sRational'
sRational :: MonadSymbolic m => String -> m SRational
sRational = symbolic
-- | Generalization of 'Data.SBV.sRational_'
sRational_ :: MonadSymbolic m => m SRational
sRational_ = free_
-- | Generalization of 'Data.SBV.sRationals'
sRationals :: MonadSymbolic m => [String] -> m [SRational]
sRationals = symbolics
-- | Generalization of 'Data.SBV.sSet'
sSet :: (Ord a, SymVal a, MonadSymbolic m) => String -> m (SSet a)
sSet = symbolic
-- | Generalization of 'Data.SBV.sMaybe_'
sSet_ :: (Ord a, SymVal a, MonadSymbolic m) => m (SSet a)
sSet_ = free_
-- | Generalization of 'Data.SBV.sMaybes'
sSets :: (Ord a, SymVal a, MonadSymbolic m) => [String] -> m [SSet a]
sSets = symbolics
-- | Generalization of 'Data.SBV.solve'
solve :: MonadSymbolic m => [SBool] -> m SBool
solve = pure . sAnd
-- | Convert an SReal to an SInteger. That is, it computes the
-- largest integer @n@ that satisfies @sIntegerToSReal n <= r@
-- essentially giving us the @floor@.
--
-- For instance, @1.3@ will be @1@, but @-1.3@ will be @-2@.
sRealToSInteger :: SReal -> SInteger
sRealToSInteger x
| Just i <- unliteral x, isExactRational i
= literal $ floor (toRational i)
| True
= SBV (SVal KUnbounded (Right (cache y)))
where y st = do xsv <- sbvToSV st x
newExpr st KUnbounded (SBVApp (KindCast KReal KUnbounded) [xsv])
-- | Convert an SReal to an SInteger, truncating version. Truncate simply chops of the
-- fractional part, essentially rounding towards zero.
sRealToSIntegerTruncate :: SReal -> SInteger
sRealToSIntegerTruncate x = ite (x .>= 0) (sRealToSInteger x) (- sRealToSInteger (-x))
-- | label: Label the result of an expression. This is essentially a no-op, but useful as it generates a comment in the generated C/SMT-Lib code.
-- Note that if the argument is a constant, then the label is dropped completely, per the usual constant folding strategy. Compare this to 'observe'
-- which is good for printing counter-examples.
label :: SymVal a => String -> SBV a -> SBV a
label m x
| Just _ <- unliteral x = x
| True = SBV $ SVal k $ Right $ cache r
where k = kindOf x
r st = do xsv <- sbvToSV st x
newExpr st k (SBVApp (Label m) [xsv])
-- | Observe the value of an expression, if the given condition holds. Such values are useful in model construction, as they are printed part of a satisfying model, or a
-- counter-example. The same works for quick-check as well. Useful when we want to see intermediate values, or expected/obtained
-- pairs in a particular run. Note that an observed expression is always symbolic, i.e., it won't be constant folded. Compare this to 'label'
-- which is used for putting a label in the generated SMTLib-C code.
--
-- NB. If the observed expression happens under a SBV-lambda expression, then it is silently ignored; since
-- there's no way to access the value of such a value.
observeIf :: SymVal a => (a -> Bool) -> String -> SBV a -> SBV a
observeIf cond m x
| Just bad <- checkObservableName m
= error bad
| True
= SBV $ SVal k $ Right $ cache r
where k = kindOf x
r st = do xsv <- sbvToSV st (label ("Observing: " ++ m) x)
recordObservable st (T.pack m) (cond . fromCV) xsv
pure xsv
-- | Observe the value of an expression, unconditionally. See 'observeIf' for a generalized version.
observe :: SymVal a => String -> SBV a -> SBV a
observe = observeIf (const True)
-- | Symbolic Comparisons. Similar to 'Eq', we cannot implement Haskell's 'Ord' class
-- since there is no way to return an 'Ordering' value from a symbolic comparison.
-- Furthermore, 'OrdSymbolic' requires 'Mergeable' to implement if-then-else, for the
-- benefit of implementing symbolic versions of 'max' and 'min' functions.
infix 4 .<, .<=, .>, .>=
class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
-- | Symbolic less than.
(.<) :: a -> a -> SBool
-- | Symbolic less than or equal to.
(.<=) :: a -> a -> SBool
-- | Symbolic greater than.
(.>) :: a -> a -> SBool
-- | Symbolic greater than or equal to.
(.>=) :: a -> a -> SBool
-- | Symbolic minimum.
smin :: a -> a -> a
-- | Symbolic maximum.
smax :: a -> a -> a
-- | Is the value within the allowed /inclusive/ range?
inRange :: a -> (a, a) -> SBool
{-# MINIMAL (.<) #-}
a .<= b = a .< b .|| a .== b
a .> b = b .< a
a .>= b = b .<= a
a `smin` b = ite (a .<= b) a b
a `smax` b = ite (a .<= b) b a
inRange x (y, z) = x .>= y .&& x .<= z
{- We can't have a generic instance of the form:
instance Eq a => EqSymbolic a where
x .== y = if x == y then true else sFalse
even if we're willing to allow Flexible/undecidable instances..
This is because if we allow this it would imply EqSymbolic (SBV a);
since (SBV a) has to be Eq as it must be a Num. But this wouldn't be
the right choice obviously; as the Eq instance is bogus for SBV
for natural reasons..
-}
-- It is tempting to put in an @Eq a@ superclass here. But doing so
-- is complicated, as it requires all underlying types to have equality,
-- which is at best shaky for algebraic reals and sets. So, leave it out.
instance (HasKind a, SymVal a) => EqSymbolic (SBV a) where
SBV x .== SBV y = SBV (svEqual x y)
SBV x ./= SBV y = SBV (svNotEqual x y)
SBV x .=== SBV y = SBV (svStrongEqual x y)
-- Custom version of distinct that generates better code for base types
distinct [] = sTrue
distinct [_] = sTrue
distinct xs | all isConc xs = checkDiff xs
| [SBV a, SBV b] <- xs, a `is` svBool True = SBV $ svNot b
| [SBV a, SBV b] <- xs, b `is` svBool True = SBV $ svNot a
| [SBV a, SBV b] <- xs, a `is` svBool False = SBV b
| [SBV a, SBV b] <- xs, b `is` svBool False = SBV a
-- 3 booleans can't be distinct!
| (x : _ : _ : _) <- xs, isBool x = sFalse
| True = SBV (SVal KBool (Right (cache r)))
where r st = do xsv <- mapM (sbvToSV st) xs
newExpr st KBool (SBVApp NotEqual xsv)
-- We call this in case all are concrete, which will
-- reduce to a constant and generate no code at all!
-- Note that this is essentially the same as the default
-- definition, which unfortunately we can no longer call!
checkDiff [] = sTrue
checkDiff (a:as) = sAll (a ./=) as .&& checkDiff as
-- Sigh, we can't use isConcrete since that requires SymVal
-- constraint that we don't have here. (To support SBools.)
isConc (SBV (SVal _ (Left _))) = True
isConc _ = False
-- Likewise here; need to go lower.
SVal k1 (Left c1) `is` SVal k2 (Left c2) = (k1, c1) == (k2, c2)
_ `is` _ = False
isBool (SBV (SVal KBool _)) = True
isBool _ = False
-- Custom version of distinctExcept that generates better code for base types
distinctExcept [] _ = sTrue
distinctExcept [_] _ = sTrue
distinctExcept es ignored
| all isConc (es ++ ignored)
= distinct (filter ignoreConc es)
| True
= SBV (SVal KBool (Right (cache r)))
where ignoreConc x = case x `sElem` ignored of
SBV (SVal KBool (Left cv)) -> cvToBool cv
_ -> error $ "distinctExcept: Impossible happened, concrete sElem failed: " ++ show (es, ignored, x)
r st = do let incr x table = ite (x `sElem` ignored) (0 :: SInteger) (1 + readArrayNoEq table x)
initArray :: SArray a Integer
initArray = constArray 0
finalArray = foldl' (\table x -> writeArrayNoKnd table x (incr x table)) initArray es
sbvToSV st $ sAll (\e -> readArrayNoEq finalArray e .<= (1 :: SInteger)) es
-- Sigh, we can't use isConcrete since that requires SymVal
-- constraint that we don't have here. (To support SBools.)
isConc (SBV (SVal _ (Left _))) = True
isConc _ = False
-- Version of readArray that doesn't have the Eq constraint, since we don't have it here
readArrayNoEq array key = SBV . SVal KUnbounded . Right $ cache g
where g st = do f <- sbvToSV st array
k <- sbvToSV st key
newExpr st KUnbounded (SBVApp ReadArray [f, k])
writeArrayNoKnd :: forall key. HasKind key => SArray key Integer -> SBV key -> SInteger -> SArray key Integer
writeArrayNoKnd array key value = SBV . SVal k . Right $ cache g
where k = KArray (kindOf (Proxy @key)) KUnbounded
g st = do arr <- sbvToSV st array
keyVal <- sbvToSV st key
val <- sbvToSV st value
newExpr st k (SBVApp WriteArray [arr, keyVal, val])
-- We don't want to do a generic OrdSymbolic (SBV a) instance; since that would be dangerous, like the case
-- for Num. So, we explicitly define for each type we care about.
#define MKSORD(CSTR, TYPE) \
instance CSTR => OrdSymbolic TYPE where { \
a@(SBV x) .< b@(SBV y) | smtComparable "<" a b = SBV (svLessThan x y) \
| True = SBV (svStructuralLessThan x y); \
\
a@(SBV x) .<= b@(SBV y) | smtComparable ".<=" a b = SBV (svLessEq x y) \
| True = a .< b .|| a .== b; \
\
a@(SBV x) .> b@(SBV y) | smtComparable ">" a b = SBV (svGreaterThan x y) \
| True = b .< a; \
\
a@(SBV x) .>= b@(SBV y) | smtComparable ">=" a b = SBV (svGreaterEq x y) \
| True = b .<= a; \
} \
-- Derive basic instances we need. NB. We don't give the SRational instance here. It's handled
-- in Data/SBV/Rational due to representation issues.
MKSORD((), SInteger)
MKSORD((), SWord8)
MKSORD((), SWord16)
MKSORD((), SWord32)
MKSORD((), SWord64)
MKSORD((), SInt8)
MKSORD((), SInt16)
MKSORD((), SInt32)
MKSORD((), SInt64)
MKSORD((), SFloat)
MKSORD((), SChar)
MKSORD((SymVal a), (SList a))
MKSORD((), SDouble)
MKSORD((), SReal)
MKSORD((KnownNat n, BVIsNonZero n), (SWord n))
MKSORD((KnownNat n, BVIsNonZero n), (SInt n))
MKSORD((ValidFloat eb sb), (SFloatingPoint eb sb))
-- Tuples
MKSORD((SymVal a, SymVal b), (SBV (a, b)))
MKSORD((SymVal a, SymVal b, SymVal c), (SBV (a, b, c)))
MKSORD((SymVal a, SymVal b, SymVal c, SymVal d), (SBV (a, b, c, d)))
MKSORD((SymVal a, SymVal b, SymVal c, SymVal d, SymVal e), (SBV (a, b, c, d, e)))
MKSORD((SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f), (SBV (a, b, c, d, e, f)))
MKSORD((SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g), (SBV (a, b, c, d, e, f, g)))
MKSORD((SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h), (SBV (a, b, c, d, e, f, g, h)))
#undef MKSORD
-- Is this a type that's comparable by underlying translation to SMTLib?
-- Note that we allow concrete versions to go through unless the type is a set, as there's really no reason not to.
smtComparable :: (SymVal a, HasKind a) => String -> SBV a -> SBV a -> Bool
smtComparable op x y
| isConcrete x && isConcrete y && not (isSet k)
= True
| True
= case k of
KVar {} -> False
KBool -> True
KBounded {} -> True
KUnbounded {} -> True
KReal {} -> True
KApp {} -> True
KADT {} -> True
KFloat -> True
KDouble -> True
KRational {} -> True
KFP {} -> True
KChar -> True
KString -> True
KList {} -> nope -- Unfortunately, no way for us to desugar this
KSet {} -> nope -- Ditto here..
KTuple {} -> False
KArray {} -> True
where k = kindOf x
nope = error $ "Data.SBV.OrdSymbolic: SMTLib does not support " ++ op ++ " for " ++ show k
-- Bool
instance EqSymbolic Bool where
x .== y = fromBool $ x == y
-- Lists
instance EqSymbolic a => EqSymbolic [a] where
[] .== [] = sTrue
(x:xs) .== (y:ys) = x .== y .&& xs .== ys
_ .== _ = sFalse
[] .=== [] = sTrue
(x:xs) .=== (y:ys) = x .=== y .&& xs .=== ys
_ .=== _ = sFalse
instance OrdSymbolic a => OrdSymbolic [a] where
[] .< [] = sFalse
[] .< _ = sTrue
_ .< [] = sFalse
(x:xs) .< (y:ys) = x .< y .|| (x .== y .&& xs .< ys)
-- NonEmpty
instance EqSymbolic a => EqSymbolic (NonEmpty a) where
(x :| xs) .== (y :| ys) = x : xs .== y : ys
(x :| xs) .=== (y :| ys) = x : xs .=== y : ys
instance OrdSymbolic a => OrdSymbolic (NonEmpty a) where
(x :| xs) .< (y :| ys) = x : xs .< y : ys
-- Maybe
instance EqSymbolic a => EqSymbolic (Maybe a) where
Nothing .== Nothing = sTrue
Just a .== Just b = a .== b
_ .== _ = sFalse
instance OrdSymbolic a => OrdSymbolic (Maybe a) where
Nothing .< Nothing = sFalse
Nothing .< _ = sTrue
Just _ .< Nothing = sFalse
Just a .< Just b = a .< b
-- Either
instance (EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) where
Left a .== Left b = a .== b
Right a .== Right b = a .== b
_ .== _ = sFalse
Left a .=== Left b = a .=== b
Right a .=== Right b = a .=== b
_ .=== _ = sFalse
instance (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) where
Left a .< Left b = a .< b
Left _ .< Right _ = sTrue
Right _ .< Left _ = sFalse
Right a .< Right b = a .< b
-- 2-Tuple
instance (EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) where
(a0, b0) .== (a1, b1) = a0 .== a1 .&& b0 .== b1
(a0, b0) .=== (a1, b1) = a0 .=== a1 .&& b0 .=== b1
instance (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) where
(a0, b0) .< (a1, b1) = a0 .< a1 .|| (a0 .== a1 .&& b0 .< b1)
-- 3-Tuple
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) where
(a0, b0, c0) .== (a1, b1, c1) = (a0, b0) .== (a1, b1) .&& c0 .== c1
(a0, b0, c0) .=== (a1, b1, c1) = (a0, b0) .=== (a1, b1) .&& c0 .=== c1
instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) where
(a0, b0, c0) .< (a1, b1, c1) = (a0, b0) .< (a1, b1) .|| ((a0, b0) .== (a1, b1) .&& c0 .< c1)
-- 4-Tuple
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) where
(a0, b0, c0, d0) .== (a1, b1, c1, d1) = (a0, b0, c0) .== (a1, b1, c1) .&& d0 .== d1
(a0, b0, c0, d0) .=== (a1, b1, c1, d1) = (a0, b0, c0) .=== (a1, b1, c1) .&& d0 .=== d1
instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) where
(a0, b0, c0, d0) .< (a1, b1, c1, d1) = (a0, b0, c0) .< (a1, b1, c1) .|| ((a0, b0, c0) .== (a1, b1, c1) .&& d0 .< d1)
-- 5-Tuple
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) where
(a0, b0, c0, d0, e0) .== (a1, b1, c1, d1, e1) = (a0, b0, c0, d0) .== (a1, b1, c1, d1) .&& e0 .== e1
(a0, b0, c0, d0, e0) .=== (a1, b1, c1, d1, e1) = (a0, b0, c0, d0) .=== (a1, b1, c1, d1) .&& e0 .=== e1
instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) where
(a0, b0, c0, d0, e0) .< (a1, b1, c1, d1, e1) = (a0, b0, c0, d0) .< (a1, b1, c1, d1) .|| ((a0, b0, c0, d0) .== (a1, b1, c1, d1) .&& e0 .< e1)
-- 6-Tuple
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) where
(a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) = (a0, b0, c0, d0, e0) .== (a1, b1, c1, d1, e1) .&& f0 .== f1
(a0, b0, c0, d0, e0, f0) .=== (a1, b1, c1, d1, e1, f1) = (a0, b0, c0, d0, e0) .=== (a1, b1, c1, d1, e1) .&& f0 .=== f1
instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) where
(a0, b0, c0, d0, e0, f0) .< (a1, b1, c1, d1, e1, f1) = (a0, b0, c0, d0, e0) .< (a1, b1, c1, d1, e1)
.|| ((a0, b0, c0, d0, e0) .== (a1, b1, c1, d1, e1) .&& f0 .< f1)
-- 7-Tuple
instance (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) where
(a0, b0, c0, d0, e0, f0, g0) .== (a1, b1, c1, d1, e1, f1, g1) = (a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) .&& g0 .== g1
(a0, b0, c0, d0, e0, f0, g0) .=== (a1, b1, c1, d1, e1, f1, g1) = (a0, b0, c0, d0, e0, f0) .=== (a1, b1, c1, d1, e1, f1) .&& g0 .=== g1
instance (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) where
(a0, b0, c0, d0, e0, f0, g0) .< (a1, b1, c1, d1, e1, f1, g1) = (a0, b0, c0, d0, e0, f0) .< (a1, b1, c1, d1, e1, f1)
.|| ((a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) .&& g0 .< g1)
-- | A class of values that capture the notion of a zero for measure values.
-- Used in termination checking for recursive SMT functions.
class OrdSymbolic (SBV a) => Zero a where
zero :: SBV a
-- | Component-wise non-negativity check. For scalars this is simply @>= 0@.
-- For tuples, every component must be @>= 0@, which is stronger than
-- lexicographic @>= (0, 0, ..)@. This is required for well-foundedness
-- of the lexicographic ordering on the non-negative part.
nonNeg :: SBV a -> SBool
nonNeg x = x .>= zero
-- | An integer as a measure
instance Zero Integer where
zero = literal 0
-- | Bounded bit-vectors as measures. These are all sound: each is a finite type, so a
-- non-negative, strictly-decreasing chain of values is necessarily finite. (The default
-- @nonNeg x = x .>= 0@ works for both the unsigned and signed cases.)
instance Zero Word8 where zero = literal 0
instance Zero Word16 where zero = literal 0
instance Zero Word32 where zero = literal 0
instance Zero Word64 where zero = literal 0
instance Zero Int8 where zero = literal 0
instance Zero Int16 where zero = literal 0
instance Zero Int32 where zero = literal 0
instance Zero Int64 where zero = literal 0
instance (KnownNat n, BVIsNonZero n) => Zero (WordN n) where zero = literal 0
instance (KnownNat n, BVIsNonZero n) => Zero (IntN n) where zero = literal 0
-- NB. We would like to use 'Data.SBV.Tuple.untuple' in the 'nonNeg' definitions below,
-- but 'Data.SBV.Tuple' imports 'Data.SBV.Core.Model', creating a circular dependency.
-- So we extract components at the SVal level using 'TupleAccess' directly.
-- | A tuple of integers as a measure
instance Zero (Integer, Integer) where
zero = literal (0, 0)
nonNeg = tupleNonNeg 2
-- | A triple of integers as a measure
instance Zero (Integer, Integer, Integer) where
zero = literal (0, 0, 0)
nonNeg = tupleNonNeg 3
-- | A quadruple of integers as a measure
instance Zero (Integer, Integer, Integer, Integer) where
zero = literal (0, 0, 0, 0)
nonNeg = tupleNonNeg 4
-- | A quintuple of integers as a measure
instance Zero (Integer, Integer, Integer, Integer, Integer) where
zero = literal (0, 0, 0, 0, 0)
nonNeg = tupleNonNeg 5
-- | A float as a measure
instance Zero Float where
zero = literal 0
-- | A double as a measure
instance Zero Double where
zero = literal 0
-- | Algebraic reals are /not/ permitted as measures, and we reject them at compile time.
-- The reals are dense, hence not well-ordered: a merely non-negative and strictly-decreasing
-- real measure does not imply termination (e.g. the chain @1, 1\/2, 1\/4, ...@ descends forever
-- without reaching a minimum). Use an integer-valued measure instead.
instance TypeError ( 'Text "A termination measure may not have a real-valued result."
':$$: 'Text ""
':$$: 'Text "The reals are not well-ordered: an infinite descending chain such as"
':$$: 'Text "1, 1/2, 1/4, ... has no least element, so a non-negative and strictly"
':$$: 'Text "decreasing real measure does not imply termination."
':$$: 'Text ""
':$$: 'Text "Use an integer-valued measure instead (e.g. a count of remaining steps)."
) => Zero AlgReal where
zero = error "Data.SBV.Zero(AlgReal): unreachable"
-- | A floating-point as a measure
instance ValidFloat eb sb => Zero (FloatingPoint eb sb) where
zero = literal 0
-- | Component-wise non-negativity for an n-tuple of integers.
-- Extracts each component via 'TupleAccess' and checks @>= 0@.
tupleNonNeg :: SymVal a => Int -> SBV a -> SBool
tupleNonNeg n t = sAll (.>= (0 :: SInteger)) [acc i | i <- [1..n]]
where acc i = SBV $ SVal KUnbounded $ Right $ cache $ \st -> do
sv <- sbvToSV st t
newExpr st KUnbounded (SBVApp (TupleAccess i n) [sv])
-- | Type family that maps a function type to its corresponding measure type.
-- The measure function takes the same arguments but returns a different type.
type family MeasureOf f r where
MeasureOf (SBV a -> r) r' = SBV a -> MeasureOf r r'
MeasureOf (SBV a) r = SBV r
-- | Apply a measure function to a list of SVal arguments, producing the measure value.
-- This is used internally during measure verification.
class ApplyMeasure a r where
applyMeasure :: MeasureOf a r -> [SVal] -> SBV r
instance ApplyMeasure (SBV a) r where
applyMeasure m [] = m
applyMeasure _ _ = error "Data.SBV.applyMeasure: too many arguments"
instance ApplyMeasure b r => ApplyMeasure (SBV a -> b) r where
applyMeasure _ [] = error "Data.SBV.applyMeasure: not enough arguments"
applyMeasure m (sv:svs) = applyMeasure @b @r (m (SBV sv)) svs
-- | Type family that maps a function type to its corresponding contract type.
-- A contract takes the same arguments as the function, plus the result, and returns 'SBool'.
-- For example, a contract for @SBV Integer -> SBV Integer@ has type @SBV Integer -> SBV Integer -> SBool@
-- (first arg is the input, second is the output).
type family ContractOf f where
ContractOf (SBV a) = SBV a -> SBool
ContractOf (SBV a -> r) = SBV a -> ContractOf r
-- | Apply a contract function to a list of input t'SVal' arguments and a result t'SVal'.
class ApplyContract a where
applyContract :: ContractOf a -> [SVal] -> SVal -> SBool
instance ApplyContract (SBV a) where
applyContract c [] sv = c (SBV sv)
applyContract _ _ _ = error "Data.SBV.applyContract: too many arguments"
instance ApplyContract b => ApplyContract (SBV a -> b) where
applyContract _ [] _ = error "Data.SBV.applyContract: not enough arguments"
applyContract c (sv:svs) r = applyContract @b (c (SBV sv)) svs r
-- | An evaluated measure: captures the ability to apply the measure function
-- to a list of arguments, along with the ordering and zero constraints.
data MeasureEval where
MeasureEval :: (Zero r, OrdSymbolic (SBV r), SymVal r) => ([SVal] -> SBV r) -> MeasureEval
-- | An evaluated contract: captures the ability to apply a contract predicate
-- to a list of input arguments and a result value. Used during measure verification
-- for nested recursive functions, where the inductive hypothesis provides the contract
-- on recursive call results.
data ContractEval where
ContractEval :: ([SVal] -> SVal -> SBool) -> ContractEval
-- | A measure for a function, used to prove termination of recursive definitions.
--
-- * 'AutoMeasure': The function either doesn't need a measure (because it's not recursive),
-- or SBV will automatically guess one based on argument types.
-- * 'HasMeasure': The user provided an explicit measure function.
-- * 'HasContract': The user provided a measure and a contract. The contract is a predicate
-- on the function's inputs and output that is proven simultaneously with the measure decrease
-- via well-founded induction. This handles nested recursion (e.g., McCarthy 91) where the
-- termination argument depends on the function's return value at smaller inputs.
-- * 'Productive': The function is corecursive (productive). Instead of proving termination via a
-- measure, SBV checks that every recursive call is guarded by a data constructor (list cons,
-- ADT constructor, etc.), ensuring the function always produces output incrementally.
-- * 'Unverified': No termination or productivity check is performed. The function is emitted as
-- @define-fun-rec@ and the user takes responsibility for well-definedness. Use this for functions
-- where termination is believed but cannot be proven (e.g., Collatz).
data Measure f where
AutoMeasure :: Measure f
HasMeasure :: MeasureEval -> [MeasureHelper] -> Measure f
HasContract :: MeasureEval -> ContractEval -> [MeasureHelper] -> Measure f
Productive :: Measure f
Unverified :: Measure f
-- | A helper axiom for measure verification. When a measure's correctness depends on
-- properties that require induction to prove (e.g., @ifComplexity f > 0@), the user
-- provides these properties along with their proofs. During the measure check, each
-- helper is run: the TP proof is executed to confirm the property holds, and the
-- proven property is asserted as an axiom in the measure verification session.
--
-- Use the 'Data.SBV.TP.measureLemma' smart constructor to create these from TP proofs.
newtype MeasureHelper = MeasureHelper { runMeasureHelper :: SMTConfig -> IO SBool }
-- | Verify that a measure decreases at each recursive call site.
-- Walks the expression DAG to find recursive calls, computes reaching conditions
-- via ITE analysis, and verifies the measure property in a separate solver session.
-- Throws an error with a detailed message if verification fails.
verifyMeasure :: SMTConfig -> String -> LambdaInfo -> MeasureEval -> [MeasureHelper] -> IO ()
verifyMeasure cfg funcNm info meval helpers = do
-- Run each helper with funcNm added to measuresBeingVerified, preventing re-entrant verification.
-- This is needed when a measureLemma proof uses the function whose measure is being checked
-- (e.g., revPreservesLen proves length(rev xs) == length xs, using rev itself).
let curVerifying = measuresBeingVerified (tpOptions cfg)
cfg' = cfg{tpOptions = (tpOptions cfg){measuresBeingVerified = Set.insert funcNm curVerifying}}
debug cfg ["[MEASURE] " <> T.pack funcNm <> ": verifying with " <> showText (length helpers) <> " helper(s)"
<> if Set.null curVerifying then "" else ", already verifying: " <> showText (Set.toList curVerifying)]
axioms <- mapM (`runMeasureHelper` cfg') helpers
debug cfg ["[MEASURE] " <> T.pack funcNm <> ": " <> showText (length axioms) <> " helper axiom(s) collected, checking measure"]
result <- checkMeasure cfg funcNm False info meval axioms
let prettyNm = prettyFuncNm funcNm
case result of
MeasureOK -> pure ()
MeasureNotNonNeg r -> error $ unlines $
[ ""
, "*** Data.SBV: Termination measure is not non-negative."
, "***"
, "*** Function: " ++ prettyNm
, "***"
]
++ ["*** " ++ l | l <- lines (show r)]
++
[ "***"
, "*** The measure must be non-negative for all inputs."
]
MeasureNotDecreasing r -> error $ unlines $
[ ""
, "*** Data.SBV: Termination measure does not strictly decrease at a recursive call site."
, "***"
, "*** Function: " ++ prettyNm
, "***"
]
++ ["*** " ++ l | l <- lines (show r)]
++
[ "***"
, "*** The measure must strictly decrease at every recursive call."
]
-- | Result of checking a measure.
data MeasureCheckResult = MeasureOK -- ^ Measure is valid
| MeasureNotNonNeg ThmResult -- ^ Measure can be negative
| MeasureNotDecreasing ThmResult -- ^ Measure doesn't strictly decrease
-- | Check that a measure is valid: non-negative and strictly decreasing at each recursive call.
-- Returns 'MeasureOK' if valid, or the specific failure otherwise.
-- If @skipNonNeg@ is 'True', the non-negativity check is skipped (used for ADT size measures
-- where non-negativity is guaranteed by construction).
-- The @axioms@ list contains additional properties to assert in the verification session
-- (used for user-provided measures that depend on inductively-proven helper properties).
checkMeasure :: SMTConfig -> String -> Bool -> LambdaInfo -> MeasureEval -> [SBool] -> IO MeasureCheckResult
checkMeasure cfgIn funcNm skipNonNeg LambdaInfo{liAssignments, liParams, liOutput, liConsts} (MeasureEval applyM) axioms = do
let -- Use a separate transcript for the measure check, so it doesn't clobber the main one
addSuffix s fp = dropExtension fp ++ "_measure_" ++ map (\c -> if c == ' ' then '_' else c) funcNm ++ "_" ++ s ++ takeExtension fp
cfgNonNeg = cfgIn{transcript = addSuffix "nonNeg" <$> transcript cfgIn}
cfgDecrease = cfgIn{transcript = addSuffix "decrease" <$> transcript cfgIn}
barFuncNm = barify funcNm
recCalls = [(sv, args) | (sv, SBVApp (Uninterpreted nm) args) <- F.toList liAssignments, nm == T.pack barFuncNm]
if null recCalls
then pure MeasureOK
else do
let reachConds = computeReachingConditions liAssignments liOutput
paramSVs = map snd liParams
-- Set up the proving environment: create fresh symbolic parameters,
-- constrain any axioms (which may register function definitions in this
-- session via the SVal cache mechanism), then replay the function body DAG.
-- The order matters: axioms must be constrained BEFORE replaying the DAG,
-- so that replayDAG knows which functions are available in this session.
mkProveEnv = do
st <- symbolicEnv
liftIO $ writeIORef (rSkipMeasureChecks st) True
let singleParam = length paramSVs == 1
freshParams <- liftIO $ sequence [svToSV st =<< svMkSymVar (NonQueryVar Nothing) (kindOf sv) (Just (if singleParam then "arg" else "arg" ++ show i)) st
| (i, sv) <- zip [(0::Int)..] paramSVs
]
freshConsts <- liftIO $ mapM (\(_, cv) -> svToSV st (SVal (kindOf cv) (Left cv))) liConsts
-- Constrain axioms first: forcing axiom SBools triggers newUninterpreted
-- for any functions they reference, registering those definitions in this session.
mapM_ constrain axioms
-- Now read which functions are actually available in this session
sessionDefns <- liftIO $ readIORef (rDefns st)
let sessionFuncs = Map.keysSet sessionDefns
let constMapping = zip (map fst liConsts) freshConsts
paramMapping = zip paramSVs freshParams
initMap = Map.fromList (constMapping ++ paramMapping)
builtinMap = Map.fromList [(trueSV, trueSV), (falseSV, falseSV)]
startMap = Map.union initMap builtinMap
svMap <- liftIO $ replayDAG cfgIn st (Set.singleton barFuncNm) sessionFuncs startMap (F.toList liAssignments)
let formalSVals = map (\sv -> SVal (kindOf sv) (Right (cache (\_ -> pure sv)))) freshParams
mFormal = applyM formalSVals
pure (svMap, mFormal)
-- Check 1: Non-negativity (skipped for ADT size measures, which are non-negative by construction)
nonNegOK <- if skipNonNeg
then pure (Right ())
else do nonNegResult <- proveWith cfgNonNeg (do
(_, mFormal) <- mkProveEnv
sObserve "measure" (unSBV mFormal)
pure $ nonNeg mFormal :: Symbolic SBool)
pure $ case nonNegResult of
ThmResult Unsatisfiable{} -> Right ()
_ -> Left nonNegResult
case nonNegOK of
Right () -> do
-- Check 2: Strict decrease at each recursive call
decResult <- proveWith cfgDecrease (do
(svMap, mFormal) <- mkProveEnv
-- When we have axioms from measure helpers that reference the function being
-- verified (e.g., revPreservesLen references rev), the axioms register the
-- function definition in this session via the SVal cache mechanism. We then
-- connect the fresh variables (created by replayDAG for recursive calls) to
-- actual function calls, so the axioms can reason about them.
-- For example, the axiom len(rev(xs)) = len(xs) needs to know that fresh_1
-- is actually rev(as) in order to derive len(fresh_1) = len(as).
st <- symbolicEnv
defns <- liftIO $ readIORef (rDefns st)
let funcRegistered = Map.member barFuncNm defns
when funcRegistered $
liftIO $ mapM_ (\(rcSV, callArgSVs) -> do
let freshSV = Map.findWithDefault rcSV rcSV svMap
mappedArgs = map (\sv -> Map.findWithDefault sv sv svMap) callArgSVs
k = kindOf rcSV
-- Create the actual function call: f(mapped_args)
actualSV <- newExpr st k (SBVApp (Uninterpreted (T.pack barFuncNm)) mappedArgs)
-- Assert fresh_var == f(mapped_args)
let freshSVal = SVal k (Right (cache (const (pure freshSV))))
actualSVal = SVal k (Right (cache (const (pure actualSV))))
internalConstraint st False [] (svEqual freshSVal actualSVal)
) recCalls
let singleCall = length recCalls == 1
mkObligation (i, (rcSV, callArgSVs)) = do
let mappedArgs = map (\sv -> Map.findWithDefault sv sv svMap) callArgSVs
argSVals = map (\sv -> SVal (kindOf sv) (Right (cache (\_ -> pure sv)))) mappedArgs
mCall = applyM argSVals
reachSVal = case Map.lookup rcSV reachConds of
Just conds -> sAnd [ let sv' = Map.findWithDefault condSV condSV svMap
s = SBV (SVal KBool (Right (cache (\_ -> pure sv'))))
in if pol then s else sNot s
| (condSV, pol) <- conds
]
Nothing -> sTrue
tag nm | singleCall = nm
| True = nm ++ "[" ++ show (i :: Int) ++ "]"
sObserve (tag "then") (unSBV mCall)
pure $ reachSVal .=> mFormal .> mCall
sObserve "before" (unSBV mFormal)
obligations <- mapM mkObligation (zip [1..] recCalls)
pure $ sAnd obligations :: Symbolic SBool)
case decResult of
ThmResult Unsatisfiable{} -> pure MeasureOK
_ -> pure $ MeasureNotDecreasing decResult
Left nonNegResult -> pure $ MeasureNotNonNeg nonNegResult
-- | Verify a measure with a contract for nested recursive functions.
-- Uses well-founded induction: the inductive hypothesis provides the contract
-- on recursive call results, and we prove both measure decrease and contract simultaneously.
-- One-step unfolding of the function body at each recursive call site gives the solver
-- information about base-case behavior without assuming totality.
verifyMeasureWithContract :: SMTConfig -> String -> LambdaInfo -> MeasureEval -> ContractEval -> [MeasureHelper] -> IO ()
verifyMeasureWithContract cfg funcNm info meval ceval helpers = do
-- Run helpers with funcNm added to measuresBeingVerified, same as verifyMeasure
let curVerifying = measuresBeingVerified (tpOptions cfg)
cfg' = cfg{tpOptions = (tpOptions cfg){measuresBeingVerified = Set.insert funcNm curVerifying}}
debug cfg ["[MEASURE] " <> T.pack funcNm <> " (contract): verifying with " <> showText (length helpers) <> " helper(s)"]
axioms <- mapM (`runMeasureHelper` cfg') helpers
debug cfg ["[MEASURE] " <> T.pack funcNm <> " (contract): " <> showText (length axioms) <> " helper axiom(s) collected, checking measure+contract"]
result <- checkMeasureWithContract cfg funcNm False info meval ceval axioms
let prettyNm = prettyFuncNm funcNm
case result of
MeasureOK -> pure ()
MeasureNotNonNeg r -> error $ unlines $
[ ""
, "*** Data.SBV: Termination measure is not non-negative."
, "***"
, "*** Function: " ++ prettyNm
, "***"
]
++ ["*** " ++ l | l <- lines (show r)]
++
[ "***"
, "*** The measure must be non-negative for all inputs."
]
MeasureNotDecreasing r -> error $ unlines $
[ ""
, "*** Data.SBV: Measure+contract verification failed."
, "***"
, "*** Function: " ++ prettyNm
, "***"
]
++ ["*** " ++ l | l <- lines (show r)]
++
[ "***"
, "*** The measure must strictly decrease at every recursive call,"
, "*** and the contract must hold for the function's output."
, "*** The inductive hypothesis provides the contract on recursive call"
, "*** results for inputs with strictly smaller measure."
]
-- | Check a measure with contract: non-negative, strictly decreasing, and contract holds.
-- Uses one-step unfolding at each recursive call site to give the solver base-case behavior,
-- and assumes the inductive hypothesis (contract on recursive call results) to handle
-- nested recursion where a call's argument depends on another call's result.
checkMeasureWithContract :: SMTConfig -> String -> Bool -> LambdaInfo -> MeasureEval -> ContractEval -> [SBool] -> IO MeasureCheckResult
checkMeasureWithContract cfgIn funcNm skipNonNeg LambdaInfo{liAssignments, liParams, liOutput, liConsts} (MeasureEval applyM) (ContractEval applyC) axioms = do
let addSuffix s fp = dropExtension fp ++ "_measure_" ++ map (\c -> if c == ' ' then '_' else c) funcNm ++ "_" ++ s ++ takeExtension fp
cfgNonNeg = cfgIn{transcript = addSuffix "nonNeg" <$> transcript cfgIn}
cfgDecrease = cfgIn{transcript = addSuffix "decrease" <$> transcript cfgIn}
barFuncNm = barify funcNm
recCalls = [(sv, args) | (sv, SBVApp (Uninterpreted nm) args) <- F.toList liAssignments, nm == T.pack barFuncNm]
if null recCalls
then pure MeasureOK
else do
-- Non-negativity: same as checkMeasure
nonNegOK <- if skipNonNeg
then pure (Right ())
else do nonNegResult <- proveWith cfgNonNeg (do
st <- symbolicEnv
liftIO $ writeIORef (rSkipMeasureChecks st) True
let singleParam = length paramSVs == 1
freshParams <- liftIO $ sequence [svToSV st =<< svMkSymVar (NonQueryVar Nothing) (kindOf sv) (Just (if singleParam then "arg" else "arg" ++ show i)) st
| (i, sv) <- zip [(0::Int)..] paramSVs
]
freshConsts <- liftIO $ mapM (\(_, cv) -> svToSV st (SVal (kindOf cv) (Left cv))) liConsts
mapM_ constrain axioms
sessionDefns <- liftIO $ readIORef (rDefns st)
let sessionFuncs = Map.keysSet sessionDefns
let constMapping = zip (map fst liConsts) freshConsts
paramMapping = zip paramSVs freshParams
initMap = Map.fromList (constMapping ++ paramMapping)
builtinMap = Map.fromList [(trueSV, trueSV), (falseSV, falseSV)]
startMap = Map.union initMap builtinMap
_ <- liftIO $ replayDAG cfgIn st (Set.singleton barFuncNm) sessionFuncs startMap (F.toList liAssignments)
let formalSVals = map (\sv -> SVal (kindOf sv) (Right (cache (\_ -> pure sv)))) freshParams
mFormal = applyM formalSVals
sObserve "measure" (unSBV mFormal)
pure $ nonNeg mFormal :: Symbolic SBool)
pure $ case nonNegResult of
ThmResult Unsatisfiable{} -> Right ()
_ -> Left nonNegResult
case nonNegOK of
Right () -> do
-- Decrease + contract check
decResult <- proveWith cfgDecrease (do
st <- symbolicEnv
liftIO $ writeIORef (rSkipMeasureChecks st) True
let singleParam = length paramSVs == 1
freshParams <- liftIO $ sequence [svToSV st =<< svMkSymVar (NonQueryVar Nothing) (kindOf sv) (Just (if singleParam then "arg" else "arg" ++ show i)) st
| (i, sv) <- zip [(0::Int)..] paramSVs
]
freshConsts <- liftIO $ mapM (\(_, cv) -> svToSV st (SVal (kindOf cv) (Left cv))) liConsts
mapM_ constrain axioms
sessionDefns <- liftIO $ readIORef (rDefns st)
let sessionFuncs = Map.keysSet sessionDefns
let constMapping = zip (map fst liConsts) freshConsts
paramMapping = zip paramSVs freshParams
initMap = Map.fromList (constMapping ++ paramMapping)
builtinMap = Map.fromList [(trueSV, trueSV), (falseSV, falseSV)]
startMap = Map.union initMap builtinMap
svMap <- liftIO $ replayDAG cfgIn st (Set.singleton barFuncNm) sessionFuncs startMap (F.toList liAssignments)
let formalSVals = map (\sv -> SVal (kindOf sv) (Right (cache (\_ -> pure sv)))) freshParams
mFormal = applyM formalSVals
-- One-step unfolding: for each recursive call, replay the function body
-- with the call's arguments substituted for the formal parameters.
-- This gives the solver base-case behavior without assuming totality.
let dagList = F.toList liAssignments
liftIO $ F.for_ recCalls $ \(rcSV, callArgSVs) -> do
let -- Map the call's arguments through svMap to get the fresh session SVs
mappedCallArgs = map (\sv -> Map.findWithDefault sv sv svMap) callArgSVs
-- Build the initial map for the unfolded body: formal params -> call args
unfoldParamMapping = zip paramSVs mappedCallArgs
unfoldConstMapping = zip (map fst liConsts) freshConsts
unfoldInitMap = Map.fromList (unfoldConstMapping ++ unfoldParamMapping)
unfoldStartMap = Map.union unfoldInitMap builtinMap
-- Replay the entire function body with the call's args
unfoldSvMap <- replayDAG cfgIn st (Set.singleton barFuncNm) sessionFuncs unfoldStartMap dagList
-- The unfolded output SV
let unfoldedOutputSV = Map.findWithDefault liOutput liOutput unfoldSvMap
-- The fresh variable that was assigned to this recursive call
freshCallSV = Map.findWithDefault rcSV rcSV svMap
-- Assert: fresh_call = unfolded_output
freshSVal = SVal (kindOf rcSV) (Right (cache (const (pure freshCallSV))))
unfoldedSVal = SVal (kindOf rcSV) (Right (cache (const (pure unfoldedOutputSV))))
internalConstraint st False [] (svEqual freshSVal unfoldedSVal)
-- IH contract: for each recursive call, assume the contract holds on its result.
-- This is sound because we also prove measure decrease at each call site.
liftIO $ F.for_ recCalls $ \(rcSV, callArgSVs) -> do
let mappedArgs = map (\sv -> Map.findWithDefault sv sv svMap) callArgSVs
argSVals = map (\sv -> SVal (kindOf sv) (Right (cache (\_ -> pure sv)))) mappedArgs
freshCallSV = Map.findWithDefault rcSV rcSV svMap
freshResult = SVal (kindOf rcSV) (Right (cache (const (pure freshCallSV))))
contractHolds = applyC argSVals freshResult
internalConstraint st False [] (unSBV contractHolds)
-- Proof obligations:
-- 1. Measure strictly decreases at each reachable recursive call site
let reachConds = computeReachingConditions liAssignments liOutput
singleCall = length recCalls == 1
mkDecreaseObligation (i, (rcSV, callArgSVs)) = do
let mappedArgs = map (\sv -> Map.findWithDefault sv sv svMap) callArgSVs
argSVals = map (\sv -> SVal (kindOf sv) (Right (cache (\_ -> pure sv)))) mappedArgs
mCall = applyM argSVals
reachSVal = case Map.lookup rcSV reachConds of
Just conds -> sAnd [ let sv' = Map.findWithDefault condSV condSV svMap
s = SBV (SVal KBool (Right (cache (\_ -> pure sv'))))
in if pol then s else sNot s
| (condSV, pol) <- conds
]
Nothing -> sTrue
tag nm | singleCall = nm
| True = nm ++ "[" ++ show (i :: Int) ++ "]"
sObserve (tag "then") (unSBV mCall)
pure $ reachSVal .=> mFormal .> mCall
sObserve "before" (unSBV mFormal)
decreaseObligations <- mapM mkDecreaseObligation (zip [1..] recCalls)
-- 2. Contract holds for the function's output
let mappedOutput = Map.findWithDefault liOutput liOutput svMap
resultSVal = SVal (kindOf liOutput) (Right (cache (const (pure mappedOutput))))
contractObl = applyC formalSVals resultSVal
pure $ sAnd decreaseObligations .&& contractObl :: Symbolic SBool)
case decResult of
ThmResult Unsatisfiable{} -> pure MeasureOK
_ -> pure $ MeasureNotDecreasing decResult
Left nonNegResult -> pure $ MeasureNotNonNeg nonNegResult
where paramSVs = map snd liParams
-- | Verify that a function marked as productive is guarded-recursive:
-- every recursive call must be a direct argument to a data constructor.
verifyGuardedness :: SMTConfig -> String -> LambdaInfo -> IO ()
verifyGuardedness cfg funcNm info
| isGuardedRecursive (Set.singleton (barify funcNm)) info
= debug cfg ["[MEASURE] " <> T.pack funcNm <> ": productive (all recursive calls are guarded by constructors)"]
| True
= error $ unlines
[ ""
, "*** Data.SBV: Function marked as productive is not guarded-recursive."
, "***"
, "*** Function: " ++ prettyFuncNm funcNm
, "***"
, "*** Every recursive call must be a direct argument to a data constructor"
, "*** (list cons, ADT constructor, etc.) to ensure productivity."
]
-- | Check if a recursive function is guarded: every recursive call's result
-- is consumed by a data constructor (list cons, ADT constructor, tuple constructor).
-- This ensures the function is productive — it always makes progress by producing
-- at least one constructor before recursing. The set of barified names covers
-- all functions in the mutual recursion group (or just the function itself for self-recursion).
isGuardedRecursive :: Set.Set String -> LambdaInfo -> Bool
isGuardedRecursive barFuncNms LambdaInfo{liAssignments} = all isGuarded recCallSVs
where
dagList = F.toList liAssignments
recCallSVs = [sv | (sv, SBVApp (Uninterpreted nm) _) <- dagList, nm `Set.member` Set.map T.pack barFuncNms]
-- Build a map from SV to the set of operations that consume it
consumers :: Map.Map SV [(SV, Op)]
consumers = foldl' addConsumers Map.empty dagList
where addConsumers m (sv, SBVApp op args) =
foldl' (\m' a -> Map.insertWith (\_ old -> (sv, op) : old) a [(sv, op)] m') m args
-- A recursive call is guarded if at least one of its consumers is a constructor
isGuarded sv = case Map.lookup sv consumers of
Nothing -> False
Just cons -> any (isConstructorOp . snd) cons
isConstructorOp (SeqOp SeqConcat{}) = True
isConstructorOp (ADTOp ADTConstructor{}) = True
isConstructorOp (TupleConstructor _) = True
isConstructorOp _ = False
-- | Generate candidate measures based on parameter kinds.
-- For list args, we use @length@. For integer args, we use @abs@. For recursive ADTs, we use @sbv.dt.size@.
-- ADT size measures are tried first (most likely to succeed for structural recursion).
-- If there are multiple scalar candidates, we also try their sum.
-- For two or more scalar candidates, we also try lexicographic (tuple) measures
-- using all pairs and triples, which handles functions like Ackermann that
-- decrease lexicographically.
guessMeasures :: [(Quantifier, SV)] -> [(String, MeasureEval, Maybe Int)]
guessMeasures params = map (\(d, f, mi) -> (d, MeasureEval f, mi)) (adtSingles ++ otherSingles ++ summed) ++ lexPairs ++ lexTriples
where
singles :: [(String, [SVal] -> SInteger, Maybe Int)]
singles = concatMap mkCandidates (zip [0..] params)
-- ADT size measures are most likely to succeed for ADT-recursive functions, so try them first
(adtSingles, otherSingles) = partition (\(_, _, mi) -> isJust mi) singles
mkCandidates :: (Int, (Quantifier, SV)) -> [(String, [SVal] -> SInteger, Maybe Int)]
mkCandidates (i, (_, sv)) = case kindOf sv of
KList elemK -> [("length arg" ++ show (i+1), \svs ->
let listSVal = svs !! i
in SBV $ SVal KUnbounded $ Right $ cache $ \st -> do
s <- sbvToSV st (SBV listSVal)
newExpr st KUnbounded (SBVApp (SeqOp (SeqLen elemK)) [s]), Nothing)]
-- Strings are sequences of characters in SMTLib
KString -> [("length arg" ++ show (i+1), \svs ->
let strSVal = svs !! i
in SBV $ SVal KUnbounded $ Right $ cache $ \st -> do
s <- sbvToSV st (SBV strSVal)
newExpr st KUnbounded (SBVApp (SeqOp (SeqLen KChar)) [s]), Nothing)]
-- Unbounded integers: try abs and smax 0 as measures
KUnbounded -> [ ("abs arg" ++ show (i+1), \svs -> abs (SBV (svs !! i)), Nothing)
, ("smax 0 arg" ++ show (i+1), \svs -> 0 `smax` SBV (svs !! i), Nothing)
]
-- Bounded bitvectors: cast to Integer for the measure. Unsigned values are
-- already non-negative; signed values need abs to ensure non-negativity.
KBounded False _ -> [("arg" ++ show (i+1), \svs -> SBV (svFromIntegral KUnbounded (svs !! i)), Nothing)]
KBounded True _ -> [("abs arg" ++ show (i+1), \svs -> abs (SBV (svFromIntegral KUnbounded (svs !! i))), Nothing)]
KTuple ks -> concatMap (mkTupleComponent i (length ks)) (zip [1..] ks)
KADT adtName _ ctors
| any (any (isRecKind adtName) . snd) ctors ->
let sizeName = "sbv.dt.size." ++ adtName
adtKind = kindOf sv
in [(sizeName ++ " arg" ++ show (i+1), \svs ->
SBV $ SVal KUnbounded $ Right $ cache $ \st -> do
ensureADTSizeDefined st sizeName adtKind ctors
s <- sbvToSV st (SBV (svs !! i))
newExpr st KUnbounded (SBVApp (Uninterpreted (T.pack sizeName)) [s]), Just i)]
_ -> []
mkTupleComponent :: Int -> Int -> (Int, Kind) -> [(String, [SVal] -> SInteger, Maybe Int)]
mkTupleComponent argIdx nFields (compIdx, compKind) = case compKind of
KList elemK -> [("length arg" ++ show (argIdx+1) ++ "._" ++ show compIdx, \svs ->
let comp = SBV $ SVal compKind $ Right $ cache $ \st -> do
tupSV <- sbvToSV st (SBV (svs !! argIdx))
newExpr st compKind (SBVApp (TupleAccess compIdx nFields) [tupSV])
in SBV $ SVal KUnbounded $ Right $ cache $ \st -> do
s <- sbvToSV st comp
newExpr st KUnbounded (SBVApp (SeqOp (SeqLen elemK)) [s]), Nothing)]
KUnbounded -> [("abs arg" ++ show (argIdx+1) ++ "._" ++ show compIdx, \svs ->
abs $ SBV $ SVal KUnbounded $ Right $ cache $ \st -> do
tupSV <- sbvToSV st (SBV (svs !! argIdx))
newExpr st KUnbounded (SBVApp (TupleAccess compIdx nFields) [tupSV]), Nothing)]
_ -> []
summed | length singles > 1 = [( intercalate " + " [d | (d, _, _) <- singles]
, \svs -> sum [f svs | (_, f, _) <- singles]
, Nothing
)]
| True = []
-- Lexicographic pair measures: try all ordered pairs from the scalar candidates
lexPairs :: [(String, MeasureEval, Maybe Int)]
lexPairs
| length singles < 2 = []
| True = [ ( "(" ++ d1 ++ ", " ++ d2 ++ ")"
, MeasureEval (\svs -> mkPair (f1 svs) (f2 svs))
, Nothing
)
| (d1, f1, _) <- singles
, (d2, f2, _) <- singles
, d1 /= d2
]
-- Lexicographic triple measures: try all ordered triples from the scalar candidates
lexTriples :: [(String, MeasureEval, Maybe Int)]
lexTriples
| length singles < 3 = []
| True = [ ( "(" ++ d1 ++ ", " ++ d2 ++ ", " ++ d3 ++ ")"
, MeasureEval (\svs -> mkTriple (f1 svs) (f2 svs) (f3 svs))
, Nothing
)
| (d1, f1, _) <- singles
, (d2, f2, _) <- singles
, d1 /= d2
, (d3, f3, _) <- singles
, d1 /= d3, d2 /= d3
]
-- Build an SBV (Integer, Integer) from two SIntegers
mkPair :: SInteger -> SInteger -> SBV (Integer, Integer)
mkPair a b = SBV $ SVal (KTuple [KUnbounded, KUnbounded]) $ Right $ cache $ \st -> do
sa <- sbvToSV st a
sb <- sbvToSV st b
newExpr st (KTuple [KUnbounded, KUnbounded]) (SBVApp (TupleConstructor 2) [sa, sb])
-- Build an SBV (Integer, Integer, Integer) from three SIntegers
mkTriple :: SInteger -> SInteger -> SInteger -> SBV (Integer, Integer, Integer)
mkTriple a b c = SBV $ SVal (KTuple [KUnbounded, KUnbounded, KUnbounded]) $ Right $ cache $ \st -> do
sa <- sbvToSV st a
sb <- sbvToSV st b
sc <- sbvToSV st c
newExpr st (KTuple [KUnbounded, KUnbounded, KUnbounded]) (SBVApp (TupleConstructor 3) [sa, sb, sc])
-- | Check if a kind refers back to a given ADT name (i.e., is a recursive field).
-- Recursive fields in constructor kinds use 'KApp', not 'KADT'.
isRecKind :: String -> Kind -> Bool
isRecKind adtName (KApp n _) = n == adtName
isRecKind adtName (KADT n _ _) = n == adtName
isRecKind _ _ = False
-- | Ensure that an ADT size function is defined in the given state. The size function
-- maps ADT values to non-negative integers, returning 0 for base constructors and
-- @1 + sum(sizes of recursive fields)@ for recursive constructors.
-- This is used as a termination measure for functions that recurse on ADT values.
ensureADTSizeDefined :: State -> String -> Kind -> [(String, [Kind])] -> IO ()
ensureADTSizeDefined st sizeName adtKind ctors = do
defs <- readIORef (rDefns st)
unless (Map.member sizeName defs) $ do
let argNm = "x"
smtArgType = T.unpack (smtType adtKind)
-- Build the SMT-Lib body for the size function
body = buildBody ctors
buildBody [] = "0"
buildBody [c] = caseExpr c
buildBody (c:cs) = "(ite " ++ testerExpr c ++ " " ++ caseExpr c ++ " " ++ buildBody cs ++ ")"
testerExpr (cName, _) = "(is-" ++ cName ++ " " ++ argNm ++ ")"
caseExpr (cName, flds) =
let recIdxs = [j | (j, k) <- zip [1::Int ..] flds, isRecKind (adtNameOf adtKind) k]
in if null recIdxs
then "0"
else let recCalls = ["(" ++ sizeName ++ " (get" ++ cName ++ "_" ++ show j ++ " " ++ argNm ++ "))" | j <- recIdxs]
in "(+ 1 " ++ smtSum recCalls ++ ")"
smtSum [x] = x
smtSum (x:xs) = "(+ " ++ x ++ " " ++ smtSum xs ++ ")"
smtSum [] = "0"
paramStr = T.pack $ "((" ++ argNm ++ " " ++ smtArgType ++ "))"
smtDef = SMTDef KUnbounded [sizeName] (Just paramStr) (\n -> T.pack (replicate n ' ' ++ body))
sbvTy = SBVType [adtKind, KUnbounded]
modifyIORef' (rDefns st) (Map.insert sizeName (smtDef, sbvTy))
modifyState st rUIMap (Map.insert sizeName (True, Nothing, sbvTy)) (pure ())
-- | Extract the ADT name from a KADT kind.
adtNameOf :: Kind -> String
adtNameOf (KADT n _ _) = n
adtNameOf _ = ""
-- | Check if a function is structurally recursive on a given parameter.
-- Returns 'True' if every recursive call passes a strict sub-term of the
-- formal parameter (obtained via one or more 'ADTAccessor' operations) as
-- the argument at that parameter position. Structural recursion on an ADT
-- guarantees termination by the well-foundedness of the datatype, so the
-- measure check can be skipped.
isStructurallyDecreasing :: String -> LambdaInfo -> Int -> Bool
isStructurallyDecreasing funcNm LambdaInfo{liAssignments, liParams} paramIdx =
not (null recCalls) && all checkCall recCalls
where
barFuncNm = barify funcNm
paramSV = snd (liParams !! paramIdx)
asgns = F.toList liAssignments
defMap = Map.fromList asgns
recCalls = [args | (_, SBVApp (Uninterpreted nm) args) <- asgns, nm == T.pack barFuncNm]
checkCall callArgs
| paramIdx < length callArgs = isProperSubTerm (callArgs !! paramIdx)
| True = False
-- An SV is a proper sub-term of the parameter if it is obtained by applying
-- one or more ADTAccessor operations to the parameter.
isProperSubTerm sv = case Map.lookup sv defMap of
Just (SBVApp (ADTOp (ADTAccessor _ _)) [parent]) ->
parent == paramSV || isProperSubTerm parent
_ -> False
-- | Try to auto-guess a termination measure for a recursive function. Generates candidates
-- based on parameter kinds and tries each one. Returns the first measure that passes both
-- non-negativity and strict decrease checks, or 'Nothing' if no guess works.
autoGuess :: SMTConfig -> String -> LambdaInfo -> IO (Maybe MeasureEval)
autoGuess cfg funcNm info = do
let barFuncNm = barify funcNm
recCalls = [(sv, args) | (sv, SBVApp (Uninterpreted nm) args) <- F.toList (liAssignments info), nm == T.pack barFuncNm]
allUIs = [(nm, length args) | (_, SBVApp (Uninterpreted nm) args) <- F.toList (liAssignments info)]
debug cfg ["[MEASURE] " <> T.pack funcNm <> ": barified = " <> showText barFuncNm]
debug cfg ["[MEASURE] " <> T.pack funcNm <> ": Uninterpreted ops in DAG: " <> showText allUIs]
debug cfg ["[MEASURE] " <> T.pack funcNm <> ": recursive calls found = " <> showText (length recCalls)]
go candidates
where
candidates = guessMeasures (liParams info)
go [] = pure Nothing
go ((desc, m, mbIdx):ms) = do let skipNonNeg = "sbv.dt.size." `isPrefixOf` desc
debug cfg ["[MEASURE] " <> T.pack funcNm <> ": trying " <> T.pack desc]
-- For ADT size measures, try syntactic sub-term check first.
-- This avoids calling the solver, which can hang on recursive
-- define-fun-rec definitions.
result <- case mbIdx of
Just idx | isStructurallyDecreasing funcNm info idx -> do
debug cfg ["[MEASURE] " <> T.pack funcNm <> ": " <> T.pack desc <> " -> OK (structural recursion)"]
pure MeasureOK
_ -> checkMeasure cfg funcNm skipNonNeg info m []
case result of
MeasureOK -> do debug cfg ["[MEASURE] " <> T.pack funcNm <> ": " <> T.pack desc <> " -> OK"]
pure (Just m)
MeasureNotNonNeg r -> do debug cfg ["[MEASURE] " <> T.pack funcNm <> ": " <> T.pack desc <> " failed non-negativity: " <> showText r]
debug cfg ["[MEASURE] " <> T.pack funcNm <> ": trying next candidate.."]
go ms
MeasureNotDecreasing r -> do debug cfg ["[MEASURE] " <> T.pack funcNm <> ": " <> T.pack desc <> " failed strict decrease: " <> showText r]
debug cfg ["[MEASURE] " <> T.pack funcNm <> ": trying next candidate.."]
go ms
-- | Auto-guess a termination measure, or fail with a helpful error message.
autoGuessOrFail :: SMTConfig -> String -> LambdaInfo -> IO ()
autoGuessOrFail cfg funcNm info = do
mbMeasure <- autoGuess cfg funcNm info
case mbMeasure of
Just _ -> pure ()
Nothing -> error $ unlines $
[ ""
, "*** Data.SBV: Cannot determine a termination measure."
, "***"
, "*** Function: " ++ prettyFuncNm funcNm
]
++ guessLines
++
[ "***"
, "*** Please use 'smtFunctionWithMeasure' to provide an explicit measure."
]
where candidates = guessMeasures (liParams info)
guessLines
| null candidates = [ "***"
, "*** No measure candidates could be derived from the argument types."
]
| True = [ "***"
, "*** Measures tried:"
]
++ [ "*** " ++ d | (d, _, _) <- candidates]
-- | Check mutual recursion for a function by computing the SCC from State.
-- This is called as a deferred closure from rMeasureChecks. It computes the SCC
-- of the function graph, finds the group containing the given function, and
-- verifies the whole group if it's a multi-member cycle. Multiple members of the
-- same group may register this check, but only the first execution does work;
-- after successful verification, verified members are removed from rFuncLambdaInfos,
-- so subsequent closures find insufficient infos and skip.
--
-- The optional t'MeasureEval' is a user-provided measure (from 'smtFunctionWithMeasure').
-- If given, it is tried first before falling back to auto-guessing.
checkMutualFromState :: SMTConfig -> String -> State -> Maybe MeasureEval -> IO ()
checkMutualFromState cfg funcNm st mbMeasure = do
defns <- readIORef (rDefns st)
funcInfos <- readIORef (rFuncLambdaInfos st)
let barFuncNm = barify funcNm
nodes = [(nm, nm, deps) | (nm, (SMTDef _ deps _ _, _)) <- Map.toList defns]
sccs = DG.stronglyConnComp nodes
-- Find the SCC containing our function (using barified name since rDefns keys are barified)
mySCC = [members | DG.CyclicSCC members <- sccs, barFuncNm `elem` members]
case mySCC of
[members] | length members >= 2 -> do
-- rFuncLambdaInfos uses plain names, so unbar the SCC member names for lookup.
-- Build the infos map with plain names as keys (matching rFuncLambdaInfos convention).
let plainMembers = map unBar members
infos = Map.fromList [(pnm, v) | pnm <- plainMembers, Just v <- [Map.lookup pnm funcInfos]]
if Map.size infos >= 2
then do checkMutualGroup cfg infos mbMeasure
-- Remove verified members from rFuncLambdaInfos so that subsequent closures
-- for the same group (registered by other members) find insufficient infos and skip.
modifyIORef' (rFuncLambdaInfos st) (\m -> foldl' (flip Map.delete) m plainMembers)
else do debug cfg ["[MEASURE] " <> T.pack funcNm <> ": mutual group already verified, skipping"]
modifyIORef' (rFuncLambdaInfos st) (Map.delete funcNm)
_ -> do debug cfg ["[MEASURE] " <> T.pack funcNm <> ": not in a multi-member cycle, skipping mutual check"]
modifyIORef' (rFuncLambdaInfos st) (Map.delete funcNm)
-- | Reject mutual recursion for contract-based functions. Deferred to SCC computation time
-- so that non-mutual cross-refs (helper functions, uninterpreted constants) don't cause false positives.
rejectMutualContractFromState :: SMTConfig -> String -> State -> IO ()
rejectMutualContractFromState cfg funcNm st = do
defns <- readIORef (rDefns st)
let barFuncNm = barify funcNm
nodes = [(nm, nm, deps) | (nm, (SMTDef _ deps _ _, _)) <- Map.toList defns]
sccs = DG.stronglyConnComp nodes
mySCC = [members | DG.CyclicSCC members <- sccs, barFuncNm `elem` members]
case mySCC of
[members] | length members >= 2 ->
error $ unlines [ ""
, "*** Data.SBV: smtFunctionWithContract does not support mutual recursion."
, "***"
, "*** Function: " ++ prettyFuncNm funcNm
, "***"
, "*** Please use smtFunction or smtFunctionWithMeasure for mutual recursion groups."
, ""
]
_ -> debug cfg ["[MEASURE] " <> T.pack funcNm <> ": not in a multi-member cycle, skipping mutual contract check"]
-- | Check that all members of a mutual recursion group marked as productive are guarded-recursive,
-- considering cross-calls as well as self-calls.
checkMutualProductiveFromState :: SMTConfig -> String -> State -> IO ()
checkMutualProductiveFromState cfg funcNm st = do
defns <- readIORef (rDefns st)
funcInfos <- readIORef (rFuncLambdaInfos st)
let barFuncNm = barify funcNm
nodes = [(nm, nm, deps) | (nm, (SMTDef _ deps _ _, _)) <- Map.toList defns]
sccs = DG.stronglyConnComp nodes
mySCC = [members | DG.CyclicSCC members <- sccs, barFuncNm `elem` members]
case mySCC of
[members] | length members >= 2 -> do
let plainMembers = map unBar members
infos = Map.fromList [(pnm, v) | pnm <- plainMembers, Just v <- [Map.lookup pnm funcInfos]]
if Map.size infos >= 2
then do let barNames = Set.fromList members
memberNamesStr = intercalate ", " (map prettyFuncNm plainMembers)
debug cfg ["[MEASURE] Checking mutual productive group: {" <> T.pack memberNamesStr <> "}"]
let failed = [(pnm, info) | (pnm, info) <- Map.toList infos, not (isGuardedRecursive barNames info)]
case failed of
[] -> do debug cfg ["[MEASURE] Mutual productive group: all members are guarded"]
modifyIORef' (rFuncLambdaInfos st) (\m -> foldl' (flip Map.delete) m plainMembers)
_ -> error $ unlines $
[ ""
, "*** Data.SBV: Mutual productive group has unguarded recursive calls."
, "***"
]
++ groupLines (Map.toList infos)
++
[ "*** Unguarded: " ++ intercalate ", " (map (prettyFuncNm . fst) failed)
, "***"
, "*** Every recursive call (self or cross) must be a direct argument to a data constructor."
, ""
]
else do debug cfg ["[MEASURE] " <> T.pack funcNm <> ": mutual productive group already verified, skipping"]
modifyIORef' (rFuncLambdaInfos st) (Map.delete funcNm)
_ -> do debug cfg ["[MEASURE] " <> T.pack funcNm <> ": not in a multi-member cycle, skipping mutual productive check"]
modifyIORef' (rFuncLambdaInfos st) (Map.delete funcNm)
-- | Check termination for a mutual recursion group. Each function in the group
-- gets an auto-guessed measure, and we verify that at every call edge (self or cross),
-- the caller's measure at formal parameters strictly exceeds the callee's measure at actual arguments.
--
-- If a user-provided measure is given ('Just'), it is tried first before auto-guessing.
checkMutualGroup :: SMTConfig -> Map.Map String LambdaInfo -> Maybe MeasureEval -> IO ()
checkMutualGroup cfg members mbMeasure = do
let memberNames = Map.keys members
memberNamesStr = intercalate ", " (map prettyFuncNm memberNames)
debug cfg ["[MEASURE] Checking mutual recursion group: {" <> T.pack memberNamesStr <> "}"]
-- If a user-provided measure is given, try it first
let memberList = Map.toList members
userOK <- case mbMeasure of
Nothing -> pure False
Just m -> do
debug cfg ["[MEASURE] Mutual group: trying user-provided measure for all members"]
ok <- checkMutualMeasure cfg memberList m
if ok
then do debug cfg ["[MEASURE] Mutual group: user-provided measure works for all members"]
pure True
else do debug cfg ["[MEASURE] Mutual group: user-provided measure failed, falling back to auto-guess"]
pure False
unless userOK $ do
-- Auto-guess: for each function, generate measure candidates
let memberCandidates = [(nm, info, guessMeasures (liParams info)) | (nm, info) <- memberList]
-- Check if any member has no candidates at all
case [(nm, info) | (nm, info, []) <- memberCandidates] of
(nm, _):_ -> error $ unlines $
[ ""
, "*** Data.SBV: Cannot determine a termination measure for mutual recursion group."
, "***"
]
++ groupLines memberList
++
[ "*** Function with no measure candidates: " ++ prettyFuncNm nm
, "***"
, if isJust mbMeasure
then "*** The user-provided measure did not work, and no auto-guess candidates are available."
else "*** Please use 'smtFunctionWithMeasure' to provide explicit measures."
]
[] -> pure ()
-- Try to find a working combination. For efficiency, when all members have the same
-- parameter kinds, we try the same candidate for all. Otherwise we try combinations.
let allCandidateLists = [(nm, info, cs) | (nm, info, cs) <- memberCandidates]
tryMeasures allCandidateLists
where
tryMeasures :: [(String, LambdaInfo, [(String, MeasureEval, Maybe Int)])] -> IO ()
tryMeasures memberInfos = do
-- Collect all unique candidates from all members (by description).
-- Different members may have different parameter kinds, yielding different candidates.
let allCandidates = nubBy (\(d1,_,_) (d2,_,_) -> d1 == d2)
$ concatMap (\(_, _, cs) -> cs) memberInfos
result <- go allCandidates
case result of
Just _ -> pure ()
Nothing -> do
error $ unlines $
[ ""
, "*** Data.SBV: Cannot determine a termination measure for mutual recursion group."
, "***"
]
++ groupLines (Map.toList members)
++
[ "***"
, if isJust mbMeasure
then "*** The user-provided measure did not work, and auto-guessing also failed."
else "*** Please use 'smtFunctionWithMeasure' to provide explicit measures."
]
where
go [] = pure Nothing
go ((desc, m, _mbIdx):rest) = do
debug cfg ["[MEASURE] Mutual group: trying measure " <> T.pack desc <> " for all members"]
-- Try the same measure for all members. Catch exceptions from kind mismatches
-- (e.g., applying abs to a list parameter) and treat them as failure.
let memberList = [(nm, info) | (nm, info, _) <- memberInfos]
result <- C.try $ checkMutualMeasure cfg memberList m
case result of
Right True -> do debug cfg ["[MEASURE] Mutual group: measure " <> T.pack desc <> " works for all members"]
pure (Just m)
Right False -> do debug cfg ["[MEASURE] Mutual group: measure " <> T.pack desc <> " failed, trying next"]
go rest
Left (e :: C.SomeException) -> do
debug cfg ["[MEASURE] Mutual group: measure " <> T.pack desc <> " incompatible: " <> showText e]
go rest
-- | Verify that a given measure works for all functions in a mutual recursion group.
-- Uses the same measure for all members. For each function f, check that at every call
-- site to any function g in the group, measure(f's formals) > measure(g's actuals).
checkMutualMeasure :: SMTConfig -> [(String, LambdaInfo)] -> MeasureEval -> IO Bool
checkMutualMeasure cfgIn members (MeasureEval applyM) = go members
where
-- Set of barified names of all group members
groupBarNames = Set.fromList [barify nm | (nm, _) <- members]
go [] = pure True
go ((funcNm, LambdaInfo{liAssignments, liParams, liOutput, liConsts}):rest) = do
-- Find all calls to any member of the mutual group
let allGroupCalls = [(sv, args)
| (sv, SBVApp (Uninterpreted calleeNm) args) <- F.toList liAssignments
, calleeNm `Set.member` Set.map T.pack groupBarNames
]
if null allGroupCalls
then go rest -- No calls to group members, no decrease needed
else do
let addSuffix s fp = dropExtension fp ++ "_measure_" ++ map (\c -> if c == ' ' then '_' else c) funcNm ++ "_" ++ s ++ takeExtension fp
cfgDecrease = cfgIn{transcript = addSuffix "mutual_decrease" <$> transcript cfgIn}
cfgNonNeg = cfgIn{transcript = addSuffix "mutual_nonNeg" <$> transcript cfgIn}
paramSVs = map snd liParams
reachConds = computeReachingConditions liAssignments liOutput
mkProveEnv = do
st <- symbolicEnv
liftIO $ writeIORef (rSkipMeasureChecks st) True
let singleParam = length paramSVs == 1
freshParams <- liftIO $ sequence
[svToSV st =<< svMkSymVar (NonQueryVar Nothing) (kindOf sv)
(Just (if singleParam then "arg" else "arg" ++ show i)) st
| (i, sv) <- zip [(0::Int)..] paramSVs
]
freshConsts <- liftIO $ mapM (\(_, cv) -> svToSV st (SVal (kindOf cv) (Left cv))) liConsts
sessionDefns <- liftIO $ readIORef (rDefns st)
let sessionFuncs = Map.keysSet sessionDefns
constMapping = zip (map fst liConsts) freshConsts
paramMapping = zip paramSVs freshParams
initMap = Map.fromList (constMapping ++ paramMapping)
builtinMap = Map.fromList [(trueSV, trueSV), (falseSV, falseSV)]
startMap = Map.union initMap builtinMap
svMap <- liftIO $ replayDAG cfgIn st groupBarNames sessionFuncs startMap (F.toList liAssignments)
let formalSVals = map (\sv -> SVal (kindOf sv) (Right (cache (\_ -> pure sv)))) freshParams
mFormal = applyM formalSVals
pure (svMap, mFormal)
-- Check 1: Non-negativity of caller's measure
nonNegResult <- proveWith cfgNonNeg (do
(_, mFormal) <- mkProveEnv
sObserve "measure" (unSBV mFormal)
pure $ nonNeg mFormal :: Symbolic SBool)
case nonNegResult of
ThmResult Unsatisfiable{} -> do
-- Check 2: Strict decrease at each call site
decResult <- proveWith cfgDecrease (do
(svMap, mFormal) <- mkProveEnv
let singleCall = length allGroupCalls == 1
mkObligation (i, (rcSV, callArgSVs)) = do
let mappedArgs = map (\sv -> Map.findWithDefault sv sv svMap) callArgSVs
argSVals = map (\sv -> SVal (kindOf sv) (Right (cache (\_ -> pure sv)))) mappedArgs
mCall = applyM argSVals
reachSVal = case Map.lookup rcSV reachConds of
Just conds -> sAnd [ let sv' = Map.findWithDefault condSV condSV svMap
s = SBV (SVal KBool (Right (cache (\_ -> pure sv'))))
in if pol then s else sNot s
| (condSV, pol) <- conds
]
Nothing -> sTrue
tag nm | singleCall = nm
| True = nm ++ "[" ++ show (i :: Int) ++ "]"
sObserve (tag "then") (unSBV mCall)
pure $ reachSVal .=> mFormal .> mCall
sObserve "before" (unSBV mFormal)
obligations <- mapM mkObligation (zip [1..] allGroupCalls)
pure $ sAnd obligations :: Symbolic SBool)
case decResult of
ThmResult Unsatisfiable{} -> do
debug cfgIn ["[MEASURE] Mutual group: decrease verified for " <> T.pack funcNm]
go rest
_ -> do
debug cfgIn ["[MEASURE] Mutual group: decrease failed for " <> T.pack funcNm <> ": " <> showText decResult]
pure False
_ -> do
debug cfgIn ["[MEASURE] Mutual group: non-negativity failed for " <> T.pack funcNm]
pure False
-- | Pretty-print a function name: turn @"insert @(SBV Integer -> SBV [Integer])"@ into @"insert :: SBV Integer -> SBV [Integer]"@
prettyFuncNm :: String -> String
prettyFuncNm m = case break (== '@') m of
(nm, '@':'(':tp) | not (null tp) -> dropWhileEnd (== ' ') nm ++ " :: " ++ init tp
_ -> m
-- | Format group members on separate lines, aligned on @::@.
groupLines :: [(String, LambdaInfo)] -> [String]
groupLines ms = case map (prettyFuncNm . fst) ms of
[] -> []
names -> let parts = [(nm, tp) | n <- names, let (nm, tp) = case break (== ':') n of
(a, ':':':':b) -> (dropWhileEnd (== ' ') a, " ::" ++ b)
_ -> (n, "")]
maxNm = maximum (map (length . fst) parts)
pad s = s ++ replicate (maxNm - length s) ' '
fmt (n, t) = "*** " ++ pad n ++ " " ++ t
in map fmt parts
-- | Replay the DAG in a new state, building up an SV mapping from old to new.
-- Recursive calls to the functions being verified are replaced with fresh variables.
-- Calls to other DEFINED functions (present in the parent state's rDefns) are replayed as actual calls.
-- All other Uninterpreted references (uninterpreted constants, free functions, sentinels)
-- are replaced with fresh variables since they aren't defined in the fresh proveWith session.
replayDAG :: SMTConfig -> State -> Set.Set String -> Set.Set String -> Map.Map SV SV -> [(SV, SBVExpr)] -> IO (Map.Map SV SV)
replayDAG cfg st recFuncNames definedFuncs startMap dag = do
let n = length dag
let nms = intercalate ", " (map unBar (Set.toList recFuncNames))
debug cfg ["[MEASURE] replayDAG {" <> T.pack nms <> "}: replaying " <> showText n <> " node(s)"]
go startMap dag
where -- Map an SV through the svMap. If it's not found, it's an external captured variable
-- (e.g., from a higher-order function's closure). Create a fresh unconstrained variable
-- for it to avoid leaking foreign-context SVals into the current state.
mapArg svMap a = case Map.lookup a svMap of
Just a' -> pure (a', svMap)
Nothing -> do fresh <- newInternalVariable st (kindOf a)
pure (fresh, Map.insert a fresh svMap)
mapArgs svMap [] = pure ([], svMap)
mapArgs svMap (a:as) = do (a', svMap') <- mapArg svMap a
(as', svMap'') <- mapArgs svMap' as
pure (a':as', svMap'')
go svMap [] = pure svMap
go svMap ((sv, expr):rest) = do
let SBVApp op args = expr
(mappedArgs, svMap') <- mapArgs svMap args
newSV' <- case op of
-- For recursive calls (self or mutual), create a fresh uninterpreted value instead of replaying
Uninterpreted nm | nm `Set.member` Set.map T.pack recFuncNames -> newInternalVariable st (kindOf sv)
-- For calls to other defined functions (e.g., partition), replay properly
Uninterpreted nm | nm `Set.member` Set.map T.pack definedFuncs -> do
let mappedOp = mapOpSVs (\a -> Map.findWithDefault a a svMap') op
newExpr st (kindOf sv) (SBVApp mappedOp mappedArgs)
-- For everything else that's Uninterpreted (free functions, sentinels, etc.),
-- create fresh values since they aren't defined in the proveWith session
Uninterpreted{} -> newInternalVariable st (kindOf sv)
-- For all other operations (arithmetic, list ops, etc.), replay properly
_ -> do let mappedOp = mapOpSVs (\a -> Map.findWithDefault a a svMap') op
newExpr st (kindOf sv) (SBVApp mappedOp mappedArgs)
go (Map.insert sv newSV' svMap') rest
-- | Map any SVs embedded directly in an Op (e.g., in LkUp, FP_Cast)
mapOpSVs :: (SV -> SV) -> Op -> Op
mapOpSVs f (LkUp p sv1 sv2) = LkUp p (f sv1) (f sv2)
mapOpSVs f (IEEEFP (FP_Cast fk tk sv)) = IEEEFP (FP_Cast fk tk (f sv))
mapOpSVs _ (ArrayInit (Right (SMTLambda s))) = ArrayInit (Right (SMTLambda s)) -- Lambda strings don't contain SVs to map
mapOpSVs _ op = op
-- | Compute the reaching condition for each SV: under what boolean condition
-- does the SV's value contribute to the output? Propagates conditions top-down
-- through ITE, AND, and OR nodes. Each reaching condition is a list of
-- @(condSV, polarity)@ pairs; the actual condition is the conjunction: for each
-- pair, @condSV@ if polarity is 'True', @not condSV@ if polarity is 'False'.
computeReachingConditions :: Seq.Seq (SV, SBVExpr) -> SV -> Map.Map SV [(SV, Bool)]
computeReachingConditions asgns outSV = go initMap (reverse $ F.toList asgns)
where
-- The output's reaching condition is True (empty conjunction)
initMap = Map.singleton outSV []
go condMap [] = condMap
go condMap ((sv, SBVApp op args) : rest) =
case Map.lookup sv condMap of
Nothing -> go condMap rest -- This SV doesn't contribute to the output
Just rc ->
let condMap' = case (op, args) of
(Ite, [c, t, e]) ->
let condMapT = addReach t ((c, True) : rc) condMap
condMapE = addReach e ((c, False) : rc) condMapT
in condMapE
-- For AND: each arg is only relevant when the other is True
(And, [a, b]) ->
let condMapA = addReach a ((b, True) : rc) condMap
condMapB = addReach b ((a, True) : rc) condMapA
in condMapB
-- For OR: each arg is only relevant when the other is False
(Or, [a, b]) ->
let condMapA = addReach a ((b, False) : rc) condMap
condMapB = addReach b ((a, False) : rc) condMapA
in condMapB
_ -> foldl' (\m a -> addReach a rc m) condMap args
in go condMap' rest
-- Add a reaching condition to an SV. For shared nodes, keep the first condition found
-- (most direct path from the output).
addReach sv rc m = Map.insertWith (\_ old -> old) sv rc m
-- | Regular expressions can be compared for equality. Note that we diverge here from the equality
-- in the concrete sense; i.e., the Eq instance does not match the symbolic case. This is a bit unfortunate,
-- but unavoidable with the current design of how we "distinguish" operators. Hopefully shouldn't be a big deal,
-- though one should be careful.
instance EqSymbolic RegExp where
r1 .== r2 = SBV $ SVal KBool $ Right $ cache r
where r st = newExpr st KBool $ SBVApp (RegExOp (RegExEq r1 r2)) []
r1 ./= r2 = SBV $ SVal KBool $ Right $ cache r
where r st = newExpr st KBool $ SBVApp (RegExOp (RegExNEq r1 r2)) []
-- | Symbolic Numbers. This is a simple class that simply incorporates all number like
-- base types together, simplifying writing polymorphic type-signatures that work for all
-- symbolic numbers, such as 'SWord8', 'SInt8' etc. For instance, we can write a generic
-- list-minimum function as follows:
--
-- @
-- mm :: SIntegral a => [SBV a] -> SBV a
-- mm = foldr1 (\a b -> ite (a .<= b) a b)
-- @
--
-- It is similar to the standard 'Integral' class, except ranging over symbolic instances.
class (SymVal a, Num a, Num (SBV a), Bits a, Integral a) => SIntegral a
-- 'SIntegral' Instances, skips Real/Float/Bool
instance SIntegral Word8
instance SIntegral Word16
instance SIntegral Word32
instance SIntegral Word64
instance SIntegral Int8
instance SIntegral Int16
instance SIntegral Int32
instance SIntegral Int64
instance SIntegral Integer
instance (KnownNat n, BVIsNonZero n) => SIntegral (WordN n)
instance (KnownNat n, BVIsNonZero n) => SIntegral (IntN n)
-- | Zero extend a bit-vector.
zeroExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
, KnownNat m, BVIsNonZero m, SymVal (bv m)
, n + 1 <= m
, SIntegral (bv (m - n))
, BVIsNonZero (m - n)
) => SBV (bv n) -- ^ Input, of size @n@
-> SBV (bv m) -- ^ Output, of size @m@. @n < m@ must hold
zeroExtend n = SBV $ svZeroExtend i (unSBV n)
where nv = intOfProxy (Proxy @n)
mv = intOfProxy (Proxy @m)
i = fromIntegral (mv - nv)
-- | Sign extend a bit-vector.
signExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
, KnownNat m, BVIsNonZero m, SymVal (bv m)
, n + 1 <= m
, SFiniteBits (bv n)
, SIntegral (bv (m - n))
, BVIsNonZero (m - n)
) => SBV (bv n) -- ^ Input, of size @n@
-> SBV (bv m) -- ^ Output, of size @m@. @n < m@ must hold
signExtend n = SBV $ svSignExtend i (unSBV n)
where nv = intOfProxy (Proxy @n)
mv = intOfProxy (Proxy @m)
i = fromIntegral (mv - nv)
-- | Finite bit-length symbolic values. Essentially the same as 'SIntegral', but further leaves out 'Integer'. Loosely
-- based on Haskell's @FiniteBits@ class, but with more methods defined and structured differently to fit into the
-- symbolic world view. Minimal complete definition: 'sFiniteBitSize'.
class (Ord a, SymVal a, Num a, Num (SBV a), OrdSymbolic (SBV a), Bits a) => SFiniteBits a where
-- | Bit size.
sFiniteBitSize :: SBV a -> Int
-- | Least significant bit of a word, always stored at index 0.
lsb :: SBV a -> SBool
-- | Most significant bit of a word, always stored at the last position.
msb :: SBV a -> SBool
-- | Big-endian blasting of a word into its bits.
blastBE :: SBV a -> [SBool]
-- | Little-endian blasting of a word into its bits.
blastLE :: SBV a -> [SBool]
-- | Reconstruct from given bits, given in little-endian.
fromBitsBE :: [SBool] -> SBV a
-- | Reconstruct from given bits, given in little-endian.
fromBitsLE :: [SBool] -> SBV a
-- | Replacement for 'testBit', returning 'SBool' instead of 'Bool'.
sTestBit :: SBV a -> Int -> SBool
-- | Variant of 'sTestBit', where we want to extract multiple bit positions.
sExtractBits :: SBV a -> [Int] -> [SBool]
-- | Variant of 'popCount', returning a symbolic value.
sPopCount :: SBV a -> SWord8
-- | A combo of 'setBit' and 'clearBit', when the bit to be set is symbolic.
setBitTo :: SBV a -> Int -> SBool -> SBV a
-- | Variant of 'setBitTo' when the index is symbolic. If the index it out-of-bounds,
-- then the result is underspecified.
sSetBitTo :: Integral a => SBV a -> SBV a -> SBool -> SBV a
-- | Full adder, returns carry-out from the addition. Only for unsigned quantities.
fullAdder :: SBV a -> SBV a -> (SBool, SBV a)
-- | Full multiplier, returns both high and low-order bits. Only for unsigned quantities.
fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a)
-- | Count leading zeros in a word, big-endian interpretation.
sCountLeadingZeros :: SBV a -> SWord8
-- | Count trailing zeros in a word, big-endian interpretation.
sCountTrailingZeros :: SBV a -> SWord8
{-# MINIMAL sFiniteBitSize #-}
-- Default implementations
lsb (SBV v) = SBV (svTestBit v 0)
msb x = sTestBit x (sFiniteBitSize x - 1)
blastBE = reverse . blastLE
blastLE x = map (sTestBit x) [0 .. intSizeOf x - 1]
fromBitsBE = fromBitsLE . reverse
fromBitsLE bs
| length bs /= w
= error $ "SBV.SFiniteBits.fromBitsLE/BE: Expected: " ++ show w ++ " bits, received: " ++ show (length bs)
| True
= result
where w = sFiniteBitSize result
result = go 0 0 bs
go !acc _ [] = acc
go !acc !i (x:xs) = go (ite x (setBit acc i) acc) (i+1) xs
sTestBit (SBV x) i = SBV (svTestBit x i)
sExtractBits x = map (sTestBit x)
-- NB. 'sPopCount' returns an 'SWord8', which can overflow when used on quantities that have
-- more than 255 bits. For the regular interface, this suffices for all types we support.
-- For the Dynamic interface, if we ever implement this, this will fail for bit-vectors
-- larger than that many bits. The alternative would be to return SInteger here, but that
-- seems a total overkill for most use cases. If such is required, users are encouraged
-- to define their own variants, which is rather easy.
sPopCount x
| Just v <- unliteral x = go 0 v
| True = sum [ite b 1 0 | b <- blastLE x]
where -- concrete case
go !c 0 = c
go !c w = go (c+1) (w .&. (w-1))
setBitTo x i b = ite b (setBit x i) (clearBit x i)
sSetBitTo x idx b
| Just i <- unliteral idx, Just index <- safe i
= setBitTo x index b
| True
= go x [0 .. sFiniteBitSize x - 1]
where -- paranoia check: make sure index can fit in an int
safe i = let asInteger = toInteger i
asInt = fromIntegral asInteger
backInteger = toInteger asInt
in if backInteger == asInteger
then Just asInt
else Nothing
go v [] = v
go v (i:is) = go (ite (idx .== literal (fromIntegral i)) (setBitTo v (fromIntegral i) b) v) is
fullAdder a b
| isSigned a = error "fullAdder: only works on unsigned numbers"
| True = (a .> s .|| b .> s, s)
where s = a + b
-- N.B. The higher-order bits are determined using a simple shift-add multiplier,
-- thus involving bit-blasting. It'd be naive to expect SMT solvers to deal efficiently
-- with properties involving this function, at least with the current state of the art.
fullMultiplier a b
| isSigned a = error "fullMultiplier: only works on unsigned numbers"
| True = (go (sFiniteBitSize a) 0 a, a*b)
where go 0 p _ = p
go n p x = let (c, p') = ite (lsb x) (fullAdder p b) (sFalse, p)
(o, p'') = shiftIn c p'
(_, x') = shiftIn o x
in go (n-1) p'' x'
shiftIn k v = (lsb v, mask .|. (v `shiftR` 1))
where mask = ite k (bit (sFiniteBitSize v - 1)) 0
-- See the note for 'sPopCount' for a comment on why we return 'SWord8'
sCountLeadingZeros x = fromIntegral m - go m
where m = sFiniteBitSize x - 1
-- NB. When i is 0 below, which happens when x is 0 as we count all the way down,
-- we return -1, which is equal to 2^n-1, giving us: n-1-(2^n-1) = n-2^n = n, as required, i.e., the bit-size.
go :: Int -> SWord8
go i | i < 0 = i8
| True = ite (sTestBit x i) i8 (go (i-1))
where i8 = literal (fromIntegral i :: Word8)
-- See the note for 'sPopCount' for a comment on why we return 'SWord8'
sCountTrailingZeros x = go 0
where m = sFiniteBitSize x
go :: Int -> SWord8
go i | i >= m = i8
| True = ite (sTestBit x i) i8 (go (i+1))
where i8 = literal (fromIntegral i :: Word8)
-- 'SFiniteBits' Instances, skips Real/Float/Bool/Integer
instance SFiniteBits Word8 where sFiniteBitSize _ = 8
instance SFiniteBits Word16 where sFiniteBitSize _ = 16
instance SFiniteBits Word32 where sFiniteBitSize _ = 32
instance SFiniteBits Word64 where sFiniteBitSize _ = 64
instance SFiniteBits Int8 where sFiniteBitSize _ = 8
instance SFiniteBits Int16 where sFiniteBitSize _ = 16
instance SFiniteBits Int32 where sFiniteBitSize _ = 32
instance SFiniteBits Int64 where sFiniteBitSize _ = 64
instance (KnownNat n, BVIsNonZero n) => SFiniteBits (WordN n) where sFiniteBitSize _ = intOfProxy (Proxy @n)
instance (KnownNat n, BVIsNonZero n) => SFiniteBits (IntN n) where sFiniteBitSize _ = intOfProxy (Proxy @n)
-- | Returns 1 if the boolean is 'sTrue', otherwise 0.
oneIf :: (Ord a, Num (SBV a), SymVal a) => SBool -> SBV a
oneIf t = ite t 1 0
-- | Lift a pseudo-boolean op, performing checks
liftPB :: String -> PBOp -> [SBool] -> SBool
liftPB w o xs
| Just e <- check o
= error $ "SBV." ++ w ++ ": " ++ e
| True
= result
where check (PB_AtMost k) = pos k
check (PB_AtLeast k) = pos k
check (PB_Exactly k) = pos k
check (PB_Le cs k) = pos k `mplus` match cs
check (PB_Ge cs k) = pos k `mplus` match cs
check (PB_Eq cs k) = pos k `mplus` match cs
pos k
| k < 0 = Just $ "comparison value must be positive, received: " ++ show k
| True = Nothing
match cs
| any (< 0) cs = Just $ "coefficients must be non-negative. Received: " ++ show cs
| lxs /= lcs = Just $ "coefficient length must match number of arguments. Received: " ++ show (lcs, lxs)
| True = Nothing
where lxs = length xs
lcs = length cs
result = SBV (SVal KBool (Right (cache r)))
r st = do xsv <- mapM (sbvToSV st) xs
-- PseudoBoolean's implicitly require support for integers, so make sure to register that kind!
registerKind st KUnbounded
newExpr st KBool (SBVApp (PseudoBoolean o) xsv)
-- | 'sTrue' if at most @k@ of the input arguments are 'sTrue'
pbAtMost :: [SBool] -> Int -> SBool
pbAtMost xs k
| k < 0 = error $ "SBV.pbAtMost: Non-negative value required, received: " ++ show k
| all isConcrete xs = literal $ sum (map (pbToInteger "pbAtMost" 1) xs) <= fromIntegral k
| True = liftPB "pbAtMost" (PB_AtMost k) xs
-- | 'sTrue' if at least @k@ of the input arguments are 'sTrue'
pbAtLeast :: [SBool] -> Int -> SBool
pbAtLeast xs k
| k < 0 = error $ "SBV.pbAtLeast: Non-negative value required, received: " ++ show k
| all isConcrete xs = literal $ sum (map (pbToInteger "pbAtLeast" 1) xs) >= fromIntegral k
| True = liftPB "pbAtLeast" (PB_AtLeast k) xs
-- | 'sTrue' if exactly @k@ of the input arguments are 'sTrue'
pbExactly :: [SBool] -> Int -> SBool
pbExactly xs k
| k < 0 = error $ "SBV.pbExactly: Non-negative value required, received: " ++ show k
| all isConcrete xs = literal $ sum (map (pbToInteger "pbExactly" 1) xs) == fromIntegral k
| True = liftPB "pbExactly" (PB_Exactly k) xs
-- | 'sTrue' if the sum of coefficients for 'sTrue' elements is at most @k@. Generalizes 'pbAtMost'.
pbLe :: [(Int, SBool)] -> Int -> SBool
pbLe xs k
| k < 0 = error $ "SBV.pbLe: Non-negative value required, received: " ++ show k
| all (isConcrete . snd) xs = literal $ sum [pbToInteger "pbLe" c b | (c, b) <- xs] <= fromIntegral k
| True = liftPB "pbLe" (PB_Le (map fst xs) k) (map snd xs)
-- | 'sTrue' if the sum of coefficients for 'sTrue' elements is at least @k@. Generalizes 'pbAtLeast'.
pbGe :: [(Int, SBool)] -> Int -> SBool
pbGe xs k
| k < 0 = error $ "SBV.pbGe: Non-negative value required, received: " ++ show k
| all (isConcrete . snd) xs = literal $ sum [pbToInteger "pbGe" c b | (c, b) <- xs] >= fromIntegral k
| True = liftPB "pbGe" (PB_Ge (map fst xs) k) (map snd xs)
-- | 'sTrue' if the sum of coefficients for 'sTrue' elements is exactly least @k@. Useful for coding
-- /exactly K-of-N/ constraints, and in particular mutex constraints.
pbEq :: [(Int, SBool)] -> Int -> SBool
pbEq xs k
| k < 0 = error $ "SBV.pbEq: Non-negative value required, received: " ++ show k
| all (isConcrete . snd) xs = literal $ sum [pbToInteger "pbEq" c b | (c, b) <- xs] == fromIntegral k
| True = liftPB "pbEq" (PB_Eq (map fst xs) k) (map snd xs)
-- | 'sTrue' if there is at most one set bit
pbMutexed :: [SBool] -> SBool
pbMutexed xs = pbAtMost xs 1
-- | 'sTrue' if there is exactly one set bit
pbStronglyMutexed :: [SBool] -> SBool
pbStronglyMutexed xs = pbExactly xs 1
-- | Convert a concrete pseudo-boolean to given int; converting to integer
pbToInteger :: String -> Int -> SBool -> Integer
pbToInteger w c b
| c < 0 = error $ "SBV." ++ w ++ ": Non-negative coefficient required, received: " ++ show c
| Just v <- unliteral b = if v then fromIntegral c else 0
| True = error $ "SBV.pbToInteger: Received a symbolic boolean: " ++ show (c, b)
-- | Predicate for optimizing word operations like (+) and (*).
isConcreteZero :: SBV a -> Bool
isConcreteZero (SBV (SVal _ (Left (CV _ (CInteger n))))) = n == 0
isConcreteZero (SBV (SVal KReal (Left (CV KReal (CAlgReal v))))) = isExactRational v && v == 0
isConcreteZero _ = False
-- | Predicate for optimizing word operations like (+) and (*).
isConcreteOne :: SBV a -> Bool
isConcreteOne (SBV (SVal _ (Left (CV _ (CInteger 1))))) = True
isConcreteOne (SBV (SVal KReal (Left (CV KReal (CAlgReal v))))) = isExactRational v && v == 1
isConcreteOne _ = False
-- | Symbolic exponentiation using bit blasting and repeated squaring.
--
-- N.B. The exponent must be unsigned/bounded if symbolic. Signed exponents will be rejected.
(.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
b .^ e
| isConcrete e, Just (x :: Integer) <- unliteral (sFromIntegral e)
= if x >= 0 then let go n v
| n == 0 = 1
| even n = go (n `div` 2) (v * v)
| True = v * go (n `div` 2) (v * v)
in go x b
else error $ "(.^): exponentiation: negative exponent: " ++ show x
| not (isBounded e) || isSigned e
= error $ "(.^): exponentiation only works with unsigned bounded symbolic exponents, kind: " ++ show (kindOf e)
| True
= -- NB. We can't simply use sTestBit and blastLE since they have SFiniteBit requirement
-- but we want to have SIntegral here only.
let SBV expt = e
expBit i = SBV (svTestBit expt i)
blasted = map expBit [0 .. intSizeOf e - 1]
in product $ zipWith (\use n -> ite use n 1)
blasted
(iterate (\x -> x*x) b)
infixr 8 .^
instance (Ord a, Num (SBV a), SymVal a, Fractional a) => Fractional (SBV a) where
fromRational = literal . fromRational
SBV x / sy@(SBV y) | div0 = ite (sy .== 0) 0 res
| True = res
where res = SBV (svDivide x y)
-- Identify those kinds where we have a div-0 equals 0 exception
div0 = case kindOf sy of
KVar{} -> error $ "Unexpected Fractional case for: " ++ show (kindOf sy)
KFloat -> False
KDouble -> False
KFP{} -> False
KReal -> True
KRational -> True
-- Following cases should not happen since these types should *not* be instances of Fractional
k@KBounded{} -> error $ "Unexpected Fractional case for: " ++ show k
k@KUnbounded -> error $ "Unexpected Fractional case for: " ++ show k
k@KBool -> error $ "Unexpected Fractional case for: " ++ show k
k@KString -> error $ "Unexpected Fractional case for: " ++ show k
k@KChar -> error $ "Unexpected Fractional case for: " ++ show k
k@KList{} -> error $ "Unexpected Fractional case for: " ++ show k
k@KSet{} -> error $ "Unexpected Fractional case for: " ++ show k
k@KApp{} -> error $ "Unexpected Fractional case for: " ++ show k
k@KADT{} -> error $ "Unexpected Fractional case for: " ++ show k
k@KTuple{} -> error $ "Unexpected Fractional case for: " ++ show k
k@KArray{} -> error $ "Unexpected Fractional case for: " ++ show k
-- | Define Floating instance on SBV's; only for base types that are already floating; i.e., 'SFloat', 'SDouble', and 'SReal'.
-- (See the separate definition below for 'SFloatingPoint'.) Note that unless you use delta-sat via 'Data.SBV.Provers.dReal' on 'SReal', most
-- of the fields are "undefined" for symbolic values. We will add methods as they are supported by SMTLib. Currently, the
-- only symbolically available function in this class is 'sqrt' for 'SFloat', 'SDouble' and 'SFloatingPoint'.
instance (Ord a, Num (SBV a), SymVal a, Fractional a, Floating a) => Floating (SBV a) where
pi = fromRational . toRational $ (pi :: Double)
exp = lift1FNS "exp" exp
log = lift1FNS "log" log
sqrt = lift1F FP_Sqrt sqrt
sin = lift1FNS "sin" sin
cos = lift1FNS "cos" cos
tan = lift1FNS "tan" tan
asin = lift1FNS "asin" asin
acos = lift1FNS "acos" acos
atan = lift1FNS "atan" atan
sinh = lift1FNS "sinh" sinh
cosh = lift1FNS "cosh" cosh
tanh = lift1FNS "tanh" tanh
asinh = lift1FNS "asinh" asinh
acosh = lift1FNS "acosh" acosh
atanh = lift1FNS "atanh" atanh
(**) = lift2FNS "**" (**)
logBase = lift2FNS "logBase" logBase
unsupported :: String -> a
unsupported w = error $ "Data.SBV.FloatingPoint: Unsupported operation: " ++ w ++ ". Please request this as a feature!"
-- | We give a specific instance for 'SFloatingPoint', because the underlying floating-point type doesn't support
-- fromRational directly. The overlap with the above instance is unfortunate.
instance {-# OVERLAPPING #-} ValidFloat eb sb => Floating (SFloatingPoint eb sb) where
-- Try from double; if there's enough precision this'll work, otherwise will bail out.
pi
| ei > 11 || si > 53 = unsupported $ "Floating.SFloatingPoint.pi (not-enough-precision for " ++ show (ei, si) ++ ")"
| True = literal $ FloatingPoint $ fpFromRational ei si (toRational (pi :: Double))
where ei = intOfProxy (Proxy @eb)
si = intOfProxy (Proxy @sb)
-- Likewise, exponentiation is again limited to precision of double
exp i
| ei > 11 || si > 53 = unsupported $ "Floating.SFloatingPoint.exp (not-enough-precision for " ++ show (ei, si) ++ ")"
| True = literal e ** i
where ei = intOfProxy (Proxy @eb)
si = intOfProxy (Proxy @sb)
e = FloatingPoint $ fpFromRational ei si (toRational (exp 1 :: Double))
log = lift1FNS "log" log
sqrt = lift1F FP_Sqrt sqrt
sin = lift1FNS "sin" sin
cos = lift1FNS "cos" cos
tan = lift1FNS "tan" tan
asin = lift1FNS "asin" asin
acos = lift1FNS "acos" acos
atan = lift1FNS "atan" atan
sinh = lift1FNS "sinh" sinh
cosh = lift1FNS "cosh" cosh
tanh = lift1FNS "tanh" tanh
asinh = lift1FNS "asinh" asinh
acosh = lift1FNS "acosh" acosh
atanh = lift1FNS "atanh" atanh
(**) = lift2FNS "**" (**)
logBase = lift2FNS "logBase" logBase
-- | Lift a 1 arg FP-op, using sRNE default
lift1F :: SymVal a => FPOp -> (a -> a) -> SBV a -> SBV a
lift1F w op a
| Just v <- unliteral a
= literal $ op v
| True
= SBV $ SVal k $ Right $ cache r
where k = kindOf a
r st = do swa <- sbvToSV st a
swm <- sbvToSV st sRNE
newExpr st k (SBVApp (IEEEFP w) [swm, swa])
-- | Lift a float/double unary function, only over constants
lift1FNS :: (SymVal a, Floating a) => String -> (a -> a) -> SBV a -> SBV a
lift1FNS nm f sv
| Just v <- unliteral sv = literal $ f v
| True = error $ "SBV." ++ nm ++ ": not supported for symbolic values of type " ++ show (kindOf sv)
-- | Lift a float/double binary function, only over constants
lift2FNS :: (SymVal a, Floating a) => String -> (a -> a -> a) -> SBV a -> SBV a -> SBV a
lift2FNS nm f sv1 sv2
| Just v1 <- unliteral sv1
, Just v2 <- unliteral sv2 = literal $ f v1 v2
| True = error $ "SBV." ++ nm ++ ": not supported for symbolic values of type " ++ show (kindOf sv1)
-- | SReal Floating instance, used in conjunction with the dReal solver for delta-satisfiability. Note that
-- we do not constant fold these values (except for pi), as Haskell doesn't really have any means of computing
-- them for arbitrary rationals.
instance {-# OVERLAPPING #-} Floating SReal where
-- Should we support pi? It's a transcendental value, and our SReal type has no way of representing
-- this quantity with the required fidelity. (SReal can only support roots of polynomials and rationals
-- correctly, not transcendentals.) One option is to use an approximation here. But that goes against the
-- whole idea of Real being infinitely precise. Another option is to see if the solver has support for it, such
-- as CVC5, which has the constant real.pi. Alas, that has its problems: In models CVC5 uses real.pi as a
-- model value, which we have no way of properly supporting back as a Haskell value. Worse: It uses it in
-- expressions like 1 + real.pi, which we don't have an evaluator for. So, we simply say not supported.
-- If you want it for reals, you'll have to plugin your own "approximation" for it, and thus be aware of the
-- limitations of that choice.
pi = error $ unlines [ ""
, "*** Data.SBV.SReal: Cannot represent pi as an SReal value."
, "***"
, "*** Usual trick is to use an approximation if that suits your purpose,"
, "*** or use solver-specific constants when applicable. Please get in touch"
, "*** if you'd like to explore ideas here."
]
exp = lift1SReal NR_Exp
log = lift1SReal NR_Log
sqrt = lift1SReal NR_Sqrt
sin = lift1SReal NR_Sin
cos = lift1SReal NR_Cos
tan = lift1SReal NR_Tan
asin = lift1SReal NR_ASin
acos = lift1SReal NR_ACos
atan = lift1SReal NR_ATan
sinh = lift1SReal NR_Sinh
cosh = lift1SReal NR_Cosh
tanh = lift1SReal NR_Tanh
asinh = error "Data.SBV.SReal: asinh is currently not supported. Please request this as a feature!"
acosh = error "Data.SBV.SReal: acosh is currently not supported. Please request this as a feature!"
atanh = error "Data.SBV.SReal: atanh is currently not supported. Please request this as a feature!"
(**) = lift2SReal NR_Pow
logBase x y = log y / log x
-- | Lift an sreal unary function
lift1SReal :: NROp -> SReal -> SReal
lift1SReal w a = SBV $ SVal k $ Right $ cache r
where k = kindOf a
r st = do swa <- sbvToSV st a
newExpr st k (SBVApp (NonLinear w) [swa])
-- | Lift an sreal binary function
lift2SReal :: NROp -> SReal -> SReal -> SReal
lift2SReal w a b = SBV $ SVal k $ Right $ cache r
where k = kindOf a
r st = do swa <- sbvToSV st a
swb <- sbvToSV st b
newExpr st k (SBVApp (NonLinear w) [swa, swb])
-- Bail out nicely.
noEquals :: String -> String -> (String, String) -> a
noEquals o n (l, r) = error $ unlines [ ""
, "*** Data.SBV: Comparing symbolic values using Haskell's Eq class!"
, "***"
, "*** Received: (" ++ l ++ ") " ++ o ++ " (" ++ r ++ ")"
, "*** Instead use: (" ++ l ++ ") " ++ n ++ " (" ++ r ++ ")"
, "***"
, "*** The Eq instance for symbolic values are necessiated only because"
, "*** of the Bits class requirement. You must use symbolic equality"
, "*** operators instead. (And complain to Haskell folks that they"
, "*** remove the 'Eq' superclass from 'Bits'!.)"
]
-- | This instance is only defined so that we can define an instance for
-- 'Data.Bits.Bits'. '==' and '/=' simply throw an error. Use
-- 'Data.SBV.EqSymbolic' instead.
instance SymVal a => Eq (SBV a) where
a == b = fromMaybe (noEquals "==" ".==" (show a, show b)) (unliteral (a .== b))
a /= b = fromMaybe (noEquals "/=" "./=" (show a, show b)) (unliteral (a ./= b))
-- NB. In the optimizations below, use of -1 is valid as
-- -1 has all bits set to True for both signed and unsigned values
-- | Using 'popCount' or 'testBit' on non-concrete values will result in an
-- error. Use 'sPopCount' or 'sTestBit' instead.
instance (Ord a, Num (SBV a), Num a, Bits a, SymVal a) => Bits (SBV a) where
SBV x .&. SBV y = SBV (svAnd x y)
SBV x .|. SBV y = SBV (svOr x y)
SBV x `xor` SBV y = SBV (svXOr x y)
complement (SBV x) = SBV (svNot x)
bitSize x = intSizeOf x
bitSizeMaybe x = Just $ intSizeOf x
isSigned x = hasSign x
bit i = 1 `shiftL` i
setBit x i = x .|. genLiteral (kindOf x) (bit i :: Integer)
clearBit x i = x .&. genLiteral (kindOf x) (complement (bit i) :: Integer)
complementBit x i = x `xor` genLiteral (kindOf x) (bit i :: Integer)
shiftL (SBV x) i = SBV (svShl x i)
shiftR (SBV x) i = SBV (svShr x i)
rotateL (SBV x) i = SBV (svRol x i)
rotateR (SBV x) i = SBV (svRor x i)
-- NB. testBit is *not* implementable on non-concrete symbolic words
x `testBit` i
| SBV (SVal _ (Left (CV _ (CInteger n)))) <- x
= testBit n i
| True
= error $ "SBV.testBit: Called on symbolic value: " ++ show x ++ ". Use sTestBit instead."
-- NB. popCount is *not* implementable on non-concrete symbolic words
popCount x
| SBV (SVal _ (Left (CV (KBounded _ w) (CInteger n)))) <- x
= popCount (n .&. (bit w - 1))
| True
= error $ "SBV.popCount: Called on symbolic value: " ++ show x ++ ". Use sPopCount instead."
-- | Conversion between integral-symbolic values, akin to Haskell's `fromIntegral`
sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> SBV b
sFromIntegral x
| kFrom == kTo
= SBV (unSBV x)
| isReal x
= error "SBV.sFromIntegral: Called on a real value" -- can't really happen due to types, but being overcautious
| Just v <- unliteral x
= literal (fromIntegral v)
| True
= result
where result = SBV (SVal kTo (Right (cache y)))
kFrom = kindOf x
kTo = kindOf (Proxy @b)
y st = do xsv <- sbvToSV st x
newExpr st kTo (SBVApp (KindCast kFrom kTo) [xsv])
-- | Lift a binary operation thru its dynamic counterpart. Note that
-- we still want the actual functions here as differ in their type
-- compared to their dynamic counterparts, but the implementations
-- are the same.
liftViaSVal :: (SVal -> SVal -> SVal) -> SBV a -> SBV b -> SBV c
liftViaSVal f (SBV a) (SBV b) = SBV $ f a b
-- | Generalization of 'shiftL', when the shift-amount is symbolic. Since Haskell's
-- 'shiftL' only takes an 'Int' as the shift amount, it cannot be used when we have
-- a symbolic amount to shift with.
sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sShiftLeft = liftViaSVal svShiftLeft
-- | Generalization of 'shiftR', when the shift-amount is symbolic. Since Haskell's
-- 'shiftR' only takes an 'Int' as the shift amount, it cannot be used when we have
-- a symbolic amount to shift with.
--
-- NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical,
-- following the usual Haskell convention. See 'sSignedShiftArithRight' for a variant
-- that explicitly uses the msb as the sign bit, even for unsigned underlying types.
sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sShiftRight = liftViaSVal svShiftRight
-- | Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent
-- to 'sShiftRight' when the argument is signed. However, if the argument is unsigned,
-- then it explicitly treats its msb as a sign-bit, and uses it as the bit that
-- gets shifted in. Useful when using the underlying unsigned bit representation to implement
-- custom signed operations. Note that there is no direct Haskell analogue of this function.
sSignedShiftArithRight:: (SFiniteBits a, SIntegral b) => SBV a -> SBV b -> SBV a
sSignedShiftArithRight x i
| isSigned i = error "sSignedShiftArithRight: shift amount should be unsigned"
| isSigned x = ssa x i
| True = ite (msb x)
(complement (ssa (complement x) i))
(ssa x i)
where ssa = liftViaSVal svShiftRight
-- | Generalization of 'rotateL', when the shift-amount is symbolic. Since Haskell's
-- 'rotateL' only takes an 'Int' as the shift amount, it cannot be used when we have
-- a symbolic amount to shift with. The first argument should be a bounded quantity.
sRotateLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sRotateLeft = liftViaSVal svRotateLeft
-- | An implementation of rotate-left, using a barrel shifter like design. Only works when both
-- arguments are finite bit-vectors, and furthermore when the second argument is unsigned.
-- The first condition is enforced by the type, but the second is dynamically checked.
-- We provide this implementation as an alternative to `sRotateLeft` since SMTLib logic
-- does not support variable argument rotates (as opposed to shifts), and thus this
-- implementation can produce better code for verification compared to `sRotateLeft`.
sBarrelRotateLeft :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a
sBarrelRotateLeft = liftViaSVal svBarrelRotateLeft
-- | Generalization of 'rotateR', when the shift-amount is symbolic. Since Haskell's
-- 'rotateR' only takes an 'Int' as the shift amount, it cannot be used when we have
-- a symbolic amount to shift with. The first argument should be a bounded quantity.
sRotateRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
sRotateRight = liftViaSVal svRotateRight
-- | An implementation of rotate-right, using a barrel shifter like design. See comments
-- for `sBarrelRotateLeft` for details.
sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a
sBarrelRotateRight = liftViaSVal svBarrelRotateRight
-- | Capturing non-matching instances for better error messages, conversions from sized
type FromSizedErr (arg :: Type) = 'Text "fromSized: Cannot convert from type: " ':<>: 'ShowType arg
':$$: 'Text " Source type must be one of SInt N, SWord N, IntN N, WordN N"
':$$: 'Text " where N is 8, 16, 32, or 64."
-- | Capturing non-matching instances for better error messages, conversions to sized
type ToSizedErr (arg :: Type) = 'Text "toSized: Cannot convert from type: " ':<>: 'ShowType arg
':$$: 'Text " Source type must be one of Int8/16/32/64"
':$$: 'Text " OR Word8/16/32/64"
':$$: 'Text " OR their symbolic variants."
-- | Capture the correspondence between sized and fixed-sized BVs
type family FromSized (t :: Type) :: Type where
FromSized (WordN 8) = Word8
FromSized (WordN 16) = Word16
FromSized (WordN 32) = Word32
FromSized (WordN 64) = Word64
FromSized (IntN 8) = Int8
FromSized (IntN 16) = Int16
FromSized (IntN 32) = Int32
FromSized (IntN 64) = Int64
FromSized (SWord 8) = SWord8
FromSized (SWord 16) = SWord16
FromSized (SWord 32) = SWord32
FromSized (SWord 64) = SWord64
FromSized (SInt 8) = SInt8
FromSized (SInt 16) = SInt16
FromSized (SInt 32) = SInt32
FromSized (SInt 64) = SInt64
-- | Capture the correspondence, in terms of a constraint
type family FromSizedCstr (t :: Type) :: Constraint where
FromSizedCstr (WordN 8) = ()
FromSizedCstr (WordN 16) = ()
FromSizedCstr (WordN 32) = ()
FromSizedCstr (WordN 64) = ()
FromSizedCstr (IntN 8) = ()
FromSizedCstr (IntN 16) = ()
FromSizedCstr (IntN 32) = ()
FromSizedCstr (IntN 64) = ()
FromSizedCstr (SWord 8) = ()
FromSizedCstr (SWord 16) = ()
FromSizedCstr (SWord 32) = ()
FromSizedCstr (SWord 64) = ()
FromSizedCstr (SInt 8) = ()
FromSizedCstr (SInt 16) = ()
FromSizedCstr (SInt 32) = ()
FromSizedCstr (SInt 64) = ()
FromSizedCstr arg = TypeError (FromSizedErr arg)
-- | Conversion from a sized BV to a fixed-sized bit-vector.
class FromSizedBV a where
-- | Convert a sized bit-vector to the corresponding fixed-sized bit-vector,
-- for instance 'SWord 16' to 'SWord16'. See also 'toSized'.
fromSized :: a -> FromSized a
default fromSized :: (Num (FromSized a), Integral a) => a -> FromSized a
fromSized = fromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (WordN 8)
instance {-# OVERLAPPING #-} FromSizedBV (WordN 16)
instance {-# OVERLAPPING #-} FromSizedBV (WordN 32)
instance {-# OVERLAPPING #-} FromSizedBV (WordN 64)
instance {-# OVERLAPPING #-} FromSizedBV (IntN 8)
instance {-# OVERLAPPING #-} FromSizedBV (IntN 16)
instance {-# OVERLAPPING #-} FromSizedBV (IntN 32)
instance {-# OVERLAPPING #-} FromSizedBV (IntN 64)
instance {-# OVERLAPPING #-} FromSizedBV (SWord 8) where fromSized = sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SWord 16) where fromSized = sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SWord 32) where fromSized = sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SWord 64) where fromSized = sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SInt 8) where fromSized = sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SInt 16) where fromSized = sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SInt 32) where fromSized = sFromIntegral
instance {-# OVERLAPPING #-} FromSizedBV (SInt 64) where fromSized = sFromIntegral
instance {-# OVERLAPPABLE #-} FromSizedCstr arg => FromSizedBV arg where fromSized = error "unreachable"
-- | Capture the correspondence between fixed-sized and sized BVs
type family ToSized (t :: Type) :: Type where
ToSized Word8 = WordN 8
ToSized Word16 = WordN 16
ToSized Word32 = WordN 32
ToSized Word64 = WordN 64
ToSized Int8 = IntN 8
ToSized Int16 = IntN 16
ToSized Int32 = IntN 32
ToSized Int64 = IntN 64
ToSized SWord8 = SWord 8
ToSized SWord16 = SWord 16
ToSized SWord32 = SWord 32
ToSized SWord64 = SWord 64
ToSized SInt8 = SInt 8
ToSized SInt16 = SInt 16
ToSized SInt32 = SInt 32
ToSized SInt64 = SInt 64
-- | Capture the correspondence in terms of a constraint
type family ToSizedCstr (t :: Type) :: Constraint where
ToSizedCstr Word8 = ()
ToSizedCstr Word16 = ()
ToSizedCstr Word32 = ()
ToSizedCstr Word64 = ()
ToSizedCstr Int8 = ()
ToSizedCstr Int16 = ()
ToSizedCstr Int32 = ()
ToSizedCstr Int64 = ()
ToSizedCstr SWord8 = ()
ToSizedCstr SWord16 = ()
ToSizedCstr SWord32 = ()
ToSizedCstr SWord64 = ()
ToSizedCstr SInt8 = ()
ToSizedCstr SInt16 = ()
ToSizedCstr SInt32 = ()
ToSizedCstr SInt64 = ()
ToSizedCstr arg = TypeError (ToSizedErr arg)
-- | Conversion from a fixed-sized BV to a sized bit-vector.
class ToSizedBV a where
-- | Convert a fixed-sized bit-vector to the corresponding sized bit-vector,
-- for instance 'SWord16' to 'SWord 16'. See also 'fromSized'.
toSized :: a -> ToSized a
default toSized :: (Num (ToSized a), Integral a) => (a -> ToSized a)
toSized = fromIntegral
instance {-# OVERLAPPING #-} ToSizedBV Word8
instance {-# OVERLAPPING #-} ToSizedBV Word16
instance {-# OVERLAPPING #-} ToSizedBV Word32
instance {-# OVERLAPPING #-} ToSizedBV Word64
instance {-# OVERLAPPING #-} ToSizedBV Int8
instance {-# OVERLAPPING #-} ToSizedBV Int16
instance {-# OVERLAPPING #-} ToSizedBV Int32
instance {-# OVERLAPPING #-} ToSizedBV Int64
instance {-# OVERLAPPING #-} ToSizedBV SWord8 where toSized = sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SWord16 where toSized = sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SWord32 where toSized = sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SWord64 where toSized = sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SInt8 where toSized = sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SInt16 where toSized = sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SInt32 where toSized = sFromIntegral
instance {-# OVERLAPPING #-} ToSizedBV SInt64 where toSized = sFromIntegral
instance {-# OVERLAPPABLE #-} ToSizedCstr arg => ToSizedBV arg where toSized = error "unreachable"
-- | The 'SDivisible' class captures the essence of division.
-- Unfortunately we cannot use Haskell's 'Integral' class since the 'Real'
-- and 'Enum' superclasses are not implementable for symbolic bit-vectors.
-- However, 'quotRem' and 'divMod' both make perfect sense, and the 'SDivisible' class captures
-- this operation. One issue is how division by 0 behaves. The verification
-- technology requires total functions, and there are several design choices
-- here. We follow Isabelle/HOL approach of assigning the value 0 for division
-- by 0. Therefore, we impose the following pair of laws:
--
-- @
-- x `sQuotRem` 0 = (0, x)
-- x `sDivMod` 0 = (0, x)
-- @
--
-- Note that our instances implement this law even when @x@ is @0@ itself.
--
-- NB. 'quot' truncates toward zero, while 'div' truncates toward negative infinity.
--
-- === C code generation of division operations
--
-- In the case of division or modulo of a minimal signed value (e.g. @-128@ for
-- 'SInt8') by @-1@, SMTLIB and Haskell agree on what the result should be.
-- Unfortunately the result in C code depends on CPU architecture and compiler
-- settings, as this is undefined behaviour in C. **SBV does not guarantee**
-- what will happen in generated C code in this corner case.
class SDivisible a where
sQuotRem :: a -> a -> (a, a)
sDivMod :: a -> a -> (a, a)
sQuot :: a -> a -> a
sRem :: a -> a -> a
sDiv :: a -> a -> a
sMod :: a -> a -> a
{-# MINIMAL sQuotRem, sDivMod #-}
x `sQuot` y = fst $ x `sQuotRem` y
x `sRem` y = snd $ x `sQuotRem` y
x `sDiv` y = fst $ x `sDivMod` y
x `sMod` y = snd $ x `sDivMod` y
instance SDivisible Word64 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Int64 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Word32 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Int32 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Word16 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Int16 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Word8 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Int8 where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible Integer where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
instance SDivisible CV where
sQuotRem a b
| CInteger x <- cvVal a, CInteger y <- cvVal b
= let (r1, r2) = sQuotRem x y in (normCV a{ cvVal = CInteger r1 }, normCV b{ cvVal = CInteger r2 })
sQuotRem a b = error $ "SBV.sQuotRem: impossible, unexpected args received: " ++ show (a, b)
sDivMod a b
| CInteger x <- cvVal a, CInteger y <- cvVal b
= let (r1, r2) = sDivMod x y in (normCV a{ cvVal = CInteger r1 }, normCV b{ cvVal = CInteger r2 })
sDivMod a b = error $ "SBV.sDivMod: impossible, unexpected args received: " ++ show (a, b)
instance SDivisible SWord64 where {sQuotRem = liftQRem; sDivMod = liftDMod}
instance SDivisible SWord32 where {sQuotRem = liftQRem; sDivMod = liftDMod}
instance SDivisible SWord16 where {sQuotRem = liftQRem; sDivMod = liftDMod}
instance SDivisible SWord8 where {sQuotRem = liftQRem; sDivMod = liftDMod}
instance SDivisible SInt64 where {sQuotRem = liftQRem; sDivMod = liftDMod}
instance SDivisible SInt32 where {sQuotRem = liftQRem; sDivMod = liftDMod}
instance SDivisible SInt16 where {sQuotRem = liftQRem; sDivMod = liftDMod}
instance SDivisible SInt8 where {sQuotRem = liftQRem; sDivMod = liftDMod}
-- | 'SDivisible' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SDivisible (WordN n) where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
-- | 'SDivisible' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SDivisible (IntN n) where
sQuotRem x 0 = (0, x)
sQuotRem x y = x `quotRem` y
sDivMod x 0 = (0, x)
sDivMod x y = x `divMod` y
-- | 'SDivisible' instance for 'SWord'
instance (KnownNat n, BVIsNonZero n) => SDivisible (SWord n) where
sQuotRem = liftQRem
sDivMod = liftDMod
-- | 'SDivisible' instance for 'SInt'
instance (KnownNat n, BVIsNonZero n) => SDivisible (SInt n) where
sQuotRem = liftQRem
sDivMod = liftDMod
-- | Does the concrete positive number n divide the given integer?
sDivides :: Integer -> SInteger -> SBool
sDivides n v
| n < 0
= error $ "svDivides: First argument must be a strictly positive integer. Received: " ++ show n
| Just x <- unliteral v
= if x `mod` n == 0 then sTrue else sFalse
| True
= SBV $ svDivides n (unSBV v)
-- | Lift 'quotRem' to symbolic words. Division by 0 is defined s.t. @x/0 = 0@; which
-- holds even when @x@ is @0@ itself.
liftQRem :: (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)
liftQRem x y
| isConcreteZero x
= (x, x)
| isConcreteOne y
= (x, z)
{-------------------------------
- N.B. The seemingly innocuous variant when y == -1 only holds if the type is signed;
- and also is problematic around the minBound.. So, we refrain from that optimization
| isConcreteOnes y
= (-x, z)
--------------------------------}
| True
= ite (y .== z) (z, x) (qr x y)
where qr (SBV (SVal sgnsz (Left a))) (SBV (SVal _ (Left b))) = let (q, r) = sQuotRem a b in (SBV (SVal sgnsz (Left q)), SBV (SVal sgnsz (Left r)))
qr a@(SBV (SVal sgnsz _)) b = (SBV (SVal sgnsz (Right (cache (mk Quot)))), SBV (SVal sgnsz (Right (cache (mk Rem)))))
where mk o st = do sw1 <- sbvToSV st a
sw2 <- sbvToSV st b
mkSymOp o st sgnsz sw1 sw2
z = genLiteral (kindOf x) (0::Integer)
-- | Lift 'divMod' to symbolic words. Division by 0 is defined s.t. @x/0 = 0@; which
-- holds even when @x@ is @0@ itself. Essentially, this is conversion from quotRem
-- (truncate to 0) to divMod (truncate towards negative infinity)
liftDMod :: (Ord a, SymVal a, Num a, Num (SBV a), SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
liftDMod x y
| isConcreteZero x
= (x, x)
| isConcreteOne y
= (x, z)
{-------------------------------
- N.B. The seemingly innocuous variant when y == -1 only holds if the type is signed;
- and also is problematic around the minBound.. So, we refrain from that optimization
| isConcreteOnes y
= (-x, z)
--------------------------------}
| True
= ite (y .== z) (z, x) $ ite (signum r .== negate (signum y)) (q-i, r+y) qr
where qr@(q, r) = x `sQuotRem` y
z = genLiteral (kindOf x) (0::Integer)
i = genLiteral (kindOf x) (1::Integer)
-- SInteger instance for quotRem/divMod are tricky!
-- SMT-Lib only has Euclidean operations, but Haskell
-- uses "truncate to 0" for quotRem, and "truncate to negative infinity" for divMod.
-- So, we cannot just use the above liftings directly.
instance SDivisible SInteger where
sDivMod x y = ite (y .> 0) (sEDivMod x y) (liftDMod x y)
sQuotRem x y
| not (isSymbolic x || isSymbolic y)
= liftQRem x y
| True
= ite (y .== 0) (0, x) (qE+i, rE-i*y)
where (qE, rE) = liftQRem x y -- for integers, this is euclidean due to SMTLib semantics
i = ite (x .>= 0 .|| rE .== 0) 0
$ ite (y .> 0) 1 (-1)
-- | Euclidian division and modulus.
sEDivMod :: SInteger -> SInteger -> (SInteger, SInteger)
sEDivMod a b = (a `sEDiv` b, a `sEMod` b)
-- | Euclidian division. Note that unlike regular division, Euclidian division by @0@
-- is unconstrained. i.e., it can take any value whatsoever.
sEDiv :: SInteger -> SInteger -> SInteger
sEDiv (SBV a) (SBV b) = SBV $ a `svQuot` b
-- | Euclidian modulus. Note that unlike regular modulus, Euclidian division by @0@
-- is unconstrained. i.e., it can take any value whatsoever.
sEMod :: SInteger -> SInteger -> SInteger
sEMod (SBV a) (SBV b) = SBV $ a `svRem` b
-- Quickcheck interface
instance (SymVal a, Arbitrary a) => Arbitrary (SBV a) where
arbitrary = literal <$> arbitrary
-- | Symbolic conditionals are modeled by the 'Mergeable' class, describing
-- how to merge the results of an if-then-else call with a symbolic test. SBV
-- provides all basic types as instances of this class, so users only need
-- to declare instances for custom data-types of their programs as needed.
--
-- A 'Mergeable' instance may be automatically derived for a custom data-type
-- with a single constructor where the type of each field is an instance of
-- 'Mergeable', such as a record of symbolic values. Users only need to add
-- 'G.Generic' and 'Mergeable' to the @deriving@ clause for the data-type. See
-- 'Documentation.SBV.Examples.Puzzles.U2Bridge.Status' for an example and an
-- illustration of what the instance would look like if written by hand.
--
-- The function 'select' is a total-indexing function out of a list of choices
-- with a default value, simulating array/list indexing. It's an n-way generalization
-- of the 'ite' function.
--
-- Minimal complete definition: None, if the type is instance of @Generic@. Otherwise
-- 'symbolicMerge'. Note that most types subject to merging are likely to be
-- trivial instances of @Generic@.
class Mergeable a where
-- | Merge two values based on the condition. The first argument states
-- whether we force the then-and-else branches before the merging, at the
-- word level. This is an efficiency concern; one that we'd rather not
-- make but unfortunately necessary for getting symbolic simulation
-- working efficiently.
symbolicMerge :: Bool -> SBool -> a -> a -> a
-- | Total indexing operation. @select xs default index@ is intuitively
-- the same as @xs !! index@, except it evaluates to @default@ if @index@
-- underflows/overflows.
select :: (Ord b, SymVal b, Num b, Num (SBV b), OrdSymbolic (SBV b)) => [a] -> a -> SBV b -> a
-- NB. Earlier implementation of select used the binary-search trick
-- on the index to chop down the search space. While that is a good trick
-- in general, it doesn't work for SBV since we do not have any notion of
-- "concrete" subwords: If an index is symbolic, then all its bits are
-- symbolic as well. So, the binary search only pays off only if the indexed
-- list is really humongous, which is not very common in general. (Also,
-- for the case when the list is bit-vectors, we use SMT tables anyhow.)
select xs err ind
| isReal ind = bad "real"
| isFloat ind = bad "float"
| isDouble ind = bad "double"
| hasSign ind = ite (ind .< 0) err (walk xs ind err)
| True = walk xs ind err
where bad w = error $ "SBV.select: unsupported " ++ w ++ " valued select/index expression"
walk [] _ acc = acc
walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc)
-- Default implementation for 'symbolicMerge' if the type is 'Generic'
default symbolicMerge :: (G.Generic a, GMergeable (G.Rep a)) => Bool -> SBool -> a -> a -> a
symbolicMerge = symbolicMergeDefault
-- | If-then-else. This is by definition 'symbolicMerge' with both
-- branches forced. This is typically the desired behavior, but also
-- see 'iteLazy' should you need more laziness.
ite :: Mergeable a => SBool -> a -> a -> a
ite t a b
| Just r <- unliteral t = if r then a else b
| True = symbolicMerge True t a b
-- | A Lazy version of ite, which does not force its arguments. This might
-- cause issues for symbolic simulation with large thunks around, so use with
-- care.
iteLazy :: Mergeable a => SBool -> a -> a -> a
iteLazy t a b
| Just r <- unliteral t = if r then a else b
| True = symbolicMerge False t a b
-- | Symbolic assert. Check that the given boolean condition is always 'sTrue' in the given path. The
-- optional first argument can be used to provide call-stack info via GHC's location facilities.
sAssert :: HasKind a => Maybe CallStack -> String -> SBool -> SBV a -> SBV a
sAssert cs msg cond x
| Just mustHold <- unliteral cond
= if mustHold
then x
else error $ show $ SafeResult (locInfo . getCallStack <$> cs, msg, Satisfiable defaultSMTCfg (SMTModel [] Nothing [] []))
| True
= SBV $ SVal k $ Right $ cache r
where k = kindOf x
r st = do xsv <- sbvToSV st x
let pc = getPathCondition st
-- We're checking if there are any cases where the path-condition holds, but not the condition
-- Any violations of this, should be signaled, i.e., whenever the following formula is satisfiable
mustNeverHappen = pc .&& sNot cond
cnd <- sbvToSV st mustNeverHappen
addAssertion st cs msg cnd
pure xsv
locInfo ps = intercalate ",\n " (map loc ps)
where loc (f, sl) = concat [srcLocFile sl, ":", show (srcLocStartLine sl), ":", show (srcLocStartCol sl), ":", f]
-- | Merge two symbolic values, at kind @k@, possibly @force@'ing the branches to make
-- sure they do not evaluate to the same result. This should only be used for internal purposes;
-- as default definitions provided should suffice in many cases. (i.e., End users should
-- only need to define 'symbolicMerge' when needed; which should be rare to start with.)
symbolicMergeWithKind :: Kind -> Bool -> SBool -> SBV a -> SBV a -> SBV a
symbolicMergeWithKind k force (SBV t) (SBV a) (SBV b) = SBV (svSymbolicMerge k force t a b)
instance SymVal a => Mergeable (SBV a) where
symbolicMerge force t x y
-- Carefully use the kindOf instance to avoid strictness issues.
| force = symbolicMergeWithKind (kindOf x) True t x y
| True = symbolicMergeWithKind (kindOf (Proxy @a)) False t x y
-- Custom version of select that translates to SMT-Lib tables at the base type of words
select xs err ind
| SBV (SVal _ (Left c)) <- ind = case cvVal c of
CInteger i -> if i < 0 || i >= genericLength xs
then err
else xs `genericIndex` i
_ -> error $ "SBV.select: unsupported " ++ show (kindOf ind) ++ " valued select/index expression"
select xsOrig err ind = xs `seq` SBV (SVal kElt (Right (cache r)))
where kInd = kindOf ind
kElt = kindOf err
-- Based on the index size, we need to limit the elements. For instance if the index is 8 bits, but there
-- are 257 elements, that last element will never be used and we can chop it of..
xs = case kindOf ind of
KBounded False i -> genericTake ((2::Integer) ^ (fromIntegral i :: Integer)) xsOrig
KBounded True i -> genericTake ((2::Integer) ^ (fromIntegral (i-1) :: Integer)) xsOrig
KUnbounded -> xsOrig
_ -> error $ "SBV.select: unsupported " ++ show (kindOf ind) ++ " valued select/index expression"
r st = do sws <- mapM (sbvToSV st) xs
swe <- sbvToSV st err
if all (== swe) sws -- off-chance that all elts are the same. Note that this also correctly covers the case when list is empty.
then pure swe
else do idx <- getTableIndex st kInd kElt sws
swi <- sbvToSV st ind
let len = length xs
-- NB. No need to worry here that the index might be < 0; as the SMTLib translation takes care of that automatically
newExpr st kElt (SBVApp (LkUp (idx, kInd, kElt, len) swi swe) [])
-- | Construct a useful error message if we hit an unmergeable case.
cannotMerge :: String -> String -> String -> a
cannotMerge typ why hint = error $ unlines [ ""
, "*** Data.SBV.Mergeable: Cannot merge instances of " ++ typ ++ "."
, "*** While trying to do a symbolic if-then-else with incompatible branch results."
, "***"
, "*** " ++ why
, "*** "
, "*** Hint: " ++ hint
]
-- | Merge concrete values that can be checked for equality
concreteMerge :: Show a => String -> String -> (a -> a -> Bool) -> a -> a -> a
concreteMerge t st eq x y
| x `eq` y = x
| True = cannotMerge t
("Concrete values can only be merged when equal. Got: " ++ show x ++ " vs. " ++ show y)
("Use an " ++ st ++ " field if the values can differ.")
-- Mergeable instances for List/Maybe/Either/Array are useful, but can
-- throw exceptions if there is no structural matching of the results
-- It's a question whether we should really keep them..
-- Lists
instance Mergeable a => Mergeable [a] where
symbolicMerge f t xs ys
| lxs == lys = zipWith (symbolicMerge f t) xs ys
| True = cannotMerge "lists"
("Branches produce different sizes: " ++ show lxs ++ " vs " ++ show lys ++ ". Must have the same length.")
"Use the 'SList' type (and Data.SBV.List routines) to model fully symbolic lists."
where (lxs, lys) = (length xs, length ys)
-- NonEmpty
instance Mergeable a => Mergeable (NonEmpty a) where
symbolicMerge f t xs ys
| lxs == lys = NE.zipWith (symbolicMerge f t) xs ys
| True = cannotMerge "non-empty lists"
("Branches produce different sizes: " ++ show lxs ++ " vs " ++ show lys ++ ". Must have the same length.")
"Use the 'SList' type (and Data.SBV.List routines) to model fully symbolic lists."
where (lxs, lys) = (length xs, length ys)
-- ZipList
instance Mergeable a => Mergeable (ZipList a) where
symbolicMerge force test (ZipList xs) (ZipList ys)
= ZipList (symbolicMerge force test xs ys)
-- Maybe
instance Mergeable a => Mergeable (Maybe a) where
symbolicMerge _ _ Nothing Nothing = Nothing
symbolicMerge f t (Just a) (Just b) = Just $ symbolicMerge f t a b
symbolicMerge _ _ a b = cannotMerge "'Maybe' values"
("Branches produce different constructors: " ++ show (k a, k b))
"Instead of an option type, try using a valid bit to indicate when a result is valid."
where k :: Maybe a -> String
k Nothing = "Nothing"
k _ = "Just"
-- Either
instance (Mergeable a, Mergeable b) => Mergeable (Either a b) where
symbolicMerge f t (Left a) (Left b) = Left $ symbolicMerge f t a b
symbolicMerge f t (Right a) (Right b) = Right $ symbolicMerge f t a b
symbolicMerge _ _ a b = cannotMerge "'Either' values"
("Branches produce different constructors: " ++ show (k a, k b))
"Consider using a product type by a tag instead."
where k :: Either a b -> String
k (Left _) = "Left"
k (Right _) = "Right"
-- Arrays
instance (Ix a, Mergeable b) => Mergeable (Array a b) where
symbolicMerge f t a b
| ba == bb = DA.listArray ba (zipWith (symbolicMerge f t) (elems a) (elems b))
| True = cannotMerge "'Array' values"
("Branches produce different ranges: " ++ show (k ba, k bb))
"Consider using SBV's native 'SArray' abstraction."
where ba = bounds a
bb = bounds b
k = rangeSize
-- Functions
instance Mergeable b => Mergeable (a -> b) where
symbolicMerge f t g h x = symbolicMerge f t (g x) (h x)
{- Following definition, while correct, is utterly inefficient. Since the
application is delayed, this hangs on to the inner list and all the
impending merges, even when ind is concrete. Thus, it's much better to
simply use the default definition for the function case.
-}
-- select xs err ind = \x -> select (map ($ x) xs) (err x) ind
-- 2-Tuple
instance (Mergeable a, Mergeable b) => Mergeable (a, b) where
symbolicMerge f t (i0, i1) (j0, j1) = ( symbolicMerge f t i0 j0
, symbolicMerge f t i1 j1
)
select xs (err1, err2) ind = ( select as err1 ind
, select bs err2 ind
)
where (as, bs) = unzip xs
-- 3-Tuple
instance (Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c) where
symbolicMerge f t (i0, i1, i2) (j0, j1, j2) = ( symbolicMerge f t i0 j0
, symbolicMerge f t i1 j1
, symbolicMerge f t i2 j2
)
select xs (err1, err2, err3) ind = ( select as err1 ind
, select bs err2 ind
, select cs err3 ind
)
where (as, bs, cs) = unzip3 xs
-- 4-Tuple
instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d) where
symbolicMerge f t (i0, i1, i2, i3) (j0, j1, j2, j3) = ( symbolicMerge f t i0 j0
, symbolicMerge f t i1 j1
, symbolicMerge f t i2 j2
, symbolicMerge f t i3 j3
)
select xs (err1, err2, err3, err4) ind = ( select as err1 ind
, select bs err2 ind
, select cs err3 ind
, select ds err4 ind
)
where (as, bs, cs, ds) = unzip4 xs
-- 5-Tuple
instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e) where
symbolicMerge f t (i0, i1, i2, i3, i4) (j0, j1, j2, j3, j4) = ( symbolicMerge f t i0 j0
, symbolicMerge f t i1 j1
, symbolicMerge f t i2 j2
, symbolicMerge f t i3 j3
, symbolicMerge f t i4 j4
)
select xs (err1, err2, err3, err4, err5) ind = ( select as err1 ind
, select bs err2 ind
, select cs err3 ind
, select ds err4 ind
, select es err5 ind
)
where (as, bs, cs, ds, es) = unzip5 xs
-- 6-Tuple
instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f) where
symbolicMerge f t (i0, i1, i2, i3, i4, i5) (j0, j1, j2, j3, j4, j5) = ( symbolicMerge f t i0 j0
, symbolicMerge f t i1 j1
, symbolicMerge f t i2 j2
, symbolicMerge f t i3 j3
, symbolicMerge f t i4 j4
, symbolicMerge f t i5 j5
)
select xs (err1, err2, err3, err4, err5, err6) ind = ( select as err1 ind
, select bs err2 ind
, select cs err3 ind
, select ds err4 ind
, select es err5 ind
, select fs err6 ind
)
where (as, bs, cs, ds, es, fs) = unzip6 xs
-- 7-Tuple
instance (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g) where
symbolicMerge f t (i0, i1, i2, i3, i4, i5, i6) (j0, j1, j2, j3, j4, j5, j6) = ( symbolicMerge f t i0 j0
, symbolicMerge f t i1 j1
, symbolicMerge f t i2 j2
, symbolicMerge f t i3 j3
, symbolicMerge f t i4 j4
, symbolicMerge f t i5 j5
, symbolicMerge f t i6 j6
)
select xs (err1, err2, err3, err4, err5, err6, err7) ind = ( select as err1 ind
, select bs err2 ind
, select cs err3 ind
, select ds err4 ind
, select es err5 ind
, select fs err6 ind
, select gs err7 ind
)
where (as, bs, cs, ds, es, fs, gs) = unzip7 xs
-- Base types are mergeable so long as they are equal
instance Mergeable () where symbolicMerge _ _ = concreteMerge "()" "()" (==)
instance Mergeable Integer where symbolicMerge _ _ = concreteMerge "Integer" "SInteger" (==)
instance Mergeable Bool where symbolicMerge _ _ = concreteMerge "Bool" "SBool" (==)
instance Mergeable Char where symbolicMerge _ _ = concreteMerge "Char" "SChar" (==)
instance Mergeable Float where symbolicMerge _ _ = concreteMerge "Float" "SFloat" fpIsEqualObjectH
instance Mergeable Double where symbolicMerge _ _ = concreteMerge "Double" "SDouble" fpIsEqualObjectH
instance Mergeable Word8 where symbolicMerge _ _ = concreteMerge "Word8" "SWord8" (==)
instance Mergeable Word16 where symbolicMerge _ _ = concreteMerge "Word16" "SWord16" (==)
instance Mergeable Word32 where symbolicMerge _ _ = concreteMerge "Word32" "SWord32" (==)
instance Mergeable Word64 where symbolicMerge _ _ = concreteMerge "Word64" "SWord64" (==)
instance Mergeable Int8 where symbolicMerge _ _ = concreteMerge "Int8" "SInt8" (==)
instance Mergeable Int16 where symbolicMerge _ _ = concreteMerge "Int16" "SInt16" (==)
instance Mergeable Int32 where symbolicMerge _ _ = concreteMerge "Int32" "SInt32" (==)
instance Mergeable Int64 where symbolicMerge _ _ = concreteMerge "Int64" "SInt64" (==)
-- Arbitrary product types, using GHC.Generics
--
-- NB: Because of the way GHC.Generics works, the implementation of
-- symbolicMerge' is recursive. The derived instance for @data T a = T a a a a@
-- resembles that for (a, (a, (a, a))), not the flat 4-tuple (a, a, a, a). This
-- difference should have no effect in practice. Note also that, unlike the
-- hand-rolled tuple instances, the generic instance does not provide a custom
-- 'select' implementation, and so does not benefit from the SMT-table
-- implementation in the 'SBV a' instance.
-- | Not exported. Symbolic merge using the generic representation provided by
-- 'G.Generics'.
symbolicMergeDefault :: (G.Generic a, GMergeable (G.Rep a)) => Bool -> SBool -> a -> a -> a
symbolicMergeDefault force t x y = G.to $ symbolicMerge' force t (G.from x) (G.from y)
-- | Not exported. Used only in 'symbolicMergeDefault'. Instances are provided for
-- the generic representations of product types where each element is Mergeable.
class GMergeable f where
symbolicMerge' :: Bool -> SBool -> f a -> f a -> f a
{-
- N.B. A V1 instance like the below would be wrong!
- Why? Because inSBV, we use empty data to mean "uninterpreted" sort; not
- something that has no constructors. Perhaps that was a bad design
- decision. So, do not allow merging of such values!
instance GMergeable V1 where
symbolicMerge' _ _ x _ = x
-}
instance GMergeable U1 where
symbolicMerge' _ _ _ _ = U1
instance (Mergeable c) => GMergeable (K1 i c) where
symbolicMerge' force t (K1 x) (K1 y) = K1 $ symbolicMerge force t x y
instance (GMergeable f) => GMergeable (M1 i c f) where
symbolicMerge' force t (M1 x) (M1 y) = M1 $ symbolicMerge' force t x y
instance (GMergeable f, GMergeable g) => GMergeable (f :*: g) where
symbolicMerge' force t (x1 :*: y1) (x2 :*: y2) = symbolicMerge' force t x1 x2 :*: symbolicMerge' force t y1 y2
{- A mergeable instance for sum-types isn't possible. Why? It would something like:
instance (GMergeable f, GMergeable g) => GMergeable (f :+: g) where
symbolicMerge' force t (L1 x) (L1 y) = L1 $ symbolicMerge' force t x y
symbolicMerge' force t (R1 x) (R1 y) = R1 $ symbolicMerge' force t x y
symbolicMerge' force t l r
| Just tv <- unliteral t = if tv then l else r
| True = ????
There's really no good code to put in ????. We have no way to ask the SMT solver to merge composite values that
have different constructors. Calling "error" here would pass the type-checker, but that simply postpones the problem
to run-time. If you need mergeable on sum-types, you better write one yourself, possibly using the SEither type yourself.
As we have it, you'll get a type-error; which can be hard to read, but is preferable.
NB. This isn't a problem with the generic version of symbolic equality; since we can simply return sFalse if we
see different constructors. Such isn't the case when merging.
-}
-- Bounded instances
instance {-# OVERLAPPABLE #-} (SymVal a, Bounded a) => Bounded (SBV a) where
minBound = literal minBound
maxBound = literal maxBound
-- Haskell and SMTLib differ in their default char ranges. In Haskell, maxbound is a lot larger.
-- But in SMTLib, we only go upto 0x2FFFF. So, we adopt the SMTLib variant here. This is hardly
-- an issue in practice, but the discrepancy is disconcerting.
instance {-# OVERLAPPING #-} Bounded SChar where
minBound = literal (chr 0)
maxBound = literal (chr 0x2FFFF)
-- | Choose a value that satisfies the given predicate. This is Hillbert's choice, essentially. Note that
-- if the predicate given is not satisfiable (for instance @const sFalse@), then the element returned will be arbitrary.
-- The only guarantee is that if there's at least one element that satisfies the predicate, then the returned
-- element will be one of those that do. The returned element is not guaranteed to be unique, least, greatest etc, unless
-- there happens to be exactly one satisfying element.
some :: forall a. (SymVal a, HasKind a) => String -> (SBV a -> SBool) -> SBV a
some inpName cond = mk f
where mk = SBV . SVal k . Right . cache
k = kindOf (Proxy @a)
f st = do ctr <- incrementFreshNameCounter st
let pre = atProxy (Proxy @a) inpName
nm | ctr == 0 = pre
| True = pre ++ "_" ++ show ctr
op <- newUninterpreted st (UIGiven nm) Nothing (SBVType [k]) (UINone False)
chosen <- newExpr st k $ SBVApp op []
let ifExists = quantifiedBool $ \(Exists ex) -> cond ex
internalConstraint st False [] (unSBV (ifExists .=> cond (mk (pure (pure chosen)))))
pure chosen
-- | Find the final part of a kind that looks like an array
resKind :: Kind -> Kind
resKind (KArray _ k) = resKind k
resKind k = k
-- | SMT definable constants and functions, which can also be uninterpreted.
-- This class captures functions that we can generate standalone-code for
-- in the SMT solver. Note that we also allow uninterpreted constants and
-- functions too. An uninterpreted constant is a value that is indexed by its name. The only
-- property the prover assumes -- about these values are that they are equivalent to themselves; i.e., (for
-- functions) they return the same results when applied to same arguments.
-- We support uninterpreted-functions as a general means of black-box'ing
-- operations that are /irrelevant/ for the purposes of the proof; i.e., when
-- the proofs can be performed without any knowledge about the function itself.
--
-- Minimal complete definition: 'sbvDefineValue'. However, most instances in
-- practice are already provided by SBV, so end-users should not need to define their
-- own instances.
class SMTDefinable a where
-- | Generate the code for this value as an SMTLib function, instead of
-- the usual unrolling semantics. This is useful for generating sub-functions
-- in generated SMTLib problem, or handling recursive (and mutually-recursive)
-- definitions that wouldn't terminate in an unrolling symbolic simulation context.
--
-- __IMPORTANT NOTE__ The string argument names this function. SBV identifies
-- the function by this name: if you use this function twice (or use it recursively),
-- it will simply assume this name uniquely identifies the function being defined.
-- If two calls to 'smtFunction' (or its variants) use the same name but different
-- bodies, SBV will raise an error at runtime.
--
-- Furthermore, if the call to 'smtFunction' happens in the scope of a parameter, you
-- must make sure the string is chosen to keep it unique per parameter value. For instance,
-- if you have:
--
-- @
-- bar :: SInteger -> SInteger -> SInteger
-- bar k = smtFunction "bar" (\x -> x+k) -- Note the capture of k!
-- @
--
-- and you call @bar 2@ and @bar 3@, SBV will detect that the two bodies differ and
-- raise an error. You should use a concrete argument to make the name unique:
--
-- @
-- bar :: String -> SInteger -> SInteger -> SInteger
-- bar tag k = smtFunction ("bar_" ++ tag) (\x -> x+k) -- Tag should make the name unique!
-- @
--
-- Then, make sure you use @bar "two" 2@ and @bar "three" 3@ etc. to preserve the invariant.
--
-- Additionally, the function argument must not capture any non-constant variables in the context.
-- You can also define higher-order functions, see 'smtHOFunction' for that purpose.
smtFunctionDef :: (Typeable a, Lambda Symbolic a) => String -> Measure a -> a -> a
-- | 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.
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.
--
-- __Known issues__
--
-- Usually using an uninterpret function will register itself to the solver, but sometimes the laziness
-- of the evaluation might render this unreliable.
--
-- For example, when working with quantifiers and uninterpreted functions with the following code:
--
-- > runSMTWith z3 $ do
-- > let f = uninterpret "f" :: SInteger -> SInteger
-- > query $ do
-- > constrain $ \(Forall (b :: SInteger)) -> f b .== f b
-- > checkSat
--
-- The solver will complain about the unknown constant @f (Int)@.
--
-- A workaround of this is to explicit register them with 'Data.SBV.Control.registerUISMTFunction':
--
-- > runSMTWith z3 $ do
-- > let f = uninterpret "f" :: SInteger -> SInteger
-- > registerUISMTFunction f
-- > query $ do
-- > constrain $ \(Forall (b :: SInteger)) -> f b .== f b
-- > checkSat
--
-- See https://github.com/LeventErkok/sbv/issues/711 for more info.
uninterpret :: String -> a
-- | Uninterpret a value, with named arguments in case of functions. SBV will use these
-- names when it shows the values for the arguments. If the given names are more than needed
-- we ignore the excess. If not enough, we add from a stock set of variables.
uninterpretWithArgs :: String -> [String] -> a
-- | Uninterpret a value, only for the purposes of code-generation. For execution
-- and verification the value is used as is. For code-generation, the alternate
-- definition is used. This is useful when we want to take advantage of native
-- libraries on the target languages.
cgUninterpret :: String -> [String] -> a -> a
-- | More generalized form of uninterpretation that wraps 'sbvDefineValueFun';
-- this function should not be needed by end-user-code
sbvDefineValue :: UIName -> Maybe [String] -> UIKind a -> a
-- | The most generalized form of uninterpretation, that generates an
-- uninterpreted function over a sequence of 'SBVs' values; this function is
-- internal-only, and should not be needed by end-user-code
sbvDefineValueFun :: UIName -> Maybe [String] -> SymValInsts as ->
UIKind (SBVs as -> a) -> SBVs as -> a
-- | A synonym for 'uninterpret'. Allows us to create variables without
-- having to call 'free' explicitly, i.e., without being in the symbolic monad.
sym :: String -> a
-- | Like 'sym', but appends the type's kind to the name, ensuring uniqueness across
-- different type instantiations of the same polymorphic definition. Used internally by sCase.
symWithKind :: String -> a
symWithKind = sym
-- | Render an uninterpreted value as an SMTLib definition
sbv2smt :: ExtractIO m => a -> m String
-- | Render an uninterpreted value function as an SMTLib definition
sbvFun2smt :: (SymVals as, ExtractIO m) => (SBVs as -> a) -> m String
-- | Make this name a constructor, coming from an ADT. Only used internally
mkADTConstructor :: HasKind a => String -> a
mkADTTester :: HasKind a => String -> a
mkADTAccessor :: HasKind a => String -> a
{-# MINIMAL sbvDefineValueFun, sbvFun2smt, registerFunction #-}
-- defaults:
uninterpret nm = sbvDefineValue (UIGiven nm) Nothing $ UIFree True
uninterpretWithArgs nm as = sbvDefineValue (UIGiven nm) (Just as) $ UIFree True
cgUninterpret nm code v = sbvDefineValue (UIGiven nm) Nothing $ UICodeC (v, code)
sym = uninterpret
sbv2smt a = sbvFun2smt (\(_ :: SBVs RNil) -> a)
sbvDefineValue nm mbArgs k =
sbvDefineValueFun nm mbArgs SymValsNil (const <$> k) SBVsNil
mkADTConstructor nm = let k = resKind (kindOf v); v = sbvDefineValue (UIADT (ADTConstructor (T.pack nm) k)) Nothing $ UIFree True in v
mkADTTester nm = let k = resKind (kindOf v); v = sbvDefineValue (UIADT (ADTTester (T.pack nm) k)) Nothing $ UIFree True in v
mkADTAccessor nm = let k = resKind (kindOf v); v = sbvDefineValue (UIADT (ADTAccessor (T.pack nm) k)) Nothing $ UIFree True in v
smtFunctionDef nm msr v = sbvDefineValue (UIGiven (atProxy (Proxy @a) nm)) Nothing
$ UIFun (v, \st fk -> do
let funcNm = atProxy (Proxy @a) nm
(def, info) <- lambdaWithInfo st TopLevel fk v
-- Record LambdaInfo for SCC-aware mutual recursion checking
modifyIORef' (rFuncLambdaInfos st) (Map.insert funcNm info)
let barFuncNm = barify funcNm
tBarFuncNm = T.pack barFuncNm
isSelfRec = any (\(_, SBVApp op _) -> case op of
Uninterpreted n -> n == tBarFuncNm
_ -> False)
(liAssignments info)
hasCrossRefs = any (\(_, SBVApp op _) -> case op of
Uninterpreted n -> n /= tBarFuncNm
_ -> False)
(liAssignments info)
case msr of
AutoMeasure -> do
when isSelfRec $
modifyIORef' (rMeasureChecks st)
((funcNm, False, \cfg -> autoGuessOrFail cfg funcNm info) :)
when hasCrossRefs $
modifyIORef' (rMeasureChecks st)
((funcNm, False, \cfg -> checkMutualFromState cfg funcNm st Nothing) :)
pure def
HasMeasure eval helpers -> do
when isSelfRec $
modifyIORef' (rMeasureChecks st)
((funcNm, False, \cfg -> verifyMeasure cfg funcNm info eval helpers) :)
when hasCrossRefs $
modifyIORef' (rMeasureChecks st)
((funcNm, False, \cfg -> checkMutualFromState cfg funcNm st (Just eval)) :)
pure def
HasContract eval ceval helpers -> do
when hasCrossRefs $
modifyIORef' (rMeasureChecks st)
((funcNm, False, \cfg -> rejectMutualContractFromState cfg funcNm st) :)
modifyIORef' (rMeasureChecks st)
((funcNm, False, \cfg -> verifyMeasureWithContract cfg funcNm info eval ceval helpers) :)
pure def
Productive -> do
when isSelfRec $
modifyIORef' (rMeasureChecks st)
((funcNm, True, \cfg -> verifyGuardedness cfg funcNm info) :)
when hasCrossRefs $
modifyIORef' (rMeasureChecks st)
((funcNm, True, \cfg -> checkMutualProductiveFromState cfg funcNm st) :)
pure def
Unverified -> do modifyIORef' (rNoTermCheckFunctions st) (Set.insert nm)
debug (stCfg st) ["[MEASURE] " <> T.pack funcNm <> ": no termination check (smtFunctionNoTermination)"]
pure def)
-- | Define an SMT function. If the function is recursive, SBV will automatically try to
-- prove termination by guessing a measure based on argument types. If the guess fails,
-- use 'smtFunctionWithMeasure' to provide an explicit measure.
smtFunction :: (SMTDefinable a, Typeable a, Lambda Symbolic a) => String -> a -> a
smtFunction nm = smtFunctionDef nm AutoMeasure
-- | Define an SMT function with an explicit termination measure. Use this when 'smtFunction'
-- cannot automatically determine a suitable measure. The measure function takes the same
-- arguments as the original function but returns a value that must be non-negative and
-- strictly decrease at each recursive call.
--
-- The pair @(measure, helpers)@ provides the measure function and a list of auxiliary
-- t'MeasureHelper' properties needed to verify the measure. Each helper is first proven
-- (by running its TP proof), then asserted as an axiom in the measure verification session.
-- Use 'Data.SBV.TP.measureLemma' to create helpers from TP proofs. Pass @[]@ when no helpers are needed.
smtFunctionWithMeasure :: forall f r. (SMTDefinable f, Typeable f, Lambda Symbolic f, Zero r, OrdSymbolic (SBV r), SymVal r, ApplyMeasure f r)
=> String -> (MeasureOf f r, [MeasureHelper]) -> f -> f
smtFunctionWithMeasure nm (mf, helpers) = smtFunctionDef nm (HasMeasure (MeasureEval (applyMeasure @f @r mf)) helpers)
-- | Define an SMT function with a termination measure and a contract (post-condition).
-- Use this for nested recursive functions (like McCarthy's 91 function) where the termination
-- argument depends on the function's return value at smaller inputs.
--
-- The triple @(measure, contract, helpers)@ provides:
--
-- * A measure function (same as 'smtFunctionWithMeasure')
-- * A contract: a predicate on the function's inputs and output that is proven simultaneously
-- with the measure decrease via well-founded induction. The inductive hypothesis provides
-- the contract for all inputs with strictly smaller measure.
-- * A list of auxiliary t'MeasureHelper' properties (pass @[]@ when none are needed)
--
-- For example, for McCarthy's 91 function:
--
-- @
-- mcCarthy91 = smtFunctionWithContract \"mcCarthy91\"
-- ( \\n -> 0 \`smax\` (101 - n)
-- , \\n r -> n .<= 100 .=> r .== 91
-- , []
-- )
-- $ \\n -> ite (n .> 100) (n - 10) (mcCarthy91 (mcCarthy91 (n + 11)))
-- @
--
-- Here the contract says \"for inputs ≤ 100, the result is 91\". This is needed because the outer
-- recursive call @mcCarthy91(mcCarthy91(n + 11))@ requires knowing what @mcCarthy91(n + 11)@ returns
-- in order to verify that the measure decreases.
smtFunctionWithContract :: forall f r. (SMTDefinable f, Typeable f, Lambda Symbolic f, Zero r, OrdSymbolic (SBV r), SymVal r, ApplyMeasure f r, ApplyContract f)
=> String -> (MeasureOf f r, ContractOf f, [MeasureHelper]) -> f -> f
smtFunctionWithContract nm (mf, cf, helpers) = smtFunctionDef nm (HasContract (MeasureEval (applyMeasure @f @r mf))
(ContractEval (applyContract @f cf))
helpers)
-- | Define a productive (corecursive) SMT function. Use this for functions that intentionally
-- don't terminate but produce output incrementally, such as infinite list generators.
-- SBV verifies that every recursive call is guarded by a data constructor (list cons, ADT
-- constructor, etc.), ensuring the function is productive.
--
-- @
-- go = smtProductiveFunction \"go\" $ \\start delta -> start .: go (start + delta) delta
-- @
smtProductiveFunction :: (SMTDefinable a, Typeable a, Lambda Symbolic a) => String -> a -> a
smtProductiveFunction nm = smtFunctionDef nm Productive
-- | Define a recursive SMT function without any termination check. The function
-- is emitted as @define-fun-rec@ and the user takes responsibility for well-definedness.
-- Use this for functions where termination is believed but cannot be proven, such as
-- the Collatz function. See "Documentation.SBV.Examples.TP.Collatz" for an example use case.
smtFunctionNoTermination :: (SMTDefinable a, Typeable a, Lambda Symbolic a) => String -> a -> a
smtFunctionNoTermination nm = smtFunctionDef nm Unverified
-- | Kind of uninterpretation
data UIKind a = UIFree Bool -- ^ completely uninterpreted. If Bool is true, then this is curried.
| UIFun (a, State -> Kind -> IO SMTDef) -- ^ has code for SMTLib, with final type of kind (note this is the result
-- , not the arguments), which can be generated by calling the function on the state.
| UICodeC (a, [String]) -- ^ has code for code-generation, i.e., C
deriving Functor
-- Get the code associated with the UI, unless we've already did this once. (To support recursive defs.)
retrieveUICode :: UIName -> State -> Kind -> UIKind a -> IO UICodeKind
retrieveUICode _ _ _ (UIFree c) = pure $ UINone c
retrieveUICode (UIADT _) _ _ _ = pure $ UINone True
retrieveUICode (UIGiven nm) st fk (UIFun (_, f)) = do
compilingFuncs <- readIORef (rCompilingFuncs st)
if nm `Set.member` compilingFuncs
then -- This name is currently being compiled, so this is a recursive (or mutually recursive) self-call.
-- Break the cycle by skipping code generation.
pure $ UINone True
else do userFuncs <- readIORef (rUserFuncs st)
sn <- hashStableName <$> makeStableName f
case Map.lookup nm userFuncs of
Just (knownHashes, origLevel)
| sn `Set.member` knownHashes
-> -- Same closure we've seen before; skip immediately.
pure $ UINone True
| True
-> do -- New closure for an already-compiled name. Compile body in an isolated
-- throwaway state (to avoid side-effects like duplicate measure registrations
-- and context-dependent body differences), then compare with the existing definition.
-- We use the SAME lambda level as the original compilation so that SV names
-- in the body text match exactly; this avoids fragile string normalization.
throwaway <- mkNewState ((stCfg st) {verbose = False}) (LambdaGen origLevel)
modifyIORef' (rCompilingFuncs throwaway) (Set.insert nm)
-- If the body captures SVals from the live state's context, the throwaway
-- compilation will throw (e.g., context-mismatch). That is a definite conflict:
-- the body references different state-bound variables.
mbD <- C.try (f throwaway fk)
case mbD of
Left (_ :: C.SomeException)
-> conflictError nm
Right d
-> do defs <- readIORef (rDefns st)
case Map.lookup (barify nm) defs of
Just (oldDef, _)
| not (smtDefEq d oldDef)
-> conflictError nm
_ -> pure ()
-- Body matches; memoize this StableName hash so future calls
-- with the same closure skip instantly.
modifyState st rUserFuncs (Map.adjust (first (Set.insert sn)) nm) (pure ())
pure $ UINone True
Nothing
-> do -- First time seeing this name. Record lambda level for future comparison.
ll <- readIORef (rLambdaLevel st)
modifyState st rUserFuncs (Map.insert nm (Set.singleton sn, ll)) (pure ())
modifyState st rCompilingFuncs (Set.insert nm) (pure ())
d <- UISMT <$> f st fk
modifyState st rCompilingFuncs (Set.delete nm) (pure ())
pure d
retrieveUICode _ _ _ (UICodeC (_, c)) = pure $ UICgC c
-- Get the constant value associated with the UI
retrieveConstCode :: UIKind a -> Maybe a
retrieveConstCode UIFree{} = Nothing
retrieveConstCode (UIFun (v, _)) = Just v
retrieveConstCode (UICodeC (v, _)) = Just v
instance SymVal a => SMTDefinable (SBV a) where
sbvFun2smt (fn :: SBVs as -> SBV a)
| SymValsNil <- symValInsts :: SymValInsts as
, a <- fn SBVsNil
= do st <- mkNewState defaultSMTCfg (LambdaGen (Just 0))
s <- lambdaStr st TopLevel (kindOf a) a
pure $ intercalate "\n" [ "; Automatically generated by SBV. Do not modify!"
, "; Type: " ++ T.unpack (smtType (kindOf a))
, show s
]
sbvFun2smt fn = defs2smt (\args -> fn args .== fn args)
sbvDefineValueFun nm mbArgs insts uiKind args
| Just v <- retrieveConstCode uiKind
, foldlSymSBVs (\r x -> r && isConcrete x) True insts args
= v args
| ka <- kindOf (Proxy @a)
= SBV $ SVal ka $ Right $ cache $ \st ->
do isSMT <- inSMTMode st
case (isSMT, uiKind) of
(True, UICodeC (v, _)) -> sbvToSV st (v args)
_ -> do let ks = symValKinds insts ++ [ka]
ui <- retrieveUICode nm st ka uiKind
op <- newUninterpreted st nm mbArgs (SBVType ks) ui
svs <- rlist2list <$> mapMSBVs (sbvToSV st) args
mapM_ forceSVArg svs
newExpr st ka $ SBVApp op svs
registerFunction x = constrain $ x .== x
symWithKind nm = sym (nm ++ "_" ++ show (kindOf (Proxy @a)))
instance (SymVal a, SMTDefinable b) => SMTDefinable (SBV a -> b) where
sbvFun2smt (fn :: SBVs as -> SBV a -> b) =
sbvFun2smt (\((SBVsCons as a) :: SBVs (as :> a)) -> fn as a)
sbvDefineValueFun nm mbArgs insts uiKind args a =
sbvDefineValueFun nm mbArgs (SymValsCons insts)
((\f (SBVsCons xs x) -> f xs x) <$> uiKind) (SBVsCons args a)
registerFunction f = do let k = kindOf (Proxy @a)
st <- symbolicEnv
v <- liftIO $ newInternalVariable st k
let a = SBV $ SVal k $ Right $ cache (const (pure v))
registerFunction $ f a
-- Mark the UIKind as uncurried
mkUncurried :: UIKind a -> UIKind a
mkUncurried (UIFree _) = UIFree False
mkUncurried (UIFun a) = UIFun a
mkUncurried (UICodeC a) = UICodeC a
uncurrySBVs2 :: (SBVs as -> (SBV c, SBV b) -> SBV a) ->
(SBVs (as :> c :> b) -> SBV a)
uncurrySBVs2 fn (SBVsCons (SBVsCons as c) b) = fn as (c,b)
-- Uncurried functions of two arguments
instance (SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV c, SBV b) -> SBV a) where
sbvFun2smt = sbvFun2smt . uncurrySBVs2
registerFunction = registerFunction . curry2
sbvDefineValueFun nm mbArgs insts uiKind = uncurry2 <$> sbvDefineValueFun nm mbArgs insts (fmap curry2 <$> mkUncurried uiKind)
-- 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
sbvFun2smt = sbvFun2smt . uncurrySBVs3
where uncurrySBVs3 :: (SBVs as -> (SBV d, SBV c, SBV b) -> SBV a) -> (SBVs (as :> d :> c :> b) -> SBV a)
uncurrySBVs3 fn (SBVsCons (SBVsCons (SBVsCons as d) c) b) = fn as (d,c,b)
registerFunction = registerFunction . curry3
sbvDefineValueFun nm mbArgs insts uiKind = uncurry3 <$> sbvDefineValueFun nm mbArgs insts (fmap curry3 <$> mkUncurried uiKind)
-- Uncurried functions of four arguments
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
sbvFun2smt = sbvFun2smt . uncurrySBVs4
where uncurrySBVs4 :: (SBVs as -> (SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBVs (as :> e :> d :> c :> b) -> SBV a)
uncurrySBVs4 fn (SBVsCons (SBVsCons (SBVsCons (SBVsCons as e) d) c) b) = fn as (e,d,c,b)
registerFunction = registerFunction . curry4
sbvDefineValueFun nm mbArgs insts uiKind = uncurry4 <$> sbvDefineValueFun nm mbArgs insts (fmap curry4 <$> mkUncurried uiKind)
-- Uncurried functions of five arguments
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
sbvFun2smt = sbvFun2smt . uncurrySBVs5
where uncurrySBVs5 :: (SBVs as -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBVs (as :> f :> e :> d :> c :> b) -> SBV a)
uncurrySBVs5 fn (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons as f) e) d) c) b) = fn as (f,e,d,c,b)
registerFunction = registerFunction . curry5
sbvDefineValueFun nm mbArgs insts uiKind = uncurry5 <$> sbvDefineValueFun nm mbArgs insts (fmap curry5 <$> mkUncurried uiKind)
-- Uncurried functions of six arguments
instance (SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
sbvFun2smt = sbvFun2smt . uncurrySBVs6
where uncurrySBVs6 :: (SBVs as -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBVs (as :> g :> f :> e :> d :> c :> b) -> SBV a)
uncurrySBVs6 fn (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons as g) f) e) d) c) b) = fn as (g,f,e,d,c,b)
registerFunction = registerFunction . curry6
sbvDefineValueFun nm mbArgs insts uiKind = uncurry6 <$> sbvDefineValueFun nm mbArgs insts (fmap curry6 <$> mkUncurried uiKind)
-- Uncurried functions of seven arguments
instance (SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
sbvFun2smt = sbvFun2smt . uncurrySBVs7
where uncurrySBVs7 :: (SBVs as -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBVs (as :> h :> g :> f :> e :> d :> c :> b) -> SBV a)
uncurrySBVs7 fn (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons as h) g) f) e) d) c) b) = fn as (h,g,f,e,d,c,b)
registerFunction = registerFunction . curry7
sbvDefineValueFun nm mbArgs insts uiKind = uncurry7 <$> sbvDefineValueFun nm mbArgs insts (fmap curry7 <$> mkUncurried uiKind)
-- Uncurried functions of eight arguments
instance (SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
sbvFun2smt = sbvFun2smt . uncurrySBVs8
where uncurrySBVs8 :: (SBVs as -> (SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBVs (as :> i :> h :> g :> f :> e :> d :> c :> b) -> SBV a)
uncurrySBVs8 fn (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons as i) h) g) f) e) d) c) b) = fn as (i,h,g,f,e,d,c,b)
registerFunction = registerFunction . curry8
sbvDefineValueFun nm mbArgs insts uiKind = uncurry8 <$> sbvDefineValueFun nm mbArgs insts (fmap curry8 <$> mkUncurried uiKind)
-- Uncurried functions of nine arguments
instance (SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
sbvFun2smt = sbvFun2smt . uncurrySBVs9
where uncurrySBVs9 :: (SBVs as -> (SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBVs (as :> j :> i :> h :> g :> f :> e :> d :> c :> b) -> SBV a)
uncurrySBVs9 fn (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons as j) i) h) g) f) e) d) c) b) = fn as (j,i,h,g,f,e,d,c,b)
registerFunction = registerFunction . curry9
sbvDefineValueFun nm mbArgs insts uiKind = uncurry9 <$> sbvDefineValueFun nm mbArgs insts (fmap curry9 <$> mkUncurried uiKind)
-- Uncurried functions of ten arguments
instance (SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable ((SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where
sbvFun2smt = sbvFun2smt . uncurrySBVs10
where uncurrySBVs10 :: (SBVs as -> (SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBVs (as :> k :> j :> i :> h :> g :> f :> e :> d :> c :> b) -> SBV a)
uncurrySBVs10 fn (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons as k) j) i) h) g) f) e) d) c) b) = fn as (k,j,i,h,g,f,e,d,c,b)
registerFunction = registerFunction . curry10
sbvDefineValueFun nm mbArgs insts uiKind = uncurry10 <$> sbvDefineValueFun nm mbArgs insts (fmap curry10 <$> mkUncurried uiKind)
-- Uncurried functions of eleven arguments
instance (SymVal l, SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => 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
sbvFun2smt = sbvFun2smt . uncurrySBVs11
where uncurrySBVs11 :: (SBVs as -> (SBV l, SBV k, SBV j, SBV i, SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBVs (as :> l :> k :> j :> i :> h :> g :> f :> e :> d :> c :> b) -> SBV a)
uncurrySBVs11 fn (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons as l) k) j) i) h) g) f) e) d) c) b) = fn as (l,k,j,i,h,g,f,e,d,c,b)
registerFunction = registerFunction . curry11
sbvDefineValueFun nm mbArgs insts uiKind = uncurry11 <$> sbvDefineValueFun nm mbArgs insts (fmap curry11 <$> mkUncurried uiKind)
-- Uncurried functions of twelve arguments
instance (SymVal m, SymVal l, SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => 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
sbvFun2smt = sbvFun2smt . uncurrySBVs12
where uncurrySBVs12 :: (SBVs as -> (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) -> (SBVs (as :> m :> l :> k :> j :> i :> h :> g :> f :> e :> d :> c :> b) -> SBV a)
uncurrySBVs12 fn (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons (SBVsCons as m) l) k) j) i) h) g) f) e) d) c) b) = fn as (m,l,k,j,i,h,g,f,e,d,c,b)
registerFunction = registerFunction . curry12
sbvDefineValueFun nm mbArgs insts uiKind = uncurry12 <$> sbvDefineValueFun nm mbArgs insts (fmap curry12 <$> mkUncurried uiKind)
-- | Symbolic computations provide a context for writing symbolic programs.
instance MonadIO m => SolverContext (SymbolicT m) where
constrain = imposeConstraint False [] . unSBV . quantifiedBool
softConstrain = imposeConstraint True [] . unSBV . quantifiedBool
namedConstraint nm = imposeConstraint False [(":named", nm)] . unSBV . quantifiedBool
constrainWithAttribute atts = imposeConstraint False atts . unSBV . quantifiedBool
contextState = symbolicEnv
setOption o = addNewSMTOption o
internalVariable k = contextState >>= \st -> liftIO $ do
sv <- newInternalVariable st k
pure $ SBV $ SVal k (Right (cache (const (pure sv))))
-- | Generalization of 'Data.SBV.assertWithPenalty'
assertWithPenalty :: MonadSymbolic m => String -> SBool -> Penalty -> m ()
assertWithPenalty nm o p = addSValOptGoal $ unSBV <$> AssertWithPenalty nm o p
-- | Class of metrics we can optimize for. Currently, booleans,
-- bounded signed/unsigned bit-vectors, unbounded integers,
-- algebraic reals and floats can be optimized. You can add
-- your instances, but bewared that the 'MetricSpace' should
-- map your type to something the backend solver understands, which
-- are limited to unsigned bit-vectors, reals, and unbounded integers
-- for z3.
--
-- A good reference on these features is given in the following paper:
-- <http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf>.
--
-- Minimal completion: None. However, if @MetricSpace@ is not identical to the type, you want
-- to define 'toMetricSpace'/'annotateForMS', and possibly 'minimize'/'maximize' to add extra constraints as necessary.
class Metric a where
-- | The metric space we optimize the goal over. Usually the same as the type itself, but not always!
-- For instance, signed bit-vectors are optimized over their unsigned counterparts, floats are
-- optimized over their 'Word32' comparable counterparts, etc.
type MetricSpace a :: Type
type MetricSpace a = a
-- | Compute the metric value to optimize.
toMetricSpace :: SBV a -> SBV (MetricSpace a)
-- | Compute the value itself from the metric corresponding to it.
fromMetricSpace :: SBV (MetricSpace a) -> SBV a
-- | Annotate for the metric space, to clarify the new name. If this result is not identity,
-- we will add an sObserve on the original.
annotateForMS :: Proxy a -> String -> String
-- | Minimizing a metric space
msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()
msMinimize nm o = do let nm' = annotateForMS (Proxy @a) nm
when (nm' /= nm) $ sObserve nm (unSBV o)
addSValOptGoal $ unSBV <$> Minimize nm' (toMetricSpace o)
-- | Maximizing a metric space
msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()
msMaximize nm o = do let nm' = annotateForMS (Proxy @a) nm
when (nm' /= nm) $ sObserve nm (unSBV o)
addSValOptGoal $ unSBV <$> Maximize nm' (toMetricSpace o)
-- if MetricSpace is the same, we can give a default definition
default toMetricSpace :: (a ~ MetricSpace a) => SBV a -> SBV (MetricSpace a)
toMetricSpace = id
default fromMetricSpace :: (a ~ MetricSpace a) => SBV (MetricSpace a) -> SBV a
fromMetricSpace = id
-- Annotations to indicate if the metric space transition was needed
default annotateForMS :: (a ~ MetricSpace a) => Proxy a -> String -> String
annotateForMS _ s = s
-- Booleans assume True is greater than False
instance Metric Bool where
type MetricSpace Bool = Word8
toMetricSpace t = ite t 1 0
fromMetricSpace w = w ./= 0
annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"
-- | Generalization of 'Data.SBV.minimize'
minimize :: (Metric a, MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()
minimize = msMinimize
-- | Generalization of 'Data.SBV.maximize'
maximize :: (Metric a, MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()
maximize = msMaximize
-- Unsigned types, integers, and reals directly optimize
instance Metric Word8
instance Metric Word16
instance Metric Word32
instance Metric Word64
instance Metric Integer
instance Metric AlgReal
-- To optimize signed bounded values, we have to adjust to the range
instance Metric Int8 where
type MetricSpace Int8 = Word8
toMetricSpace x = sFromIntegral x + 128 -- 2^7
fromMetricSpace x = sFromIntegral x - 128
annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"
instance Metric Int16 where
type MetricSpace Int16 = Word16
toMetricSpace x = sFromIntegral x + 32768 -- 2^15
fromMetricSpace x = sFromIntegral x - 32768
annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"
instance Metric Int32 where
type MetricSpace Int32 = Word32
toMetricSpace x = sFromIntegral x + 2147483648 -- 2^31
fromMetricSpace x = sFromIntegral x - 2147483648
annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"
instance Metric Int64 where
type MetricSpace Int64 = Word64
toMetricSpace x = sFromIntegral x + 9223372036854775808 -- 2^63
fromMetricSpace x = sFromIntegral x - 9223372036854775808
annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"
-- | Optimizing 'WordN'
instance (KnownNat n, BVIsNonZero n) => Metric (WordN n)
-- | Optimizing 'IntN'
instance (KnownNat n, BVIsNonZero n) => Metric (IntN n) where
type MetricSpace (IntN n) = WordN n
toMetricSpace x = sFromIntegral x + 2 ^ (intOfProxy (Proxy @n) - 1)
fromMetricSpace x = sFromIntegral x - 2 ^ (intOfProxy (Proxy @n) - 1)
annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"
-- Quickcheck interface on symbolic-booleans..
instance Testable SBool where
property (SBV (SVal _ (Left b))) = property (cvToBool b)
property s = cantQuickCheck $ "Result did not evaluate to a concrete boolean: " ++ show s
instance Testable (Symbolic SBool) where
property prop = QC.monadicIO $ do (cond, r, modelVals) <- QC.run test
QC.pre cond
unless (r || null modelVals) $ QC.monitor (QC.counterexample (complain modelVals))
QC.assert r
where test = do (r, Result{resTraces=tvals, resObservables=ovals, resConsts=(_, cs), resConstraints=cstrs, resUIConsts=unints}) <-
C.catch (runSymbolic defaultSMTCfg (Concrete Nothing) prop)
(\(e :: C.SomeException) -> cantQuickCheck (show e))
let cval = fromMaybe (cantQuickCheck "A constraint did not evaluate to a concrete boolean") . (`lookup` cs)
cond = -- Only pick-up "hard" constraints, as indicated by False in the fist component
and [cvToBool (cval v) | (False, _, v) <- F.toList cstrs]
getObservable (nm, f, v) = case v `lookup` cs of
Just cv -> if f cv then Just (nm, cv) else Nothing
Nothing -> cantQuickCheck "An observable did not evaluate to a concrete value"
case map fst unints of
[] -> case unliteral r of
Nothing -> cantQuickCheck "The result did not evaluate to a concrete value"
Just b -> pure (cond, b, tvals ++ mapMaybe getObservable ovals)
uis -> cantQuickCheck $ "Uninterpreted constants remain: " ++ unwords uis
complain qcInfo = showModel defaultSMTCfg (SMTModel [] Nothing qcInfo [])
-- Complain if what we got isn't something we can quick-check
cantQuickCheck :: String -> a
cantQuickCheck why = error $ unlines [ "*** Data.SBV: Cannot quickcheck the given property."
, "***"
, "*** Certain SBV properties cannot be quick-checked. In particular,"
, "*** SBV can't quick-check in the presence of:"
, "***"
, "*** - Uninterpreted constants."
, "*** - Uninterpreted types."
, "*** - Floating point operations with rounding modes other than RNE."
, "*** - Floating point FMA operation, regardless of rounding mode."
, "*** - Quantified booleans, i.e., uses of Forall/Exists/ExistsUnique."
, "*** - Uses of quantifiedBool"
, "*** - Calls to 'observe' (use 'sObserve' instead)"
, "***"
, "*** If you can't avoid the above features or run into an issue with"
, "*** quickcheck even though you haven't used these features, please report this as a bug!"
, "***"
, "*** Origin:"
, "***"
, why
]
-- | Quick check an SBV property. Note that a regular @quickCheck@ call will work just as
-- well. Use this variant if you want to receive the boolean result.
sbvQuickCheck :: Symbolic SBool -> IO Bool
sbvQuickCheck prop = QC.isSuccess <$> QC.quickCheckResult prop
-- Quickcheck interface on dynamically-typed values. A run-time check
-- ensures that the value has boolean type.
instance Testable (Symbolic SVal) where
property m = property $ do s <- m
when (kindOf s /= KBool) $ error "Cannot quickcheck non-boolean value"
pure (SBV s :: SBool)
-- | Explicit sharing combinator. The SBV library has internal caching/hash-consing mechanisms
-- built in, based on Andy Gill's type-safe observable sharing technique (see: <http://ku-fpg.github.io/files/Gill-09-TypeSafeReification.pdf>).
-- However, there might be times where being explicit on the sharing can help, especially in experimental code. The 'slet' combinator
-- ensures that its first argument is computed once and passed on to its continuation, explicitly indicating the intent of sharing. Most
-- use cases of the SBV library should simply use Haskell's @let@ construct for this purpose.
slet :: forall a b. (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b
slet x f = SBV $ SVal k $ Right $ cache r
where k = kindOf (Proxy @b)
r st = do xsv <- sbvToSV st x
let xsbv = SBV $ SVal (kindOf x) (Right (cache (const (pure xsv))))
res = f xsbv
sbvToSV st res
-- | Class of things that we can logically reduce to a boolean, by saturating and then asserting equivalence to itself
class QSaturate m a where
qSaturate :: a -> m ()
-- | Base case; simple variable in the symbolic monad
instance SolverContext m => QSaturate m SBool where
qSaturate b = constrain $ b .== b
-- | Saturate over a universal quantifier
instance (HasKind a, Monad m, SolverContext m, QSaturate m r) => QSaturate m (Forall nm a -> r) where
qSaturate f = qSaturate . f . Forall =<< internalVariable (kindOf (Proxy @a))
-- | Saturate over a pair of universal quantifiers
instance (HasKind a, HasKind b, Monad m, SolverContext m, QSaturate m r) => QSaturate m ((Forall na a, Forall nb b) -> r) where
qSaturate = qSaturate . curry
-- | Saturate over a pair of existential quantifiers
instance (HasKind a, HasKind b, Monad m, SolverContext m, QSaturate m r) => QSaturate m ((Exists na a, Exists nb b) -> r) where
qSaturate = qSaturate . curry
-- | Saturate over a number of universal quantifiers
instance (KnownNat n, HasKind a, Monad m, SolverContext m, QSaturate m r) => QSaturate m (ForallN n nm a -> r) where
qSaturate f = qSaturate . f . ForallN =<< replicateM (intOfProxy (Proxy @n)) (internalVariable (kindOf (Proxy @a)))
-- | Saturate over an existential quantifier
instance (HasKind a, Monad m, SolverContext m, QSaturate m r) => QSaturate m (Exists nm a -> r) where
qSaturate f = qSaturate . f . Exists =<< internalVariable (kindOf (Proxy @a))
-- | Saturate over an a number of existential quantifiers
instance (KnownNat n, HasKind a, Monad m, SolverContext m, QSaturate m r) => QSaturate m (ExistsN n nm a -> r) where
qSaturate f = qSaturate . f . ExistsN =<< replicateM (intOfProxy (Proxy @n)) (internalVariable (kindOf (Proxy @a)))
-- | Saturate over a unique-exists variable
instance (HasKind a, Monad m, SolverContext m, QSaturate m r) => QSaturate m (ExistsUnique nm a -> r) where
qSaturate f = qSaturate . f . ExistsUnique =<< internalVariable (kindOf (Proxy @a))
-- | Saturate a predicate, but save/restore observables so they're not messed up.
qSaturateSavingObservables :: (Monad m, MonadIO m, SolverContext m, QSaturate m a) => a -> m ()
qSaturateSavingObservables p = do State{rObservables} <- contextState
curObservables <- liftIO $ readIORef rObservables
qSaturate p
liftIO $ writeIORef rObservables curObservables
-- | Equality as a proof method. Allows for
-- very concise construction of equivalence proofs, which is very typical in
-- bit-precise proofs.
infix 4 ===
class Equality a where
(===) :: a -> a -> IO ThmResult
instance {-# OVERLAPPABLE #-} (SymVal a, EqSymbolic z) => Equality (SBV a -> z) where
k === l = prove $ \a -> k a .== l a
instance {-# OVERLAPPABLE #-} (SymVal a, SymVal b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) where
k === l = prove $ \a b -> k a b .== l a b
instance {-# OVERLAPPABLE #-} (SymVal a, SymVal b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) where
k === l = prove $ \a b -> k (a, b) .== l (a, b)
instance {-# OVERLAPPABLE #-} (SymVal a, SymVal b, SymVal c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) where
k === l = prove $ \a b c -> k a b c .== l a b c
instance {-# OVERLAPPABLE #-} (SymVal a, SymVal b, SymVal c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) where
k === l = prove $ \a b c -> k (a, b, c) .== l (a, b, c)
instance {-# OVERLAPPABLE #-} (SymVal a, SymVal b, SymVal c, SymVal d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) where
k === l = prove $ \a b c d -> k a b c d .== l a b c d
instance {-# OVERLAPPABLE #-} (SymVal a, SymVal b, SymVal c, SymVal d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) where
k === l = prove $ \a b c d -> k (a, b, c, d) .== l (a, b, c, d)
instance {-# OVERLAPPABLE #-} (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) where
k === l = prove $ \a b c d e -> k a b c d e .== l a b c d e
instance {-# OVERLAPPABLE #-} (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) where
k === l = prove $ \a b c d e -> k (a, b, c, d, e) .== l (a, b, c, d, e)
instance {-# OVERLAPPABLE #-} (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) where
k === l = prove $ \a b c d e f -> k a b c d e f .== l a b c d e f
instance {-# OVERLAPPABLE #-}
(SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) where
k === l = prove $ \a b c d e f -> k (a, b, c, d, e, f) .== l (a, b, c, d, e, f)
instance {-# OVERLAPPABLE #-}
(SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) where
k === l = prove $ \a b c d e f g -> k a b c d e f g .== l a b c d e f g
instance {-# OVERLAPPABLE #-} (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) where
k === l = prove $ \a b c d e f g -> k (a, b, c, d, e, f, g) .== l (a, b, c, d, e, f, g)
-- | Reading a value from an array.
readArray :: forall key val. (SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val
readArray array key
| eqCheckIsObjectEq ka, Just (ArrayModel tbl def) <- unliteral array, Just _ <- unliteral key, Just r <- locate (unSBV key) def tbl
= r
| True
= symRes
where symRes = SBV . SVal kb . Right $ cache g
ka = kindOf (Proxy @key)
kb = kindOf (Proxy @val)
g st = do f <- sbvToSV st array
k <- sbvToSV st key
newExpr st kb (SBVApp ReadArray [f, k])
-- return the first value, since we don't bother deleting previous writes. Note that this might
-- fail if we don't have equality; but that's OK; in that case we'll go symbolic.
locate skey def vals = go vals
where go [] = Just $ literal def
go ((k, v) : rest) = case unliteral (SBV (svStrongEqual skey (unSBV (literal k)))) of
Nothing -> Nothing
Just True -> Just $ literal v
Just False -> go rest
-- | Writing a value to an array. For the concrete case, we don't bother deleting earlier entries, we keep a history. The earlier a value is in the list, the "later" it happened; in a stack fashion.
writeArray :: forall key val. (HasKind key, SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val -> SArray key val
writeArray array key value
| Just (ArrayModel tbl def) <- unliteral array, Just keyVal <- unliteral key, Just val <- unliteral value
= literal $ ArrayModel ((keyVal, val) : tbl) def -- It's important that we "cons" the value here, since it takes precedence in a read
| True
= SBV . SVal k . Right $ cache g
where k = KArray (kindOf (Proxy @key)) (kindOf (Proxy @val))
g st = do arr <- sbvToSV st array
keyVal <- sbvToSV st key
val <- sbvToSV st value
newExpr st k (SBVApp WriteArray [arr, keyVal, val])
-- | Create a constant array. This is a special case of 'lambdaArray', but it creates a
-- simpler expression in the case of constants.
constArray :: forall key val. (SymVal key, SymVal val) => SBV val -> SArray key val
constArray v
| Just v' <- unliteral v
= literal $ ArrayModel [] v'
| True
= SBV . SVal k . Right $ cache g
where ka = kindOf (Proxy @key)
kb = kindOf (Proxy @val)
k = KArray ka kb
g st = do sv <- sbvToSV st v
newExpr st k (SBVApp (ArrayInit (Left (ka, kb))) [sv])
-- | Create a completely free array, with no constraints on it, as an expression.
-- Note that you can create an array in the symbolic context with the regular 'free'
-- calls. (Or 'sArray' if you prefer.) This variant creates it as an expression, i.e.,
-- without having to be in the monadic context. We take a name identifier here as an
-- argument which uniquely identifies this array. Note that this is necessary, as otherwise
-- there would be no way to distinguish two different calls in the pure context. If you
-- use the same name, then you'll get the same array, much like uninterpreted functions.
freeArray :: forall key val. (SymVal key, SymVal val) => String -> SArray key val
freeArray = lambdaArray . uninterpret
-- | Using a lambda as an array. We can turn a function into an array, relating indexes
-- to their values. (That is, passing @f@ would create an array where entry @i@
-- is initialized to value @f i@.) For the special case of initializing with a constant
-- value, either pass @const val@, or use 'constArray'.
--
-- __Arrays vs. uninterpreted functions:__ The basic array theory provides only
-- @select@ ('readArray'), @store@ ('writeArray'), and @const@ ('constArray'). These operations
-- can only construct arrays that differ from a constant in finitely many positions. For instance,
-- the identity array (where @a[i] = i@ for every @i@) cannot be built from 'constArray' plus
-- finitely many 'writeArray' calls. The @lambdaArray@ function goes beyond this: it uses the
-- solver's ability to identify arrays with function spaces, allowing the creation of arrays like
-- @lambdaArray id@ that correspond to arbitrary functions.
--
-- This identification has a model-theoretic consequence. The pure array theory (with only
-- @select@\/@store@\/@const@) is a weaker theory: it admits models where the array sort does
-- not contain all functions, only those reachable by finitely many stores on constants. This means
-- certain formulas are satisfiable in the pure theory (because the solver has more freedom in choosing
-- what arrays exist) that become unsatisfiable when arrays are identified with functions (because the
-- richer array sort can provide counterexamples). In practice, modern solvers use the stronger
-- identification, so @lambdaArray@, 'constArray', and 'writeArray' all operate in this richer setting.
lambdaArray :: forall a b. (SymVal a, HasKind b) => (SBV a -> SBV b) -> SArray a b
lambdaArray f = SBV . SVal k . Right $ cache g
where k = KArray (kindOf (Proxy @a)) (kindOf (Proxy @b))
g st = do def <- lambdaStr st TopLevel (kindOf (Proxy @b)) f
newExpr st k (SBVApp (ArrayInit (Right def)) [])
-- | Turn a constant association-list and a default into a symbolic array.
listArray :: (SymVal a, SymVal b) => [(a, b)] -> b -> SArray a b
listArray ascs def = literal $ ArrayModel ascs def
-- | Create a closure, wrapping the free variables together with the function. When using higher-order functions
-- in SBV (like map), the function passed must be closed, i.e., not have any free variables. If you need to call
-- such a function with a function capturing a free variable, you should create a closure instead.
data Closure env a = Closure { closureEnv :: env
, closureFun :: env -> a
}
-- | Define a higher-order function. Similar to 'smtFunction', but when we have a higher-order argument. Note that
-- the higher-order argument cannot have free variables. Also, if the function is recursive, you should call
-- the first argument of the defining function, which SBV uses to tie the recursive knot. (Note that recursive
-- functions defined via 'smtFunction' don't have this latter requirement as they can figure out the recursion
-- automatically. Higher-order functions, unfortunately, can't do this: They firstify their high-order argument,
-- giving the whole function a unique name; captured via the call to the recursive definition.)
smtHOFunction :: forall a b f.
( SMTDefinable (a -> SBV b)
, Lambda Symbolic f
, Lambda Symbolic (a -> SBV b)
, HasKind b
, HasKind f
, Typeable a
, Typeable b
, Typeable f
) => String -- prefix to use
-> f -- The higher-order argument. We're very generic here!
-> (a -> SBV b) -- The ho-function we're modeling
-> a -> SBV b -- The resulting function, that can be used as is, and will be rendered in SMTLib without unfolding
smtHOFunction nm f = smtHOFunctionGen nm f AutoMeasure
-- | Like 'smtHOFunction', but with an explicit termination measure. Use this when the
-- auto-guess measure doesn't work for a higher-order recursive function.
smtHOFunctionWithMeasure :: forall a b f r.
( SMTDefinable (a -> SBV b)
, Lambda Symbolic f
, Lambda Symbolic (a -> SBV b)
, HasKind b
, HasKind f
, Typeable a
, Typeable b
, Typeable f
, Zero r, OrdSymbolic (SBV r), SymVal r
, ApplyMeasure (a -> SBV b) r
) => String -- ^ prefix to use
-> f -- ^ The higher-order argument
-> MeasureOf (a -> SBV b) r -- ^ Termination measure
-> (a -> SBV b) -- ^ The ho-function we're modeling
-> a -> SBV b -- ^ The resulting function
smtHOFunctionWithMeasure nm f msr = smtHOFunctionGen nm f (HasMeasure (MeasureEval (applyMeasure @(a -> SBV b) @r msr)) [])
-- | Common implementation for higher-order SMT function definitions.
smtHOFunctionGen :: forall a b f.
( SMTDefinable (a -> SBV b)
, Lambda Symbolic f
, Lambda Symbolic (a -> SBV b)
, HasKind b
, HasKind f
, Typeable a
, Typeable b
, Typeable f
) => String -- ^ prefix to use
-> f -- ^ The higher-order argument
-> Measure (a -> SBV b) -- ^ Termination measure
-> (a -> SBV b) -- ^ The ho-function we're modeling
-> a -> SBV b -- ^ The resulting function
smtHOFunctionGen nm f measure hof arg = SBV $ SVal (kindOf (Proxy @(SBV b))) $ Right $ cache r
where r st = do SMTLambda lam <- lambdaStr st HigherOrderArg (arrayResultKind (kindOf (Proxy @f))) f
let uniq = lambdaFingerprint st (T.unpack lam)
sbvToSV st (smtFunctionDef (atProxy (Proxy @f) nm <> "_" <> uniq) measure hof arg)
-- | Chase through nested array kinds to find the final result kind. Higher-order
-- arguments are firstified into arrays, so we peel off the array wrappers.
arrayResultKind :: Kind -> Kind
arrayResultKind (KArray _ k) = arrayResultKind k
arrayResultKind k = k
-- | Generate a short fingerprint from a lambda body string, used to give
-- unique names to firstified higher-order function instantiations.
lambdaFingerprint :: State -> String -> String
lambdaFingerprint st lam = take uniqLen (BC.unpack (B.encode (hash (BC.pack (unwords (words lam))))))
where uniqLen = firstifyUniqueLen $ stCfg st
{- HLint ignore module "Reduce duplication" -}
{- HLint ignore module "Eta reduce" -}
{- HLint ignore module "Avoid NonEmpty.unzip" -}
{- HLint ignore module "Redundant id" -}
{- HLint ignore module "Use second" -}