Emit the special functions in the correct order

LeventErkok · Dec 1, 2024 · 016c6f1 · 016c6f1
1 parent 1e6e998
commit 016c6f1
Show file tree

Hide file tree

Showing 6 changed files with 47 additions and 33 deletions.
diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs
@@ -256,7 +256,7 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs
              ++ [ "; --- uninterpreted constants ---" ]
              ++ concatMap (declUI curProgInfo) uis
              ++ [ "; --- SBV Function definitions" | not (null specialFuncs) ]
-             ++ concat [declSBVFunc cfg op | op <- specialFuncs]
+             ++ concat [declSBVFunc cfg op | op <- reverse specialFuncs]
              ++ [ "; --- user defined functions ---"]
              ++ userDefs
              ++ [ "; --- assignments ---" ]

diff --git a/SBVTestSuite/GoldFiles/lambda05.gold b/SBVTestSuite/GoldFiles/lambda05.gold
@@ -21,22 +21,22 @@
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_1))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| ((lst (Seq Int))) (Seq Int)
+[GOOD] (define-fun-rec |sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| ((lst (Seq Int))) (Seq Int)
                      (ite (= lst (as seq.empty (Seq Int)))
                           (as seq.empty (Seq Int))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 Int))
-                                 (let ((l1_s1 1))
+                                 (let ((l1_s1 2))
                                  (let ((l1_s2 (+ l1_s0 l1_s1)))
                                  l1_s2))) (seq.nth lst 0)))
-                                  (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_1))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
-[GOOD] (define-fun-rec |sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| ((lst (Seq Int))) (Seq Int)
+                                  (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
+[GOOD] (define-fun-rec |sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_1))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| ((lst (Seq Int))) (Seq Int)
                      (ite (= lst (as seq.empty (Seq Int)))
                           (as seq.empty (Seq Int))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 Int))
-                                 (let ((l1_s1 2))
+                                 (let ((l1_s1 1))
                                  (let ((l1_s2 (+ l1_s0 l1_s1)))
                                  l1_s2))) (seq.nth lst 0)))
-                                  (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
+                                  (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_1))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))

