More tests

SBVTestSuite/GoldFiles/array_misc_1.gold

@@ -0,0 +1,36 @@
+** 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-option :pp.max_depth      4294967295)
+[GOOD] (set-option :pp.min_alias_size 4294967295)
+[GOOD] (set-option :model.inline_def  true      )
+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
+[GOOD] ; --- uninterpreted sorts ---
+[GOOD] ; --- tuples ---
+[GOOD] ; --- sums ---
+[GOOD] ; --- literal constants ---
+[GOOD] (define-fun s1 () (Array Bool Int) (store (store ((as const (Array Bool Int)) 3) false 0) true 1))
+[GOOD] (define-fun s3 () Int 1)
+[GOOD] ; --- top level inputs ---
+[GOOD] (declare-fun s0 () Bool)
+[GOOD] ; --- constant tables ---
+[GOOD] ; --- non-constant tables ---
+[GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- user defined functions ---
+[GOOD] ; --- assignments ---
+[GOOD] (define-fun s2 () Int (select s1 s0))
+[GOOD] (define-fun s4 () Bool (<= s2 s3))
+[GOOD] ; --- delayedEqualities ---
+[GOOD] ; --- formula ---
+[GOOD] (assert (not s4))
+[SEND] (check-sat)
+[RECV] unsat
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+FINAL OUTPUT:
+Q.E.D.

SBVTestSuite/GoldFiles/array_misc_2.gold

@@ -0,0 +1,58 @@
+** 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-option :pp.max_depth      4294967295)
+[GOOD] (set-option :pp.min_alias_size 4294967295)
+[GOOD] (set-option :model.inline_def  true      )
+[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
+[GOOD] ; --- uninterpreted sorts ---
+[GOOD] ; --- tuples ---
+[GOOD] ; --- sums ---
+[GOOD] ; --- literal constants ---
+[GOOD] (define-fun s5 () Int 4)
+[GOOD] (define-fun s8 () Int 5)
+[GOOD] (define-fun s11 () Int 12)
+[GOOD] ; --- top level inputs ---
+[GOOD] (declare-fun s0 () (Array Int Int))
+[GOOD] (declare-fun s1 () Int)
+[GOOD] (declare-fun s2 () Int)
+[GOOD] (declare-fun s3 () Int)
+[GOOD] ; --- constant tables ---
+[GOOD] ; --- non-constant tables ---
+[GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- user defined functions ---
+[GOOD] ; --- assignments ---
+[GOOD] (define-fun s4 () Int (select s0 s1))
+[GOOD] (define-fun s6 () Bool (= s4 s5))
+[GOOD] (define-fun s7 () Int (select s0 s2))
+[GOOD] (define-fun s9 () Bool (= s7 s8))
+[GOOD] (define-fun s10 () Int (select s0 s3))
+[GOOD] (define-fun s12 () Bool (= s10 s11))
+[GOOD] (define-fun s13 () Bool (and s9 s12))
+[GOOD] (define-fun s14 () Bool (and s6 s13))
+[GOOD] ; --- delayedEqualities ---
+[GOOD] ; --- formula ---
+[GOOD] (assert s14)
+[SEND] (check-sat)
+[RECV] sat
+[SEND] (get-value (s0))
+[RECV] ((s0 (store (store ((as const (Array Int Int)) 4) 6 12) 3 5)))
+[SEND] (get-value (s1))
+[RECV] ((s1 2))
+[SEND] (get-value (s2))
+[RECV] ((s2 3))
+[SEND] (get-value (s3))
+[RECV] ((s3 6))
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+FINAL OUTPUT:
+Satisfiable. Model:
+  s0 = ([(3,5),(6,12)], 4) :: Array Integer Integer
+  s1 =                   2 :: Integer
+  s2 =                   3 :: Integer
+  s3 =                   6 :: Integer

SBVTestSuite/TestSuite/Arrays/InitVals.hs

@@ -16,6 +16,7 @@
 
 module TestSuite.Arrays.InitVals(tests) where
 
+import Data.SBV
 import Utils.SBVTestFramework
 
 readDef :: Predicate
@@ -56,16 +57,19 @@ constArr2 = do i :: SInteger <- sInteger "i"
   where myArray = listArray [(1, 12), (2, 5) , (3, 6), (75, 5)] (2 :: Integer)
 
 tests :: TestTree
-tests =
-  testGroup "Arrays.InitVals"
-    [ testCase "readDef_SArray"              $ assertIsThm readDef
-    , testCase "readDef2_SArray2"            $ assertIsSat readNoDef
-    , goldenCapturedIO "constArr_SArray"     t
-    , goldenCapturedIO "constArr2_SArray"    t2
-    ]
-    where t  goldFile = do r <- satWith defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} constArr
-                           appendFile goldFile ("\nFINAL OUTPUT:\n" ++ show r ++ "\n")
-          t2 goldFile = do r <- satWith defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} constArr2
-                           appendFile goldFile ("\nFINAL OUTPUT:\n" ++ show r ++ "\n")
+tests = testGroup "Arrays" [
+    testGroup "Arrays.InitVals"
+      [ testCase "readDef_SArray"           $ assertIsThm readDef
+      , testCase "readDef2_SArray2"         $ assertIsSat readNoDef
+      , goldenCapturedIO "constArr_SArray"  $ t satWith constArr
+      , goldenCapturedIO "constArr2_SArray" $ t satWith constArr2
+      ]
+  , testGroup "Arrays.Misc"
+      [ goldenCapturedIO "array_misc_1" $ t proveWith $ \i -> readArray (listArray [(True,1),(False,0)] 3) i .<= (1::SInteger)
+      , goldenCapturedIO "array_misc_2" $ t satWith   $ \(x :: SArray Integer Integer) i1 i2 i3 -> readArray x i1 .== 4 .&& readArray x i2 .== 5 .&& readArray x i3 .== 12
+      ]
+  ]
+    where t p f goldFile = do r <- p defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} f
+                              appendFile goldFile ("\nFINAL OUTPUT:\n" ++ show r ++ "\n")
 
 {- HLint ignore module "Reduce duplication" -}