sbv 13.1 → 13.2
raw patch · 36 files changed
+1250/−512 lines, 36 files
Files
- CHANGES.md +12/−0
- Data/SBV.hs +3/−1
- Data/SBV/Core/Data.hs +75/−1
- Data/SBV/Core/Model.hs +116/−436
- Data/SBV/Provers/Prover.hs +13/−0
- Data/SBV/Set.hs +5/−5
- Data/SBV/TP/Utils.hs +16/−8
- Documentation/SBV/Examples/ADT/Expr.hs +2/−2
- Documentation/SBV/Examples/ADT/Param.hs +2/−2
- Documentation/SBV/Examples/ADT/Types.hs +4/−4
- Documentation/SBV/Examples/Lists/BoundedMutex.hs +1/−1
- Documentation/SBV/Examples/Misc/Enumerate.hs +2/−2
- Documentation/SBV/Examples/Misc/SetAlgebra.hs +1/−1
- Documentation/SBV/Examples/Puzzles/Murder.hs +4/−4
- Documentation/SBV/Examples/TP/GCD.hs +2/−1
- Documentation/SBV/Examples/TP/Primes.hs +487/−0
- Documentation/SBV/Examples/Uninterpreted/EUFLogic.hs +340/−0
- Documentation/SBV/Examples/WeakestPreconditions/Sum.hs +2/−2
- README.md +1/−0
- SBVTestSuite/GoldFiles/adt06.gold +2/−2
- SBVTestSuite/GoldFiles/adt_gen00.gold +4/−2
- SBVTestSuite/GoldFiles/adt_gen08.gold +2/−2
- SBVTestSuite/GoldFiles/adt_gen09.gold +2/−2
- SBVTestSuite/GoldFiles/adt_gen10.gold +2/−2
- SBVTestSuite/GoldFiles/adt_mr00.gold +8/−7
- SBVTestSuite/GoldFiles/adt_mr04.gold +3/−2
- SBVTestSuite/GoldFiles/doctest_sanity.gold +3/−3
- SBVTestSuite/GoldFiles/qUninterp1.gold +2/−2
- SBVTestSuite/GoldFiles/set_tupleSet.gold +2/−3
- SBVTestSuite/GoldFiles/set_uninterp1.gold +12/−12
- SBVTestSuite/GoldFiles/set_uninterp2.gold +2/−2
- SBVTestSuite/GoldFiles/uninterpreted-1a.gold +53/−0
- SBVTestSuite/SBVTest.hs +2/−0
- SBVTestSuite/TestSuite/Uninterpreted/EUFLogic.hs +48/−0
- SBVTestSuite/TestSuite/Uninterpreted/Uninterpreted.hs +11/−0
- sbv.cabal +4/−1
CHANGES.md view
@@ -1,6 +1,18 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 13.2, 2025-12-01++ * Improve support for SMTDefinable class, allowing support for on-the-fly generated functions.+ Thanks to Eddy Westbrook for the patch. This should have no impact on existing code or usage,+ just allowing new use cases. Let us know if it breaks anything.++ * SBV now supports uninterpreted functions of arbitrary arities. (Previously, we had support for upto+ 12 args; Eddy's work above generalized this to arbitrary arity.)++ * Added Documentation.SBV.Examples.TP.Primes, which formalizes prime numbers and proves that there are+ an infinite number of primes.+ ### Version 13.1, 2025-10-31 * Tweaks to make sure SBV compiles with GHC 9.8.4. No other changes on top of 13.0 below.
Data/SBV.hs view
@@ -1139,7 +1139,9 @@ mkSymbolic [''X] @ -Note the magic incantation @mkSymbolic [''X]@, requires certain extensions to be turned on. Simply follow GHC's advice.+Note the magic incantation @mkSymbolic [''X]@, requires the following extensions:+@TemplateHaskell@, @TypeApplications@, and @FlexibleInstances@.+Parametric data-types also require @ScopedTypeVariables@. SBV also supports good old ADT's as well, with fields. The support for this is similar, where SBV will create the corresponding datatype in a symbolic manner:
Data/SBV/Core/Data.hs view
@@ -16,7 +16,9 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}@@ -36,7 +38,7 @@ , STuple, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7, STuple8 , RCSet(..), SSet , nan, infinity, sNaN, sInfinity, RoundingMode(..), SRoundingMode- , SymVal(..)+ , SymVal(..), SymValInsts(..), symValKinds, SymVals(..) , CV(..), CVal(..), AlgReal(..), AlgRealPoly(..), ExtCV(..), GeneralizedCV(..), isRegularCV, cvSameType, cvToBool , mkConstCV , mapCV, mapCV2 , SV(..), trueSV, falseSV, trueCV, falseCV, normCV@@ -44,6 +46,8 @@ , sTrue, sFalse, sNot, (.&&), (.||), (.<+>), (.~&), (.~|), (.=>), (.<=>), sAnd, sOr, sAny, sAll, fromBool , SBV(..), NodeId(..), mkSymSBV , sbvToSV, sbvToSymSV, forceSVArg+ , RList(..), RNil, (:>), rlist2list+ , SBVs(..), foldlSBVs, mapMSBVs, foldlSymSBVs , SBVExpr(..), newExpr , cache, Cached, uncache, HasKind(..) , Op(..), PBOp(..), FPOp(..), StrOp(..), RegExOp(..), SeqOp(..), RegExp(..), NamedSymVar(..), OvOp(..), getTableIndex@@ -345,6 +349,51 @@ sbvToSV :: State -> SBV a -> IO SV sbvToSV st (SBV s) = svToSV st s +-- | A datakind for lists with cons on the right+data RList a = RNil | (RList a) :> a++-- | Convert an 'RList' into a reversed standard list+rlist2listRev :: RList a -> [a]+rlist2listRev RNil = []+rlist2listRev (as :> a) = a : rlist2listRev as++-- | Convert an 'RList' into a standard list+rlist2list :: RList a -> [a]+rlist2list = reverse . rlist2listRev++-- | Helper for writing types containing @RNil@+type RNil = 'RNil++-- | Helper for writing types containing @:>@+type (:>) = '(:>)++-- | A sequence of elements of types @SBV a1,...,SBV an@ given the list+-- @[a1,...,an]@ of Haskell types+data SBVs as where+ SBVsNil :: SBVs RNil+ SBVsCons :: SBVs as -> SBV a -> SBVs (as :> a)++-- | Fold a function over each SBV value in an SBVs sequence in a manner similar+-- to 'foldr' for lists, except backwards because the lists are stored in+-- reverse order+foldlSBVs :: (forall a. r -> SBV a -> r) -> r -> SBVs as -> r+foldlSBVs _ r SBVsNil = r+foldlSBVs f r (SBVsCons args arg) = f (foldlSBVs f r args) arg++-- | Map a monadic function over the SBV values in an SBVs sequence in a+-- manner similar to 'mapM' for lists+mapMSBVs :: Monad m => (forall a. SBV a -> m r) -> SBVs as -> m (RList r)+mapMSBVs f = foldlSBVs (\m arg -> (:>) <$> m <*> f arg) (return RNil)++-- | Fold a function over each SBV value in an SBVs sequence in a manner similar+-- to 'foldr' for lists (but backwards because SBVs have cons on the right),+-- using 'SymVal' instances for each value+foldlSymSBVs :: (forall a. SymVal a => r -> SBV a -> r) -> r ->+ SymValInsts as -> SBVs as -> r+foldlSymSBVs _ r _ SBVsNil = r+foldlSymSBVs f r (SymValsCons symvs) (SBVsCons args arg) =+ f (foldlSymSBVs f r symvs args) arg+ ------------------------------------------------------------------------- -- * Symbolic Computations -------------------------------------------------------------------------@@ -630,6 +679,31 @@ -- | Is the symbolic word really symbolic? isSymbolic :: SBV a -> Bool isSymbolic = not . isConcrete++-- | A sequence of instance dictionaries for each type @ai@ in the type list+-- @[a1,...,an]@+data SymValInsts as where+ SymValsNil :: SymValInsts RNil+ SymValsCons :: SymVal a => SymValInsts as -> SymValInsts (as :> a)++-- | Get the 'Kind' of each type in the type list of a 'SymValInsts' sequence+symValKinds :: SymValInsts as -> [Kind]+symValKinds = rlist2list . helper where+ helper :: SymValInsts as -> RList Kind+ helper SymValsNil = RNil+ helper insts@(SymValsCons insts') = helper insts' :> kindOf (headPrx insts)+ headPrx :: SymValInsts (bs :> b) -> Proxy b+ headPrx _ = Proxy++-- | A 'SymVals' is a list of types that all satisfy 'SymVal'+class SymVals as where+ symValInsts :: SymValInsts as++instance SymVals RNil where+ symValInsts = SymValsNil++instance (SymVal a, SymVals as) => SymVals (as :> a) where+ symValInsts = SymValsCons symValInsts instance (Random a, SymVal a) => Random (SBV a) where randomR (l, h) g = case (unliteral l, unliteral h) of
Data/SBV/Core/Model.hs view
@@ -16,8 +16,10 @@ {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}@@ -2710,10 +2712,16 @@ -- libraries on the target languages. cgUninterpret :: String -> [String] -> a -> a - -- | Most generalized form of uninterpretation, this function should not be needed- -- by end-user-code, but is rather useful for the library development.+ -- | 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@@ -2721,31 +2729,32 @@ -- | Render an uninterpeted value as an SMTLib definition sbv2smt :: ExtractIO m => a -> m String + -- | Render an uninterpeted 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 sbvDefineValue, sbv2smt #-}+ {-# 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 (fmap const k) SBVsNil+ mkADTConstructor nm = let k = resKind (kindOf v); v = sbvDefineValue (UIADT (ADTConstructor nm k)) Nothing $ UIFree True in v mkADTTester nm = let k = resKind (kindOf v); v = sbvDefineValue (UIADT (ADTTester nm k)) Nothing $ UIFree True in v mkADTAccessor nm = let k = resKind (kindOf v); v = sbvDefineValue (UIADT (ADTAccessor nm k)) Nothing $ UIFree True in v smtFunction nm v = sbvDefineValue (UIGiven (atProxy (Proxy @a) nm)) Nothing $ UIFun (v, \st fk -> lambda st TopLevel fk v) - default registerFunction :: forall b c. (a ~ (SBV b -> c), SymVal b, SMTDefinable c) => a -> Symbolic ()- registerFunction f = do let k = kindOf (Proxy @b)- st <- symbolicEnv- v <- liftIO $ newInternalVariable st k- let b = SBV $ SVal k $ Right $ cache (const (pure v))- registerFunction $ f b -- | Kind of uninterpretation data UIKind a = UIFree Bool -- ^ completely uninterpreted. If Bool is true, then this is curried.@@ -2771,406 +2780,50 @@ retrieveConstCode (UIFun (v, _)) = Just v retrieveConstCode (UICodeC (v, _)) = Just v --- Plain constants-instance (SymVal a, HasKind a) => SMTDefinable (SBV a) where- sbv2smt a = 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: " ++ smtType (kindOf a)- , show s- ]+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: " ++ 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 - sbvDefineValue nm mbArgs uiKind- | Just v <- retrieveConstCode uiKind- = v- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st v- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [ka]) =<< retrieveUICode nm st ka uiKind- newExpr st ka $ SBVApp op [] --- Functions of one argument-instance (SymVal b, SymVal a, HasKind a) => SMTDefinable (SBV b -> SBV a) where- sbv2smt fn = defs2smt $ \b -> fn b .== fn b-- sbvDefineValue nm mbArgs uiKind = f- where f arg0- | Just v <- retrieveConstCode uiKind, isConcrete arg0- = v arg0- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- mapM_ forceSVArg [sw0]- newExpr st ka $ SBVApp op [sw0]---- Functions of two arguments-instance (SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable (SBV c -> SBV b -> SBV a) where- sbv2smt fn = defs2smt $ \c b -> fn c b .== fn c b-- sbvDefineValue nm mbArgs uiKind = f- where f arg0 arg1- | Just v <- retrieveConstCode uiKind, isConcrete arg0, isConcrete arg1- = v arg0 arg1- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- kc = kindOf (Proxy @c)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [kc, kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- sw1 <- sbvToSV st arg1- mapM_ forceSVArg [sw0, sw1]- newExpr st ka $ SBVApp op [sw0, sw1]---- Functions of three arguments-instance (SymVal d, SymVal c, SymVal b, SymVal a, HasKind a) => SMTDefinable (SBV d -> SBV c -> SBV b -> SBV a) where- sbv2smt fn = defs2smt $ \d c b -> fn d c b .== fn d c b-- sbvDefineValue nm mbArgs uiKind = f- where f arg0 arg1 arg2- | Just v <- retrieveConstCode uiKind, isConcrete arg0, isConcrete arg1, isConcrete arg2- = v arg0 arg1 arg2- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- kc = kindOf (Proxy @c)- kd = kindOf (Proxy @d)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- sw1 <- sbvToSV st arg1- sw2 <- sbvToSV st arg2- mapM_ forceSVArg [sw0, sw1, sw2]- newExpr st ka $ SBVApp op [sw0, sw1, sw2]---- 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- sbv2smt fn = defs2smt $ \e d c b -> fn e d c b .== fn e d c b-- sbvDefineValue nm mbArgs uiKind = f- where f arg0 arg1 arg2 arg3- | Just v <- retrieveConstCode uiKind, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3- = v arg0 arg1 arg2 arg3- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- kc = kindOf (Proxy @c)- kd = kindOf (Proxy @d)- ke = kindOf (Proxy @e)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- sw1 <- sbvToSV st arg1- sw2 <- sbvToSV st arg2- sw3 <- sbvToSV st arg3- mapM_ forceSVArg [sw0, sw1, sw2, sw3]- newExpr st ka $ SBVApp op [sw0, sw1, sw2, sw3]---- 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- sbv2smt fn = defs2smt $ \f e d c b -> fn f e d c b .== fn f e d c b-- sbvDefineValue nm mbArgs uiKind = f- where f arg0 arg1 arg2 arg3 arg4- | Just v <- retrieveConstCode uiKind, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4- = v arg0 arg1 arg2 arg3 arg4- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- kc = kindOf (Proxy @c)- kd = kindOf (Proxy @d)- ke = kindOf (Proxy @e)- kf = kindOf (Proxy @f)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- sw1 <- sbvToSV st arg1- sw2 <- sbvToSV st arg2- sw3 <- sbvToSV st arg3- sw4 <- sbvToSV st arg4- mapM_ forceSVArg [sw0, sw1, sw2, sw3, sw4]- newExpr st ka $ SBVApp op [sw0, sw1, sw2, sw3, sw4]---- 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- sbv2smt fn = defs2smt $ \f g e d c b -> fn g f e d c b .== fn g f e d c b-- sbvDefineValue nm mbArgs uiKind = f- where f arg0 arg1 arg2 arg3 arg4 arg5- | Just v <- retrieveConstCode uiKind, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5- = v arg0 arg1 arg2 arg3 arg4 arg5- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- kc = kindOf (Proxy @c)- kd = kindOf (Proxy @d)- ke = kindOf (Proxy @e)- kf = kindOf (Proxy @f)- kg = kindOf (Proxy @g)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- sw1 <- sbvToSV st arg1- sw2 <- sbvToSV st arg2- sw3 <- sbvToSV st arg3- sw4 <- sbvToSV st arg4- sw5 <- sbvToSV st arg5- mapM_ forceSVArg [sw0, sw1, sw2, sw3, sw4, sw5]- newExpr st ka $ SBVApp op [sw0, sw1, sw2, sw3, sw4, sw5]---- 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- sbv2smt fn = defs2smt $ \h g f e d c b -> fn h g f e d c b .== fn h g f e d c b-- sbvDefineValue nm mbArgs uiKind = f- where f arg0 arg1 arg2 arg3 arg4 arg5 arg6- | Just v <- retrieveConstCode uiKind, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5, isConcrete arg6- = v arg0 arg1 arg2 arg3 arg4 arg5 arg6- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- kc = kindOf (Proxy @c)- kd = kindOf (Proxy @d)- ke = kindOf (Proxy @e)- kf = kindOf (Proxy @f)- kg = kindOf (Proxy @g)- kh = kindOf (Proxy @h)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- sw1 <- sbvToSV st arg1- sw2 <- sbvToSV st arg2- sw3 <- sbvToSV st arg3- sw4 <- sbvToSV st arg4- sw5 <- sbvToSV st arg5- sw6 <- sbvToSV st arg6- mapM_ forceSVArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]- newExpr st ka $ SBVApp op [sw0, sw1, sw2, sw3, sw4, sw5, sw6]---- Functions of eight arguments-instance (SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c, SymVal b, SymVal a, SymVal a, HasKind a)- => SMTDefinable (SBV i -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where- sbv2smt fn = defs2smt $ \i h g f e d c b -> fn i h g f e d c b .== fn i h g f e d c b-- sbvDefineValue nm mbArgs uiKind = f- where f arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7- | Just v <- retrieveConstCode uiKind, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5, isConcrete arg6, isConcrete arg7- = v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- kc = kindOf (Proxy @c)- kd = kindOf (Proxy @d)- ke = kindOf (Proxy @e)- kf = kindOf (Proxy @f)- kg = kindOf (Proxy @g)- kh = kindOf (Proxy @h)- ki = kindOf (Proxy @i)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- sw1 <- sbvToSV st arg1- sw2 <- sbvToSV st arg2- sw3 <- sbvToSV st arg3- sw4 <- sbvToSV st arg4- sw5 <- sbvToSV st arg5- sw6 <- sbvToSV st arg6- sw7 <- sbvToSV st arg7- mapM_ forceSVArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6, sw7]- newExpr st ka $ SBVApp op [sw0, sw1, sw2, sw3, sw4, sw5, sw6, sw7]---- 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- sbv2smt fn = defs2smt $ \j i h g f e d c b -> fn j i h g f e d c b .== fn j i h g f e d c b-- sbvDefineValue nm mbArgs uiKind = f- where f arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8- | Just v <- retrieveConstCode uiKind, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5, isConcrete arg6, isConcrete arg7, isConcrete arg8- = v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- kc = kindOf (Proxy @c)- kd = kindOf (Proxy @d)- ke = kindOf (Proxy @e)- kf = kindOf (Proxy @f)- kg = kindOf (Proxy @g)- kh = kindOf (Proxy @h)- ki = kindOf (Proxy @i)- kj = kindOf (Proxy @j)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- sw1 <- sbvToSV st arg1- sw2 <- sbvToSV st arg2- sw3 <- sbvToSV st arg3- sw4 <- sbvToSV st arg4- sw5 <- sbvToSV st arg5- sw6 <- sbvToSV st arg6- sw7 <- sbvToSV st arg7- sw8 <- sbvToSV st arg8- mapM_ forceSVArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6, sw7, sw8]- newExpr st ka $ SBVApp op [sw0, sw1, sw2, sw3, sw4, sw5, sw6, sw7, sw8]---- 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- sbv2smt fn = defs2smt $ \k j i h g f e d c b -> fn k j i h g f e d c b .== fn k j i h g f e d c b-- sbvDefineValue nm mbArgs uiKind = f- where f arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9- | Just v <- retrieveConstCode uiKind, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5, isConcrete arg6, isConcrete arg7, isConcrete arg8, isConcrete arg9- = v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- kc = kindOf (Proxy @c)- kd = kindOf (Proxy @d)- ke = kindOf (Proxy @e)- kf = kindOf (Proxy @f)- kg = kindOf (Proxy @g)- kh = kindOf (Proxy @h)- ki = kindOf (Proxy @i)- kj = kindOf (Proxy @j)- kk = kindOf (Proxy @k)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- sw1 <- sbvToSV st arg1- sw2 <- sbvToSV st arg2- sw3 <- sbvToSV st arg3- sw4 <- sbvToSV st arg4- sw5 <- sbvToSV st arg5- sw6 <- sbvToSV st arg6- sw7 <- sbvToSV st arg7- sw8 <- sbvToSV st arg8- sw9 <- sbvToSV st arg9- mapM_ forceSVArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6, sw7, sw8, sw9]- newExpr st ka $ SBVApp op [sw0, sw1, sw2, sw3, sw4, sw5, sw6, sw7, sw8, sw9]---- 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- sbv2smt fn = defs2smt $ \l k j i h g f e d c b -> fn l k j i h g f e d c b .== fn l k j i h g f e d c b-- sbvDefineValue nm mbArgs uiKind = f- where f arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10- | Just v <- retrieveConstCode uiKind, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5, isConcrete arg6, isConcrete arg7, isConcrete arg8, isConcrete arg9, isConcrete arg10- = v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- kc = kindOf (Proxy @c)- kd = kindOf (Proxy @d)- ke = kindOf (Proxy @e)- kf = kindOf (Proxy @f)- kg = kindOf (Proxy @g)- kh = kindOf (Proxy @h)- ki = kindOf (Proxy @i)- kj = kindOf (Proxy @j)- kk = kindOf (Proxy @k)- kl = kindOf (Proxy @l)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [kl, kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- sw1 <- sbvToSV st arg1- sw2 <- sbvToSV st arg2- sw3 <- sbvToSV st arg3- sw4 <- sbvToSV st arg4- sw5 <- sbvToSV st arg5- sw6 <- sbvToSV st arg6- sw7 <- sbvToSV st arg7- sw8 <- sbvToSV st arg8- sw9 <- sbvToSV st arg9- sw10 <- sbvToSV st arg10- mapM_ forceSVArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6, sw7, sw8, sw9, sw10]- newExpr st ka $ SBVApp op [sw0, sw1, sw2, sw3, sw4, sw5, sw6, sw7, sw8, sw9, sw10]+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) --- 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- sbv2smt fn = defs2smt $ \m l k j i h g f e d c b -> fn m l k j i h g f e d c b .== fn m l k j i h g f e d c b+ sbvDefineValueFun nm mbArgs insts uiKind args a =+ sbvDefineValueFun nm mbArgs (SymValsCons insts)+ (fmap (\f (SBVsCons xs x) -> f xs x) uiKind) (SBVsCons args a) - sbvDefineValue nm mbArgs uiKind = f- where f arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10 arg11- | Just v <- retrieveConstCode uiKind, isConcrete arg0, isConcrete arg1, isConcrete arg2, isConcrete arg3, isConcrete arg4, isConcrete arg5, isConcrete arg6, isConcrete arg7, isConcrete arg8, isConcrete arg9, isConcrete arg10, isConcrete arg11- = v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10 arg11- | True- = SBV $ SVal ka $ Right $ cache result- where ka = kindOf (Proxy @a)- kb = kindOf (Proxy @b)- kc = kindOf (Proxy @c)- kd = kindOf (Proxy @d)- ke = kindOf (Proxy @e)- kf = kindOf (Proxy @f)- kg = kindOf (Proxy @g)- kh = kindOf (Proxy @h)- ki = kindOf (Proxy @i)- kj = kindOf (Proxy @j)- kk = kindOf (Proxy @k)- kl = kindOf (Proxy @l)- km = kindOf (Proxy @m)- result st = do isSMT <- inSMTMode st- case (isSMT, uiKind) of- (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10 arg11)- _ -> do op <- newUninterpreted st nm mbArgs (SBVType [km, kl, kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind- sw0 <- sbvToSV st arg0- sw1 <- sbvToSV st arg1- sw2 <- sbvToSV st arg2- sw3 <- sbvToSV st arg3- sw4 <- sbvToSV st arg4- sw5 <- sbvToSV st arg5- sw6 <- sbvToSV st arg6- sw7 <- sbvToSV st arg7- sw8 <- sbvToSV st arg8- sw9 <- sbvToSV st arg9- sw10 <- sbvToSV st arg10- sw11 <- sbvToSV st arg11- mapM_ forceSVArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6, sw7, sw8, sw9, sw10, sw11]- newExpr st ka $ SBVApp op [sw0, sw1, sw2, sw3, sw4, sw5, sw6, sw7, sw8, sw9, sw10, sw11]+ 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@@ -3178,71 +2831,98 @@ 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- sbv2smt fn = defs2smt $ \p -> fn p .== fn p- registerFunction = registerFunction . curry2- sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry2 <$> mkUncurried uiKind) in uncurry2 f+ 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- sbv2smt fn = defs2smt $ \p -> fn p .== fn p- registerFunction = registerFunction . curry3- sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry3 <$> mkUncurried uiKind) in uncurry3 f+ 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- sbv2smt fn = defs2smt $ \p -> fn p .== fn p- registerFunction = registerFunction . curry4- sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry4 <$> mkUncurried uiKind) in uncurry4 f+ 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- sbv2smt fn = defs2smt $ \p -> fn p .== fn p- registerFunction = registerFunction . curry5- sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry5 <$> mkUncurried uiKind) in uncurry5 f+ 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- sbv2smt fn = defs2smt $ \p -> fn p .== fn p- registerFunction = registerFunction . curry6- sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry6 <$> mkUncurried uiKind) in uncurry6 f+ 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- sbv2smt fn = defs2smt $ \p -> fn p .== fn p- registerFunction = registerFunction . curry7- sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry7 <$> mkUncurried uiKind) in uncurry7 f+ 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- sbv2smt fn = defs2smt $ \p -> fn p .== fn p- registerFunction = registerFunction . curry8- sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry8 <$> mkUncurried uiKind) in uncurry8 f+ 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- sbv2smt fn = defs2smt $ \p -> fn p .== fn p- registerFunction = registerFunction . curry9- sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry9 <$> mkUncurried uiKind) in uncurry9 f+ 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- sbv2smt fn = defs2smt $ \p -> fn p .== fn p- registerFunction = registerFunction . curry10- sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry10 <$> mkUncurried uiKind) in uncurry10 f+ 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- sbv2smt fn = defs2smt $ \p -> fn p .== fn p- registerFunction = registerFunction . curry11- sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry11 <$> mkUncurried uiKind) in uncurry11 f+ 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- sbv2smt fn = defs2smt $ \p -> fn p .== fn p- registerFunction = registerFunction . curry12- sbvDefineValue nm mbArgs uiKind = let f = sbvDefineValue nm mbArgs (curry12 <$> mkUncurried uiKind) in uncurry12 f+ 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
Data/SBV/Provers/Prover.hs view
@@ -12,6 +12,7 @@ {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -683,6 +684,18 @@ instance (SymVal a, ProvableM m p) => ProvableM m (SBV a -> p) where proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ fn a++-- | Create an 'SBVs' sequence of arguments+mkArgs :: MonadSymbolic m => SymValInsts as -> m (SBVs as)+mkArgs SymValsNil = return SBVsNil+mkArgs (SymValsCons insts) = SBVsCons <$> mkArgs insts <*> mkArg++-- Multi-arity Functions+instance (SymVals as, SatisfiableM m p) => SatisfiableM m (SBVs as -> p) where+ satArgReduce fn = mkArgs symValInsts >>= \args -> satArgReduce $ fn args++instance (SymVals as, ProvableM m p) => ProvableM m (SBVs as -> p) where+ proofArgReduce fn = mkArgs symValInsts >>= \args -> proofArgReduce $ fn args -- 2 Tuple instance (SymVal a, SymVal b, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b) -> p) where
Data/SBV/Set.hs view
@@ -147,8 +147,8 @@ -- -- >>> prove $ \x (s :: SSet Integer) -> x `delete` (x `insert` s) .== s -- Falsifiable. Counter-example:--- s0 = 2 :: Integer--- s1 = U :: {Integer}+-- s0 = 2 :: Integer+-- s1 = {2} :: {Integer} -- -- But the above is true if the element isn't in the set to start with: --@@ -190,8 +190,8 @@ -- -- >>> prove $ \x (s :: SSet Integer) -> x `insert` (x `delete` s) .== s -- Falsifiable. Counter-example:--- s0 = 2 :: Integer--- s1 = U - {2} :: {Integer}+-- s0 = 2 :: Integer+-- s1 = {} :: {Integer} -- -- But the above is true if the element is in the set to start with: --@@ -515,7 +515,7 @@ False >>> sat $ \(x::SSet (Maybe Integer)) y z -> distinct [x, y, z] Satisfiable. Model:- s0 = {Just 3} :: {Maybe Integer}+ s0 = {Just 2} :: {Maybe Integer} s1 = {} :: {Maybe Integer} s2 = U :: {Maybe Integer}
Data/SBV/TP/Utils.hs view
@@ -26,7 +26,7 @@ TP, runTP, runTPWith, Proof(..), ProofObj(..), assumptionFromProof, sorry, quickCheckProof , startTP, finishTP, getTPState, getTPConfig, setTPConfig, tpGetNextUnique, TPState(..), TPStats(..), RootOfTrust(..) , TPProofContext(..), message, updStats, rootOfTrust, concludeModulo- , ProofTree(..), TPUnique(..), showProofTree, showProofTreeHTML, shortProofName+ , ProofTree(..), TPUnique(..), showProofTree, showProofTreeHTML , withProofCache , tpQuiet, tpRibbon, tpAsms, tpStats, tpCache ) where@@ -223,6 +223,16 @@ | True = s where s = proofName p +-- | Nicely format a bunch of proof-names, shortened and uniquified. Note that if we get a dependency+-- via multiple routes, they can get different uniqid's; so we do a bit of compression here.+shortProofNames :: [ProofObj] -> String+shortProofNames = intercalate ", " . map merge . compress . sort . map shortProofName . nubBy (\a b -> uniqId a == uniqId b)+ where compress [] = []+ compress (a:as) = case span (a ==) as of+ (same, other) -> (a, length same + 1) : compress other+ merge (n, 1) = n+ merge (n, x) = n ++ " (x" ++ show x ++ ")"+ -- | Keeping track of where the sorry originates from. Used in displaying dependencies. newtype RootOfTrust = RootOfTrust (Maybe [ProofObj]) @@ -230,7 +240,7 @@ instance Show RootOfTrust where show (RootOfTrust mbp) = case mbp of Nothing -> "Nothing"- Just ps -> "Just [" ++ intercalate ", " (map shortProofName ps) ++ "]"+ Just ps -> "Just [" ++ shortProofNames ps ++ "]" -- | Trust forms a semigroup instance Semigroup RootOfTrust where@@ -317,14 +327,12 @@ -- | Show instance for t'Proof' instance Typeable a => Show (Proof a) where show p@(Proof po@ProofObj{proofName = nm}) = '[' : sh (rootOfTrust p) ++ "] " ++ nm ++ " :: " ++ pretty (show (typeOf p))- where sh (RootOfTrust Nothing) = "Proven" ++ cacheInfo- sh (RootOfTrust (Just ps)) = "Modulo: " ++ join ps ++ cacheInfo-- join = intercalate ", " . sort . map shortProofName+ where sh (RootOfTrust Nothing) = "Proven" ++ cacheInfo+ sh (RootOfTrust (Just ps)) = "Modulo: " ++ shortProofNames ps ++ cacheInfo cacheInfo = case cachedProofs po of [] -> ""- cs -> ". Cached: " ++ join (nubBy (\p1 p2 -> uniqId p1 == uniqId p2) cs)+ cs -> ". Cached: " ++ shortProofNames (nubBy (\p1 p2 -> uniqId p1 == uniqId p2) cs) cachedProofs prf@ProofObj{isCached} = if isCached then prf : rest else rest where rest = concatMap cachedProofs (dependencies prf)@@ -434,7 +442,7 @@ concludeModulo :: [ProofObj] -> String concludeModulo by = case foldMap (rootOfTrust . Proof) by of RootOfTrust Nothing -> ""- RootOfTrust (Just ps) -> " [Modulo: " ++ intercalate ", " (map shortProofName ps) ++ "]"+ RootOfTrust (Just ps) -> " [Modulo: " ++ shortProofNames ps ++ "]" -- | Make TP proofs quiet. Note that this setting will be effective with the -- call to 'runTP'\/'runTPWith', i.e., if you change the solver in a call to 'Data.SBV.TP.lemmaWith'\/'Data.SBV.TP.theoremWith', we
Documentation/SBV/Examples/ADT/Expr.hs view
@@ -123,7 +123,7 @@ -- -- >>> genE -- Satisfiable. Model:--- e1 = Let "p" (Val 5) (Val 3) :: Expr+-- e1 = Let "h" (Val 4) (Val 3) :: Expr -- e2 = Val (-2) :: Expr genE :: IO SatResult genE = sat $ do e1 :: SExpr <- free "e1"@@ -140,7 +140,7 @@ -- | Query mode example. -- -- >>> queryE--- e1: (let p = 5 in 3)+-- e1: (let h = 4 in 3) -- e2: -2 queryE :: IO () queryE = runSMT $ do
Documentation/SBV/Examples/ADT/Param.hs view
@@ -149,9 +149,9 @@ -- | Query mode example. -- -- >>> queryE--- e1: (let p = (-3 * -1) in (1 * p))+-- e1: (let p = (-1 * 1) in (-3 * p)) -- e2: -2--- e3: (let q = 96 % 97 in q)+-- e3: (let q = 95 % 96 in q) queryE :: IO () queryE = runSMT $ do e1 :: SExpr String Integer <- free "e1"
Documentation/SBV/Examples/ADT/Types.hs view
@@ -88,13 +88,13 @@ -- >>> idWF -- Satisfiable. Model: -- env :: String -> T--- env _ = TStr+-- env _ = TInt -- <BLANKLINE> -- typeOf :: M -> T--- typeOf _ = TArr TStr TStr+-- typeOf _ = TArr TInt TInt ----- The model is rather uninteresting, but it shows that identity can have the type String to String, where--- all variables are mapped to Strings.+-- The model is rather uninteresting, but it shows that identity can have the type Integer to Integer, where+-- all variables are mapped to Integers. idWF :: IO SatResult idWF = sat $ wellTyped $ sLam x vx where x = literal "x"
Documentation/SBV/Examples/Lists/BoundedMutex.hs view
@@ -110,7 +110,7 @@ -- -- >>> notFair 10 -- Fairness is violated at bound: 10--- P1: [Idle,Idle,Ready,Critical,Idle,Ready,Critical,Critical,Idle,Ready]+-- P1: [Idle,Idle,Idle,Idle,Ready,Critical,Critical,Critical,Idle,Ready] -- P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready] -- Ts: [1,1,1,1,1,1,1,1,1,1] --
Documentation/SBV/Examples/Misc/Enumerate.hs view
@@ -35,11 +35,11 @@ -- -- >>> elts -- Solution #1:--- s0 = C :: E+-- s0 = B :: E -- Solution #2: -- s0 = A :: E -- Solution #3:--- s0 = B :: E+-- s0 = C :: E -- Found 3 different solutions. elts :: IO AllSatResult elts = allSat $ \(x::SE) -> x .== x
Documentation/SBV/Examples/Misc/SetAlgebra.hs view
@@ -348,7 +348,7 @@ >>> prove $ \(a :: SI) b c -> a `isSubsetOf` (b `union` c) .=> a `isSubsetOf` b .&& a `isSubsetOf` c Falsifiable. Counter-example:- s0 = {2} :: {Integer}+ s0 = U :: {Integer} s1 = U :: {Integer} s2 = U - {2} :: {Integer}
Documentation/SBV/Examples/Puzzles/Murder.hs view
@@ -87,10 +87,10 @@ -- | Solve the puzzle. We have: -- -- >>> killer--- Alice 48 Bar Female Bystander--- Husband 47 Beach Male Killer--- Brother 48 Beach Male Victim--- Daughter 21 Alone Female Bystander+-- Alice 47 Bar Female Bystander+-- Husband 46 Beach Male Killer+-- Brother 47 Beach Male Victim+-- Daughter 20 Alone Female Bystander -- Son 20 Bar Male Bystander -- -- That is, Alice's brother was the victim and Alice's husband was the killer.
Documentation/SBV/Examples/TP/GCD.hs view
@@ -184,7 +184,7 @@ -- * Divisibility --- | Divides relation. By definition we @0@ only divides @0@. (But every number divides @0@).+-- | Divides relation. By definition @0@ only divides @0@. (But every number divides @0@). dvd :: SInteger -> SInteger -> SBool a `dvd` b = ite (a .== 0) (b .== 0) (b `sEMod` a .== 0) @@ -321,6 +321,7 @@ =: a .== d * n -- Thus we can deduce d must divide a+ ?? d `dvd` (d * n) =: d `dvd` a -- Done!
+ Documentation/SBV/Examples/TP/Primes.hs view
@@ -0,0 +1,487 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.TP.Primes+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- Prove that there are an infinite number of primes. Along the way we formalize+-- and prove a number of properties about divisibility as well. Our proof is inspired by+-- the ACL2 proof in <https://github.com/acl2/acl2/blob/master/books/projects/numbers/euclid.lisp>.+-----------------------------------------------------------------------------++{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeApplications #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Documentation.SBV.Examples.TP.Primes where++import Data.SBV+import Data.SBV.TP++#ifdef DOCTEST+-- $setup+-- >>> import Data.SBV.TP+#endif++-- * Divisibility++-- | Divides relation. By definition @0@ only divides @0@. (But every number divides @0@).+dvd :: SInteger -> SInteger -> SBool+x `dvd` y = ite (x .== 0) (y .== 0) (y `sEMod` x .== 0)++-- | \(x \mid y \implies x \mid y * z\)+--+-- === __Proof__+-- >>> runTP dividesProduct+-- Lemma: dividesProduct+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.2.3 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] dividesProduct :: Ɐx ∷ Integer → Ɐy ∷ Integer → Ɐz ∷ Integer → Bool+dividesProduct :: TP (Proof (Forall "x" Integer -> Forall "y" Integer -> Forall "z" Integer -> SBool))+dividesProduct = calc "dividesProduct"+ (\(Forall x) (Forall y) (Forall z) -> x `dvd` y .=> x `dvd` (y*z)) $+ \x y z -> [x `dvd` y]+ |- cases [ x .== 0 ==> x `dvd` (y*z)+ ?? y .== 0+ =: sTrue+ =: qed+ , x ./= 0 ==> x `dvd` (y*z)+ ?? y .== x * y `sEDiv` x+ =: x `dvd` ((x * y `sEDiv` x) * z)+ =: x `dvd` (x * ((y `sEDiv` x) * z))+ =: sTrue+ =: qed+ ]+-- | \(x \mid y \land y \mid z \implies x \mid z\)+--+-- === __Proof__+-- >>> runTP dividesTransitive+-- Lemma: dividesProduct Q.E.D.+-- Lemma: dividesTransitive+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.2.3 (hard) Q.E.D.+-- Step: 1.2.4 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] dividesTransitive :: Ɐx ∷ Integer → Ɐy ∷ Integer → Ɐz ∷ Integer → Bool+dividesTransitive :: TP (Proof (Forall "x" Integer -> Forall "y" Integer -> Forall "z" Integer -> SBool))+dividesTransitive = do+ dp <- recall "dividesProduct" dividesProduct++ calc "dividesTransitive"+ (\(Forall x) (Forall y) (Forall z) -> x `dvd` y .&& y `dvd` z .=> x `dvd` z) $+ \x y z -> [x `dvd` y, y `dvd` z]+ |- cases [ x .== 0 .|| y .== 0 .|| z .== 0 ==> trivial+ , x ./= 0 .&& y ./= 0 .&& z ./= 0+ ==> x `dvd` z+ ?? z .== z `sEDiv` y * y+ =: x `dvd` (z `sEDiv` y * y)+ ?? y .== y `sEDiv` x * x+ =: x `dvd` ((z `sEDiv` y) * (y `sEDiv` x * x))+ ?? "hard"+ =: x `dvd` (x * ((z `sEDiv` y) * (y `sEDiv` x)))+ ?? dp `at` (Inst @"x" x, Inst @"y" x, Inst @"z" ((z `sEDiv` y) * (y `sEDiv` x)))+ =: sTrue+ =: qed+ ]++-- * The least divisor++-- | The definition of primality will depend on the notion of least divisor. Given @k@ and @n@, the least-divisor of+-- @n@ that is at least @k@ is the number that is at least @k@ and divides @n@ evenly. The idea is that a number is+-- prime if the least divisor starting from @2@ is itself.+ld :: SInteger -> SInteger -> SInteger+ld = smtFunction "ld" $ \k n -> ite (n `sEMod` k .== 0) k (ld (k+1) n)++-- | \(1 < k \leq n \implies \mathit{ld}\,k\,n \mid n \land k \leq \mathit{ld}\,k\,n \leq n\)+--+-- === __Proof__+-- >>> runTP leastDivisorDivides+-- Inductive lemma (strong): leastDivisorDivides+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] leastDivisorDivides :: Ɐk ∷ Integer → Ɐn ∷ Integer → Bool+leastDivisorDivides :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))+leastDivisorDivides =+ sInduct "leastDivisorDivides"+ (\(Forall k) (Forall n) -> 1 .< k .&& k .<= n .=> let d = ld k n in d `dvd` n .&& k .<= d .&& d .<= n)+ (\k n -> n - k, []) $+ \ih k n -> [1 .< k, k .<= n]+ |- let d = ld k n+ in cases [ n `sEMod` k .== 0 ==> d `dvd` n .&& k .<= d .&& d .<= n+ ?? d .== k+ =: sTrue+ =: qed+ , n `sEMod` k ./= 0 ==> d `dvd` n .&& k .<= d .&& d .<= n+ ?? d .== ld (k+1) n+ ?? ih+ =: sTrue+ =: qed+ ]++-- | \(1 < k \leq n \land d \mid n \land k \leq d \implies \mathit{ld}\,k\,n \leq d\)+--+-- === __Proof__+-- >>> runTP leastDivisorIsLeast+-- Inductive lemma (strong): leastDivisorisLeast+-- Step: Measure is non-negative Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] leastDivisorisLeast :: Ɐk ∷ Integer → Ɐn ∷ Integer → Ɐd ∷ Integer → Bool+leastDivisorIsLeast :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> Forall "d" Integer -> SBool))+leastDivisorIsLeast =+ sInduct "leastDivisorisLeast"+ (\(Forall k) (Forall n) (Forall d) -> 1 .< k .&& k .<= n .&& d `dvd` n .&& k .<= d .=> ld k n .<= d)+ (\k n _d -> n - k, []) $+ \ih k n d -> [1 .< k, k .<= n, d `dvd` n, k .<= d]+ |- cases [ n `sEMod` k .== 0 ==> ld k n .<= d+ =: k .<= d+ =: qed+ , n `sEMod` k ./= 0 ==> ld k n .<= d+ ?? ih+ =: sTrue+ =: qed+ ]++-- | \(n \geq k \geq 2 \implies \mathit{ld}\,k\,(\mathit{ld}\,k\,n) = \mathit{ld}\,k\,n\)+--+-- === __Proof__+-- >>> runTP leastDivisorTwice+-- Lemma: dividesTransitive Q.E.D.+-- Lemma: leastDivisorDivides Q.E.D.+-- Lemma: leastDivisorIsLeast Q.E.D.+-- Lemma: helper1 Q.E.D.+-- Lemma: helper2 Q.E.D.+-- Lemma: helper3 Q.E.D.+-- Lemma: helper4 Q.E.D.+-- Lemma: helper5+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- Lemma: leastDivisorTwice Q.E.D.+-- [Proven] leastDivisorTwice :: Ɐk ∷ Integer → Ɐn ∷ Integer → Bool+leastDivisorTwice :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> SBool))+leastDivisorTwice = do+ dt <- recall "dividesTransitive" dividesTransitive+ ldd <- recall "leastDivisorDivides" leastDivisorDivides+ ldl <- recall "leastDivisorIsLeast" leastDivisorIsLeast++ h1 <- lemma "helper1"+ (\(Forall @"k" k) (Forall @"n" n) -> n .>= k .&& k .>= 2 .=> ld k (ld k n) `dvd` ld k n .&& ld k (ld k n) .<= ld k n)+ [proofOf ldd]++ h2 <- lemma "helper2"+ (\(Forall @"k" k) (Forall @"n" n) -> n .>= k .&& k .>= 2 .=> ld k n `dvd` n)+ [proofOf ldd]++ h3 <- lemma "helper3"+ (\(Forall @"k" k) (Forall @"n" n) -> n .>= k .&& k .>= 2 .=> ld k (ld k n) `dvd` n)+ [proofOf h1, proofOf h2, proofOf dt]++ h4 <- lemma "helper4"+ (\(Forall @"k" k) (Forall @"n" n) -> n .>= k .&& k .>= 2 .=> k .<= ld k (ld k n))+ [proofOf ldd]++ h5 <- calc "helper5"+ (\(Forall @"k" k) (Forall @"n" n) -> n .>= k .&& k .>= 2 .=> ld k n .<= ld k (ld k n)) $+ \k n -> [n .>= k, k .>= 2]+ |- ld k n .<= ld k (ld k n)+ ?? h3 `at` (Inst @"k" k, Inst @"n" n)+ ?? h4 `at` (Inst @"k" k, Inst @"n" n)+ ?? ldl `at` (Inst @"k" k, Inst @"n" n, Inst @"d" (ld k (ld k n)))+ =: sTrue+ =: qed++ lemma "leastDivisorTwice"+ (\(Forall k) (Forall n) -> n .>= k .&& k .>= 2 .=> ld k (ld k n) .== ld k n)+ [proofOf h1, proofOf h5]++-- * Primality++-- | A number is prime if its least divisor greater than or equal to @2@ is itself.+isPrime :: SInteger -> SBool+isPrime n = n .>= 2 .&& ld 2 n .== n++-- | \(\mathit{isPrime}\,p \implies p \geq 2\)+--+-- === __Proof__+-- >>> runTP primeAtLeast2+-- Lemma: primeAtLeast2 Q.E.D.+-- [Proven] primeAtLeast2 :: Ɐp ∷ Integer → Bool+primeAtLeast2 :: TP (Proof (Forall "p" Integer -> SBool))+primeAtLeast2 = lemma "primeAtLeast2" (\(Forall p) -> isPrime p .=> p .>= 2) []++-- | \(n \geq 2 \implies \mathit{isPrime}\,(\mathit{ld}\,2\,n)\)+--+-- === __Proof__+-- >>> runTP leastDivisorIsPrime+-- Lemma: leastDivisorTwice Q.E.D.+-- Lemma: leastDivisorDivides Q.E.D.+-- Lemma: leastDivisorIsPrime+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- [Proven] leastDivisorIsPrime :: Ɐn ∷ Integer → Bool+leastDivisorIsPrime :: TP (Proof (Forall "n" Integer -> SBool))+leastDivisorIsPrime = do+ ldt <- recall "leastDivisorTwice" leastDivisorTwice+ ldd <- recall "leastDivisorDivides" leastDivisorDivides++ calc "leastDivisorIsPrime"+ (\(Forall n) -> n .>= 2 .=> isPrime (ld 2 n)) $+ \n -> [n .>= 2] |- isPrime (ld 2 n)+ ?? ldt `at` (Inst @"k" 2, Inst @"n" n)+ ?? ldd `at` (Inst @"k" 2, Inst @"n" n)+ =: sTrue+ =: qed++-- | The least prime divisor is the least divisor of it starting from @2@. By 'leastDivisorIsPrime', this number+-- is guaranteed to be prime.+leastPrimeDivisor :: SInteger -> SInteger+leastPrimeDivisor n = ld 2 n++-- * Formalizing factorial++-- | The factorial function.+fact :: SInteger -> SInteger+fact = smtFunction "fact" $ \n -> ite (n .<= 0) 1 (n * fact (n - 1))++-- | \(n! \geq 1\)+--+-- === __Proof__+-- >>> runTP factAtLeast1+-- Inductive lemma: factAtLeast1+-- Step: Base Q.E.D.+-- Step: 1 (2 way case split)+-- Step: 1.1 Q.E.D.+-- Step: 1.2.1 Q.E.D.+-- Step: 1.2.2 Q.E.D.+-- Step: 1.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] factAtLeast1 :: Ɐn ∷ Integer → Bool+factAtLeast1 :: TP (Proof (Forall "n" Integer -> SBool))+factAtLeast1 = inductWith cvc5 "factAtLeast1"+ (\(Forall n) -> fact n .>= 1) $+ \ih n -> [] |- fact (n+1) .>= 1+ =: cases [ n+1 .<= 0 ==> trivial+ , n+1 .> 0 ==> (n+1) * fact n .>= 1+ ?? ih+ =: sTrue+ =: qed+ ]++-- | \(1 \leq k \land k \leq n \implies k \mid n!\)+--+-- === __Proof__+-- >>> runTP dividesFact+-- Lemma: dividesProduct Q.E.D.+-- Inductive lemma: dividesFact+-- Step: Base Q.E.D.+-- Step: 1 Q.E.D.+-- Step: 2 (2 way case split)+-- Step: 2.1.1 Q.E.D.+-- Step: 2.1.2 Q.E.D.+-- Step: 2.2.1 Q.E.D.+-- Step: 2.2.2 Q.E.D.+-- Step: 2.Completeness Q.E.D.+-- Result: Q.E.D.+-- [Proven] dividesFact :: Ɐn ∷ Integer → Ɐk ∷ Integer → Bool+dividesFact :: TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))+dividesFact = do+ dvp <- recall "dividesProduct" dividesProduct++ induct "dividesFact"+ (\(Forall n) (Forall k) -> 1 .<= k .&& k .<= n .=> k `dvd` fact n) $+ \ih n k -> [1 .<= k, k .<= n + 1]+ |- k `dvd` fact (n + 1)+ =: k `dvd` ((n + 1) * fact n)+ =: cases [ k .== n + 1 ==> k `dvd` ((n + 1) * fact n)+ ?? dvp `at` (Inst @"x" k, Inst @"y" (n+1), Inst @"z" (fact n))+ =: sTrue+ =: qed+ , k ./= n + 1 ==> k `dvd` ((n + 1) * fact n)+ ?? ih+ ?? dvp `at` (Inst @"x" k, Inst @"y" (fact n), Inst @"z" (n+1))+ =: sTrue+ =: qed+ ]++-- | \(1 \leq k \land k \leq n \implies \neg (k \mid n! + 1)\)+--+-- === __Proof__+-- >>> runTP notDividesFactP1+-- Lemma: dividesFact Q.E.D.+-- Lemma: notDividesFactP1+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- [Proven] notDividesFactP1 :: Ɐn ∷ Integer → Ɐk ∷ Integer → Bool+notDividesFactP1 :: TP (Proof (Forall "n" Integer -> Forall "k" Integer -> SBool))+notDividesFactP1 = do+ df <- recall "dividesFact" dividesFact++ calc "notDividesFactP1"+ (\(Forall n) (Forall k) -> 1 .< k .&& k .<= n .=> sNot (k `dvd` (fact n + 1))) $+ \n k -> [1 .< k, k .<= n]+ |- k `dvd` (fact n + 1)+ ?? df `at` (Inst @"n" n, Inst @"k" k)+ =: k `dvd` (k * fact n `sEDiv` k + 1)+ =: k `dvd` 1+ =: contradiction++-- * Finding a greater prime++-- | Given a number, return another number which is both prime and is larger than the input. Note that+-- we don't claim to return the closest prime to the input. Just some prime that is larger, as we shall prove.+greaterPrime :: SInteger -> SInteger+greaterPrime n = leastPrimeDivisor (1 + fact n)++-- | \(\mathit{greaterPrime}\, n \mid n! + 1\)+--+-- === __Proof__+-- >>> runTP greaterPrimeDivides+-- Lemma: leastDivisorDivides Q.E.D.+-- Lemma: factAtLeast1 Q.E.D.+-- Lemma: greaterPrimeDivides+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- [Proven] greaterPrimeDivides :: Ɐn ∷ Integer → Bool+greaterPrimeDivides :: TP (Proof (Forall "n" Integer -> SBool))+greaterPrimeDivides = do+ ldd <- recall "leastDivisorDivides" leastDivisorDivides+ fal1 <- recall "factAtLeast1" factAtLeast1++ calc "greaterPrimeDivides"+ (\(Forall n) -> greaterPrime n `dvd` (1 + fact n)) $+ \n -> [] |- greaterPrime n `dvd` (1 + fact n)+ =: leastPrimeDivisor (1 + fact n) `dvd` (1 + fact n)+ =: ld 2 (1 + fact n) `dvd` (1 + fact n)+ ?? ldd `at` (Inst @"k" 2, Inst @"n" (1 + fact n))+ ?? fal1 `at` Inst @"n" n+ =: sTrue+ =: qed++-- | \(\mathit{greaterPrime}\, n > n\)+--+-- === __Proof__+-- >>> runTP greaterPrimeGreater+-- Lemma: notDividesFactP1 Q.E.D.+-- Lemma: greaterPrimeDivides Q.E.D.+-- Lemma: leastDivisorIsPrime Q.E.D.+-- Lemma: factAtLeast1 Q.E.D.+-- Lemma: primeAtLeast2 Q.E.D.+-- Lemma: greaterPrimeGreater+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Step: 4 Q.E.D.+-- Step: 5 Q.E.D.+-- Step: 6 Q.E.D.+-- Result: Q.E.D.+-- [Proven] greaterPrimeGreater :: Ɐn ∷ Integer → Bool+greaterPrimeGreater :: TP (Proof (Forall "n" Integer -> SBool))+greaterPrimeGreater = do+ ndfp1 <- recall "notDividesFactP1" notDividesFactP1+ gpd <- recall "greaterPrimeDivides" greaterPrimeDivides+ ldp <- recall "leastDivisorIsPrime" leastDivisorIsPrime+ fal1 <- recall "factAtLeast1" factAtLeast1+ pal2 <- recall "primeAtLeast2" primeAtLeast2++ calc "greaterPrimeGreater"+ (\(Forall n) -> greaterPrime n .> n) $+ \n -> [] |-> sTrue+ ?? ndfp1 `at` (Inst @"n" n, Inst @"k" (greaterPrime n))+ ?? gpd `at` Inst @"n" n+ =: sNot (1 .< greaterPrime n .&& greaterPrime n .<= n)+ =: (1 .>= greaterPrime n .|| greaterPrime n .> n)+ =: (1 .>= leastPrimeDivisor (1 + fact n) .|| greaterPrime n .> n)+ =: (1 .>= leastPrimeDivisor (1 + fact n) .|| greaterPrime n .> n)+ =: (1 .>= ld 2 (1 + fact n) .|| greaterPrime n .> n)+ ?? ldp `at` Inst @"n" (1 + fact n)+ ?? pal2 `at` Inst @"p" (ld 2 (1 + fact n))+ ?? fal1 `at` Inst @"n" n+ =: greaterPrime n .> n+ =: qed++-- * Infinitude of primes++-- | \(\mathit{isPrime}\,(\mathit{greaterPrime}\,n) \land \mathit{greaterPrime}\,n > n\)+--+-- We can finally prove our goal: For each given number, there is a larger number that is prime. This+-- establishes that we have an infinite number of primes.+--+-- === __Proof__+-- >>> runTP infinitudeOfPrimes+-- Lemma: leastDivisorIsPrime Q.E.D.+-- Lemma: factAtLeast1 Q.E.D.+-- Lemma: greaterPrimeGreater Q.E.D.+-- Lemma: infinitudeOfPrimes+-- Step: 1 Q.E.D.+-- Step: 2 Q.E.D.+-- Step: 3 Q.E.D.+-- Result: Q.E.D.+-- [Proven] infinitudeOfPrimes :: Ɐn ∷ Integer → Bool+infinitudeOfPrimes :: TP (Proof (Forall "n" Integer -> SBool))+infinitudeOfPrimes = do+ ldp <- recall "leastDivisorIsPrime" leastDivisorIsPrime+ fa1 <- recall "factAtLeast1" factAtLeast1+ gpg <- recall "greaterPrimeGreater" greaterPrimeGreater++ calc "infinitudeOfPrimes"+ (\(Forall n) -> let p = greaterPrime n in p .> n .&& isPrime p) $+ \n -> [] |- let p = greaterPrime n+ in p .> n .&& isPrime (greaterPrime n)+ =: p .> n .&& isPrime (leastPrimeDivisor (1 + fact n))+ =: p .> n .&& isPrime (ld 2 (1 + fact n))+ ?? ldp `at` Inst @"n" (1 + fact n)+ ?? fa1 `at` Inst @"n" n+ ?? gpg `at` Inst @"n" n+ =: sTrue+ =: qed++-- | \(\forall n. \exists p. \mathit{isPrime}\,p \land p > n\)+--+-- Another expression of the fact that there are infinitely many primes. One might prefer this+-- version as it only refers to the 'isPrime' predicate only.+--+-- === __Proof__+-- >>> runTP noLargestPrime+-- Lemma: infinitudeOfPrimes Q.E.D.+-- Lemma: noLargestPrime+-- Step: 1 Q.E.D.+-- Result: Q.E.D.+-- [Proven] noLargestPrime :: Ɐn ∷ Integer → Bool+noLargestPrime :: TP (Proof (Forall "n" Integer -> SBool))+noLargestPrime = do+ iop <- recall "infinitudeOfPrimes" infinitudeOfPrimes++ calc "noLargestPrime"+ (\(Forall n) -> quantifiedBool (\(Exists p) -> isPrime p .&& p .> n)) $+ \n -> [] |- quantifiedBool (\(Exists p) -> isPrime p .&& p .> n)+ ?? iop `at` Inst @"n" n+ =: sTrue+ =: qed++{- HLint ignore module "Avoid lambda" -}+{- HLint ignore module "Eta reduce" -}
+ Documentation/SBV/Examples/Uninterpreted/EUFLogic.hs view
@@ -0,0 +1,340 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.Uninterpreted.EUFLogic+-- License : BSD3+-- Stability : experimental+--+-- Demonstrates the ability to generate uninterpreted functions of arbitrarily+-- many arguments, whose types are generated programmatically. The high-level+-- idea of this module is to provide a strongly-typed representation, using a+-- GADT, of a logic that includes uninterpreted functions. This module then+-- defines an interpretation of this logic into SBV, which it uses to perform+-- SMT queries in the logic.+-----------------------------------------------------------------------------++{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++module Documentation.SBV.Examples.Uninterpreted.EUFLogic where++import Data.SBV++import Control.Monad.State++import Data.Kind+import Data.Type.Equality+import Data.Map (Map)+import qualified Data.Map as Map++import GHC.TypeLits++#ifdef DOCTEST+-- $setup+-- >>> import Data.SBV+#endif++----------------------------------------------------------------------+-- * Types of the EUF Logic+----------------------------------------------------------------------++-- | The datakind for the types in our EUF logic.+data EUFType = Tp_Bool | Tp_BV Natural++-- | A singleton type for natural numbers that can be used as the widths of bitvectors.+data BVWidth w = (KnownNat w, BVIsNonZero w) => BVWidth (SNat w)++-- | Create a t'BVWidth' object for a 'KnownNat' that is non-zero+knownBVWidth :: (KnownNat w, BVIsNonZero w) => BVWidth w+knownBVWidth = BVWidth natSing++-- | TestEquality instance for BVWidth.+instance TestEquality BVWidth where+ testEquality (BVWidth w1) (BVWidth w2) | Just Refl <- testEquality w1 w2 = Just Refl+ | True = Nothing++-- | A singleton type that represents type-level 'EUFType's at the object level+data TypeRepr (tp :: EUFType) where+ Repr_Bool :: TypeRepr Tp_Bool+ Repr_BV :: BVWidth w -> TypeRepr (Tp_BV w)++-- | TestEquality instance for Type representations+instance TestEquality TypeRepr where+ testEquality Repr_Bool Repr_Bool = Just Refl+ testEquality (Repr_BV w1) (Repr_BV w2) | Just Refl <- testEquality w1 w2 = Just Refl+ testEquality _ _ = Nothing++-- | A list of 'TypeRepr's for each type in a type-level list+data TypeReprs tps where+ Repr_Nil :: TypeReprs '[]+ Repr_Cons :: TypeRepr tp -> TypeReprs tps -> TypeReprs (tp ': tps)++instance TestEquality TypeReprs where+ testEquality Repr_Nil Repr_Nil = Just Refl+ testEquality (Repr_Cons tps1 tp1) (Repr_Cons tps2 tp2) | Just Refl <- testEquality tps1 tps2+ , Just Refl <- testEquality tp1 tp2 = Just Refl+ testEquality _ _ = Nothing++-- | An 'EUFType' with a known 'TypeRepr' representation+class KnownEUFType tp where+ knownEUFType :: TypeRepr tp++-- | Mapping from Tp_Bool+instance KnownEUFType Tp_Bool where+ knownEUFType = Repr_Bool++-- | Mapping from Tp_BV+instance (KnownNat w, BVIsNonZero w) => KnownEUFType (Tp_BV w) where+ knownEUFType = Repr_BV (BVWidth natSing)++-- | A sequence of types t'EUFType' with a known 'TypeReprs' representation+class KnownEUFTypes tps where+ knownEUFTypes :: TypeReprs tps++instance KnownEUFTypes '[] where+ knownEUFTypes = Repr_Nil++instance (KnownEUFType tp, KnownEUFTypes tps) => KnownEUFTypes (tp ': tps) where+ knownEUFTypes = Repr_Cons knownEUFType knownEUFTypes++----------------------------------------------------------------------+-- * Operations of the EUF Logic+----------------------------------------------------------------------++-- | An uninterpreted function in our EUF logic, which is a string name plus the input and output types.+data UnintOp (ins :: [EUFType]) (out :: EUFType) = UnintOp { unintOpName :: String+ , unintOpIns :: TypeReprs ins+ , unintOpOut :: TypeRepr out+ }++-- | The operations of our EUF logic, which are indexed by a list of 0 or more+-- input types and a single output type.+data Op (ins :: [EUFType]) (out :: EUFType) where+ -- Uninterpreted functions+ Op_Unint :: UnintOp ins out -> Op ins out++ -- Boolean operations+ Op_And :: Op (Tp_Bool ': Tp_Bool ': '[]) Tp_Bool+ Op_Or :: Op (Tp_Bool ': Tp_Bool ': '[]) Tp_Bool+ Op_Not :: Op (Tp_Bool ': '[]) Tp_Bool+ Op_BoolLit :: Bool -> Op '[] Tp_Bool+ Op_IfThenElse :: TypeRepr a -> Op (Tp_Bool ': a ': a ': '[]) a++ -- Bitvector operations+ Op_Plus :: BVWidth w -> Op (Tp_BV w ': Tp_BV w ': '[]) (Tp_BV w)+ Op_Minus :: BVWidth w -> Op (Tp_BV w ': Tp_BV w ': '[]) (Tp_BV w)+ Op_Times :: BVWidth w -> Op (Tp_BV w ': Tp_BV w ': '[]) (Tp_BV w)++ Op_Abs :: BVWidth w -> Op (Tp_BV w ': '[]) (Tp_BV w)+ Op_Signum :: BVWidth w -> Op (Tp_BV w ': '[]) (Tp_BV w)++ Op_BVLit :: BVWidth w -> Integer -> Op '[] (Tp_BV w)++ Op_BVEq :: BVWidth w -> Op (Tp_BV w ': Tp_BV w ': '[]) Tp_Bool+ Op_BVLt :: BVWidth w -> Op (Tp_BV w ': Tp_BV w ': '[]) Tp_Bool++-- | Create an uninterpreted 'Op' of known type+mkUnintOp :: (KnownEUFTypes ins, KnownEUFType out) => String -> Op ins out+mkUnintOp nm = Op_Unint $ UnintOp nm knownEUFTypes knownEUFType++-- | Get the input types and output type of an 'Op'+opInsOut :: Op ins out -> (TypeReprs ins, TypeRepr out)+opInsOut (Op_Unint uop) = (unintOpIns uop, unintOpOut uop)+opInsOut Op_And = (knownEUFTypes, knownEUFType)+opInsOut Op_Or = (knownEUFTypes, knownEUFType)+opInsOut Op_Not = (knownEUFTypes, knownEUFType)+opInsOut (Op_BoolLit _) = (knownEUFTypes, knownEUFType)+opInsOut (Op_IfThenElse Repr_Bool) = (knownEUFTypes, knownEUFType)+opInsOut (Op_IfThenElse (Repr_BV BVWidth{})) = (knownEUFTypes, knownEUFType)+opInsOut (Op_Plus BVWidth{}) = (knownEUFTypes, knownEUFType)+opInsOut (Op_Minus BVWidth{}) = (knownEUFTypes, knownEUFType)+opInsOut (Op_Times BVWidth{}) = (knownEUFTypes, knownEUFType)+opInsOut (Op_Abs BVWidth{}) = (knownEUFTypes, knownEUFType)+opInsOut (Op_Signum BVWidth{}) = (knownEUFTypes, knownEUFType)+opInsOut (Op_BVLit BVWidth{} _) = (knownEUFTypes, knownEUFType)+opInsOut (Op_BVEq BVWidth{}) = (knownEUFTypes, knownEUFType)+opInsOut (Op_BVLt BVWidth{}) = (knownEUFTypes, knownEUFType)++-- | Get the input types of an 'Op'+opIns :: Op ins out -> TypeReprs ins+opIns = fst . opInsOut++----------------------------------------------------------------------+-- * Expressions of the EUF Logic+----------------------------------------------------------------------++-- | The expressions of our EUF logic, which are just operations applied to argument expressions.+data EUFExpr tp where+ EUFExpr :: Op ins out -> EUFExprs ins -> EUFExpr out++-- | A sequence of expressions for each type in a type-level list+data EUFExprs tps where+ EUFExprsNil :: EUFExprs '[]+ EUFExprsCons :: EUFExpr tp -> EUFExprs tps -> EUFExprs (tp ': tps)++-- | Build the type @t'EUFExpr' in1 -> ... -> t'EUFExpr' inn -> out@+type family EUFExprFun (ins :: [EUFType]) (out :: EUFType) :: Type where+ EUFExprFun '[] out = EUFExpr out+ EUFExprFun (tp ': tps) out = EUFExpr tp -> EUFExprFun tps out++-- | Build an t'EUFExprFun' from a function on t'EUFExprs'+lambdaEUFExprFun :: TypeReprs ins -> (EUFExprs ins -> EUFExpr out) -> EUFExprFun ins out+lambdaEUFExprFun Repr_Nil f = f EUFExprsNil+lambdaEUFExprFun (Repr_Cons _ tps) f = \e -> lambdaEUFExprFun tps (f . EUFExprsCons e)++-- | Apply an 'Op' to t'EUFExprs' for its input types, returning an t'EUFExpr' for its output type+applyOp :: Op ins out -> EUFExprFun ins out+applyOp op = lambdaEUFExprFun (opIns op) (EUFExpr op)++instance (KnownNat w, BVIsNonZero w) => Num (EUFExpr (Tp_BV w)) where+ fromInteger i = applyOp (Op_BVLit knownBVWidth i)++ e1 + e2 = applyOp (Op_Plus knownBVWidth) e1 e2+ e1 - e2 = applyOp (Op_Minus knownBVWidth) e1 e2+ e1 * e2 = applyOp (Op_Times knownBVWidth) e1 e2++ abs e = applyOp (Op_Abs knownBVWidth) e+ signum e = applyOp (Op_Signum knownBVWidth) e++-- | Build an expression from an uninterpreted operation of a known type+mkUnintExpr :: KnownEUFType tp => String -> EUFExpr tp+mkUnintExpr nm = EUFExpr (mkUnintOp nm) EUFExprsNil++----------------------------------------------------------------------+-- * Interpreting the EUF Logic into SBV+----------------------------------------------------------------------++-- | Convert an 'EUFType' to a type of SBV expressions+type family Type2SBV (tp :: EUFType) :: Type where+ Type2SBV Tp_Bool = SBool+ Type2SBV (Tp_BV w) = SBV (WordN w)++-- | Convert the type inputs plus output of an 'Op' to a function over 'SBV' values+type family OpTypes2SBV (ins :: [EUFType]) (out :: EUFType) :: Type where+ OpTypes2SBV '[] out = Type2SBV out+ OpTypes2SBV (tp ': tps) out = Type2SBV tp -> OpTypes2SBV tps out++-- | Create an 'SMTDefinable' instance for the type returned by 'OpTypes2SBV' and pass it to a local function+withSMTDefOpTypes :: TypeReprs ins -> TypeRepr out -> (SMTDefinable (OpTypes2SBV ins out) => a) -> a+withSMTDefOpTypes Repr_Nil Repr_Bool f = f+withSMTDefOpTypes Repr_Nil (Repr_BV BVWidth{}) f = f+withSMTDefOpTypes (Repr_Cons Repr_Bool ins) out f = withSMTDefOpTypes ins out f+withSMTDefOpTypes (Repr_Cons (Repr_BV BVWidth{}) ins) out f = withSMTDefOpTypes ins out f++-- | An uninterpreted function that has been resolved to an 'SBV' function+data ResolvedUnintOp = forall ins out. ResolvedUnintOp (UnintOp ins out) (OpTypes2SBV ins out)++-- | A 'Map' for resolving uninterpreted operations+type UnintMap = Map String ResolvedUnintOp++-- | Look up the uninterpreted op associated with a 'String' in an 'UnintMap' at+-- a particular type, raising an error if that 'String' is associated with a+-- different type. If the 'String' is not associated with any uninterpreted+-- function, create one and return it, updating the 'UnintMap'.+unintEnsure :: UnintOp ins out -> UnintMap -> (OpTypes2SBV ins out, UnintMap)+unintEnsure uop m+ | Just (ResolvedUnintOp uop' f) <- Map.lookup (unintOpName uop) m+ , Just Refl <- testEquality (unintOpIns uop) (unintOpIns uop')+ , Just Refl <- testEquality (unintOpOut uop) (unintOpOut uop')+ = (f, m)+unintEnsure uop m+ | Just _ <- Map.lookup (unintOpName uop) m+ = error $ "unintEnsure: uninterpreted op " ++ unintOpName uop ++ " used at incorrect type"+unintEnsure uop m =+ withSMTDefOpTypes (unintOpIns uop) (unintOpOut uop)+ $ let f = uninterpret (unintOpName uop)+ in (f, Map.insert (unintOpName uop) (ResolvedUnintOp uop f) m)++-- | The monad for interpreting t'EUFExpr's into SBV, which is just a state monad+-- over an 'UnintMap'+type InterpM = State UnintMap++-- | Run an 'InterpM' computation starting with the empty 'UnintMap'+runInterpM :: InterpM a -> a+runInterpM = flip evalState Map.empty++-- | Interpret an 'Op' into a function over SBV values+interpOp :: Op ins out -> InterpM (OpTypes2SBV ins out)+interpOp (Op_Unint uop) = state (unintEnsure uop)+interpOp Op_And = return (.&&)+interpOp Op_Or = return (.||)+interpOp Op_Not = return sNot+interpOp (Op_BoolLit b) = return $ fromBool b+interpOp (Op_IfThenElse Repr_Bool) = return ite+interpOp (Op_IfThenElse (Repr_BV BVWidth{})) = return ite+interpOp (Op_Plus BVWidth{}) = return (+)+interpOp (Op_Minus BVWidth{}) = return (-)+interpOp (Op_Times BVWidth{}) = return (*)+interpOp (Op_Abs BVWidth{}) = return abs+interpOp (Op_Signum BVWidth{}) = return signum+interpOp (Op_BVLit BVWidth{} i) = return $ fromInteger i+interpOp (Op_BVEq BVWidth{}) = return (.==)+interpOp (Op_BVLt BVWidth{}) = return (.<)++-- | Interpret an t'EUFExpr' into an SBV value.+interpEUFExpr :: EUFExpr tp -> InterpM (Type2SBV tp)+interpEUFExpr (EUFExpr op args) = do f <- interpOp op+ interpApplyEUFExprs op f args++-- | Apply an interpretation of an operator to the interpretations of a sequence of arguments for it.+interpApplyEUFExprs :: ghost out -> OpTypes2SBV ins out -> EUFExprs ins -> InterpM (Type2SBV out)+interpApplyEUFExprs _ f EUFExprsNil = return f+interpApplyEUFExprs out f (EUFExprsCons e es) = do f_app <- f <$> interpEUFExpr e+ interpApplyEUFExprs out f_app es++-- | Top-level call to interpret an t'EUFExpr' to an 'SBV' value+interpEUF :: EUFExpr a -> Type2SBV a+interpEUF = runInterpM . interpEUFExpr++----------------------------------------------------------------------+-- * Examples+----------------------------------------------------------------------++-- | Example EUF problem+--+-- > f (f (a) - f (b)) /= f (c), b >= a, a >= b + c, c >= 0+--+-- from <https://goto.ucsd.edu/~rjhala/classes/sp13/cse291/slides/lec-smt.markdown.pdf>+-- noting that @x >= y@ is the same as @not (x < y)@. We have:+--+-- >>> sat $ interpEUF example+-- Satisfiable. Model:+-- a = 996506182 :: Word32+-- b = 3298461113 :: Word32+-- c = 1445036292 :: Word32+-- <BLANKLINE>+-- f :: Word32 -> Word32+-- f 0 = 4188219399+-- f 1445036292 = 285239361+-- f 3298461113 = 4054018119+-- f 996506182 = 4054018119+-- f _ = 0+--+-- Note that the original example is unsatisfiable over integers. It is however satisfiable+-- over 32-bit words, hence the model above.+example :: EUFExpr Tp_Bool+example =+ applyOp Op_And (applyOp Op_Not (applyOp (Op_BVEq knownBVWidth)+ (applyOp f (applyOp f a - applyOp f b))+ (applyOp f c)))+ (applyOp Op_And (applyOp Op_Not (applyOp (Op_BVLt knownBVWidth) b a))+ (applyOp Op_And+ (applyOp Op_Not (applyOp (Op_BVLt knownBVWidth) a (b + c)))+ (applyOp Op_Not (applyOp (Op_BVLt knownBVWidth) c 0))))+ where+ f :: Op '[Tp_BV 32] (Tp_BV 32)+ f = mkUnintOp "f"++ a, b, c :: EUFExpr (Tp_BV 32)+ a = mkUnintExpr "a"+ b = mkUnintExpr "b"+ c = mkUnintExpr "c"++{- HLint ignore "Use camelCase" -}+{- HLint ignore "Eta reduce" -}
Documentation/SBV/Examples/WeakestPreconditions/Sum.hs view
@@ -207,8 +207,8 @@ Following proof obligation failed: ================================== Invariant for loop "i < n" is not maintained by the body:- Before: SumS {n = 2, i = 1, s = 1}- After : SumS {n = 2, i = 2, s = 3}+ Before: SumS {n = 3, i = 1, s = 1}+ After : SumS {n = 3, i = 2, s = 3} Here, we posed the extra incorrect invariant that @s <= i@ must be maintained, and SBV found us a reachable state that violates the invariant. The /before/ state indeed satisfies @s <= i@, but the /after/ state does not. Note that the proof fails in this case not because the program
README.md view
@@ -231,6 +231,7 @@ May Torrence, Daniel Wagner, Sean Weaver,+Eddy Westbrook, Nis Wegmann, Jared Ziegler, and Marco Zocca.
SBVTestSuite/GoldFiles/adt06.gold view
@@ -95,9 +95,9 @@ [RECV] ((s0 (AMaybe (Just (mkSBVTuple3 2.0 (fp #b0 #x00 #b00000000000000000000001) (mkSBVTuple2 (Right (fp #b0 #x01 #b00000000000010000000000))- (seq.unit true)))))))+ (seq.unit false))))))) -getValue: AMaybe (Just (2.0,1.0e-45,(Right 1.1756378e-38,[True])))+getValue: AMaybe (Just (2.0,1.0e-45,(Right 1.1756378e-38,[False]))) DONE *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/adt_gen00.gold view
@@ -136,9 +136,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (Let "k" (Val 7) (Let "c" (Val 6) (Add (Var "c") (Var "c"))))))+[RECV] ((s0 (Let "h"+ (Let "p" (Val 5) (Var "p"))+ (Let "p" (Val 6) (Add (Var "p") (Var "p")))))) -Got: (let k = 7 in (let c = 6 in (c + c)))+Got: (let h = (let p = 5 in p) in (let p = 6 in (p + p))) DONE *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/adt_gen08.gold view
@@ -77,9 +77,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (Add (Val 3) (Val 2))))+[RECV] ((s0 (Add (Var "!0!") (Var "!0!")))) -Got: (3 + 2)+Got: (!0! + !0!) DONE *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/adt_gen09.gold view
@@ -77,9 +77,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (Mul (Val 3) (Val 2))))+[RECV] ((s0 (Mul (Var "!0!") (Var "!0!")))) -Got: (3 * 2)+Got: (!0! * !0!) DONE *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/adt_gen10.gold view
@@ -77,9 +77,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (Let "!0!" (Val 3) (Val 2))))+[RECV] ((s0 (Let "!0!" (Var "!0!") (Var "!0!")))) -Got: (let !0! = 3 in 2)+Got: (let !0! = !0! in !0!) DONE *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/adt_mr00.gold view
@@ -54,15 +54,16 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (Seq (Assign "!2!" (Con 3))- (Seq (Assign "!4!" (Con 5))- (Seq (Assign "!3!" (Con 4)) (Assign "!0!" (Add (Var "!1!") (Con 2))))))))+[RECV] ((s0 (Seq (Assign "!3!" (Var "!6!"))+ (Seq (Assign "!5!" (Var "!8!"))+ (Seq (Assign "!4!" (Var "!7!"))+ (Assign "!0!" (Add (Var "!1!") (Var "!2!")))))))) Got:-!2! := 3;-!4! := 5;-!3! := 4;-!0! := (!1! + 2)+!3! := !6!;+!5! := !8!;+!4! := !7!;+!0! := (!1! + !2!) DONE *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/adt_mr04.gold view
@@ -41,10 +41,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 ((as A2 (A Int (A (_ FloatingPoint 8 24) Bool))) (A3 (Aab "!0!" (Ab false))))))+[RECV] ((s0 ((as A2 (A Int (A (_ FloatingPoint 8 24) Bool))) (A3 (Aab "!0!"+ (Aab (_ +zero 8 24) false)))))) Got:-A2 {a2 = A3 {a3 = Aab {aba = "!0!", abb = Ab {ab = False}}}}+A2 {a2 = A3 {a3 = Aab {aba = "!0!", abb = Aab {aba = 0.0, abb = False}}}} DONE *** Solver : Z3 *** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/doctest_sanity.gold view
@@ -1,3 +1,3 @@-Total: 1069; Tried: 1069; Skipped: 0; Success: 1069; Errors: 0; Failures 0-Examples: 954; Tried: 954; Skipped: 0; Success: 954; Errors: 0; Failures 0-Setup: 115; Tried: 115; Skipped: 0; Success: 115; Errors: 0; Failures 0+Total: 1086; Tried: 1086; Skipped: 0; Success: 1086; Errors: 0; Failures 0+Examples: 969; Tried: 969; Skipped: 0; Success: 969; Errors: 0; Failures 0+Setup: 117; Tried: 117; Skipped: 0; Success: 117; Errors: 0; Failures 0
SBVTestSuite/GoldFiles/qUninterp1.gold view
@@ -30,9 +30,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 B))+[RECV] ((s0 A)) *** Solver : Z3 *** Exit code: ExitSuccess - FINAL:B+ FINAL:A DONE!
SBVTestSuite/GoldFiles/set_tupleSet.gold view
@@ -30,12 +30,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (mkSBVTuple2 (lambda ((x!1 Bool)) x!1)- (store ((as const (Array Bool Bool)) false) false true))))+[RECV] ((s0 (mkSBVTuple2 (lambda ((x!1 Bool)) x!1) ((as const (Array Bool Bool)) true)))) *** Solver : Z3 *** Exit code: ExitSuccess FINAL: Satisfiable. Model:- s0 = ({True},{False}) :: ({Bool}, {Bool})+ s0 = ({True},U) :: ({Bool}, {Bool}) DONE!
SBVTestSuite/GoldFiles/set_uninterp1.gold view
@@ -60,18 +60,18 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array E Bool)) false) A true)))+[RECV] ((s0 (store ((as const (Array E Bool)) true) C false))) [GOOD] (push 1)-[GOOD] (define-fun s7 () (Array E Bool) (store ((as const (Array E Bool)) false) (as A E) true))+[GOOD] (define-fun s7 () (Array E Bool) (store ((as const (Array E Bool)) true) (as C E) false)) [GOOD] (define-fun s8 () Bool (distinct s0 s7)) [GOOD] (assert s8) Fast allSat, Looking for solution 5 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) A true)))+[RECV] ((s0 (store (store ((as const (Array E Bool)) true) C false) B false))) [GOOD] (push 1)-[GOOD] (define-fun s9 () (Array E Bool) (store (store ((as const (Array E Bool)) false) (as C E) true) (as A E) true))+[GOOD] (define-fun s9 () (Array E Bool) (store (store ((as const (Array E Bool)) true) (as C E) false) (as B E) false)) [GOOD] (define-fun s10 () Bool (distinct s0 s9)) [GOOD] (assert s10) Fast allSat, Looking for solution 6@@ -87,18 +87,18 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store (store ((as const (Array E Bool)) true) C false) A false)))+[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) A true))) [GOOD] (push 1)-[GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) true) (as C E) false) (as A E) false))+[GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) false) (as C E) true) (as A E) true)) [GOOD] (define-fun s14 () Bool (distinct s0 s13)) [GOOD] (assert s14) Fast allSat, Looking for solution 8 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array E Bool)) true) C false)))+[RECV] ((s0 (store ((as const (Array E Bool)) false) B true))) [GOOD] (push 1)-[GOOD] (define-fun s15 () (Array E Bool) (store ((as const (Array E Bool)) true) (as C E) false))+[GOOD] (define-fun s15 () (Array E Bool) (store ((as const (Array E Bool)) false) (as B E) true)) [GOOD] (define-fun s16 () Bool (distinct s0 s15)) [GOOD] (assert s16) Fast allSat, Looking for solution 9@@ -117,15 +117,15 @@ FINAL: Solution #1:- s0 = U - {C} :: {E}+ s0 = {B} :: {E} Solution #2:- s0 = U - {A,C} :: {E}+ s0 = {A,C} :: {E} Solution #3: s0 = {C} :: {E} Solution #4:- s0 = {A,C} :: {E}+ s0 = U - {B,C} :: {E} Solution #5:- s0 = {A} :: {E}+ s0 = U - {C} :: {E} Solution #6: s0 = U - {A} :: {E} Solution #7:
SBVTestSuite/GoldFiles/set_uninterp2.gold view
@@ -34,12 +34,12 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array E Bool)) false) B true)))+[RECV] ((s0 (store ((as const (Array E Bool)) false) C true))) [SEND] (get-value (s1)) [RECV] ((s1 ((as const (Array E Bool)) false))) *** Solver : Z3 *** Exit code: ExitSuccess FINAL:-({B},{})+({C},{}) DONE!
+ SBVTestSuite/GoldFiles/uninterpreted-1a.gold view
@@ -0,0 +1,53 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic QF_UFBV)+[GOOD] ; --- tuples ---+[GOOD] ; --- sums ---+[GOOD] ; --- literal constants ---+[GOOD] ; --- top level inputs ---+[GOOD] (declare-fun s0 () (_ BitVec 8))+[GOOD] (declare-fun s1 () (_ BitVec 16))+[GOOD] (declare-fun s2 () (_ BitVec 16))+[GOOD] ; --- constant tables ---+[GOOD] ; --- non-constant tables ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] (declare-fun g ((_ BitVec 8) (_ BitVec 16)) (_ BitVec 32))+[GOOD] ; --- user defined functions ---+[GOOD] ; --- assignments ---+[GOOD] (define-fun s3 () Bool (= s1 s2))+[GOOD] (define-fun s4 () (_ BitVec 32) (g s0 s1))+[GOOD] (define-fun s5 () (_ BitVec 32) (g s0 s2))+[GOOD] (define-fun s6 () Bool (= s4 s5))+[GOOD] (define-fun s7 () Bool (=> s3 s6))+[GOOD] ; --- delayedEqualities ---+[GOOD] ; --- formula ---+[GOOD] (assert s7)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 #x00))+[SEND] (get-value (s1))+[RECV] ((s1 #x0000))+[SEND] (get-value (s2))+[RECV] ((s2 #x0000))+[GOOD] (set-option :pp.max_depth 4294967295)+[GOOD] (set-option :pp.min_alias_size 4294967295)+[GOOD] (set-option :model.inline_def true )+[SEND] (get-value (g))+[RECV] ((g ((as const (Array (_ BitVec 8) (_ BitVec 16) (_ BitVec 32))) #x00000000)))+*** Solver : Z3+*** Exit code: ExitSuccess++ FINAL:Satisfiable. Model:+ s0 = 0 :: Int8+ s1 = 0 :: Word16+ s2 = 0 :: Word16++ g :: (Int8, Word16) -> Word32+ g (_, _) = 0+DONE!
SBVTestSuite/SBVTest.hs view
@@ -126,6 +126,7 @@ import qualified TestSuite.Transformers.SymbolicEval import qualified TestSuite.Uninterpreted.AUF import qualified TestSuite.Uninterpreted.Axioms+import qualified TestSuite.Uninterpreted.EUFLogic import qualified TestSuite.Uninterpreted.Function import qualified TestSuite.Uninterpreted.Sort import qualified TestSuite.Uninterpreted.Uninterpreted@@ -248,5 +249,6 @@ , TestSuite.Uninterpreted.Function.tests , TestSuite.Uninterpreted.Sort.tests , TestSuite.Uninterpreted.Uninterpreted.tests+ , TestSuite.Uninterpreted.EUFLogic.tests , sCaseTests ]
+ SBVTestSuite/TestSuite/Uninterpreted/EUFLogic.hs view
@@ -0,0 +1,48 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.Uninterpreted.EUFLogic+-- License : BSD3+-- Stability : experimental+--+-- Test suite for the EUFLogic example+-----------------------------------------------------------------------------++{-# LANGUAGE DataKinds #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module TestSuite.Uninterpreted.EUFLogic where++import Documentation.SBV.Examples.Uninterpreted.EUFLogic++import Utils.SBVTestFramework++-- Test suite+tests :: TestTree+tests =+ testGroup "Uninterpreted.LargeArgs"+ [ testCase "euflogic-1" $ assertIsSat (interpEUF fourteen)+ , testCase "unint17arg" $ assertIsSat f17Args+ ]++fourteen :: EUFExpr Tp_Bool+fourteen = applyOp (Op_BVEq knownBVWidth)+ (applyOp f14 0 0 0 0 0 0 0 0 0 0 0 0 0 0)+ (applyOp (Op_Plus knownBVWidth) a b)+ where+ f14 :: Op '[Tp_BV 8, Tp_BV 8, Tp_BV 8, Tp_BV 8, Tp_BV 8, Tp_BV 8, Tp_BV 8,+ Tp_BV 8, Tp_BV 8, Tp_BV 8, Tp_BV 8, Tp_BV 8, Tp_BV 8, Tp_BV 8]+ (Tp_BV 8)++ f14 = mkUnintOp "f"+ a, b :: EUFExpr (Tp_BV 8)+ a = mkUnintExpr "a"+ b = mkUnintExpr "b"++f17Args :: SWord 1 -> SWord 2 -> SWord 3 -> SWord 4 -> SWord 5 -> SWord 6 -> SWord 7 -> SWord 8+ -> SWord 9 -> SWord 10 -> SWord 11 -> SWord 12 -> SWord 13 -> SWord 14 -> SWord 15 -> SWord 16+ -> SWord 17+ -> SBool+f17Args = uninterpret "f17Args"++{- HLint ignore "Use camelCase" -}
SBVTestSuite/TestSuite/Uninterpreted/Uninterpreted.hs view
@@ -25,6 +25,7 @@ testGroup "Uninterpreted.Uninterpreted" [ testCase "uninterpreted-0" $ assertIsThm p0 , testCase "uninterpreted-1" $ assertIsThm p1+ , goldenCapturedIO "uninterpreted-1a" $ t p1_unc satWith , testCase "uninterpreted-2" $ assertIsntThm p2 , goldenCapturedIO "uninterpreted-3" $ t p3 satWith , goldenCapturedIO "uninterpreted-3a" $ t p3 allSatWith@@ -49,7 +50,15 @@ p2 :: SInt8 -> SWord16 -> SWord16 -> SBool p2 x y z = y .== z .=> g x y .== f x -- Not true +-- | Uncurried version of 'g'+g_unc :: (SInt8, SWord16) -> SWord32+g_unc = uninterpret "g" +-- | Same as 'p1' but using the uncurried version 'g_unc' of 'g'+p1_unc :: SInt8 -> SWord16 -> SWord16 -> SBool+p1_unc x y z = y .== z .=> g_unc (x, y) .== g_unc (x, z) -- OK++ a, b :: SBool a = sym "p" b = sym "q"@@ -63,3 +72,5 @@ p4 :: SBool p4 = c ./= d++{- HLint ignore type g_unc "Use camelCase" -}
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 13.1+Version : 13.2 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT@@ -253,6 +253,7 @@ , Documentation.SBV.Examples.TP.Numeric , Documentation.SBV.Examples.TP.Peano , Documentation.SBV.Examples.TP.PowerMod+ , Documentation.SBV.Examples.TP.Primes , Documentation.SBV.Examples.TP.QuickSort , Documentation.SBV.Examples.TP.RevAcc , Documentation.SBV.Examples.TP.Reverse@@ -266,6 +267,7 @@ , Documentation.SBV.Examples.Transformers.SymbolicEval , Documentation.SBV.Examples.Uninterpreted.AUF , Documentation.SBV.Examples.Uninterpreted.Deduce+ , Documentation.SBV.Examples.Uninterpreted.EUFLogic , Documentation.SBV.Examples.Uninterpreted.Function , Documentation.SBV.Examples.Uninterpreted.Multiply , Documentation.SBV.Examples.Uninterpreted.Shannon@@ -456,6 +458,7 @@ , TestSuite.Uninterpreted.Function , TestSuite.Uninterpreted.Sort , TestSuite.Uninterpreted.Uninterpreted+ , TestSuite.Uninterpreted.EUFLogic , TestSuite.CantTypeCheck.Misc Test-Suite SBVConnections