Skip to content

Commit

Permalink
Update golds to match the new higher-order output syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
@LeventErkok
LeventErkok committed Nov 30, 2024
1 parent e41bbeb commit dcda373
Show file tree
Hide file tree
Showing 6 changed files with 170 additions and 150 deletions.
50 changes: 27 additions & 23 deletions SBVTestSuite/GoldFiles/lambda27.gold
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
[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] (set-logic ALL) ; has lambda expressions, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
Expand All @@ -20,31 +20,35 @@
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- SBV Function definitions
[GOOD] (define-fun-rec |sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| ((lst (Seq Int))) Bool
(ite (= lst (as seq.empty (Seq Int)))
true
(and (select (lambda ((l1_s0 Int))
(let ((l1_s1 2))
(let ((l1_s3 0))
(let ((l1_s7 1))
(let ((l1_s13 (- 1)))
(let ((l1_s2 (mod l1_s0 l1_s1)))
(let ((l1_s4 (>= l1_s0 l1_s3)))
(let ((l1_s5 (= l1_s2 l1_s3)))
(let ((l1_s6 (or l1_s4 l1_s5)))
(let ((l1_s8 (ite l1_s6 l1_s3 l1_s7)))
(let ((l1_s9 (* l1_s1 l1_s8)))
(let ((l1_s10 (- l1_s2 l1_s9)))
(let ((l1_s11 (> l1_s10 l1_s3)))
(let ((l1_s12 (< l1_s10 l1_s3)))
(let ((l1_s14 (ite l1_s12 l1_s13 l1_s10)))
(let ((l1_s15 (ite l1_s11 l1_s7 l1_s14)))
(let ((l1_s16 (= l1_s13 l1_s15)))
(let ((l1_s17 (+ l1_s1 l1_s10)))
(let ((l1_s18 (ite l1_s16 l1_s17 l1_s10)))
(let ((l1_s19 (= l1_s3 l1_s18)))
l1_s19)))))))))))))))))))) (seq.nth lst 0)) (|sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1))))))
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s3 () Bool (= s0 s2))
[GOOD] (define-fun s4 () Bool (seq.foldl (lambda ((l1_s0 Bool) (l1_s1 Int))
(let ((l1_s2 2))
(let ((l1_s4 0))
(let ((l1_s8 1))
(let ((l1_s14 (- 1)))
(let ((l1_s3 (mod l1_s1 l1_s2)))
(let ((l1_s5 (>= l1_s1 l1_s4)))
(let ((l1_s6 (= l1_s3 l1_s4)))
(let ((l1_s7 (or l1_s5 l1_s6)))
(let ((l1_s9 (ite l1_s7 l1_s4 l1_s8)))
(let ((l1_s10 (* l1_s2 l1_s9)))
(let ((l1_s11 (- l1_s3 l1_s10)))
(let ((l1_s12 (> l1_s11 l1_s4)))
(let ((l1_s13 (< l1_s11 l1_s4)))
(let ((l1_s15 (ite l1_s13 l1_s14 l1_s11)))
(let ((l1_s16 (ite l1_s12 l1_s8 l1_s15)))
(let ((l1_s17 (= l1_s14 l1_s16)))
(let ((l1_s18 (+ l1_s2 l1_s11)))
(let ((l1_s19 (ite l1_s17 l1_s18 l1_s11)))
(let ((l1_s20 (= l1_s4 l1_s19)))
(let ((l1_s21 (and l1_s0 l1_s20)))
l1_s21))))))))))))))))))))) true s0))
[GOOD] (define-fun s4 () Bool (|sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| s0))
[GOOD] (define-fun s5 () Bool (= s1 s4))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
Expand Down
50 changes: 27 additions & 23 deletions SBVTestSuite/GoldFiles/lambda28.gold
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
[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] (set-logic ALL) ; has lambda expressions, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
Expand All @@ -20,31 +20,35 @@
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- SBV Function definitions
[GOOD] (define-fun-rec |sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| ((lst (Seq Int))) Bool
(ite (= lst (as seq.empty (Seq Int)))
true
(and (select (lambda ((l1_s0 Int))
(let ((l1_s1 2))
(let ((l1_s3 0))
(let ((l1_s7 1))
(let ((l1_s13 (- 1)))
(let ((l1_s2 (mod l1_s0 l1_s1)))
(let ((l1_s4 (>= l1_s0 l1_s3)))
(let ((l1_s5 (= l1_s2 l1_s3)))
(let ((l1_s6 (or l1_s4 l1_s5)))
(let ((l1_s8 (ite l1_s6 l1_s3 l1_s7)))
(let ((l1_s9 (* l1_s1 l1_s8)))
(let ((l1_s10 (- l1_s2 l1_s9)))
(let ((l1_s11 (> l1_s10 l1_s3)))
(let ((l1_s12 (< l1_s10 l1_s3)))
(let ((l1_s14 (ite l1_s12 l1_s13 l1_s10)))
(let ((l1_s15 (ite l1_s11 l1_s7 l1_s14)))
(let ((l1_s16 (= l1_s13 l1_s15)))
(let ((l1_s17 (+ l1_s1 l1_s10)))
(let ((l1_s18 (ite l1_s16 l1_s17 l1_s10)))
(let ((l1_s19 (= l1_s3 l1_s18)))
l1_s19)))))))))))))))))))) (seq.nth lst 0)) (|sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1))))))
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s3 () Bool (= s0 s2))
[GOOD] (define-fun s4 () Bool (seq.foldl (lambda ((l1_s0 Bool) (l1_s1 Int))
(let ((l1_s2 2))
(let ((l1_s4 0))
(let ((l1_s8 1))
(let ((l1_s14 (- 1)))
(let ((l1_s3 (mod l1_s1 l1_s2)))
(let ((l1_s5 (>= l1_s1 l1_s4)))
(let ((l1_s6 (= l1_s3 l1_s4)))
(let ((l1_s7 (or l1_s5 l1_s6)))
(let ((l1_s9 (ite l1_s7 l1_s4 l1_s8)))
(let ((l1_s10 (* l1_s2 l1_s9)))
(let ((l1_s11 (- l1_s3 l1_s10)))
(let ((l1_s12 (> l1_s11 l1_s4)))
(let ((l1_s13 (< l1_s11 l1_s4)))
(let ((l1_s15 (ite l1_s13 l1_s14 l1_s11)))
(let ((l1_s16 (ite l1_s12 l1_s8 l1_s15)))
(let ((l1_s17 (= l1_s14 l1_s16)))
(let ((l1_s18 (+ l1_s2 l1_s11)))
(let ((l1_s19 (ite l1_s17 l1_s18 l1_s11)))
(let ((l1_s20 (= l1_s4 l1_s19)))
(let ((l1_s21 (and l1_s0 l1_s20)))
l1_s21))))))))))))))))))))) true s0))
[GOOD] (define-fun s4 () Bool (|sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| s0))
[GOOD] (define-fun s5 () Bool (= s1 s4))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
Expand Down
50 changes: 27 additions & 23 deletions SBVTestSuite/GoldFiles/lambda29.gold
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
[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] (set-logic ALL) ; has lambda expressions, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
Expand All @@ -20,31 +20,35 @@
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- SBV Function definitions
[GOOD] (define-fun-rec |sbv.seqAny_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(distinct_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| ((lst (Seq Int))) Bool
(ite (= lst (as seq.empty (Seq Int)))
false
(or (select (lambda ((l1_s0 Int))
(let ((l1_s1 2))
(let ((l1_s3 0))
(let ((l1_s7 1))
(let ((l1_s13 (- 1)))
(let ((l1_s2 (mod l1_s0 l1_s1)))
(let ((l1_s4 (>= l1_s0 l1_s3)))
(let ((l1_s5 (= l1_s2 l1_s3)))
(let ((l1_s6 (or l1_s4 l1_s5)))
(let ((l1_s8 (ite l1_s6 l1_s3 l1_s7)))
(let ((l1_s9 (* l1_s1 l1_s8)))
(let ((l1_s10 (- l1_s2 l1_s9)))
(let ((l1_s11 (> l1_s10 l1_s3)))
(let ((l1_s12 (< l1_s10 l1_s3)))
(let ((l1_s14 (ite l1_s12 l1_s13 l1_s10)))
(let ((l1_s15 (ite l1_s11 l1_s7 l1_s14)))
(let ((l1_s16 (= l1_s13 l1_s15)))
(let ((l1_s17 (+ l1_s1 l1_s10)))
(let ((l1_s18 (ite l1_s16 l1_s17 l1_s10)))
(let ((l1_s19 (distinct l1_s3 l1_s18)))
l1_s19)))))))))))))))))))) (seq.nth lst 0)) (|sbv.seqAny_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(distinct_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1))))))
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s3 () Bool (= s0 s2))
[GOOD] (define-fun s4 () Bool (seq.foldl (lambda ((l1_s0 Bool) (l1_s1 Int))
(let ((l1_s2 2))
(let ((l1_s4 0))
(let ((l1_s8 1))
(let ((l1_s14 (- 1)))
(let ((l1_s3 (mod l1_s1 l1_s2)))
(let ((l1_s5 (>= l1_s1 l1_s4)))
(let ((l1_s6 (= l1_s3 l1_s4)))
(let ((l1_s7 (or l1_s5 l1_s6)))
(let ((l1_s9 (ite l1_s7 l1_s4 l1_s8)))
(let ((l1_s10 (* l1_s2 l1_s9)))
(let ((l1_s11 (- l1_s3 l1_s10)))
(let ((l1_s12 (> l1_s11 l1_s4)))
(let ((l1_s13 (< l1_s11 l1_s4)))
(let ((l1_s15 (ite l1_s13 l1_s14 l1_s11)))
(let ((l1_s16 (ite l1_s12 l1_s8 l1_s15)))
(let ((l1_s17 (= l1_s14 l1_s16)))
(let ((l1_s18 (+ l1_s2 l1_s11)))
(let ((l1_s19 (ite l1_s17 l1_s18 l1_s11)))
(let ((l1_s20 (distinct l1_s4 l1_s19)))
(let ((l1_s21 (or l1_s0 l1_s20)))
l1_s21))))))))))))))))))))) false s0))
[GOOD] (define-fun s4 () Bool (|sbv.seqAny_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(distinct_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| s0))
[GOOD] (define-fun s5 () Bool (= s1 s4))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
Expand Down
Loading

0 comments on commit dcda373

Please sign in to comment.