diff --git a/SBVTestSuite/GoldFiles/lambda07.gold b/SBVTestSuite/GoldFiles/lambda07.gold
@@ -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 ---
@@ -21,16 +21,30 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- SBV Function definitions
+[GOOD] (define-fun-rec |sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))| ((base Int) (lst (Seq Int))) Int
+                       (ite (= lst (as seq.empty (Seq Int)))
+                            base
+                            (|sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))| (select (lambda ((l2_s0 Int) (l2_s1 Int))
+         (+ l2_s0 l2_s1)) base (seq.nth lst 0)) (seq.extract lst 1 (- (seq.len lst) 1)))))
+[GOOD] (define-fun-rec |sbv.map_@(([SInteger],_SInteger))_(lambda_((l1_s0_(Seq_Int)))_(let_((l1_s1_0))_(let_((l1_s2_(_sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))__l1_s1_l1_s0)))_l1_s2)))| ((lst (Seq (Seq Int)))) (Seq Int)
+                     (ite (= lst (as seq.empty (Seq (Seq Int))))
+                          (as seq.empty (Seq Int))
+                          (seq.++ (seq.unit (select (lambda ((l1_s0 (Seq Int)))
+                                 (let ((l1_s1 0))
+                                 (let ((l1_s2 (|sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))| l1_s1 l1_s0)))
+                                 l1_s2))) (seq.nth lst 0)))
+                                  (|sbv.map_@(([SInteger],_SInteger))_(lambda_((l1_s0_(Seq_Int)))_(let_((l1_s1_0))_(let_((l1_s2_(_sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))__l1_s1_l1_s0)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
+[GOOD] (define-fun-rec |sbv.foldl_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| ((base Int) (lst (Seq Int))) Int
+                       (ite (= lst (as seq.empty (Seq Int)))
+                            base
+                            (|sbv.foldl_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| (select (lambda ((l1_s0 Int) (l1_s1 Int))
+         (+ l1_s0 l1_s1)) base (seq.nth lst 0)) (seq.extract lst 1 (- (seq.len lst) 1)))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))
-[GOOD] (define-fun s5 () (Seq Int) (seq.map (lambda ((l1_s0 (Seq Int)))
-                                 (let ((l1_s1 0))
-                                 (let ((l1_s2 (seq.foldl (lambda ((l2_s0 Int) (l2_s1 Int))
-         (+ l2_s0 l2_s1)) l1_s1 l1_s0)))
-                                 l1_s2))) s0))
-[GOOD] (define-fun s6 () Int (seq.foldl (lambda ((l1_s0 Int) (l1_s1 Int))
-         (+ l1_s0 l1_s1)) s4 s5))
+[GOOD] (define-fun s5 () (Seq Int) (|sbv.map_@(([SInteger],_SInteger))_(lambda_((l1_s0_(Seq_Int)))_(let_((l1_s1_0))_(let_((l1_s2_(_sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))__l1_s1_l1_s0)))_l1_s2)))| s0))
+[GOOD] (define-fun s6 () Int (|sbv.foldl_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| s4 s5))
 [GOOD] (define-fun s7 () Bool (= s1 s6))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---

diff --git a/SBVTestSuite/GoldFiles/lambda18.gold b/SBVTestSuite/GoldFiles/lambda18.gold
@@ -26,6 +26,10 @@
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- SBV Function definitions
+[GOOD] (define-fun-rec |sbv.zip_@((SInteger,_SInteger))| ((lst1 (Seq Int)) (lst2 (Seq Int))) (Seq (SBVTuple2 Int Int))
+                      (ite (or (= lst1 (as seq.empty (Seq Int))) (= lst2 (as seq.empty (Seq Int))))
+                           (as seq.empty (Seq (SBVTuple2 Int Int)))
+                           (seq.++ (seq.unit ((as mkSBVTuple2 (SBVTuple2 Int Int)) (seq.nth lst1 0) (seq.nth lst2 0))) (|sbv.zip_@((SInteger,_SInteger))| (seq.extract lst1 1 (- (seq.len lst1) 1)) (seq.extract lst2 1 (- (seq.len lst2) 1))))))
 [GOOD] (define-fun-rec |sbv.foldl_@(((SInteger,_SInteger),_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_(SBVTuple2_Int_Int)))_(let_((l1_s2_(proj_1_SBVTuple2_l1_s1)))_(let_((l1_s3_(+_l1_s0_l1_s2)))_(let_((l1_s4_(proj_2_SBVTuple2_l1_s1)))_(let_((l1_s5_(+_l1_s3_l1_s4)))_l1_s5)))))| ((base Int) (lst (Seq (SBVTuple2 Int Int)))) Int
                        (ite (= lst (as seq.empty (Seq (SBVTuple2 Int Int))))
                             base
@@ -35,10 +39,6 @@
                                  (let ((l1_s4 (proj_2_SBVTuple2 l1_s1)))
                                  (let ((l1_s5 (+ l1_s3 l1_s4)))
                                  l1_s5))))) base (seq.nth lst 0)) (seq.extract lst 1 (- (seq.len lst) 1)))))
-[GOOD] (define-fun-rec |sbv.zip_@((SInteger,_SInteger))| ((lst1 (Seq Int)) (lst2 (Seq Int))) (Seq (SBVTuple2 Int Int))
-                      (ite (or (= lst1 (as seq.empty (Seq Int))) (= lst2 (as seq.empty (Seq Int))))
-                           (as seq.empty (Seq (SBVTuple2 Int Int)))
-                           (seq.++ (seq.unit ((as mkSBVTuple2 (SBVTuple2 Int Int)) (seq.nth lst1 0) (seq.nth lst2 0))) (|sbv.zip_@((SInteger,_SInteger))| (seq.extract lst1 1 (- (seq.len lst1) 1)) (seq.extract lst2 1 (- (seq.len lst2) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))

diff --git a/SBVTestSuite/GoldFiles/lambda23.gold b/SBVTestSuite/GoldFiles/lambda23.gold
@@ -27,11 +27,10 @@
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.foldr_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| ((base Int) (lst (Seq Int))) Int
-                       (ite (= lst (as seq.empty (Seq Int)))
-                            base
-                            (select (lambda ((l1_s0 Int) (l1_s1 Int))
-         (+ l1_s0 l1_s1)) (seq.nth lst 0) (|sbv.foldr_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| base (seq.extract lst 1 (- (seq.len lst) 1))))))
+[GOOD] (define-fun-rec |sbv.zip_@((SInteger,_SInteger))| ((lst1 (Seq Int)) (lst2 (Seq Int))) (Seq (SBVTuple2 Int Int))
+                      (ite (or (= lst1 (as seq.empty (Seq Int))) (= lst2 (as seq.empty (Seq Int))))
+                           (as seq.empty (Seq (SBVTuple2 Int Int)))
+                           (seq.++ (seq.unit ((as mkSBVTuple2 (SBVTuple2 Int Int)) (seq.nth lst1 0) (seq.nth lst2 0))) (|sbv.zip_@((SInteger,_SInteger))| (seq.extract lst1 1 (- (seq.len lst1) 1)) (seq.extract lst2 1 (- (seq.len lst2) 1))))))
 [GOOD] (define-fun-rec |sbv.map_@(((SInteger,_SInteger),_SInteger))_(lambda_((l1_s0_(SBVTuple2_Int_Int)))_(let_((l1_s1_(proj_1_SBVTuple2_l1_s0)))_(let_((l1_s2_(proj_2_SBVTuple2_l1_s0)))_(let_((l1_s3_(+_l1_s1_l1_s2)))_l1_s3))))| ((lst (Seq (SBVTuple2 Int Int)))) (Seq Int)
                      (ite (= lst (as seq.empty (Seq (SBVTuple2 Int Int))))
                           (as seq.empty (Seq Int))
@@ -41,10 +40,11 @@
                                  (let ((l1_s3 (+ l1_s1 l1_s2)))
                                  l1_s3)))) (seq.nth lst 0)))
                                   (|sbv.map_@(((SInteger,_SInteger),_SInteger))_(lambda_((l1_s0_(SBVTuple2_Int_Int)))_(let_((l1_s1_(proj_1_SBVTuple2_l1_s0)))_(let_((l1_s2_(proj_2_SBVTuple2_l1_s0)))_(let_((l1_s3_(+_l1_s1_l1_s2)))_l1_s3))))| (seq.extract lst 1 (- (seq.len lst) 1))))))
