Skip to content

Commit

Permalink
more tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@LeventErkok
LeventErkok committed Sep 18, 2024
1 parent fabb37c commit 68263c8
Show file tree
Hide file tree
Showing 5 changed files with 135 additions and 0 deletions.
28 changes: 28 additions & 0 deletions SBVTestSuite/GoldFiles/array_misc_31.gold
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
** 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_BV)
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- top level inputs ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert false)
[SEND] (check-sat)
[RECV] unsat
*** Solver : Z3
*** Exit code: ExitSuccess

FINAL OUTPUT:
Q.E.D.
34 changes: 34 additions & 0 deletions SBVTestSuite/GoldFiles/array_misc_32.gold
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
** 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 s0 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))))
[GOOD] (define-fun s1 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0))))
[GOOD] ; --- top level inputs ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s2 () Bool (= s0 s1))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s2))
[SEND] (check-sat)
[RECV] unsat
*** Solver : Z3
*** Exit code: ExitSuccess

FINAL OUTPUT:
Q.E.D.
34 changes: 34 additions & 0 deletions SBVTestSuite/GoldFiles/array_misc_33.gold
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
** 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 s0 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 1.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))))
[GOOD] (define-fun s1 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0))))
[GOOD] ; --- top level inputs ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s2 () Bool (= s0 s1))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s2))
[SEND] (check-sat)
[RECV] sat
*** Solver : Z3
*** Exit code: ExitSuccess

FINAL OUTPUT:
Falsifiable
34 changes: 34 additions & 0 deletions SBVTestSuite/GoldFiles/array_misc_34.gold
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
** 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 s0 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 1.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))))
[GOOD] (define-fun s1 () (Array Int (_ FloatingPoint 11 53)) (store (store ((as const (Array Int (_ FloatingPoint 11 53))) ((_ to_fp 11 53) roundNearestTiesToEven (/ 5.0 1.0))) 1 ((_ to_fp 11 53) roundNearestTiesToEven (/ 2.0 1.0))) 3 ((_ to_fp 11 53) roundNearestTiesToEven (/ 4.0 1.0))))
[GOOD] ; --- top level inputs ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s2 () Bool (distinct s0 s1))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s2))
[SEND] (check-sat)
[RECV] unsat
*** Solver : Z3
*** Exit code: ExitSuccess

FINAL OUTPUT:
Q.E.D.
5 changes: 5 additions & 0 deletions SBVTestSuite/TestSuite/Arrays/InitVals.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,6 +122,11 @@ tests = testGroup "Arrays" [
, goldenCapturedIO "array_misc_28" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Float Integer) (-1/0))
, goldenCapturedIO "array_misc_29" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Double Integer) (-1/0))
, goldenCapturedIO "array_misc_30" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (-1/0))

, goldenCapturedIO "array_misc_31" $ t proveWith (listArray [(1, 2), (3, 4)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Integer))
, goldenCapturedIO "array_misc_32" $ t proveWith (listArray [(1, 2), (3, 4)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double))
, goldenCapturedIO "array_misc_33" $ t proveWith (listArray [(1, 2), (3, 1)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double))
, goldenCapturedIO "array_misc_34" $ t proveWith (listArray [(1, 2), (3, 1)] 5 ./= listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double))
]
]
where t p f goldFile = do r <- p defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} f
Expand Down

0 comments on commit 68263c8

Please sign in to comment.