From d40ee8c181bd1f9163390abac848525499b348ed Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 16 Sep 2024 10:28:53 -0700 Subject: [PATCH] simplify --- .../SBV/Examples/Uninterpreted/AUF.hs | 29 +++++++------------ 1 file changed, 11 insertions(+), 18 deletions(-) diff --git a/Documentation/SBV/Examples/Uninterpreted/AUF.hs b/Documentation/SBV/Examples/Uninterpreted/AUF.hs index 273170196..d00cb266e 100644 --- a/Documentation/SBV/Examples/Uninterpreted/AUF.hs +++ b/Documentation/SBV/Examples/Uninterpreted/AUF.hs @@ -6,7 +6,7 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental -- --- Formalizes and proves the following theorem, about arithmetic, +-- Formalizes and proves the following theorem about arithmetic, -- uninterpreted functions, and arrays. (For reference, see -- slide number 24): -- @@ -27,6 +27,7 @@ -- The function @read@ and @write@ are usual array operations. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -35,30 +36,22 @@ module Documentation.SBV.Examples.Uninterpreted.AUF where import Data.SBV --------------------------------------------------------------- --- * Model using functional arrays --------------------------------------------------------------- +#ifndef HADDOCK +-- $setup +-- >>> -- For doctest purposes only: +-- >>> import Data.SBV +#endif -- | Uninterpreted function in the theorem f :: SWord32 -> SWord64 f = uninterpret "f" --- | Correctness theorem. We state it for all values of @x@, @y@, and --- the given array @a@. Note that we're being generic in the type of --- array we're expecting. +-- | Correctness theorem. We state it for all values of @x@, @y@, and the given array @a@. We have: +-- +-- >>> prove thm +-- Q.E.D. thm :: SWord32 -> SWord32 -> SArray Word32 Word32 -> SBool thm x y a = lhs .=> rhs where lhs = x + 2 .== y rhs = f (readArray (writeArray a x 3) (y - 2)) .== f (y - x + 1) - --- | Prove it using SMT-Lib arrays. --- --- >>> proveSArray --- Q.E.D. -proveSArray :: IO ThmResult -proveSArray = prove $ do - x <- free "x" - y <- free "y" - a :: SArray Word32 Word32 <- sArray_ - return $ thm x y a