Skip to content

Commit

Permalink
more tests
Browse files Browse the repository at this point in the history
  • Loading branch information
LeventErkok committed Sep 18, 2024
1 parent d1bc45c commit ed34d0f
Show file tree
Hide file tree
Showing 3 changed files with 87 additions and 0 deletions.
42 changes: 42 additions & 0 deletions SBVTestSuite/GoldFiles/array_misc_11.gold
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
** 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] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
((mkSBVTuple2 (proj_1_SBVTuple2 T1)
(proj_2_SBVTuple2 T2))))))
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () (SBVTuple2 Int Int) (mkSBVTuple2 1 2))
[GOOD] (define-fun s3 () Int 3)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (Array (SBVTuple2 Int Int) Int))
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s2 () Int (select s0 s1))
[GOOD] (define-fun s4 () Bool (= s2 s3))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s4)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 ((as const (Array (SBVTuple2 Int Int) Int)) 3)))
*** Solver : Z3
*** Exit code: ExitSuccess

FINAL OUTPUT:
Satisfiable. Model:
s0 = ([], 3) :: Array (Integer, Integer) Integer
42 changes: 42 additions & 0 deletions SBVTestSuite/GoldFiles/array_misc_12.gold
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
** 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] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
((mkSBVTuple2 (proj_1_SBVTuple2 T1)
(proj_2_SBVTuple2 T2))))))
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () Int 3)
[GOOD] (define-fun s3 () (SBVTuple2 Int Int) (mkSBVTuple2 1 2))
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (Array Int (SBVTuple2 Int Int)))
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s2 () (SBVTuple2 Int Int) (select s0 s1))
[GOOD] (define-fun s4 () Bool (= s2 s3))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s4)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 ((as const (Array Int (SBVTuple2 Int Int))) (mkSBVTuple2 1 2))))
*** Solver : Z3
*** Exit code: ExitSuccess

FINAL OUTPUT:
Satisfiable. Model:
s0 = ([], (1,2)) :: Array Integer (Integer, Integer)
3 changes: 3 additions & 0 deletions SBVTestSuite/TestSuite/Arrays/InitVals.hs
Original file line number Diff line number Diff line change
Expand Up @@ -95,6 +95,9 @@ tests = testGroup "Arrays" [

, testCase "array_misc_10" $ (write (empty 0) [(i, i+1) | i <- [0 .. (3 :: WordN 2)]]
.== write (empty 0) [(i, i ) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "False"

, goldenCapturedIO "array_misc_11" $ t satWith $ \(a :: SArray (Integer, Integer) Integer) -> readArray a (literal (1, 2)) .== 3
, goldenCapturedIO "array_misc_12" $ t satWith $ \(a :: SArray Integer (Integer, Integer)) -> readArray a 3 .== literal (1, 2)
]
]
where t p f goldFile = do r <- p defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} f
Expand Down

0 comments on commit ed34d0f

Please sign in to comment.