-[GOOD] (define-fun-rec |sbv.zip_@((SInteger,_SInteger))| ((lst1 (Seq Int)) (lst2 (Seq Int))) (Seq (SBVTuple2 Int Int))
-                      (ite (or (= lst1 (as seq.empty (Seq Int))) (= lst2 (as seq.empty (Seq Int))))
-                           (as seq.empty (Seq (SBVTuple2 Int Int)))
-                           (seq.++ (seq.unit ((as mkSBVTuple2 (SBVTuple2 Int Int)) (seq.nth lst1 0) (seq.nth lst2 0))) (|sbv.zip_@((SInteger,_SInteger))| (seq.extract lst1 1 (- (seq.len lst1) 1)) (seq.extract lst2 1 (- (seq.len lst2) 1))))))
+[GOOD] (define-fun-rec |sbv.foldr_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| ((base Int) (lst (Seq Int))) Int
+                       (ite (= lst (as seq.empty (Seq Int)))
+                            base
+                            (select (lambda ((l1_s0 Int) (l1_s1 Int))
+         (+ l1_s0 l1_s1)) (seq.nth lst 0) (|sbv.foldr_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| base (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s4 () Bool (= s0 s3))

diff --git a/SBVTestSuite/GoldFiles/lambda25.gold b/SBVTestSuite/GoldFiles/lambda25.gold
@@ -24,16 +24,16 @@
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.foldr_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| ((base Int) (lst (Seq Int))) Int
-                       (ite (= lst (as seq.empty (Seq Int)))
-                            base
-                            (select (lambda ((l1_s0 Int) (l1_s1 Int))
-         (+ l1_s0 l1_s1)) (seq.nth lst 0) (|sbv.foldr_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| base (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] (define-fun-rec |sbv.zipWith_@((SInteger,_SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| ((lst1 (Seq Int)) (lst2 (Seq Int))) (Seq Int)
                       (ite (or (= lst1 (as seq.empty (Seq Int))) (= lst2 (as seq.empty (Seq Int))))
                            (as seq.empty (Seq Int))
                            (seq.++ (seq.unit (select (lambda ((l1_s0 Int) (l1_s1 Int))
          (+ l1_s0 l1_s1)) (seq.nth lst1 0) (seq.nth lst2 0))) (|sbv.zipWith_@((SInteger,_SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| (seq.extract lst1 1 (- (seq.len lst1) 1)) (seq.extract lst2 1 (- (seq.len lst2) 1))))))
+[GOOD] (define-fun-rec |sbv.foldr_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| ((base Int) (lst (Seq Int))) Int
+                       (ite (= lst (as seq.empty (Seq Int)))
+                            base
+                            (select (lambda ((l1_s0 Int) (l1_s1 Int))
+         (+ l1_s0 l1_s1)) (seq.nth lst 0) (|sbv.foldr_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| base (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s4 () Bool (= s0 s3))