-
Notifications
You must be signed in to change notification settings - Fork 32
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Showing
4 changed files
with
84 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,44 @@ | ||
** 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 ALL) ; has unbounded values, using catch-all. | ||
[GOOD] ; --- uninterpreted sorts --- | ||
[GOOD] ; --- tuples --- | ||
[GOOD] ; --- sums --- | ||
[GOOD] ; --- literal constants --- | ||
[GOOD] ; --- top level inputs --- | ||
[GOOD] ; --- constant tables --- | ||
[GOOD] ; --- non-constant tables --- | ||
[GOOD] ; --- arrays --- | ||
[GOOD] (declare-fun array_0 () (Array Int Int)) | ||
[GOOD] ; --- uninterpreted constants --- | ||
[GOOD] ; --- user defined functions --- | ||
[GOOD] ; --- assignments --- | ||
[GOOD] ; --- arrayDelayeds --- | ||
[GOOD] ; --- arraySetups --- | ||
[GOOD] (define-fun array_0_initializer () Bool true) ; no initialization needed | ||
[GOOD] ; --- delayedEqualities --- | ||
[GOOD] ; --- formula --- | ||
[SEND] (check-sat) | ||
[RECV] sat | ||
[GOOD] (define-fun s0 () Int 1) | ||
[GOOD] (define-fun s1 () Int 2) | ||
[GOOD] (declare-fun array_1 () (Array Int Int)) | ||
[GOOD] (define-fun array_1_initializer_0 () Bool (= array_1 (store array_0 s0 s1))) | ||
[GOOD] (define-fun s2 () Int (select array_1 s0)) | ||
[GOOD] (define-fun array_1_initializer () Bool array_1_initializer_0) | ||
[GOOD] (assert array_1_initializer) | ||
[NOTE] getValue: There are outstanding asserts. Ensuring we're still sat. | ||
[SEND] (check-sat) | ||
[RECV] sat | ||
[SEND] (get-value (s2)) | ||
[RECV] ((s2 2)) | ||
*** Solver : Z3 | ||
*** Exit code: ExitSuccess | ||
|
||
FINAL:2 | ||
DONE! |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,37 @@ | ||
----------------------------------------------------------------------------- | ||
-- | | ||
-- Module : TestSuite.Queries.ArrayGetVal | ||
-- Copyright : (c) Levent Erkok | ||
-- License : BSD3 | ||
-- Maintainer: erkokl@gmail.com | ||
-- Stability : experimental | ||
-- | ||
-- Making sure array get-value works, since we might send extra asserts after | ||
-- check-sat. | ||
----------------------------------------------------------------------------- | ||
|
||
{-# LANGUAGE ScopedTypeVariables #-} | ||
|
||
{-# OPTIONS_GHC -Wall -Werror #-} | ||
|
||
module TestSuite.Queries.ArrayGetVal (tests) where | ||
|
||
import Data.SBV.Control | ||
|
||
import Utils.SBVTestFramework | ||
|
||
-- Test suite | ||
tests :: TestTree | ||
tests = | ||
testGroup "Basics.ArrayGetVal" | ||
[ goldenCapturedIO "arrayGetValTest1" testQuery | ||
] | ||
|
||
testQuery :: FilePath -> IO () | ||
testQuery rf = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just rf} t1 | ||
appendFile rf ("\n FINAL:" ++ show r ++ "\nDONE!\n") | ||
|
||
t1 :: Symbolic Integer | ||
t1 = do a :: SArray Integer Integer <- newArray "a" Nothing | ||
query $ do ensureSat | ||
getValue (readArray (writeArray a 1 2) 1) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters