From abd3db09ad3089f3adb86514a7a01d0bdd84f106 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Sat, 21 Dec 2024 10:37:48 -0800 Subject: [PATCH 1/9] fix comments --- Data/SBV/String.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Data/SBV/String.hs b/Data/SBV/String.hs index 6af7d75d..1af224d5 100644 --- a/Data/SBV/String.hs +++ b/Data/SBV/String.hs @@ -119,8 +119,7 @@ init s | True = subStr s 0 (length s - 1) --- | @`singleton` c@ is the string of length 1 that contains the only character --- whose value is the 8-bit value @c@. +-- | @`singleton` c@ is the string of length 1 that contains the only character @c@. -- -- >>> prove $ \c -> c .== literal 'A' .=> singleton c .== "A" -- Q.E.D. @@ -141,7 +140,7 @@ singleton = lift1 StrUnit (Just wrap) strToStrAt :: SString -> SInteger -> SString strToStrAt s offset = subStr s offset 1 --- | @`strToCharAt` s i@ is the 8-bit value stored at location @i@. Unspecified if +-- | @`strToCharAt` s i@ is the character stored at location @i@. Unspecified if -- index is out of bounds. -- -- >>> prove $ \i -> i .>= 0 .&& i .<= 4 .=> "AAAAA" `strToCharAt` i .== literal 'A' From 4bc0e1fd34038b979dd2ea8c788d0c9cf54203db Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 23 Dec 2024 08:57:36 -0800 Subject: [PATCH 2/9] pass allow-newer to cabal invocations --- Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index 266cfb1c..3766c306 100644 --- a/Makefile +++ b/Makefile @@ -50,7 +50,7 @@ DOCTESTTIMEOUT = 300 all: quick quick: tags - @$(TIME) cabal new-install --lib --force-reinstalls + @$(TIME) cabal new-install --lib --allow-newer --force-reinstalls install: tags @$(TIME) cabal new-configure --enable-tests --allow-newer --ghc-options=$(CONFIGOPTS) @@ -137,10 +137,10 @@ ifdef TGT ifdef FAST cabal-docspec --timeout ${DOCTESTTIMEOUT} --module $(basename $(subst /,.,${TGT})) else - cabal new-run SBVDocTest -- --timeout ${DOCTESTTIMEOUT} --module $(basename $(subst /,.,${TGT})) + cabal new-run SBVDocTest --allow-newer -- --timeout ${DOCTESTTIMEOUT} --module $(basename $(subst /,.,${TGT})) endif else - @$(TIME) cabal new-run SBVDocTest -- --timeout ${DOCTESTTIMEOUT} + @$(TIME) cabal new-run SBVDocTest --allow-newer -- --timeout ${DOCTESTTIMEOUT} endif test: From 20a0afa992ae262d72b673fe22f0ad790c667945 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 23 Dec 2024 11:49:11 -0800 Subject: [PATCH 3/9] Add and/or to Data.SBV.List --- Data/SBV/List.hs | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs index 8b31cd48..ef153550 100644 --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -41,11 +41,12 @@ module Data.SBV.List ( -- * Filtering , filter -- * Other list functions - , all, any + , all, any, and, or ) where import Prelude hiding (head, tail, init, length, take, drop, concat, null, elem, - notElem, reverse, (++), (!!), map, foldl, foldr, zip, zipWith, filter, all, any) + notElem, reverse, (++), (!!), map, foldl, foldr, zip, zipWith, filter, + all, any, and, or) import qualified Prelude as P import Data.SBV.Core.Kind @@ -579,6 +580,14 @@ any f l registerSpecialFunction st op newExpr st KBool (SBVApp op [sva]) +-- | Conjunction of all the elements. +and :: SList Bool -> SBool +and = all id + +-- | Disjunction of all the elements. +or :: SList Bool -> SBool +or = any id + -- | @filter f xs@ filters the list with the given predicate. -- -- >>> filter (\x -> x `sMod` 2 .== 0) [1 .. 10 :: Integer] From d4e79e626d94736e55e4da751eadafaa0489e066 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 23 Dec 2024 11:49:29 -0800 Subject: [PATCH 4/9] Fix return type in Data.SBV.List.zipWith --- Data/SBV/List.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs index ef153550..79a67ccd 100644 --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -530,7 +530,7 @@ zipWith f xs ys r st = do svxs <- sbvToSV st xs svys <- sbvToSV st ys - lam <- lambdaStr st False kb f + lam <- lambdaStr st False kc f let op = SeqOp (SBVZipWith ka kb kc lam) registerSpecialFunction st op newExpr st kr (SBVApp op [svxs, svys]) From a68c53d5d275a6b96a2fcb0c527ecd37e5580bb3 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 23 Dec 2024 11:50:08 -0800 Subject: [PATCH 5/9] Remove old golds --- SBVTestSuite/GoldFiles/concreteFoldl.gold | 24 --- SBVTestSuite/GoldFiles/concreteFoldr.gold | 24 --- SBVTestSuite/GoldFiles/concreteReverse.gold | 24 --- SBVTestSuite/GoldFiles/concreteSort.gold | 24 --- SBVTestSuite/GoldFiles/foldlABC1.gold | 50 ------ SBVTestSuite/GoldFiles/foldlABC2.gold | 58 ------ SBVTestSuite/GoldFiles/foldlABC3.gold | 65 ------- SBVTestSuite/GoldFiles/foldrAB1.gold | 44 ----- SBVTestSuite/GoldFiles/foldrAB2.gold | 52 ------ SBVTestSuite/GoldFiles/foldrAB3.gold | 59 ------- SBVTestSuite/GoldFiles/mapNoFailure.gold | 157 ----------------- SBVTestSuite/GoldFiles/mapWithFailure.gold | 184 -------------------- SBVTestSuite/GoldFiles/maxlWithFailure.gold | 162 ----------------- SBVTestSuite/GoldFiles/maxrWithFailure.gold | 171 ------------------ SBVTestSuite/GoldFiles/reverse.gold | 123 ------------- SBVTestSuite/GoldFiles/reverseAlt10.gold | 129 -------------- SBVTestSuite/GoldFiles/sort.gold | 169 ------------------ 17 files changed, 1519 deletions(-) delete mode 100644 SBVTestSuite/GoldFiles/concreteFoldl.gold delete mode 100644 SBVTestSuite/GoldFiles/concreteFoldr.gold delete mode 100644 SBVTestSuite/GoldFiles/concreteReverse.gold delete mode 100644 SBVTestSuite/GoldFiles/concreteSort.gold delete mode 100644 SBVTestSuite/GoldFiles/foldlABC1.gold delete mode 100644 SBVTestSuite/GoldFiles/foldlABC2.gold delete mode 100644 SBVTestSuite/GoldFiles/foldlABC3.gold delete mode 100644 SBVTestSuite/GoldFiles/foldrAB1.gold delete mode 100644 SBVTestSuite/GoldFiles/foldrAB2.gold delete mode 100644 SBVTestSuite/GoldFiles/foldrAB3.gold delete mode 100644 SBVTestSuite/GoldFiles/mapNoFailure.gold delete mode 100644 SBVTestSuite/GoldFiles/mapWithFailure.gold delete mode 100644 SBVTestSuite/GoldFiles/maxlWithFailure.gold delete mode 100644 SBVTestSuite/GoldFiles/maxrWithFailure.gold delete mode 100644 SBVTestSuite/GoldFiles/reverse.gold delete mode 100644 SBVTestSuite/GoldFiles/reverseAlt10.gold delete mode 100644 SBVTestSuite/GoldFiles/sort.gold diff --git a/SBVTestSuite/GoldFiles/concreteFoldl.gold b/SBVTestSuite/GoldFiles/concreteFoldl.gold deleted file mode 100644 index c409a37c..00000000 --- a/SBVTestSuite/GoldFiles/concreteFoldl.gold +++ /dev/null @@ -1,24 +0,0 @@ -** 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) ; external query, using all logics. -[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 --- -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/concreteFoldr.gold b/SBVTestSuite/GoldFiles/concreteFoldr.gold deleted file mode 100644 index c409a37c..00000000 --- a/SBVTestSuite/GoldFiles/concreteFoldr.gold +++ /dev/null @@ -1,24 +0,0 @@ -** 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) ; external query, using all logics. -[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 --- -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/concreteReverse.gold b/SBVTestSuite/GoldFiles/concreteReverse.gold deleted file mode 100644 index c409a37c..00000000 --- a/SBVTestSuite/GoldFiles/concreteReverse.gold +++ /dev/null @@ -1,24 +0,0 @@ -** 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) ; external query, using all logics. -[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 --- -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/concreteSort.gold b/SBVTestSuite/GoldFiles/concreteSort.gold deleted file mode 100644 index c409a37c..00000000 --- a/SBVTestSuite/GoldFiles/concreteSort.gold +++ /dev/null @@ -1,24 +0,0 @@ -** 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) ; external query, using all logics. -[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 --- -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldlABC1.gold b/SBVTestSuite/GoldFiles/foldlABC1.gold deleted file mode 100644 index 14334426..00000000 --- a/SBVTestSuite/GoldFiles/foldlABC1.gold +++ /dev/null @@ -1,50 +0,0 @@ -** 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 s3 () Int 0) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" -[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s4 () Bool (> s0 s3)) -[GOOD] (define-fun s5 () Bool (> s1 s3)) -[GOOD] (define-fun s6 () Bool (> s2 s3)) -[GOOD] (define-fun s7 () (Seq Int) (seq.unit s0)) -[GOOD] (define-fun s8 () (Seq Int) (seq.unit s1)) -[GOOD] (define-fun s9 () (Seq Int) (seq.unit s2)) -[GOOD] (define-fun s10 () (Seq Int) (seq.++ s8 s9)) -[GOOD] (define-fun s11 () (Seq Int) (seq.++ s7 s10)) -[GOOD] (define-fun s12 () Int (seq.len s11)) -[GOOD] (define-fun s13 () Bool (= s3 s12)) -[GOOD] (define-fun s14 () Int (seq.nth s11 s3)) -[GOOD] (define-fun s15 () Int (ite s13 s3 s14)) -[GOOD] (define-fun s16 () Int (+ s0 s1)) -[GOOD] (define-fun s17 () Int (+ s2 s16)) -[GOOD] (define-fun s18 () Bool (= s15 s17)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s4) -[GOOD] (assert s5) -[GOOD] (assert s6) -[GOOD] (assert s18) -[SEND] (check-sat) -[RECV] unsat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldlABC2.gold b/SBVTestSuite/GoldFiles/foldlABC2.gold deleted file mode 100644 index 878a5daa..00000000 --- a/SBVTestSuite/GoldFiles/foldlABC2.gold +++ /dev/null @@ -1,58 +0,0 @@ -** 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 s3 () Int 0) -[GOOD] (define-fun s15 () Int 1) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" -[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s4 () Bool (> s0 s3)) -[GOOD] (define-fun s5 () Bool (> s1 s3)) -[GOOD] (define-fun s6 () Bool (> s2 s3)) -[GOOD] (define-fun s7 () (Seq Int) (seq.unit s0)) -[GOOD] (define-fun s8 () (Seq Int) (seq.unit s1)) -[GOOD] (define-fun s9 () (Seq Int) (seq.unit s2)) -[GOOD] (define-fun s10 () (Seq Int) (seq.++ s8 s9)) -[GOOD] (define-fun s11 () (Seq Int) (seq.++ s7 s10)) -[GOOD] (define-fun s12 () Int (seq.len s11)) -[GOOD] (define-fun s13 () Bool (= s3 s12)) -[GOOD] (define-fun s14 () Int (seq.nth s11 s3)) -[GOOD] (define-fun s16 () Int (- s12 s15)) -[GOOD] (define-fun s17 () (Seq Int) (seq.extract s11 s15 s16)) -[GOOD] (define-fun s18 () Int (seq.len s17)) -[GOOD] (define-fun s19 () Bool (= s3 s18)) -[GOOD] (define-fun s20 () Int (seq.nth s17 s3)) -[GOOD] (define-fun s21 () Int (ite s19 s3 s20)) -[GOOD] (define-fun s22 () Int (+ s14 s21)) -[GOOD] (define-fun s23 () Int (ite s13 s3 s22)) -[GOOD] (define-fun s24 () Int (+ s0 s1)) -[GOOD] (define-fun s25 () Int (+ s2 s24)) -[GOOD] (define-fun s26 () Bool (= s23 s25)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s4) -[GOOD] (assert s5) -[GOOD] (assert s6) -[GOOD] (assert s26) -[SEND] (check-sat) -[RECV] unsat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldlABC3.gold b/SBVTestSuite/GoldFiles/foldlABC3.gold deleted file mode 100644 index 6570ca0c..00000000 --- a/SBVTestSuite/GoldFiles/foldlABC3.gold +++ /dev/null @@ -1,65 +0,0 @@ -** 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 s3 () Int 0) -[GOOD] (define-fun s15 () Int 1) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" -[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s4 () Bool (> s0 s3)) -[GOOD] (define-fun s5 () Bool (> s1 s3)) -[GOOD] (define-fun s6 () Bool (> s2 s3)) -[GOOD] (define-fun s7 () (Seq Int) (seq.unit s0)) -[GOOD] (define-fun s8 () (Seq Int) (seq.unit s1)) -[GOOD] (define-fun s9 () (Seq Int) (seq.unit s2)) -[GOOD] (define-fun s10 () (Seq Int) (seq.++ s8 s9)) -[GOOD] (define-fun s11 () (Seq Int) (seq.++ s7 s10)) -[GOOD] (define-fun s12 () Int (seq.len s11)) -[GOOD] (define-fun s13 () Bool (= s3 s12)) -[GOOD] (define-fun s14 () Int (seq.nth s11 s3)) -[GOOD] (define-fun s16 () Int (- s12 s15)) -[GOOD] (define-fun s17 () (Seq Int) (seq.extract s11 s15 s16)) -[GOOD] (define-fun s18 () Int (seq.len s17)) -[GOOD] (define-fun s19 () Bool (= s3 s18)) -[GOOD] (define-fun s20 () Int (seq.nth s17 s3)) -[GOOD] (define-fun s21 () Int (- s18 s15)) -[GOOD] (define-fun s22 () (Seq Int) (seq.extract s17 s15 s21)) -[GOOD] (define-fun s23 () Int (seq.len s22)) -[GOOD] (define-fun s24 () Bool (= s3 s23)) -[GOOD] (define-fun s25 () Int (seq.nth s22 s3)) -[GOOD] (define-fun s26 () Int (ite s24 s3 s25)) -[GOOD] (define-fun s27 () Int (+ s20 s26)) -[GOOD] (define-fun s28 () Int (ite s19 s3 s27)) -[GOOD] (define-fun s29 () Int (+ s14 s28)) -[GOOD] (define-fun s30 () Int (ite s13 s3 s29)) -[GOOD] (define-fun s31 () Int (+ s0 s1)) -[GOOD] (define-fun s32 () Int (+ s2 s31)) -[GOOD] (define-fun s33 () Bool (= s30 s32)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s4) -[GOOD] (assert s5) -[GOOD] (assert s6) -[GOOD] (assert s33) -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldrAB1.gold b/SBVTestSuite/GoldFiles/foldrAB1.gold deleted file mode 100644 index 35faed41..00000000 --- a/SBVTestSuite/GoldFiles/foldrAB1.gold +++ /dev/null @@ -1,44 +0,0 @@ -** 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 s2 () Int 0) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" -[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s3 () Bool (> s0 s2)) -[GOOD] (define-fun s4 () Bool (> s1 s2)) -[GOOD] (define-fun s5 () (Seq Int) (seq.unit s0)) -[GOOD] (define-fun s6 () (Seq Int) (seq.unit s1)) -[GOOD] (define-fun s7 () (Seq Int) (seq.++ s5 s6)) -[GOOD] (define-fun s8 () Int (seq.len s7)) -[GOOD] (define-fun s9 () Bool (= s2 s8)) -[GOOD] (define-fun s10 () Int (seq.nth s7 s2)) -[GOOD] (define-fun s11 () Int (ite s9 s2 s10)) -[GOOD] (define-fun s12 () Int (+ s0 s1)) -[GOOD] (define-fun s13 () Bool (= s11 s12)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s3) -[GOOD] (assert s4) -[GOOD] (assert s13) -[SEND] (check-sat) -[RECV] unsat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldrAB2.gold b/SBVTestSuite/GoldFiles/foldrAB2.gold deleted file mode 100644 index 3053c047..00000000 --- a/SBVTestSuite/GoldFiles/foldrAB2.gold +++ /dev/null @@ -1,52 +0,0 @@ -** 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 s2 () Int 0) -[GOOD] (define-fun s11 () Int 1) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" -[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s3 () Bool (> s0 s2)) -[GOOD] (define-fun s4 () Bool (> s1 s2)) -[GOOD] (define-fun s5 () (Seq Int) (seq.unit s0)) -[GOOD] (define-fun s6 () (Seq Int) (seq.unit s1)) -[GOOD] (define-fun s7 () (Seq Int) (seq.++ s5 s6)) -[GOOD] (define-fun s8 () Int (seq.len s7)) -[GOOD] (define-fun s9 () Bool (= s2 s8)) -[GOOD] (define-fun s10 () Int (seq.nth s7 s2)) -[GOOD] (define-fun s12 () Int (- s8 s11)) -[GOOD] (define-fun s13 () (Seq Int) (seq.extract s7 s11 s12)) -[GOOD] (define-fun s14 () Int (seq.len s13)) -[GOOD] (define-fun s15 () Bool (= s2 s14)) -[GOOD] (define-fun s16 () Int (seq.nth s13 s2)) -[GOOD] (define-fun s17 () Int (ite s15 s2 s16)) -[GOOD] (define-fun s18 () Int (+ s10 s17)) -[GOOD] (define-fun s19 () Int (ite s9 s2 s18)) -[GOOD] (define-fun s20 () Int (+ s0 s1)) -[GOOD] (define-fun s21 () Bool (= s19 s20)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s3) -[GOOD] (assert s4) -[GOOD] (assert s21) -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/foldrAB3.gold b/SBVTestSuite/GoldFiles/foldrAB3.gold deleted file mode 100644 index 75d23891..00000000 --- a/SBVTestSuite/GoldFiles/foldrAB3.gold +++ /dev/null @@ -1,59 +0,0 @@ -** 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 s2 () Int 0) -[GOOD] (define-fun s11 () Int 1) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" -[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s3 () Bool (> s0 s2)) -[GOOD] (define-fun s4 () Bool (> s1 s2)) -[GOOD] (define-fun s5 () (Seq Int) (seq.unit s0)) -[GOOD] (define-fun s6 () (Seq Int) (seq.unit s1)) -[GOOD] (define-fun s7 () (Seq Int) (seq.++ s5 s6)) -[GOOD] (define-fun s8 () Int (seq.len s7)) -[GOOD] (define-fun s9 () Bool (= s2 s8)) -[GOOD] (define-fun s10 () Int (seq.nth s7 s2)) -[GOOD] (define-fun s12 () Int (- s8 s11)) -[GOOD] (define-fun s13 () (Seq Int) (seq.extract s7 s11 s12)) -[GOOD] (define-fun s14 () Int (seq.len s13)) -[GOOD] (define-fun s15 () Bool (= s2 s14)) -[GOOD] (define-fun s16 () Int (seq.nth s13 s2)) -[GOOD] (define-fun s17 () Int (- s14 s11)) -[GOOD] (define-fun s18 () (Seq Int) (seq.extract s13 s11 s17)) -[GOOD] (define-fun s19 () Int (seq.len s18)) -[GOOD] (define-fun s20 () Bool (= s2 s19)) -[GOOD] (define-fun s21 () Int (seq.nth s18 s2)) -[GOOD] (define-fun s22 () Int (ite s20 s2 s21)) -[GOOD] (define-fun s23 () Int (+ s16 s22)) -[GOOD] (define-fun s24 () Int (ite s15 s2 s23)) -[GOOD] (define-fun s25 () Int (+ s10 s24)) -[GOOD] (define-fun s26 () Int (ite s9 s2 s25)) -[GOOD] (define-fun s27 () Int (+ s0 s1)) -[GOOD] (define-fun s28 () Bool (= s26 s27)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s3) -[GOOD] (assert s4) -[GOOD] (assert s28) -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/mapNoFailure.gold b/SBVTestSuite/GoldFiles/mapNoFailure.gold deleted file mode 100644 index 023b3f63..00000000 --- a/SBVTestSuite/GoldFiles/mapNoFailure.gold +++ /dev/null @@ -1,157 +0,0 @@ -** 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 6) -[GOOD] (define-fun s7 () Int 0) -[GOOD] (define-fun s20 () Int 1) -[GOOD] (define-fun s59 () Int 10) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" -[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s3 () Int (+ s0 s1)) -[GOOD] (define-fun s4 () Int (+ s2 s3)) -[GOOD] (define-fun s6 () Bool (= s4 s5)) -[GOOD] (define-fun s8 () Bool (> s0 s7)) -[GOOD] (define-fun s9 () Bool (> s1 s7)) -[GOOD] (define-fun s10 () Bool (> s2 s7)) -[GOOD] (define-fun s11 () Bool (and s9 s10)) -[GOOD] (define-fun s12 () Bool (and s8 s11)) -[GOOD] (define-fun s13 () (Seq Int) (seq.unit s0)) -[GOOD] (define-fun s14 () (Seq Int) (seq.unit s1)) -[GOOD] (define-fun s15 () (Seq Int) (seq.unit s2)) -[GOOD] (define-fun s16 () (Seq Int) (seq.++ s14 s15)) -[GOOD] (define-fun s17 () (Seq Int) (seq.++ s13 s16)) -[GOOD] (define-fun s18 () Int (seq.len s17)) -[GOOD] (define-fun s19 () Bool (= s7 s18)) -[GOOD] (define-fun s21 () Int (- s18 s20)) -[GOOD] (define-fun s22 () (Seq Int) (seq.extract s17 s20 s21)) -[GOOD] (define-fun s23 () Int (seq.len s22)) -[GOOD] (define-fun s24 () Bool (= s7 s23)) -[GOOD] (define-fun s25 () Int (- s23 s20)) -[GOOD] (define-fun s26 () (Seq Int) (seq.extract s22 s20 s25)) -[GOOD] (define-fun s27 () Int (seq.len s26)) -[GOOD] (define-fun s28 () Bool (= s7 s27)) -[GOOD] (define-fun s29 () Int (- s27 s20)) -[GOOD] (define-fun s30 () (Seq Int) (seq.extract s26 s20 s29)) -[GOOD] (define-fun s31 () Int (seq.len s30)) -[GOOD] (define-fun s32 () Bool (= s7 s31)) -[GOOD] (define-fun s33 () Int (- s31 s20)) -[GOOD] (define-fun s34 () (Seq Int) (seq.extract s30 s20 s33)) -[GOOD] (define-fun s35 () Int (seq.len s34)) -[GOOD] (define-fun s36 () Bool (= s7 s35)) -[GOOD] (define-fun s37 () Int (- s35 s20)) -[GOOD] (define-fun s38 () (Seq Int) (seq.extract s34 s20 s37)) -[GOOD] (define-fun s39 () Int (seq.len s38)) -[GOOD] (define-fun s40 () Bool (= s7 s39)) -[GOOD] (define-fun s41 () Int (- s39 s20)) -[GOOD] (define-fun s42 () (Seq Int) (seq.extract s38 s20 s41)) -[GOOD] (define-fun s43 () Int (seq.len s42)) -[GOOD] (define-fun s44 () Bool (= s7 s43)) -[GOOD] (define-fun s45 () Int (- s43 s20)) -[GOOD] (define-fun s46 () (Seq Int) (seq.extract s42 s20 s45)) -[GOOD] (define-fun s47 () Int (seq.len s46)) -[GOOD] (define-fun s48 () Bool (= s7 s47)) -[GOOD] (define-fun s49 () Int (- s47 s20)) -[GOOD] (define-fun s50 () (Seq Int) (seq.extract s46 s20 s49)) -[GOOD] (define-fun s51 () Int (seq.len s50)) -[GOOD] (define-fun s52 () Bool (= s7 s51)) -[GOOD] (define-fun s53 () Int (- s51 s20)) -[GOOD] (define-fun s54 () (Seq Int) (seq.extract s50 s20 s53)) -[GOOD] (define-fun s55 () Int (seq.len s54)) -[GOOD] (define-fun s56 () Bool (= s7 s55)) -[GOOD] (define-fun s57 () Int (seq.nth s54 s7)) -[GOOD] (define-fun s58 () Bool (< s57 s7)) -[GOOD] (define-fun s60 () Bool (> s57 s59)) -[GOOD] (define-fun s61 () Bool (or s58 s60)) -[GOOD] (define-fun s62 () Bool (not s56)) -[GOOD] (define-fun s63 () Bool (and s61 s62)) -[GOOD] (define-fun s64 () Int (seq.nth s50 s7)) -[GOOD] (define-fun s65 () Bool (< s64 s7)) -[GOOD] (define-fun s66 () Bool (> s64 s59)) -[GOOD] (define-fun s67 () Bool (or s65 s66)) -[GOOD] (define-fun s68 () Bool (or s63 s67)) -[GOOD] (define-fun s69 () Bool (not s52)) -[GOOD] (define-fun s70 () Bool (and s68 s69)) -[GOOD] (define-fun s71 () Int (seq.nth s46 s7)) -[GOOD] (define-fun s72 () Bool (< s71 s7)) -[GOOD] (define-fun s73 () Bool (> s71 s59)) -[GOOD] (define-fun s74 () Bool (or s72 s73)) -[GOOD] (define-fun s75 () Bool (or s70 s74)) -[GOOD] (define-fun s76 () Bool (not s48)) -[GOOD] (define-fun s77 () Bool (and s75 s76)) -[GOOD] (define-fun s78 () Int (seq.nth s42 s7)) -[GOOD] (define-fun s79 () Bool (< s78 s7)) -[GOOD] (define-fun s80 () Bool (> s78 s59)) -[GOOD] (define-fun s81 () Bool (or s79 s80)) -[GOOD] (define-fun s82 () Bool (or s77 s81)) -[GOOD] (define-fun s83 () Bool (not s44)) -[GOOD] (define-fun s84 () Bool (and s82 s83)) -[GOOD] (define-fun s85 () Int (seq.nth s38 s7)) -[GOOD] (define-fun s86 () Bool (< s85 s7)) -[GOOD] (define-fun s87 () Bool (> s85 s59)) -[GOOD] (define-fun s88 () Bool (or s86 s87)) -[GOOD] (define-fun s89 () Bool (or s84 s88)) -[GOOD] (define-fun s90 () Bool (not s40)) -[GOOD] (define-fun s91 () Bool (and s89 s90)) -[GOOD] (define-fun s92 () Int (seq.nth s34 s7)) -[GOOD] (define-fun s93 () Bool (< s92 s7)) -[GOOD] (define-fun s94 () Bool (> s92 s59)) -[GOOD] (define-fun s95 () Bool (or s93 s94)) -[GOOD] (define-fun s96 () Bool (or s91 s95)) -[GOOD] (define-fun s97 () Bool (not s36)) -[GOOD] (define-fun s98 () Bool (and s96 s97)) -[GOOD] (define-fun s99 () Int (seq.nth s30 s7)) -[GOOD] (define-fun s100 () Bool (< s99 s7)) -[GOOD] (define-fun s101 () Bool (> s99 s59)) -[GOOD] (define-fun s102 () Bool (or s100 s101)) -[GOOD] (define-fun s103 () Bool (or s98 s102)) -[GOOD] (define-fun s104 () Bool (not s32)) -[GOOD] (define-fun s105 () Bool (and s103 s104)) -[GOOD] (define-fun s106 () Int (seq.nth s26 s7)) -[GOOD] (define-fun s107 () Bool (< s106 s7)) -[GOOD] (define-fun s108 () Bool (> s106 s59)) -[GOOD] (define-fun s109 () Bool (or s107 s108)) -[GOOD] (define-fun s110 () Bool (or s105 s109)) -[GOOD] (define-fun s111 () Bool (not s28)) -[GOOD] (define-fun s112 () Bool (and s110 s111)) -[GOOD] (define-fun s113 () Int (seq.nth s22 s7)) -[GOOD] (define-fun s114 () Bool (< s113 s7)) -[GOOD] (define-fun s115 () Bool (> s113 s59)) -[GOOD] (define-fun s116 () Bool (or s114 s115)) -[GOOD] (define-fun s117 () Bool (or s112 s116)) -[GOOD] (define-fun s118 () Bool (not s24)) -[GOOD] (define-fun s119 () Bool (and s117 s118)) -[GOOD] (define-fun s120 () Int (seq.nth s17 s7)) -[GOOD] (define-fun s121 () Bool (< s120 s7)) -[GOOD] (define-fun s122 () Bool (> s120 s59)) -[GOOD] (define-fun s123 () Bool (or s121 s122)) -[GOOD] (define-fun s124 () Bool (or s119 s123)) -[GOOD] (define-fun s125 () Bool (not s19)) -[GOOD] (define-fun s126 () Bool (and s124 s125)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s6) -[GOOD] (assert s12) -[GOOD] (assert s126) -[SEND] (check-sat) -[RECV] unsat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/mapWithFailure.gold b/SBVTestSuite/GoldFiles/mapWithFailure.gold deleted file mode 100644 index 8274d9af..00000000 --- a/SBVTestSuite/GoldFiles/mapWithFailure.gold +++ /dev/null @@ -1,184 +0,0 @@ -** 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 s2 () Int 0) -[GOOD] (define-fun s4 () (Seq Int) (as seq.empty (Seq Int))) -[GOOD] (define-fun s6 () Int 1) -[GOOD] (define-fun s91 () Int 2) -[GOOD] (define-fun s93 () Int 11) -[GOOD] (define-fun s96 () Int 10) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "ints" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s1 () Int (seq.len s0)) -[GOOD] (define-fun s3 () Bool (= s1 s2)) -[GOOD] (define-fun s5 () Int (seq.nth s0 s2)) -[GOOD] (define-fun s7 () Int (+ s5 s6)) -[GOOD] (define-fun s8 () (Seq Int) (seq.unit s7)) -[GOOD] (define-fun s9 () Int (- s1 s6)) -[GOOD] (define-fun s10 () (Seq Int) (seq.extract s0 s6 s9)) -[GOOD] (define-fun s11 () Int (seq.len s10)) -[GOOD] (define-fun s12 () Bool (= s2 s11)) -[GOOD] (define-fun s13 () Int (seq.nth s10 s2)) -[GOOD] (define-fun s14 () Int (+ s6 s13)) -[GOOD] (define-fun s15 () (Seq Int) (seq.unit s14)) -[GOOD] (define-fun s16 () Int (- s11 s6)) -[GOOD] (define-fun s17 () (Seq Int) (seq.extract s10 s6 s16)) -[GOOD] (define-fun s18 () Int (seq.len s17)) -[GOOD] (define-fun s19 () Bool (= s2 s18)) -[GOOD] (define-fun s20 () Int (seq.nth s17 s2)) -[GOOD] (define-fun s21 () Int (+ s6 s20)) -[GOOD] (define-fun s22 () (Seq Int) (seq.unit s21)) -[GOOD] (define-fun s23 () Int (- s18 s6)) -[GOOD] (define-fun s24 () (Seq Int) (seq.extract s17 s6 s23)) -[GOOD] (define-fun s25 () Int (seq.len s24)) -[GOOD] (define-fun s26 () Bool (= s2 s25)) -[GOOD] (define-fun s27 () Int (seq.nth s24 s2)) -[GOOD] (define-fun s28 () Int (+ s6 s27)) -[GOOD] (define-fun s29 () (Seq Int) (seq.unit s28)) -[GOOD] (define-fun s30 () Int (- s25 s6)) -[GOOD] (define-fun s31 () (Seq Int) (seq.extract s24 s6 s30)) -[GOOD] (define-fun s32 () Int (seq.len s31)) -[GOOD] (define-fun s33 () Bool (= s2 s32)) -[GOOD] (define-fun s34 () Int (seq.nth s31 s2)) -[GOOD] (define-fun s35 () Int (+ s6 s34)) -[GOOD] (define-fun s36 () (Seq Int) (seq.unit s35)) -[GOOD] (define-fun s37 () Int (- s32 s6)) -[GOOD] (define-fun s38 () (Seq Int) (seq.extract s31 s6 s37)) -[GOOD] (define-fun s39 () Int (seq.len s38)) -[GOOD] (define-fun s40 () Bool (= s2 s39)) -[GOOD] (define-fun s41 () Int (seq.nth s38 s2)) -[GOOD] (define-fun s42 () Int (+ s6 s41)) -[GOOD] (define-fun s43 () (Seq Int) (seq.unit s42)) -[GOOD] (define-fun s44 () Int (- s39 s6)) -[GOOD] (define-fun s45 () (Seq Int) (seq.extract s38 s6 s44)) -[GOOD] (define-fun s46 () Int (seq.len s45)) -[GOOD] (define-fun s47 () Bool (= s2 s46)) -[GOOD] (define-fun s48 () Int (seq.nth s45 s2)) -[GOOD] (define-fun s49 () Int (+ s6 s48)) -[GOOD] (define-fun s50 () (Seq Int) (seq.unit s49)) -[GOOD] (define-fun s51 () Int (- s46 s6)) -[GOOD] (define-fun s52 () (Seq Int) (seq.extract s45 s6 s51)) -[GOOD] (define-fun s53 () Int (seq.len s52)) -[GOOD] (define-fun s54 () Bool (= s2 s53)) -[GOOD] (define-fun s55 () Int (seq.nth s52 s2)) -[GOOD] (define-fun s56 () Int (+ s6 s55)) -[GOOD] (define-fun s57 () (Seq Int) (seq.unit s56)) -[GOOD] (define-fun s58 () Int (- s53 s6)) -[GOOD] (define-fun s59 () (Seq Int) (seq.extract s52 s6 s58)) -[GOOD] (define-fun s60 () Int (seq.len s59)) -[GOOD] (define-fun s61 () Bool (= s2 s60)) -[GOOD] (define-fun s62 () Int (seq.nth s59 s2)) -[GOOD] (define-fun s63 () Int (+ s6 s62)) -[GOOD] (define-fun s64 () (Seq Int) (seq.unit s63)) -[GOOD] (define-fun s65 () Int (- s60 s6)) -[GOOD] (define-fun s66 () (Seq Int) (seq.extract s59 s6 s65)) -[GOOD] (define-fun s67 () Int (seq.len s66)) -[GOOD] (define-fun s68 () Bool (= s2 s67)) -[GOOD] (define-fun s69 () Int (seq.nth s66 s2)) -[GOOD] (define-fun s70 () Int (+ s6 s69)) -[GOOD] (define-fun s71 () (Seq Int) (seq.unit s70)) -[GOOD] (define-fun s72 () (Seq Int) (ite s68 s4 s71)) -[GOOD] (define-fun s73 () (Seq Int) (seq.++ s64 s72)) -[GOOD] (define-fun s74 () (Seq Int) (ite s61 s4 s73)) -[GOOD] (define-fun s75 () (Seq Int) (seq.++ s57 s74)) -[GOOD] (define-fun s76 () (Seq Int) (ite s54 s4 s75)) -[GOOD] (define-fun s77 () (Seq Int) (seq.++ s50 s76)) -[GOOD] (define-fun s78 () (Seq Int) (ite s47 s4 s77)) -[GOOD] (define-fun s79 () (Seq Int) (seq.++ s43 s78)) -[GOOD] (define-fun s80 () (Seq Int) (ite s40 s4 s79)) -[GOOD] (define-fun s81 () (Seq Int) (seq.++ s36 s80)) -[GOOD] (define-fun s82 () (Seq Int) (ite s33 s4 s81)) -[GOOD] (define-fun s83 () (Seq Int) (seq.++ s29 s82)) -[GOOD] (define-fun s84 () (Seq Int) (ite s26 s4 s83)) -[GOOD] (define-fun s85 () (Seq Int) (seq.++ s22 s84)) -[GOOD] (define-fun s86 () (Seq Int) (ite s19 s4 s85)) -[GOOD] (define-fun s87 () (Seq Int) (seq.++ s15 s86)) -[GOOD] (define-fun s88 () (Seq Int) (ite s12 s4 s87)) -[GOOD] (define-fun s89 () (Seq Int) (seq.++ s8 s88)) -[GOOD] (define-fun s90 () (Seq Int) (ite s3 s4 s89)) -[GOOD] (define-fun s92 () Int (seq.nth s90 s91)) -[GOOD] (define-fun s94 () Bool (> s92 s93)) -[GOOD] (define-fun s95 () Bool (< s69 s2)) -[GOOD] (define-fun s97 () Bool (> s69 s96)) -[GOOD] (define-fun s98 () Bool (or s95 s97)) -[GOOD] (define-fun s99 () Bool (not s68)) -[GOOD] (define-fun s100 () Bool (and s98 s99)) -[GOOD] (define-fun s101 () Bool (< s62 s2)) -[GOOD] (define-fun s102 () Bool (> s62 s96)) -[GOOD] (define-fun s103 () Bool (or s101 s102)) -[GOOD] (define-fun s104 () Bool (or s100 s103)) -[GOOD] (define-fun s105 () Bool (not s61)) -[GOOD] (define-fun s106 () Bool (and s104 s105)) -[GOOD] (define-fun s107 () Bool (< s55 s2)) -[GOOD] (define-fun s108 () Bool (> s55 s96)) -[GOOD] (define-fun s109 () Bool (or s107 s108)) -[GOOD] (define-fun s110 () Bool (or s106 s109)) -[GOOD] (define-fun s111 () Bool (not s54)) -[GOOD] (define-fun s112 () Bool (and s110 s111)) -[GOOD] (define-fun s113 () Bool (< s48 s2)) -[GOOD] (define-fun s114 () Bool (> s48 s96)) -[GOOD] (define-fun s115 () Bool (or s113 s114)) -[GOOD] (define-fun s116 () Bool (or s112 s115)) -[GOOD] (define-fun s117 () Bool (not s47)) -[GOOD] (define-fun s118 () Bool (and s116 s117)) -[GOOD] (define-fun s119 () Bool (< s41 s2)) -[GOOD] (define-fun s120 () Bool (> s41 s96)) -[GOOD] (define-fun s121 () Bool (or s119 s120)) -[GOOD] (define-fun s122 () Bool (or s118 s121)) -[GOOD] (define-fun s123 () Bool (not s40)) -[GOOD] (define-fun s124 () Bool (and s122 s123)) -[GOOD] (define-fun s125 () Bool (< s34 s2)) -[GOOD] (define-fun s126 () Bool (> s34 s96)) -[GOOD] (define-fun s127 () Bool (or s125 s126)) -[GOOD] (define-fun s128 () Bool (or s124 s127)) -[GOOD] (define-fun s129 () Bool (not s33)) -[GOOD] (define-fun s130 () Bool (and s128 s129)) -[GOOD] (define-fun s131 () Bool (< s27 s2)) -[GOOD] (define-fun s132 () Bool (> s27 s96)) -[GOOD] (define-fun s133 () Bool (or s131 s132)) -[GOOD] (define-fun s134 () Bool (or s130 s133)) -[GOOD] (define-fun s135 () Bool (not s26)) -[GOOD] (define-fun s136 () Bool (and s134 s135)) -[GOOD] (define-fun s137 () Bool (< s20 s2)) -[GOOD] (define-fun s138 () Bool (> s20 s96)) -[GOOD] (define-fun s139 () Bool (or s137 s138)) -[GOOD] (define-fun s140 () Bool (or s136 s139)) -[GOOD] (define-fun s141 () Bool (not s19)) -[GOOD] (define-fun s142 () Bool (and s140 s141)) -[GOOD] (define-fun s143 () Bool (< s13 s2)) -[GOOD] (define-fun s144 () Bool (> s13 s96)) -[GOOD] (define-fun s145 () Bool (or s143 s144)) -[GOOD] (define-fun s146 () Bool (or s142 s145)) -[GOOD] (define-fun s147 () Bool (not s12)) -[GOOD] (define-fun s148 () Bool (and s146 s147)) -[GOOD] (define-fun s149 () Bool (< s5 s2)) -[GOOD] (define-fun s150 () Bool (> s5 s96)) -[GOOD] (define-fun s151 () Bool (or s149 s150)) -[GOOD] (define-fun s152 () Bool (or s148 s151)) -[GOOD] (define-fun s153 () Bool (not s3)) -[GOOD] (define-fun s154 () Bool (and s152 s153)) -[GOOD] (define-fun s155 () Bool (=> s94 s154)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s155) -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/maxlWithFailure.gold b/SBVTestSuite/GoldFiles/maxlWithFailure.gold deleted file mode 100644 index e84bb621..00000000 --- a/SBVTestSuite/GoldFiles/maxlWithFailure.gold +++ /dev/null @@ -1,162 +0,0 @@ -** 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 s2 () Int 0) -[GOOD] (define-fun s4 () Int 1) -[GOOD] (define-fun s81 () Int 10) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "ints" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s1 () Int (seq.len s0)) -[GOOD] (define-fun s3 () Bool (= s1 s2)) -[GOOD] (define-fun s5 () Int (- s1 s4)) -[GOOD] (define-fun s6 () (Seq Int) (seq.extract s0 s4 s5)) -[GOOD] (define-fun s7 () Int (seq.len s6)) -[GOOD] (define-fun s8 () Bool (= s2 s7)) -[GOOD] (define-fun s9 () Int (seq.nth s0 s2)) -[GOOD] (define-fun s10 () Bool (<= s9 s2)) -[GOOD] (define-fun s11 () Int (ite s10 s2 s9)) -[GOOD] (define-fun s12 () Int (- s7 s4)) -[GOOD] (define-fun s13 () (Seq Int) (seq.extract s6 s4 s12)) -[GOOD] (define-fun s14 () Int (seq.len s13)) -[GOOD] (define-fun s15 () Bool (= s2 s14)) -[GOOD] (define-fun s16 () Int (seq.nth s6 s2)) -[GOOD] (define-fun s17 () Bool (<= s16 s11)) -[GOOD] (define-fun s18 () Int (ite s17 s11 s16)) -[GOOD] (define-fun s19 () Int (- s14 s4)) -[GOOD] (define-fun s20 () (Seq Int) (seq.extract s13 s4 s19)) -[GOOD] (define-fun s21 () Int (seq.len s20)) -[GOOD] (define-fun s22 () Bool (= s2 s21)) -[GOOD] (define-fun s23 () Int (seq.nth s13 s2)) -[GOOD] (define-fun s24 () Bool (<= s23 s18)) -[GOOD] (define-fun s25 () Int (ite s24 s18 s23)) -[GOOD] (define-fun s26 () Int (- s21 s4)) -[GOOD] (define-fun s27 () (Seq Int) (seq.extract s20 s4 s26)) -[GOOD] (define-fun s28 () Int (seq.len s27)) -[GOOD] (define-fun s29 () Bool (= s2 s28)) -[GOOD] (define-fun s30 () Int (seq.nth s20 s2)) -[GOOD] (define-fun s31 () Bool (<= s30 s25)) -[GOOD] (define-fun s32 () Int (ite s31 s25 s30)) -[GOOD] (define-fun s33 () Int (- s28 s4)) -[GOOD] (define-fun s34 () (Seq Int) (seq.extract s27 s4 s33)) -[GOOD] (define-fun s35 () Int (seq.len s34)) -[GOOD] (define-fun s36 () Bool (= s2 s35)) -[GOOD] (define-fun s37 () Int (seq.nth s27 s2)) -[GOOD] (define-fun s38 () Bool (<= s37 s32)) -[GOOD] (define-fun s39 () Int (ite s38 s32 s37)) -[GOOD] (define-fun s40 () Int (- s35 s4)) -[GOOD] (define-fun s41 () (Seq Int) (seq.extract s34 s4 s40)) -[GOOD] (define-fun s42 () Int (seq.len s41)) -[GOOD] (define-fun s43 () Bool (= s2 s42)) -[GOOD] (define-fun s44 () Int (seq.nth s34 s2)) -[GOOD] (define-fun s45 () Bool (<= s44 s39)) -[GOOD] (define-fun s46 () Int (ite s45 s39 s44)) -[GOOD] (define-fun s47 () Int (- s42 s4)) -[GOOD] (define-fun s48 () (Seq Int) (seq.extract s41 s4 s47)) -[GOOD] (define-fun s49 () Int (seq.len s48)) -[GOOD] (define-fun s50 () Bool (= s2 s49)) -[GOOD] (define-fun s51 () Int (seq.nth s41 s2)) -[GOOD] (define-fun s52 () Bool (<= s51 s46)) -[GOOD] (define-fun s53 () Int (ite s52 s46 s51)) -[GOOD] (define-fun s54 () Int (- s49 s4)) -[GOOD] (define-fun s55 () (Seq Int) (seq.extract s48 s4 s54)) -[GOOD] (define-fun s56 () Int (seq.len s55)) -[GOOD] (define-fun s57 () Bool (= s2 s56)) -[GOOD] (define-fun s58 () Int (seq.nth s48 s2)) -[GOOD] (define-fun s59 () Bool (<= s58 s53)) -[GOOD] (define-fun s60 () Int (ite s59 s53 s58)) -[GOOD] (define-fun s61 () Int (- s56 s4)) -[GOOD] (define-fun s62 () (Seq Int) (seq.extract s55 s4 s61)) -[GOOD] (define-fun s63 () Int (seq.len s62)) -[GOOD] (define-fun s64 () Bool (= s2 s63)) -[GOOD] (define-fun s65 () Int (seq.nth s55 s2)) -[GOOD] (define-fun s66 () Bool (<= s65 s60)) -[GOOD] (define-fun s67 () Int (ite s66 s60 s65)) -[GOOD] (define-fun s68 () Int (seq.nth s62 s2)) -[GOOD] (define-fun s69 () Bool (<= s68 s67)) -[GOOD] (define-fun s70 () Int (ite s69 s67 s68)) -[GOOD] (define-fun s71 () Int (ite s64 s67 s70)) -[GOOD] (define-fun s72 () Int (ite s57 s60 s71)) -[GOOD] (define-fun s73 () Int (ite s50 s53 s72)) -[GOOD] (define-fun s74 () Int (ite s43 s46 s73)) -[GOOD] (define-fun s75 () Int (ite s36 s39 s74)) -[GOOD] (define-fun s76 () Int (ite s29 s32 s75)) -[GOOD] (define-fun s77 () Int (ite s22 s25 s76)) -[GOOD] (define-fun s78 () Int (ite s15 s18 s77)) -[GOOD] (define-fun s79 () Int (ite s8 s11 s78)) -[GOOD] (define-fun s80 () Int (ite s3 s2 s79)) -[GOOD] (define-fun s82 () Bool (> s80 s81)) -[GOOD] (define-fun s83 () Bool (< s9 s2)) -[GOOD] (define-fun s84 () Bool (> s9 s81)) -[GOOD] (define-fun s85 () Bool (or s83 s84)) -[GOOD] (define-fun s86 () Bool (< s16 s2)) -[GOOD] (define-fun s87 () Bool (> s16 s81)) -[GOOD] (define-fun s88 () Bool (or s86 s87)) -[GOOD] (define-fun s89 () Bool (or s85 s88)) -[GOOD] (define-fun s90 () Bool (< s23 s2)) -[GOOD] (define-fun s91 () Bool (> s23 s81)) -[GOOD] (define-fun s92 () Bool (or s90 s91)) -[GOOD] (define-fun s93 () Bool (or s89 s92)) -[GOOD] (define-fun s94 () Bool (< s30 s2)) -[GOOD] (define-fun s95 () Bool (> s30 s81)) -[GOOD] (define-fun s96 () Bool (or s94 s95)) -[GOOD] (define-fun s97 () Bool (or s93 s96)) -[GOOD] (define-fun s98 () Bool (< s37 s2)) -[GOOD] (define-fun s99 () Bool (> s37 s81)) -[GOOD] (define-fun s100 () Bool (or s98 s99)) -[GOOD] (define-fun s101 () Bool (or s97 s100)) -[GOOD] (define-fun s102 () Bool (< s44 s2)) -[GOOD] (define-fun s103 () Bool (> s44 s81)) -[GOOD] (define-fun s104 () Bool (or s102 s103)) -[GOOD] (define-fun s105 () Bool (or s101 s104)) -[GOOD] (define-fun s106 () Bool (< s51 s2)) -[GOOD] (define-fun s107 () Bool (> s51 s81)) -[GOOD] (define-fun s108 () Bool (or s106 s107)) -[GOOD] (define-fun s109 () Bool (or s105 s108)) -[GOOD] (define-fun s110 () Bool (< s58 s2)) -[GOOD] (define-fun s111 () Bool (> s58 s81)) -[GOOD] (define-fun s112 () Bool (or s110 s111)) -[GOOD] (define-fun s113 () Bool (or s109 s112)) -[GOOD] (define-fun s114 () Bool (< s65 s2)) -[GOOD] (define-fun s115 () Bool (> s65 s81)) -[GOOD] (define-fun s116 () Bool (or s114 s115)) -[GOOD] (define-fun s117 () Bool (or s113 s116)) -[GOOD] (define-fun s118 () Bool (< s68 s2)) -[GOOD] (define-fun s119 () Bool (> s68 s81)) -[GOOD] (define-fun s120 () Bool (or s118 s119)) -[GOOD] (define-fun s121 () Bool (or s117 s120)) -[GOOD] (define-fun s122 () Bool (ite s64 s117 s121)) -[GOOD] (define-fun s123 () Bool (ite s57 s113 s122)) -[GOOD] (define-fun s124 () Bool (ite s50 s109 s123)) -[GOOD] (define-fun s125 () Bool (ite s43 s105 s124)) -[GOOD] (define-fun s126 () Bool (ite s36 s101 s125)) -[GOOD] (define-fun s127 () Bool (ite s29 s97 s126)) -[GOOD] (define-fun s128 () Bool (ite s22 s93 s127)) -[GOOD] (define-fun s129 () Bool (ite s15 s89 s128)) -[GOOD] (define-fun s130 () Bool (ite s8 s85 s129)) -[GOOD] (define-fun s131 () Bool (not s3)) -[GOOD] (define-fun s132 () Bool (and s130 s131)) -[GOOD] (define-fun s133 () Bool (=> s82 s132)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s133) -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/maxrWithFailure.gold b/SBVTestSuite/GoldFiles/maxrWithFailure.gold deleted file mode 100644 index f7399a2a..00000000 --- a/SBVTestSuite/GoldFiles/maxrWithFailure.gold +++ /dev/null @@ -1,171 +0,0 @@ -** 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 s2 () Int 0) -[GOOD] (define-fun s5 () Int 1) -[GOOD] (define-fun s81 () Int 10) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "ints" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s1 () Int (seq.len s0)) -[GOOD] (define-fun s3 () Bool (= s1 s2)) -[GOOD] (define-fun s4 () Int (seq.nth s0 s2)) -[GOOD] (define-fun s6 () Int (- s1 s5)) -[GOOD] (define-fun s7 () (Seq Int) (seq.extract s0 s5 s6)) -[GOOD] (define-fun s8 () Int (seq.len s7)) -[GOOD] (define-fun s9 () Bool (= s2 s8)) -[GOOD] (define-fun s10 () Int (seq.nth s7 s2)) -[GOOD] (define-fun s11 () Int (- s8 s5)) -[GOOD] (define-fun s12 () (Seq Int) (seq.extract s7 s5 s11)) -[GOOD] (define-fun s13 () Int (seq.len s12)) -[GOOD] (define-fun s14 () Bool (= s2 s13)) -[GOOD] (define-fun s15 () Int (seq.nth s12 s2)) -[GOOD] (define-fun s16 () Int (- s13 s5)) -[GOOD] (define-fun s17 () (Seq Int) (seq.extract s12 s5 s16)) -[GOOD] (define-fun s18 () Int (seq.len s17)) -[GOOD] (define-fun s19 () Bool (= s2 s18)) -[GOOD] (define-fun s20 () Int (seq.nth s17 s2)) -[GOOD] (define-fun s21 () Int (- s18 s5)) -[GOOD] (define-fun s22 () (Seq Int) (seq.extract s17 s5 s21)) -[GOOD] (define-fun s23 () Int (seq.len s22)) -[GOOD] (define-fun s24 () Bool (= s2 s23)) -[GOOD] (define-fun s25 () Int (seq.nth s22 s2)) -[GOOD] (define-fun s26 () Int (- s23 s5)) -[GOOD] (define-fun s27 () (Seq Int) (seq.extract s22 s5 s26)) -[GOOD] (define-fun s28 () Int (seq.len s27)) -[GOOD] (define-fun s29 () Bool (= s2 s28)) -[GOOD] (define-fun s30 () Int (seq.nth s27 s2)) -[GOOD] (define-fun s31 () Int (- s28 s5)) -[GOOD] (define-fun s32 () (Seq Int) (seq.extract s27 s5 s31)) -[GOOD] (define-fun s33 () Int (seq.len s32)) -[GOOD] (define-fun s34 () Bool (= s2 s33)) -[GOOD] (define-fun s35 () Int (seq.nth s32 s2)) -[GOOD] (define-fun s36 () Int (- s33 s5)) -[GOOD] (define-fun s37 () (Seq Int) (seq.extract s32 s5 s36)) -[GOOD] (define-fun s38 () Int (seq.len s37)) -[GOOD] (define-fun s39 () Bool (= s2 s38)) -[GOOD] (define-fun s40 () Int (seq.nth s37 s2)) -[GOOD] (define-fun s41 () Int (- s38 s5)) -[GOOD] (define-fun s42 () (Seq Int) (seq.extract s37 s5 s41)) -[GOOD] (define-fun s43 () Int (seq.len s42)) -[GOOD] (define-fun s44 () Bool (= s2 s43)) -[GOOD] (define-fun s45 () Int (seq.nth s42 s2)) -[GOOD] (define-fun s46 () Int (- s43 s5)) -[GOOD] (define-fun s47 () (Seq Int) (seq.extract s42 s5 s46)) -[GOOD] (define-fun s48 () Int (seq.len s47)) -[GOOD] (define-fun s49 () Bool (= s2 s48)) -[GOOD] (define-fun s50 () Int (seq.nth s47 s2)) -[GOOD] (define-fun s51 () Bool (<= s50 s2)) -[GOOD] (define-fun s52 () Int (ite s51 s2 s50)) -[GOOD] (define-fun s53 () Int (ite s49 s2 s52)) -[GOOD] (define-fun s54 () Bool (<= s45 s53)) -[GOOD] (define-fun s55 () Int (ite s54 s53 s45)) -[GOOD] (define-fun s56 () Int (ite s44 s2 s55)) -[GOOD] (define-fun s57 () Bool (<= s40 s56)) -[GOOD] (define-fun s58 () Int (ite s57 s56 s40)) -[GOOD] (define-fun s59 () Int (ite s39 s2 s58)) -[GOOD] (define-fun s60 () Bool (<= s35 s59)) -[GOOD] (define-fun s61 () Int (ite s60 s59 s35)) -[GOOD] (define-fun s62 () Int (ite s34 s2 s61)) -[GOOD] (define-fun s63 () Bool (<= s30 s62)) -[GOOD] (define-fun s64 () Int (ite s63 s62 s30)) -[GOOD] (define-fun s65 () Int (ite s29 s2 s64)) -[GOOD] (define-fun s66 () Bool (<= s25 s65)) -[GOOD] (define-fun s67 () Int (ite s66 s65 s25)) -[GOOD] (define-fun s68 () Int (ite s24 s2 s67)) -[GOOD] (define-fun s69 () Bool (<= s20 s68)) -[GOOD] (define-fun s70 () Int (ite s69 s68 s20)) -[GOOD] (define-fun s71 () Int (ite s19 s2 s70)) -[GOOD] (define-fun s72 () Bool (<= s15 s71)) -[GOOD] (define-fun s73 () Int (ite s72 s71 s15)) -[GOOD] (define-fun s74 () Int (ite s14 s2 s73)) -[GOOD] (define-fun s75 () Bool (<= s10 s74)) -[GOOD] (define-fun s76 () Int (ite s75 s74 s10)) -[GOOD] (define-fun s77 () Int (ite s9 s2 s76)) -[GOOD] (define-fun s78 () Bool (<= s4 s77)) -[GOOD] (define-fun s79 () Int (ite s78 s77 s4)) -[GOOD] (define-fun s80 () Int (ite s3 s2 s79)) -[GOOD] (define-fun s82 () Bool (> s80 s81)) -[GOOD] (define-fun s83 () Bool (< s50 s2)) -[GOOD] (define-fun s84 () Bool (> s50 s81)) -[GOOD] (define-fun s85 () Bool (or s83 s84)) -[GOOD] (define-fun s86 () Bool (not s49)) -[GOOD] (define-fun s87 () Bool (and s85 s86)) -[GOOD] (define-fun s88 () Bool (< s45 s2)) -[GOOD] (define-fun s89 () Bool (> s45 s81)) -[GOOD] (define-fun s90 () Bool (or s88 s89)) -[GOOD] (define-fun s91 () Bool (or s87 s90)) -[GOOD] (define-fun s92 () Bool (not s44)) -[GOOD] (define-fun s93 () Bool (and s91 s92)) -[GOOD] (define-fun s94 () Bool (< s40 s2)) -[GOOD] (define-fun s95 () Bool (> s40 s81)) -[GOOD] (define-fun s96 () Bool (or s94 s95)) -[GOOD] (define-fun s97 () Bool (or s93 s96)) -[GOOD] (define-fun s98 () Bool (not s39)) -[GOOD] (define-fun s99 () Bool (and s97 s98)) -[GOOD] (define-fun s100 () Bool (< s35 s2)) -[GOOD] (define-fun s101 () Bool (> s35 s81)) -[GOOD] (define-fun s102 () Bool (or s100 s101)) -[GOOD] (define-fun s103 () Bool (or s99 s102)) -[GOOD] (define-fun s104 () Bool (not s34)) -[GOOD] (define-fun s105 () Bool (and s103 s104)) -[GOOD] (define-fun s106 () Bool (< s30 s2)) -[GOOD] (define-fun s107 () Bool (> s30 s81)) -[GOOD] (define-fun s108 () Bool (or s106 s107)) -[GOOD] (define-fun s109 () Bool (or s105 s108)) -[GOOD] (define-fun s110 () Bool (not s29)) -[GOOD] (define-fun s111 () Bool (and s109 s110)) -[GOOD] (define-fun s112 () Bool (< s25 s2)) -[GOOD] (define-fun s113 () Bool (> s25 s81)) -[GOOD] (define-fun s114 () Bool (or s112 s113)) -[GOOD] (define-fun s115 () Bool (or s111 s114)) -[GOOD] (define-fun s116 () Bool (not s24)) -[GOOD] (define-fun s117 () Bool (and s115 s116)) -[GOOD] (define-fun s118 () Bool (< s20 s2)) -[GOOD] (define-fun s119 () Bool (> s20 s81)) -[GOOD] (define-fun s120 () Bool (or s118 s119)) -[GOOD] (define-fun s121 () Bool (or s117 s120)) -[GOOD] (define-fun s122 () Bool (not s19)) -[GOOD] (define-fun s123 () Bool (and s121 s122)) -[GOOD] (define-fun s124 () Bool (< s15 s2)) -[GOOD] (define-fun s125 () Bool (> s15 s81)) -[GOOD] (define-fun s126 () Bool (or s124 s125)) -[GOOD] (define-fun s127 () Bool (or s123 s126)) -[GOOD] (define-fun s128 () Bool (not s14)) -[GOOD] (define-fun s129 () Bool (and s127 s128)) -[GOOD] (define-fun s130 () Bool (< s10 s2)) -[GOOD] (define-fun s131 () Bool (> s10 s81)) -[GOOD] (define-fun s132 () Bool (or s130 s131)) -[GOOD] (define-fun s133 () Bool (or s129 s132)) -[GOOD] (define-fun s134 () Bool (not s9)) -[GOOD] (define-fun s135 () Bool (and s133 s134)) -[GOOD] (define-fun s136 () Bool (< s4 s2)) -[GOOD] (define-fun s137 () Bool (> s4 s81)) -[GOOD] (define-fun s138 () Bool (or s136 s137)) -[GOOD] (define-fun s139 () Bool (or s135 s138)) -[GOOD] (define-fun s140 () Bool (not s3)) -[GOOD] (define-fun s141 () Bool (and s139 s140)) -[GOOD] (define-fun s142 () Bool (=> s82 s141)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s142) -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/reverse.gold b/SBVTestSuite/GoldFiles/reverse.gold deleted file mode 100644 index a64ea2ee..00000000 --- a/SBVTestSuite/GoldFiles/reverse.gold +++ /dev/null @@ -1,123 +0,0 @@ -** 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 s12 () Int 0) -[GOOD] (define-fun s14 () (Seq Int) (as seq.empty (Seq Int))) -[GOOD] (define-fun s15 () Int 1) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" -[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" -[GOOD] (declare-fun s3 () Int) ; tracks user variable "d" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s4 () (Seq Int) (seq.unit s0)) -[GOOD] (define-fun s5 () (Seq Int) (seq.unit s1)) -[GOOD] (define-fun s6 () (Seq Int) (seq.unit s2)) -[GOOD] (define-fun s7 () (Seq Int) (seq.unit s3)) -[GOOD] (define-fun s8 () (Seq Int) (seq.++ s6 s7)) -[GOOD] (define-fun s9 () (Seq Int) (seq.++ s5 s8)) -[GOOD] (define-fun s10 () (Seq Int) (seq.++ s4 s9)) -[GOOD] (define-fun s11 () Int (seq.len s10)) -[GOOD] (define-fun s13 () Bool (= s11 s12)) -[GOOD] (define-fun s16 () Int (- s11 s15)) -[GOOD] (define-fun s17 () (Seq Int) (seq.extract s10 s15 s16)) -[GOOD] (define-fun s18 () Int (seq.len s17)) -[GOOD] (define-fun s19 () Bool (= s12 s18)) -[GOOD] (define-fun s20 () Int (- s18 s15)) -[GOOD] (define-fun s21 () (Seq Int) (seq.extract s17 s15 s20)) -[GOOD] (define-fun s22 () Int (seq.len s21)) -[GOOD] (define-fun s23 () Bool (= s12 s22)) -[GOOD] (define-fun s24 () Int (- s22 s15)) -[GOOD] (define-fun s25 () (Seq Int) (seq.extract s21 s15 s24)) -[GOOD] (define-fun s26 () Int (seq.len s25)) -[GOOD] (define-fun s27 () Bool (= s12 s26)) -[GOOD] (define-fun s28 () Int (- s26 s15)) -[GOOD] (define-fun s29 () (Seq Int) (seq.extract s25 s15 s28)) -[GOOD] (define-fun s30 () Int (seq.len s29)) -[GOOD] (define-fun s31 () Bool (= s12 s30)) -[GOOD] (define-fun s32 () Int (- s30 s15)) -[GOOD] (define-fun s33 () (Seq Int) (seq.extract s29 s15 s32)) -[GOOD] (define-fun s34 () Int (seq.len s33)) -[GOOD] (define-fun s35 () Bool (= s12 s34)) -[GOOD] (define-fun s36 () Int (- s34 s15)) -[GOOD] (define-fun s37 () (Seq Int) (seq.extract s33 s15 s36)) -[GOOD] (define-fun s38 () Int (seq.len s37)) -[GOOD] (define-fun s39 () Bool (= s12 s38)) -[GOOD] (define-fun s40 () Int (- s38 s15)) -[GOOD] (define-fun s41 () (Seq Int) (seq.extract s37 s15 s40)) -[GOOD] (define-fun s42 () Int (seq.len s41)) -[GOOD] (define-fun s43 () Bool (= s12 s42)) -[GOOD] (define-fun s44 () Int (- s42 s15)) -[GOOD] (define-fun s45 () (Seq Int) (seq.extract s41 s15 s44)) -[GOOD] (define-fun s46 () Int (seq.len s45)) -[GOOD] (define-fun s47 () Bool (= s12 s46)) -[GOOD] (define-fun s48 () Int (- s46 s15)) -[GOOD] (define-fun s49 () (Seq Int) (seq.extract s45 s15 s48)) -[GOOD] (define-fun s50 () Int (seq.len s49)) -[GOOD] (define-fun s51 () Bool (= s12 s50)) -[GOOD] (define-fun s52 () Int (seq.nth s49 s12)) -[GOOD] (define-fun s53 () (Seq Int) (seq.unit s52)) -[GOOD] (define-fun s54 () (Seq Int) (ite s51 s14 s53)) -[GOOD] (define-fun s55 () Int (seq.nth s45 s12)) -[GOOD] (define-fun s56 () (Seq Int) (seq.unit s55)) -[GOOD] (define-fun s57 () (Seq Int) (seq.++ s54 s56)) -[GOOD] (define-fun s58 () (Seq Int) (ite s47 s14 s57)) -[GOOD] (define-fun s59 () Int (seq.nth s41 s12)) -[GOOD] (define-fun s60 () (Seq Int) (seq.unit s59)) -[GOOD] (define-fun s61 () (Seq Int) (seq.++ s58 s60)) -[GOOD] (define-fun s62 () (Seq Int) (ite s43 s14 s61)) -[GOOD] (define-fun s63 () Int (seq.nth s37 s12)) -[GOOD] (define-fun s64 () (Seq Int) (seq.unit s63)) -[GOOD] (define-fun s65 () (Seq Int) (seq.++ s62 s64)) -[GOOD] (define-fun s66 () (Seq Int) (ite s39 s14 s65)) -[GOOD] (define-fun s67 () Int (seq.nth s33 s12)) -[GOOD] (define-fun s68 () (Seq Int) (seq.unit s67)) -[GOOD] (define-fun s69 () (Seq Int) (seq.++ s66 s68)) -[GOOD] (define-fun s70 () (Seq Int) (ite s35 s14 s69)) -[GOOD] (define-fun s71 () Int (seq.nth s29 s12)) -[GOOD] (define-fun s72 () (Seq Int) (seq.unit s71)) -[GOOD] (define-fun s73 () (Seq Int) (seq.++ s70 s72)) -[GOOD] (define-fun s74 () (Seq Int) (ite s31 s14 s73)) -[GOOD] (define-fun s75 () Int (seq.nth s25 s12)) -[GOOD] (define-fun s76 () (Seq Int) (seq.unit s75)) -[GOOD] (define-fun s77 () (Seq Int) (seq.++ s74 s76)) -[GOOD] (define-fun s78 () (Seq Int) (ite s27 s14 s77)) -[GOOD] (define-fun s79 () Int (seq.nth s21 s12)) -[GOOD] (define-fun s80 () (Seq Int) (seq.unit s79)) -[GOOD] (define-fun s81 () (Seq Int) (seq.++ s78 s80)) -[GOOD] (define-fun s82 () (Seq Int) (ite s23 s14 s81)) -[GOOD] (define-fun s83 () Int (seq.nth s17 s12)) -[GOOD] (define-fun s84 () (Seq Int) (seq.unit s83)) -[GOOD] (define-fun s85 () (Seq Int) (seq.++ s82 s84)) -[GOOD] (define-fun s86 () (Seq Int) (ite s19 s14 s85)) -[GOOD] (define-fun s87 () Int (seq.nth s10 s12)) -[GOOD] (define-fun s88 () (Seq Int) (seq.unit s87)) -[GOOD] (define-fun s89 () (Seq Int) (seq.++ s86 s88)) -[GOOD] (define-fun s90 () (Seq Int) (ite s13 s14 s89)) -[GOOD] (define-fun s91 () (Seq Int) (seq.++ s5 s4)) -[GOOD] (define-fun s92 () (Seq Int) (seq.++ s6 s91)) -[GOOD] (define-fun s93 () (Seq Int) (seq.++ s7 s92)) -[GOOD] (define-fun s94 () Bool (= s90 s93)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s94) -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/reverseAlt10.gold b/SBVTestSuite/GoldFiles/reverseAlt10.gold deleted file mode 100644 index 7272995b..00000000 --- a/SBVTestSuite/GoldFiles/reverseAlt10.gold +++ /dev/null @@ -1,129 +0,0 @@ -** 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 s2 () Int 0) -[GOOD] (define-fun s4 () (Seq Int) (as seq.empty (Seq Int))) -[GOOD] (define-fun s5 () Int 1) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "xs" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s1 () Int (seq.len s0)) -[GOOD] (define-fun s3 () Bool (= s1 s2)) -[GOOD] (define-fun s6 () Int (- s1 s5)) -[GOOD] (define-fun s7 () (Seq Int) (seq.extract s0 s5 s6)) -[GOOD] (define-fun s8 () Int (seq.len s7)) -[GOOD] (define-fun s9 () Bool (= s2 s8)) -[GOOD] (define-fun s10 () Int (- s8 s5)) -[GOOD] (define-fun s11 () (Seq Int) (seq.extract s7 s5 s10)) -[GOOD] (define-fun s12 () Int (seq.len s11)) -[GOOD] (define-fun s13 () Bool (= s2 s12)) -[GOOD] (define-fun s14 () Int (- s12 s5)) -[GOOD] (define-fun s15 () (Seq Int) (seq.extract s11 s5 s14)) -[GOOD] (define-fun s16 () Int (seq.len s15)) -[GOOD] (define-fun s17 () Bool (= s2 s16)) -[GOOD] (define-fun s18 () Int (- s16 s5)) -[GOOD] (define-fun s19 () (Seq Int) (seq.extract s15 s5 s18)) -[GOOD] (define-fun s20 () Int (seq.len s19)) -[GOOD] (define-fun s21 () Bool (= s2 s20)) -[GOOD] (define-fun s22 () Int (- s20 s5)) -[GOOD] (define-fun s23 () (Seq Int) (seq.extract s19 s5 s22)) -[GOOD] (define-fun s24 () Int (seq.len s23)) -[GOOD] (define-fun s25 () Bool (= s2 s24)) -[GOOD] (define-fun s26 () Int (- s24 s5)) -[GOOD] (define-fun s27 () (Seq Int) (seq.extract s23 s5 s26)) -[GOOD] (define-fun s28 () Int (seq.len s27)) -[GOOD] (define-fun s29 () Bool (= s2 s28)) -[GOOD] (define-fun s30 () Int (- s28 s5)) -[GOOD] (define-fun s31 () (Seq Int) (seq.extract s27 s5 s30)) -[GOOD] (define-fun s32 () Int (seq.len s31)) -[GOOD] (define-fun s33 () Bool (= s2 s32)) -[GOOD] (define-fun s34 () Int (- s32 s5)) -[GOOD] (define-fun s35 () (Seq Int) (seq.extract s31 s5 s34)) -[GOOD] (define-fun s36 () Int (seq.len s35)) -[GOOD] (define-fun s37 () Bool (= s2 s36)) -[GOOD] (define-fun s38 () Int (- s36 s5)) -[GOOD] (define-fun s39 () (Seq Int) (seq.extract s35 s5 s38)) -[GOOD] (define-fun s40 () Int (seq.len s39)) -[GOOD] (define-fun s41 () Bool (= s2 s40)) -[GOOD] (define-fun s42 () Int (seq.nth s39 s2)) -[GOOD] (define-fun s43 () (Seq Int) (seq.unit s42)) -[GOOD] (define-fun s44 () (Seq Int) (ite s41 s4 s43)) -[GOOD] (define-fun s45 () Int (seq.nth s35 s2)) -[GOOD] (define-fun s46 () (Seq Int) (seq.unit s45)) -[GOOD] (define-fun s47 () (Seq Int) (seq.++ s44 s46)) -[GOOD] (define-fun s48 () (Seq Int) (ite s37 s4 s47)) -[GOOD] (define-fun s49 () Int (seq.nth s31 s2)) -[GOOD] (define-fun s50 () (Seq Int) (seq.unit s49)) -[GOOD] (define-fun s51 () (Seq Int) (seq.++ s48 s50)) -[GOOD] (define-fun s52 () (Seq Int) (ite s33 s4 s51)) -[GOOD] (define-fun s53 () Int (seq.nth s27 s2)) -[GOOD] (define-fun s54 () (Seq Int) (seq.unit s53)) -[GOOD] (define-fun s55 () (Seq Int) (seq.++ s52 s54)) -[GOOD] (define-fun s56 () (Seq Int) (ite s29 s4 s55)) -[GOOD] (define-fun s57 () Int (seq.nth s23 s2)) -[GOOD] (define-fun s58 () (Seq Int) (seq.unit s57)) -[GOOD] (define-fun s59 () (Seq Int) (seq.++ s56 s58)) -[GOOD] (define-fun s60 () (Seq Int) (ite s25 s4 s59)) -[GOOD] (define-fun s61 () Int (seq.nth s19 s2)) -[GOOD] (define-fun s62 () (Seq Int) (seq.unit s61)) -[GOOD] (define-fun s63 () (Seq Int) (seq.++ s60 s62)) -[GOOD] (define-fun s64 () (Seq Int) (ite s21 s4 s63)) -[GOOD] (define-fun s65 () Int (seq.nth s15 s2)) -[GOOD] (define-fun s66 () (Seq Int) (seq.unit s65)) -[GOOD] (define-fun s67 () (Seq Int) (seq.++ s64 s66)) -[GOOD] (define-fun s68 () (Seq Int) (ite s17 s4 s67)) -[GOOD] (define-fun s69 () Int (seq.nth s11 s2)) -[GOOD] (define-fun s70 () (Seq Int) (seq.unit s69)) -[GOOD] (define-fun s71 () (Seq Int) (seq.++ s68 s70)) -[GOOD] (define-fun s72 () (Seq Int) (ite s13 s4 s71)) -[GOOD] (define-fun s73 () Int (seq.nth s7 s2)) -[GOOD] (define-fun s74 () (Seq Int) (seq.unit s73)) -[GOOD] (define-fun s75 () (Seq Int) (seq.++ s72 s74)) -[GOOD] (define-fun s76 () (Seq Int) (ite s9 s4 s75)) -[GOOD] (define-fun s77 () Int (seq.nth s0 s2)) -[GOOD] (define-fun s78 () (Seq Int) (seq.unit s77)) -[GOOD] (define-fun s79 () (Seq Int) (seq.++ s76 s78)) -[GOOD] (define-fun s80 () (Seq Int) (ite s3 s4 s79)) -[GOOD] (define-fun s81 () (Seq Int) (seq.++ s74 s78)) -[GOOD] (define-fun s82 () (Seq Int) (seq.++ s70 s81)) -[GOOD] (define-fun s83 () (Seq Int) (seq.++ s66 s82)) -[GOOD] (define-fun s84 () (Seq Int) (seq.++ s62 s83)) -[GOOD] (define-fun s85 () (Seq Int) (seq.++ s58 s84)) -[GOOD] (define-fun s86 () (Seq Int) (seq.++ s54 s85)) -[GOOD] (define-fun s87 () (Seq Int) (seq.++ s50 s86)) -[GOOD] (define-fun s88 () (Seq Int) (seq.++ s46 s87)) -[GOOD] (define-fun s89 () (Seq Int) (seq.++ s43 s88)) -[GOOD] (define-fun s90 () (Seq Int) (ite s41 s88 s89)) -[GOOD] (define-fun s91 () (Seq Int) (ite s37 s87 s90)) -[GOOD] (define-fun s92 () (Seq Int) (ite s33 s86 s91)) -[GOOD] (define-fun s93 () (Seq Int) (ite s29 s85 s92)) -[GOOD] (define-fun s94 () (Seq Int) (ite s25 s84 s93)) -[GOOD] (define-fun s95 () (Seq Int) (ite s21 s83 s94)) -[GOOD] (define-fun s96 () (Seq Int) (ite s17 s82 s95)) -[GOOD] (define-fun s97 () (Seq Int) (ite s13 s81 s96)) -[GOOD] (define-fun s98 () (Seq Int) (ite s9 s78 s97)) -[GOOD] (define-fun s99 () (Seq Int) (ite s3 s4 s98)) -[GOOD] (define-fun s100 () Bool (distinct s80 s99)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s100) -[SEND] (check-sat) -[RECV] unsat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/sort.gold b/SBVTestSuite/GoldFiles/sort.gold deleted file mode 100644 index 8ebd9100..00000000 --- a/SBVTestSuite/GoldFiles/sort.gold +++ /dev/null @@ -1,169 +0,0 @@ -** 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 s12 () Int 0) -[GOOD] (define-fun s14 () (Seq Int) (as seq.empty (Seq Int))) -[GOOD] (define-fun s15 () Int 1) -[GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" -[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" -[GOOD] ; --- constant tables --- -[GOOD] ; --- non-constant tables --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user defined functions --- -[GOOD] ; --- assignments --- -[GOOD] (define-fun s3 () Bool (<= s0 s1)) -[GOOD] (define-fun s4 () Bool (<= s1 s2)) -[GOOD] (define-fun s5 () Bool (and s3 s4)) -[GOOD] (define-fun s6 () (Seq Int) (seq.unit s0)) -[GOOD] (define-fun s7 () (Seq Int) (seq.unit s1)) -[GOOD] (define-fun s8 () (Seq Int) (seq.unit s2)) -[GOOD] (define-fun s9 () (Seq Int) (seq.++ s7 s8)) -[GOOD] (define-fun s10 () (Seq Int) (seq.++ s6 s9)) -[GOOD] (define-fun s11 () Int (seq.len s10)) -[GOOD] (define-fun s13 () Bool (= s11 s12)) -[GOOD] (define-fun s16 () Int (- s11 s15)) -[GOOD] (define-fun s17 () (Seq Int) (seq.extract s10 s15 s16)) -[GOOD] (define-fun s18 () Int (seq.len s17)) -[GOOD] (define-fun s19 () Bool (= s12 s18)) -[GOOD] (define-fun s20 () Int (- s18 s15)) -[GOOD] (define-fun s21 () (Seq Int) (seq.extract s17 s15 s20)) -[GOOD] (define-fun s22 () Int (seq.len s21)) -[GOOD] (define-fun s23 () Bool (= s12 s22)) -[GOOD] (define-fun s24 () Int (seq.nth s21 s12)) -[GOOD] (define-fun s25 () (Seq Int) (seq.unit s24)) -[GOOD] (define-fun s26 () (Seq Int) (ite s23 s14 s25)) -[GOOD] (define-fun s27 () Int (seq.len s26)) -[GOOD] (define-fun s28 () Bool (= s12 s27)) -[GOOD] (define-fun s29 () Int (seq.nth s17 s12)) -[GOOD] (define-fun s30 () (Seq Int) (seq.unit s29)) -[GOOD] (define-fun s31 () Int (seq.nth s26 s12)) -[GOOD] (define-fun s32 () Bool (< s29 s31)) -[GOOD] (define-fun s33 () (Seq Int) (seq.unit s31)) -[GOOD] (define-fun s34 () Int (- s27 s15)) -[GOOD] (define-fun s35 () (Seq Int) (seq.extract s26 s15 s34)) -[GOOD] (define-fun s36 () (Seq Int) (seq.++ s33 s35)) -[GOOD] (define-fun s37 () (Seq Int) (seq.++ s30 s36)) -[GOOD] (define-fun s38 () Int (seq.len s35)) -[GOOD] (define-fun s39 () Bool (= s12 s38)) -[GOOD] (define-fun s40 () Int (seq.nth s35 s12)) -[GOOD] (define-fun s41 () Bool (< s29 s40)) -[GOOD] (define-fun s42 () (Seq Int) (seq.unit s40)) -[GOOD] (define-fun s43 () Int (- s38 s15)) -[GOOD] (define-fun s44 () (Seq Int) (seq.extract s35 s15 s43)) -[GOOD] (define-fun s45 () (Seq Int) (seq.++ s42 s44)) -[GOOD] (define-fun s46 () (Seq Int) (seq.++ s30 s45)) -[GOOD] (define-fun s47 () Int (seq.len s44)) -[GOOD] (define-fun s48 () Bool (= s12 s47)) -[GOOD] (define-fun s49 () Int (seq.nth s44 s12)) -[GOOD] (define-fun s50 () Bool (< s29 s49)) -[GOOD] (define-fun s51 () (Seq Int) (seq.unit s49)) -[GOOD] (define-fun s52 () Int (- s47 s15)) -[GOOD] (define-fun s53 () (Seq Int) (seq.extract s44 s15 s52)) -[GOOD] (define-fun s54 () (Seq Int) (seq.++ s51 s53)) -[GOOD] (define-fun s55 () (Seq Int) (seq.++ s30 s54)) -[GOOD] (define-fun s56 () (Seq Int) (seq.++ s51 s30)) -[GOOD] (define-fun s57 () (Seq Int) (ite s50 s55 s56)) -[GOOD] (define-fun s58 () (Seq Int) (ite s48 s30 s57)) -[GOOD] (define-fun s59 () (Seq Int) (seq.++ s42 s58)) -[GOOD] (define-fun s60 () (Seq Int) (ite s41 s46 s59)) -[GOOD] (define-fun s61 () (Seq Int) (ite s39 s30 s60)) -[GOOD] (define-fun s62 () (Seq Int) (seq.++ s33 s61)) -[GOOD] (define-fun s63 () (Seq Int) (ite s32 s37 s62)) -[GOOD] (define-fun s64 () (Seq Int) (ite s28 s30 s63)) -[GOOD] (define-fun s65 () (Seq Int) (ite s19 s14 s64)) -[GOOD] (define-fun s66 () Int (seq.len s65)) -[GOOD] (define-fun s67 () Bool (= s12 s66)) -[GOOD] (define-fun s68 () Int (seq.nth s10 s12)) -[GOOD] (define-fun s69 () (Seq Int) (seq.unit s68)) -[GOOD] (define-fun s70 () Int (seq.nth s65 s12)) -[GOOD] (define-fun s71 () Bool (< s68 s70)) -[GOOD] (define-fun s72 () (Seq Int) (seq.unit s70)) -[GOOD] (define-fun s73 () Int (- s66 s15)) -[GOOD] (define-fun s74 () (Seq Int) (seq.extract s65 s15 s73)) -[GOOD] (define-fun s75 () (Seq Int) (seq.++ s72 s74)) -[GOOD] (define-fun s76 () (Seq Int) (seq.++ s69 s75)) -[GOOD] (define-fun s77 () Int (seq.len s74)) -[GOOD] (define-fun s78 () Bool (= s12 s77)) -[GOOD] (define-fun s79 () Int (seq.nth s74 s12)) -[GOOD] (define-fun s80 () Bool (< s68 s79)) -[GOOD] (define-fun s81 () (Seq Int) (seq.unit s79)) -[GOOD] (define-fun s82 () Int (- s77 s15)) -[GOOD] (define-fun s83 () (Seq Int) (seq.extract s74 s15 s82)) -[GOOD] (define-fun s84 () (Seq Int) (seq.++ s81 s83)) -[GOOD] (define-fun s85 () (Seq Int) (seq.++ s69 s84)) -[GOOD] (define-fun s86 () Int (seq.len s83)) -[GOOD] (define-fun s87 () Bool (= s12 s86)) -[GOOD] (define-fun s88 () Int (seq.nth s83 s12)) -[GOOD] (define-fun s89 () Bool (< s68 s88)) -[GOOD] (define-fun s90 () (Seq Int) (seq.unit s88)) -[GOOD] (define-fun s91 () Int (- s86 s15)) -[GOOD] (define-fun s92 () (Seq Int) (seq.extract s83 s15 s91)) -[GOOD] (define-fun s93 () (Seq Int) (seq.++ s90 s92)) -[GOOD] (define-fun s94 () (Seq Int) (seq.++ s69 s93)) -[GOOD] (define-fun s95 () (Seq Int) (seq.++ s90 s69)) -[GOOD] (define-fun s96 () (Seq Int) (ite s89 s94 s95)) -[GOOD] (define-fun s97 () (Seq Int) (ite s87 s69 s96)) -[GOOD] (define-fun s98 () (Seq Int) (seq.++ s81 s97)) -[GOOD] (define-fun s99 () (Seq Int) (ite s80 s85 s98)) -[GOOD] (define-fun s100 () (Seq Int) (ite s78 s69 s99)) -[GOOD] (define-fun s101 () (Seq Int) (seq.++ s72 s100)) -[GOOD] (define-fun s102 () (Seq Int) (ite s71 s76 s101)) -[GOOD] (define-fun s103 () (Seq Int) (ite s67 s69 s102)) -[GOOD] (define-fun s104 () (Seq Int) (ite s13 s14 s103)) -[GOOD] (define-fun s105 () Bool (= s10 s104)) -[GOOD] (define-fun s106 () Bool (=> s5 s105)) -[GOOD] (define-fun s107 () Bool (<= s0 s2)) -[GOOD] (define-fun s108 () Bool (<= s2 s1)) -[GOOD] (define-fun s109 () Bool (and s107 s108)) -[GOOD] (define-fun s110 () (Seq Int) (seq.++ s8 s7)) -[GOOD] (define-fun s111 () (Seq Int) (seq.++ s6 s110)) -[GOOD] (define-fun s112 () Bool (= s104 s111)) -[GOOD] (define-fun s113 () Bool (=> s109 s112)) -[GOOD] (define-fun s114 () Bool (<= s1 s0)) -[GOOD] (define-fun s115 () Bool (and s107 s114)) -[GOOD] (define-fun s116 () (Seq Int) (seq.++ s6 s8)) -[GOOD] (define-fun s117 () (Seq Int) (seq.++ s7 s116)) -[GOOD] (define-fun s118 () Bool (= s104 s117)) -[GOOD] (define-fun s119 () Bool (=> s115 s118)) -[GOOD] (define-fun s120 () Bool (<= s2 s0)) -[GOOD] (define-fun s121 () Bool (and s4 s120)) -[GOOD] (define-fun s122 () (Seq Int) (seq.++ s8 s6)) -[GOOD] (define-fun s123 () (Seq Int) (seq.++ s7 s122)) -[GOOD] (define-fun s124 () Bool (= s104 s123)) -[GOOD] (define-fun s125 () Bool (=> s121 s124)) -[GOOD] (define-fun s126 () Bool (and s3 s120)) -[GOOD] (define-fun s127 () (Seq Int) (seq.++ s6 s7)) -[GOOD] (define-fun s128 () (Seq Int) (seq.++ s8 s127)) -[GOOD] (define-fun s129 () Bool (= s104 s128)) -[GOOD] (define-fun s130 () Bool (=> s126 s129)) -[GOOD] (define-fun s131 () Bool (and s108 s114)) -[GOOD] (define-fun s132 () (Seq Int) (seq.++ s7 s6)) -[GOOD] (define-fun s133 () (Seq Int) (seq.++ s8 s132)) -[GOOD] (define-fun s134 () Bool (= s104 s133)) -[GOOD] (define-fun s135 () Bool (=> s131 s134)) -[GOOD] ; --- delayedEqualities --- -[GOOD] ; --- formula --- -[GOOD] (assert s106) -[GOOD] (assert s113) -[GOOD] (assert s119) -[GOOD] (assert s125) -[GOOD] (assert s130) -[GOOD] (assert s135) -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess From 8f1e7c14bb5248d9721840c32782f2f5732098c3 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 23 Dec 2024 11:50:19 -0800 Subject: [PATCH 6/9] Remove boundedlist tests --- SBVTestSuite/SBVTest.hs | 2 - SBVTestSuite/TestSuite/Basics/BoundedList.hs | 201 ------------------- 2 files changed, 203 deletions(-) delete mode 100644 SBVTestSuite/TestSuite/Basics/BoundedList.hs diff --git a/SBVTestSuite/SBVTest.hs b/SBVTestSuite/SBVTest.hs index f37d1164..98946777 100644 --- a/SBVTestSuite/SBVTest.hs +++ b/SBVTestSuite/SBVTest.hs @@ -28,7 +28,6 @@ import qualified TestSuite.Basics.ArithSolver import qualified TestSuite.Basics.Assert import qualified TestSuite.Basics.BasicTests import qualified TestSuite.Basics.BarrelRotate -import qualified TestSuite.Basics.BoundedList import qualified TestSuite.Basics.DynSign import qualified TestSuite.Basics.Exceptions import qualified TestSuite.Basics.EqSym @@ -140,7 +139,6 @@ main = defaultMain $ testGroup "SBV" [ , TestSuite.Basics.Assert.tests , TestSuite.Basics.BarrelRotate.tests , TestSuite.Basics.BasicTests.tests - , TestSuite.Basics.BoundedList.tests , TestSuite.Basics.DynSign.tests , TestSuite.Basics.EqSym.tests , TestSuite.Basics.Exceptions.testsLocal diff --git a/SBVTestSuite/TestSuite/Basics/BoundedList.hs b/SBVTestSuite/TestSuite/Basics/BoundedList.hs deleted file mode 100644 index 8bb0730f..00000000 --- a/SBVTestSuite/TestSuite/Basics/BoundedList.hs +++ /dev/null @@ -1,201 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : TestSuite.Basics.BoundedList --- Copyright : (c) Joel Burget --- License : BSD3 --- Maintainer: erkokl@gmail.com --- Stability : experimental --- --- Test the bounded sequence/list functions. ------------------------------------------------------------------------------ - -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE OverloadedLists #-} -{-# LANGUAGE ScopedTypeVariables #-} - -{-# OPTIONS_GHC -Wall -Werror #-} - -module TestSuite.Basics.BoundedList(tests) where - -import Data.SBV.Control -import Utils.SBVTestFramework - -import Prelude hiding ((!!)) -import Data.SBV.List ((.:), (!!)) -import qualified Data.SBV.List as L -import qualified Data.SBV.Tools.BoundedList as BL - -import Control.Monad (unless) -import Control.Monad.State (MonadState(..), State, modify, runState) - --- | Flag to mark a failed computation -newtype Failure = Failure SBool - deriving (Mergeable, EqSymbolic) - --- | Evaluation monad with failure -newtype Eval a = Eval { unEval :: State Failure a } - deriving (Functor, Applicative, Monad, MonadState Failure) - -runEval :: Eval a -> (a, Failure) -runEval (Eval eval) = runState eval (Failure sFalse) - -instance Mergeable a => Mergeable (Eval a) where - symbolicMerge force test left right = Eval $ state $ \s0 -> - let (resL, sL) = runState (unEval left) s0 - (resR, sR) = runState (unEval right) s0 - in ( symbolicMerge force test resL resR - , symbolicMerge force test sL sR - ) - -markFailure :: SBool -> Eval () -markFailure failure = modify (\(Failure b) -> Failure (b .|| failure)) - --- Test suite -tests :: TestTree -tests = - testGroup "Basics.BoundedList" [ - goldenCapturedIO "concreteFoldr" $ \rf -> checkWith z3{redirectVerbose=Just rf} concreteFoldrSat Sat - , goldenCapturedIO "concreteFoldl" $ \rf -> checkWith z3{redirectVerbose=Just rf} concreteFoldlSat Sat - , goldenCapturedIO "foldrAB1" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldrAB 1) Unsat - , goldenCapturedIO "foldrAB2" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldrAB 2) Sat - , goldenCapturedIO "foldrAB3" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldrAB 3) Sat - , goldenCapturedIO "foldlABC1" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldlABC 1) Unsat - , goldenCapturedIO "foldlABC2" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldlABC 2) Unsat - , goldenCapturedIO "foldlABC3" $ \rf -> checkWith z3{redirectVerbose=Just rf} (foldlABC 3) Sat - , goldenCapturedIO "concreteReverse" $ \rf -> checkWith z3{redirectVerbose=Just rf} concreteReverseSat Sat - , goldenCapturedIO "reverse" $ \rf -> checkWith z3{redirectVerbose=Just rf} reverseSat Sat - , goldenCapturedIO "reverseAlt10" $ \rf -> checkWith z3{redirectVerbose=Just rf} (reverseAlt 10) Unsat - , goldenCapturedIO "concreteSort" $ \rf -> checkWith z3{redirectVerbose=Just rf} concreteSortSat Sat - , goldenCapturedIO "sort" $ \rf -> checkWith z3{redirectVerbose=Just rf} sortSat Sat - , goldenCapturedIO "mapWithFailure" $ \rf -> checkWith z3{redirectVerbose=Just rf} mapWithFailure Sat - , goldenCapturedIO "mapNoFailure" $ \rf -> checkWith z3{redirectVerbose=Just rf} mapNoFailure Unsat - , goldenCapturedIO "maxlWithFailure" $ \rf -> checkWith z3{redirectVerbose=Just rf} maxlWithFailure Sat - , goldenCapturedIO "maxrWithFailure" $ \rf -> checkWith z3{redirectVerbose=Just rf} maxrWithFailure Sat - ] - -checkWith :: SMTConfig -> Symbolic () -> CheckSatResult -> IO () -checkWith cfg props csExpected = runSMTWith cfg{verbose=True} $ do - _ <- props - query $ do cs <- checkSat - unless (cs == csExpected) $ - case cs of - Unsat -> error $ "Failed! Expected " ++ show csExpected ++ ", got Unsat" - DSat{} -> error $ "Failed! Expected " ++ show csExpected ++ ", got delta-sat" - Sat -> getModel >>= \r -> error $ "Failed! Expected " ++ show csExpected ++ ", got Sat:\n" ++ show (SatResult (Satisfiable cfg r)) - Unk -> getUnknownReason >>= \r -> error $ "Failed! Expected " ++ show csExpected ++ ", got Unk:\n" ++ show r - -concreteFoldrSat :: Symbolic () -concreteFoldrSat = constrain $ BL.bfoldr 3 (+) 0 [1..3] .== (6 :: SInteger) - -concreteFoldlSat :: Symbolic () -concreteFoldlSat = constrain $ BL.bfoldl 10 (+) 0 [1..3] .== (6 :: SInteger) - --- unsatisfiable at bound = 1, satisfiable at bound = 2 or bound = 3 -foldrAB :: Int -> Symbolic () -foldrAB bound = do - [a, b] <- sIntegers ["a", "b"] - constrain $ a .> 0 - constrain $ b .> 0 - constrain $ BL.bfoldr bound (+) 0 (L.implode [a, b]) .== a + b - --- unsatisfiable at bound = 1 or bound = 2, satisfiable at bound = 3 -foldlABC :: Int -> Symbolic () -foldlABC bound = do - [a, b, c] <- sIntegers ["a", "b", "c"] - constrain $ a .> 0 - constrain $ b .> 0 - constrain $ c .> 0 - constrain $ BL.bfoldr bound (+) 0 (L.implode [a, b, c]) .== a + b + c - -concreteReverseSat :: Symbolic () -concreteReverseSat = constrain $ BL.breverse 10 [1..10] .== ([10,9..1] :: SList Integer) - -reverseSat :: Symbolic () -reverseSat = do - abcd <- sIntegers ["a", "b", "c", "d"] - constrain $ BL.breverse 10 (L.implode abcd) .== L.implode (reverse abcd) - -reverseAlt :: Int -> Symbolic () -reverseAlt i = do - xs <- sList "xs" - - -- Assert the negation; so Unsat response means it's all good! - constrain $ BL.breverse i xs ./= rev i xs ([] :: SList Integer) - where -- classic reverse with accumulator - rev 0 _ sofar = sofar - rev c xs sofar = ite (L.null xs) - sofar - (rev (c-1) (L.tail xs) (L.head xs .: sofar)) - - -concreteSortSat :: Symbolic () -concreteSortSat = constrain $ BL.bsort 10 [5,6,3,8,9,2,1,7,10,4] .== ([1..10] :: SList Integer) - -sortSat :: Symbolic () -sortSat = do [a, b, c] <- sIntegers ["a", "b", "c"] - - let sorted = BL.bsort 3 $ L.implode [a, b, c] - - ordered :: (SInteger, SInteger, SInteger) -> SBool - ordered (x, y, z) = x .<= y .&& y .<= z - - constrain $ ordered (a, b, c) .=> sorted .== L.implode [a, b, c] - constrain $ ordered (a, c, b) .=> sorted .== L.implode [a, c, b] - constrain $ ordered (b, a, c) .=> sorted .== L.implode [b, a, c] - constrain $ ordered (b, c, a) .=> sorted .== L.implode [b, c, a] - constrain $ ordered (c, a, b) .=> sorted .== L.implode [c, a, b] - constrain $ ordered (c, b, a) .=> sorted .== L.implode [c, b, a] - --- | Increment, failing if a value lies outside of [0, 10] -boundedIncr :: SList Integer -> Eval (SList Integer) -boundedIncr = BL.bmapM 10 $ \i -> do - markFailure $ i .< 0 .|| i .> 10 - pure $ i + 1 - --- | Max (based on foldr), failing if a value lies outside of [0, 10] -boundedMaxr :: SList Integer -> Eval SInteger -boundedMaxr = BL.bfoldrM 10 - (\i maxi -> do - markFailure $ i .< 0 .|| i .> 10 - pure $ smax i maxi) - 0 - --- | Max (based on foldl), failing if a value lies outside of [0, 10] -boundedMaxl :: SList Integer -> Eval SInteger -boundedMaxl = BL.bfoldlM 10 - (\maxi i -> do - markFailure $ i .< 0 .|| i .> 10 - pure $ smax i maxi) - 0 - --- the mapping will have failed if one of the resulting values is greater than --- 11 -mapWithFailure :: Symbolic () -mapWithFailure = do - lst <- sList "ints" - let (lst', failure) = runEval $ boundedIncr lst - constrain $ lst' !! 2 .> 11 .=> failure .== Failure sTrue - --- mapping over these values of a, b, and c cannot fail (this is unsat) -mapNoFailure :: Symbolic () -mapNoFailure = do - [a, b, c] <- sIntegers ["a", "b", "c"] - let (_lst', Failure failure) = runEval $ boundedIncr $ L.implode [a, b, c] - constrain $ a + b + c .== 6 - constrain $ a .> 0 .&& b .> 0 .&& c .> 0 - constrain failure - --- boundedMaxl fails if one of the values is too big -maxlWithFailure :: Symbolic () -maxlWithFailure = do - lst <- sList "ints" - let (maxi, Failure failure) = runEval $ boundedMaxl lst - constrain $ maxi .> 10 .=> failure - --- boundedMaxl fails if one of the values is too big -maxrWithFailure :: Symbolic () -maxrWithFailure = do - lst <- sList "ints" - let (maxi, Failure failure) = runEval $ boundedMaxr lst - constrain $ maxi .> 10 .=> failure From b88dabe853893f249c77be89e8132698a3bbcdef Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 23 Dec 2024 11:50:36 -0800 Subject: [PATCH 7/9] pass allow-newer to more cabal targets --- Makefile | 33 ++++++++++++++++++--------------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/Makefile b/Makefile index 3766c306..3d49ce1b 100644 --- a/Makefile +++ b/Makefile @@ -45,15 +45,18 @@ endif # How long to wait for each doctest to run (in seconds) DOCTESTTIMEOUT = 300 +# Allow newer versions +CABAL_OPTS=--allow-newer + .PHONY: install docs testsuite release tags clean veryclean timeRelease all: quick quick: tags - @$(TIME) cabal new-install --lib --allow-newer --force-reinstalls + @$(TIME) cabal new-install --lib ${CABAL_OPTS} --force-reinstalls install: tags - @$(TIME) cabal new-configure --enable-tests --allow-newer --ghc-options=$(CONFIGOPTS) + @$(TIME) cabal new-configure --enable-tests ${CABAL_OPTS} --ghc-options=$(CONFIGOPTS) @$(TIME) cabal new-install --lib --force-reinstalls docs: @@ -66,38 +69,38 @@ hackage-docs: @echo " cabal upload -d --publish ./dist-newstyle/sbv-XXX-docs.tar.gz" ghci: - cabal new-repl --repl-options=-Wno-unused-packages + cabal new-repl ${CABAL_OPTS} --repl-options=-Wno-unused-packages ghcid: ifdef TGT - ghcid --command="cabal new-repl --repl-options=-Wno-unused-packages" -T $(subst /,.,${TGT}) + ghcid --command="cabal new-repl ${CABAL_OPTS} --repl-options=-Wno-unused-packages" -T $(subst /,.,${TGT}) else - ghcid --command="cabal new-repl --repl-options=-Wno-unused-packages" + ghcid --command="cabal new-repl ${CABAL_OPTS} --repl-options=-Wno-unused-packages" endif ghci_SBVTest: - cabal new-repl --repl-options=-Wno-unused-packages SBVTest + cabal new-repl ${CABAL_OPTS} --repl-options=-Wno-unused-packages SBVTest ghcid_SBVTest: - ghcid --command="cabal new-repl --repl-options=-Wno-unused-packages SBVTest" + ghcid --command="cabal new-repl ${CABAL_OPTS} --repl-options=-Wno-unused-packages SBVTest" ghci_SBVDocTest: - cabal new-repl --repl-options=-Wno-unused-packages SBVDocTest + cabal new-repl ${CABAL_OPTS} --repl-options=-Wno-unused-packages SBVDocTest ghcid_SBVDocTest: - ghcid --command="cabal new-repl --repl-options=-Wno-unused-packages SBVDocTest" + ghcid --command="cabal new-repl ${CABAL_OPTS} --repl-options=-Wno-unused-packages SBVDocTest" ghci_HLint: - cabal new-repl --repl-options=-Wno-unused-packages SBVHLint + cabal new-repl ${CABAL_OPTS} --repl-options=-Wno-unused-packages SBVHLint ghcid_HLint: - ghcid --command="cabal new-repl --repl-options=-Wno-unused-packages SBVHLint" + ghcid --command="cabal new-repl ${CABAL_OPTS} --repl-options=-Wno-unused-packages SBVHLint" ghci_Bench: - cabal new-repl --repl-options=-Wno-unused-packages SBVBench + cabal new-repl ${CABAL_OPTS} --repl-options=-Wno-unused-packages SBVBench ghcid_Bench: - ghcid --command="cabal new-repl --repl-options=-Wno-unused-packages SBVBench" + ghcid --command="cabal new-repl ${CABAL_OPTS} --repl-options=-Wno-unused-packages SBVBench" bench: cabal new-bench @@ -137,10 +140,10 @@ ifdef TGT ifdef FAST cabal-docspec --timeout ${DOCTESTTIMEOUT} --module $(basename $(subst /,.,${TGT})) else - cabal new-run SBVDocTest --allow-newer -- --timeout ${DOCTESTTIMEOUT} --module $(basename $(subst /,.,${TGT})) + cabal new-run SBVDocTest ${CABAL_OPTS} -- --timeout ${DOCTESTTIMEOUT} --module $(basename $(subst /,.,${TGT})) endif else - @$(TIME) cabal new-run SBVDocTest --allow-newer -- --timeout ${DOCTESTTIMEOUT} + @$(TIME) cabal new-run SBVDocTest ${CABAL_OPTS} -- --timeout ${DOCTESTTIMEOUT} endif test: From 69542deb7a2626bec6833461fb7234d4c3c308a1 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 23 Dec 2024 11:51:31 -0800 Subject: [PATCH 8/9] Remove boundedfix and boundedlist These are relatively unused and more or less obsolete with support for recursive functions and proper sequences --- CHANGES.md | 5 ++ Data/SBV/Tools/BoundedFix.hs | 88 -------------------- Data/SBV/Tools/BoundedList.hs | 150 ---------------------------------- sbv.cabal | 3 - 4 files changed, 5 insertions(+), 241 deletions(-) delete mode 100644 Data/SBV/Tools/BoundedFix.hs delete mode 100644 Data/SBV/Tools/BoundedList.hs diff --git a/CHANGES.md b/CHANGES.md index 8db8b405..64f24af1 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -19,6 +19,11 @@ * [BACKWARDS COMPATIBILITY] Removed rarely used functions mapi, foldli, foldri from Data.SBV.List. These can now be defined by the user as we have proper support for fold and map using lambdas. + * [BACKWARDS COMPATIBILITY] Removed "Data/SBV/Tools/BoundedFix.hs", and "Data/SBV/Tools/BoundedList.hs", which + were relatively unused and are more or less obsolete with SBV's new support for sequences and recursive + functions. If you were using these functions you could easily recreate them. Please get in touch if you + need this old functionality. + ### Version 11.0, 2024-11-06 * [BACKWARDS COMPATIBILITY] SBV now handles arrays in a much more uniform way, unifying diff --git a/Data/SBV/Tools/BoundedFix.hs b/Data/SBV/Tools/BoundedFix.hs deleted file mode 100644 index 0336015b..00000000 --- a/Data/SBV/Tools/BoundedFix.hs +++ /dev/null @@ -1,88 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : Data.SBV.Tools.BoundedFix --- Copyright : (c) Levent Erkok --- License : BSD3 --- Maintainer: erkokl@gmail.com --- Stability : experimental --- --- Bounded fixed-point unrolling. ------------------------------------------------------------------------------ - -{-# LANGUAGE FlexibleContexts #-} - -{-# OPTIONS_GHC -Wall -Werror #-} - -module Data.SBV.Tools.BoundedFix ( - bfix - ) where - -import Data.SBV - --- $setup --- >>> -- For doctest purposes only: --- >>> import Data.SBV --- >>> bfac = bfix 10 "fac" fact where fact f n = ite (n .== 0) 1 ((n :: SInteger) * f (n-1)) - --- | Bounded fixed-point operation. The call @bfix bnd nm f@ unrolls the recursion in @f@ at most --- @bnd@ times, and uninterprets the function (with the name @nm@) after the bound is reached. --- --- This combinator is handy for dealing with recursive definitions that are not symbolically terminating --- and when the property we are interested in does not require an infinite unrolling, or when we are happy --- with a bounded proof. In particular, this operator can be used as a basis of software-bounded model --- checking algorithms built on top of SBV. The bound can be successively refined in a CEGAR like loop --- as necessary, by analyzing the counter-examples and rejecting them if they are false-negatives. --- --- For instance, we can define the factorial function using the bounded fixed-point operator like this: --- --- @ --- bfac :: SInteger -> SInteger --- bfac = bfix 10 "fac" fact --- where fact f n = ite (n .== 0) 1 (n * f (n-1)) --- @ --- --- This definition unrolls the recursion in factorial at most 10 times before uninterpreting the result. --- We can now prove: --- --- >>> prove $ \n -> n .>= 1 .&& n .<= 9 .=> bfac n .== n * bfac (n-1) --- Q.E.D. --- --- And we would get a bogus counter-example if the proof of our property needs a larger bound: --- --- >>> prove $ \n -> n .== 10 .=> bfac n .== 3628800 --- Falsifiable. Counter-example: --- s0 = 10 :: Integer --- --- fac :: Integer -> Integer --- fac _ = 2 --- --- The counter-example is telling us how it instantiated the function @fac@ when the recursion --- bottomed out: It simply made it return @2@ for all arguments at that point, which provides --- the (unintended) counter-example. --- --- By design, if a function defined via `bfix` is given a concrete argument, it will unroll --- the recursion as much as necessary to complete the call (which can of course diverge). The bound --- only applies if the given argument is symbolic. This fact can be used to observe concrete --- values to see where the bounded-model-checking approach fails: --- --- >>> prove $ \n -> n .== 10 .=> observe "bfac_n" (bfac n) .== observe "bfac_10" (bfac 10) --- Falsifiable. Counter-example: --- bfac_10 = 3628800 :: Integer --- bfac_n = 7257600 :: Integer --- s0 = 10 :: Integer --- --- fac :: Integer -> Integer --- fac _ = 2 --- --- Here, we see further evidence that the SMT solver must have decided to assign the --- value @2@ in the final call just as it was reaching the base case, and thus got the --- final result incorrect. (Note that @7257600 = 2 * 3628800@.) A wrapper algorithm can --- then assert the actual value of @bfac 10@ here as an extra constraint and can --- search for "deeper bugs." -bfix :: (SymVal a, SMTDefinable (SBV a -> r)) => Int -> String -> ((SBV a -> r) -> (SBV a -> r)) -> SBV a -> r -bfix bound nm f x - | isConcrete x = g x - | True = unroll bound x - where g = f g - unroll 0 = uninterpret nm - unroll i = f (unroll (i-1)) diff --git a/Data/SBV/Tools/BoundedList.hs b/Data/SBV/Tools/BoundedList.hs deleted file mode 100644 index f22a419e..00000000 --- a/Data/SBV/Tools/BoundedList.hs +++ /dev/null @@ -1,150 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : Data.SBV.Tools.BoundedList --- Copyright : (c) Levent Erkok --- License : BSD3 --- Maintainer: erkokl@gmail.com --- Stability : experimental --- --- A collection of bounded list utilities, useful when working with symbolic lists. --- These functions all take a concrete bound, and operate on the prefix of a symbolic --- list that is at most that long. Due to limitations on writing recursive functions --- over lists (the classic symbolic termination problem), we cannot write arbitrary --- recursive programs on symbolic lists. But most of the time all we need is a --- bounded prefix of this list, at which point these functions come in handy. ------------------------------------------------------------------------------ - -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE OverloadedLists #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE ScopedTypeVariables #-} - -{-# OPTIONS_GHC -Wall -Werror #-} - -module Data.SBV.Tools.BoundedList ( - -- * General folds - bfoldr, bfoldrM, bfoldl, bfoldlM - -- * Map, filter, zipWith, elem - , bmap, bmapM, bfilter, bzipWith, belem - -- * Aggregates - , bsum, bprod, band, bor, bany, ball, bmaximum, bminimum - -- * Miscellaneous: Reverse and sort - , breverse, bsort - ) - where - -import Prelude hiding ((++)) - -import Data.SBV -import Data.SBV.List ((.:), (++)) -import qualified Data.SBV.List as L - --- | Case analysis on a symbolic list. (Not exported.) -lcase :: (SymVal a, Mergeable b) => SList a -> b -> (SBV a -> SList a -> b) -> b -lcase s e c = ite (L.null s) e (c (L.head s) (L.tail s)) - --- | Bounded fold from the right. -bfoldr :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b -bfoldr cnt f b = go (cnt `max` 0) - where go 0 _ = b - go i s = lcase s b (\h t -> h `f` go (i-1) t) - --- | Bounded monadic fold from the right. -bfoldrM :: forall a b m. (SymVal a, SymVal b, Monad m, Mergeable (m (SBV b))) - => Int -> (SBV a -> SBV b -> m (SBV b)) -> SBV b -> SList a -> m (SBV b) -bfoldrM cnt f b = go (cnt `max` 0) - where go :: Int -> SList a -> m (SBV b) - go 0 _ = return b - go i s = lcase s (return b) (\h t -> f h =<< go (i-1) t) - --- | Bounded fold from the left. -bfoldl :: (SymVal a, SymVal b) => Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b -bfoldl cnt f = go (cnt `max` 0) - where go 0 b _ = b - go i b s = lcase s b (\h t -> go (i-1) (b `f` h) t) - --- | Bounded monadic fold from the left. -bfoldlM :: forall a b m. (SymVal a, SymVal b, Monad m, Mergeable (m (SBV b))) - => Int -> (SBV b -> SBV a -> m (SBV b)) -> SBV b -> SList a -> m (SBV b) -bfoldlM cnt f = go (cnt `max` 0) - where go :: Int -> SBV b -> SList a -> m (SBV b) - go 0 b _ = return b - go i b s = lcase s (return b) (\h t -> do { fbh <- f b h; go (i-1) fbh t }) - --- | Bounded sum. -bsum :: (SymVal a, Num a, Num (SBV a), Ord a) => Int -> SList a -> SBV a -bsum i = bfoldl i (+) 0 - --- | Bounded product. -bprod :: (SymVal a, Num a, Num (SBV a), Ord a) => Int -> SList a -> SBV a -bprod i = bfoldl i (*) 1 - --- | Bounded map. -bmap :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV b) -> SList a -> SList b -bmap i f = bfoldr i (\x -> (f x .:)) [] - --- | Bounded monadic map. -bmapM :: (SymVal a, SymVal b, Monad m, Mergeable (m (SBV [b]))) - => Int -> (SBV a -> m (SBV b)) -> SList a -> m (SList b) -bmapM i f = bfoldrM i (\a bs -> (.:) <$> f a <*> pure bs) [] - --- | Bounded filter. -bfilter :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SList a -bfilter i f = bfoldr i (\x y -> ite (f x) (x .: y) y) [] - --- | Bounded logical and -band :: Int -> SList Bool -> SBool -band i = bfoldr i (.&&) (sTrue :: SBool) - --- | Bounded logical or -bor :: Int -> SList Bool -> SBool -bor i = bfoldr i (.||) (sFalse :: SBool) - --- | Bounded any -bany :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool -bany i f = bor i . bmap i f - --- | Bounded all -ball :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool -ball i f = band i . bmap i f - --- | Bounded maximum. Undefined if list is empty. -bmaximum :: (Ord a, SymVal a) => Int -> SList a -> SBV a -bmaximum i l = bfoldl (i-1) smax (L.head l) (L.tail l) - --- | Bounded minimum. Undefined if list is empty. -bminimum :: (Ord a, SymVal a) => Int -> SList a -> SBV a -bminimum i l = bfoldl (i-1) smin (L.head l) (L.tail l) - --- | Bounded zipWith -bzipWith :: (SymVal a, SymVal b, SymVal c) => Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c -bzipWith cnt f = go (cnt `max` 0) - where go 0 _ _ = [] - go i xs ys = ite (L.null xs .|| L.null ys) - [] - (f (L.head xs) (L.head ys) .: go (i-1) (L.tail xs) (L.tail ys)) - --- | Bounded element check -belem :: (Eq a, SymVal a) => Int -> SBV a -> SList a -> SBool -belem i e = bany i (e .==) - --- | Bounded reverse -breverse :: SymVal a => Int -> SList a -> SList a -breverse cnt = bfoldr cnt (\a b -> b ++ L.singleton a) [] - --- | Bounded paramorphism (not exported). -bpara :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV [a] -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b -bpara cnt f b = go (cnt `max` 0) - where go 0 _ = b - go i s = lcase s b (\h t -> f h t (go (i-1) t)) - --- | Insert an element into a sorted list (not exported). -binsert :: (Ord a, SymVal a) => Int -> SBV a -> SList a -> SList a -binsert cnt a = bpara cnt f (L.singleton a) - where f sortedHd sortedTl sortedTl' = ite (a .< sortedHd) - (a .: sortedHd .: sortedTl) - (sortedHd .: sortedTl') - --- | Bounded insertion sort -bsort :: (Ord a, SymVal a) => Int -> SList a -> SList a -bsort cnt = bfoldr cnt (binsert cnt) [] diff --git a/sbv.cabal b/sbv.cabal index 81090daf..94728602 100644 --- a/sbv.cabal +++ b/sbv.cabal @@ -121,10 +121,8 @@ Library , Data.SBV.Tuple , Data.SBV.RegExp , Data.SBV.Tools.BMC - , Data.SBV.Tools.BoundedList , Data.SBV.Tools.BVOptimize , Data.SBV.Tools.Induction - , Data.SBV.Tools.BoundedFix , Data.SBV.Tools.CodeGen , Data.SBV.Tools.GenTest , Data.SBV.Tools.KnuckleDragger @@ -321,7 +319,6 @@ Test-Suite SBVTest , TestSuite.Basics.Assert , TestSuite.Basics.BarrelRotate , TestSuite.Basics.BasicTests - , TestSuite.Basics.BoundedList , TestSuite.Basics.DynSign , TestSuite.Basics.EqSym , TestSuite.Basics.Exceptions From c1d251ff4ed409499e3641f25d98059dfe1a2a46 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 23 Dec 2024 11:51:56 -0800 Subject: [PATCH 9/9] Rewrite this example to use regular lists --- .../SBV/Examples/Lists/BoundedMutex.hs | 28 +++++++++---------- 1 file changed, 13 insertions(+), 15 deletions(-) diff --git a/Documentation/SBV/Examples/Lists/BoundedMutex.hs b/Documentation/SBV/Examples/Lists/BoundedMutex.hs index c386024e..3264b1f0 100644 --- a/Documentation/SBV/Examples/Lists/BoundedMutex.hs +++ b/Documentation/SBV/Examples/Lists/BoundedMutex.hs @@ -6,8 +6,7 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental -- --- Demonstrates use of bounded list utilities, proving a simple --- mutex algorithm correct up to given bounds. +-- Proves a simple mutex algorithm correct up to a given bound. ----------------------------------------------------------------------------- {-# LANGUAGE DeriveAnyClass #-} @@ -27,8 +26,7 @@ import Data.SBV.Control import Prelude hiding ((!!)) import Data.SBV.List ((!!)) -import qualified Data.SBV.List as L -import qualified Data.SBV.Tools.BoundedList as L +import qualified Data.SBV.List as L -- | Each agent can be in one of the three states data State = Idle -- ^ Regular work @@ -38,10 +36,10 @@ data State = Idle -- ^ Regular work -- | Make 'State' a symbolic enumeration mkSymbolicEnumeration ''State --- | A bounded mutex property holds for two sequences of state transitions, if they are not in --- their critical section at the same time up to that given bound. -mutex :: Int -> SList State -> SList State -> SBool -mutex i p1s p2s = L.band i $ L.bzipWith i (\p1 p2 -> p1 ./= sCritical .|| p2 ./= sCritical) p1s p2s +-- | The mutex property holds for two sequences of state transitions, if they are not in +-- their critical section at the same time. +mutex :: SList State -> SList State -> SBool +mutex p1s p2s = L.and $ L.zipWith (\p1 p2 -> p1 ./= sCritical .|| p2 ./= sCritical) p1s p2s -- | A sequence is valid upto a bound if it starts at 'Idle', and follows the mutex rules. That is: -- @@ -100,7 +98,7 @@ checkMutex b = runSMT $ do -- Try to assert that mutex does not hold. If we get a -- counter example, we would've found a violation! - constrain $ sNot $ mutex b p1 p2 + constrain $ sNot $ mutex p1 p2 query $ do cs <- checkSat case cs of @@ -121,11 +119,11 @@ checkMutex b = runSMT $ do -- trying to show a bounded trace of length 10, such that the second process is ready but -- never transitions to critical. We have: -- --- > ghci> notFair 10 --- > Fairness is violated at bound: 10 --- > P1: [Idle,Idle,Ready,Critical,Idle,Idle,Ready,Critical,Idle,Idle] --- > P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready] --- > Ts: [1,2,1,1,1,1,1,1,1,1] +-- >>> notFair 10 +-- Fairness is violated at bound: 10 +-- P1: [Idle,Ready,Critical,Critical,Critical,Critical,Critical,Idle,Idle,Idle] +-- P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready] +-- Ts: [1,1,1,1,1,1,1,1,1,1] -- -- As expected, P2 gets ready but never goes critical since the arbiter keeps picking -- P1 unfairly. (You might get a different trace depending on what z3 happens to produce!) @@ -148,7 +146,7 @@ notFair b = runSMT $ do p1 :: SList State <- sList "p1" -- Find a trace where p2 never goes critical -- counter example, we would've found a violation! - constrain $ sNot $ L.belem b sCritical p2 + constrain $ sNot $ sCritical `L.elem` p2 query $ do cs <- checkSat case cs of