diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs index 071909d0..d187ed06 100644 --- 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 index def3f63b..baccc410 100644 --- 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 index 7e78a041..cb92c477 100644 --- 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 index 9c999326..8f939c03 100644 --- 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 index e28c9ea0..36da87d8 100644 --- 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 index 58149bf9..5fff44dc 100644 --- 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))