unit tests for map/fold

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

regressions/smt2/testfoldl.expected.out

@@ -0,0 +1,4 @@
+sat
+sat
+sat
+sat

regressions/smt2/testfoldl.smt2

@@ -0,0 +1,34 @@
+(push)
+(declare-fun f (Int Int) Int)
+(declare-const il (Seq Int))
+(assert (= (seq.foldl f 0 il) 5))
+(check-sat)
+(pop)
+
+(push)
+(declare-const il (Seq Int))
+(declare-const F (Array Bool Int Bool))
+(assert (= (seq.foldl F true il) true))
+(assert (> (seq.len il) 0))
+(assert (not (= F ((as const (Array Bool Int Bool)) true))))
+(check-sat)
+(pop)
+
+
+(push)
+(declare-fun f (Int Int Int) Int)
+(declare-const il (Seq Int))
+(assert (= (seq.foldli f 0 0 il) 5))
+(check-sat)
+(pop)
+
+(push)
+(declare-const il (Seq Int))
+(declare-const F (Array Int Bool Int Bool))
+(assert (= (seq.foldli F 5 true il) true))
+(assert (> (seq.len il) 0))
+(assert (not (= F ((as const (Array Int Bool Int Bool)) true))))
+(check-sat)
+(pop)
+
+

regressions/smt2/testmap.expected.out

@@ -0,0 +1,8 @@
+sat
+sat
+(as seq.empty Seq)
+(seq.++ (seq.map f il_1) (seq.map f il_2))
+(seq.unit (select f 4))
+sat
+sat
+true

regressions/smt2/testmap.smt2

@@ -0,0 +1,46 @@
+(push)
+(declare-fun f (Int) Bool)
+(declare-const il (Seq Int))
+(assert (= (seq.map f il) (seq.++ (seq.unit false) (seq.unit true) (seq.unit false))))
+(check-sat)
+(pop)
+
+(push)
+(declare-const il (Seq Int))
+(declare-const F (Array Int Bool))
+(assert (= (seq.map F il) (seq.++ (seq.unit false) (seq.unit true) (seq.unit false))))
+(check-sat)
+(pop)
+
+(push)
+(declare-const f (Array Int Bool))
+(declare-const il_1 (Seq Int))
+(declare-const il_2 (Seq Int))
+(simplify (seq.map f (as seq.empty (Seq Int))))
+(simplify (seq.map f (seq.++ il_1 il_2)))
+(simplify (seq.map f (seq.unit 4)))
+(pop)
+
+(push)
+(declare-fun f (Int) Bool)
+(declare-const il (Seq Int))
+(declare-const bl (Seq Bool))
+(assert (= (seq.map f il) bl))
+(assert (> (seq.len il) 1))
+(check-sat)
+(pop)
+
+
+(push)
+(declare-fun f (Int) Bool)
+(declare-fun p ((Seq Bool)) Bool)
+(declare-const il (Seq Int))
+(assert (p (seq.map f il)))
+(assert (not (p (seq.unit false))))
+(assert (not (p (seq.unit true))))
+(assert (not (= il (as seq.empty (Seq Int)))))
+(check-sat)
+(eval (>= (seq.len il) 2))
+;(get-model)
+(pop)
+

regressions/smt2/testmapi.expected.out

@@ -0,0 +1,6 @@
+sat
+sat
+(as seq.empty Seq)
+(seq.++ (seq.mapi f 2 il_1) (seq.mapi f (+ 2 (seq.len il_1)) il_2))
+(seq.unit (select f 3 4))
+sat

regressions/smt2/testmapi.smt2

@@ -0,0 +1,32 @@
+(push)
+(declare-fun f (Int Int) Bool)
+(declare-const il (Seq Int))
+(assert (= (seq.mapi f 0 il) (seq.++ (seq.unit false) (seq.unit true) (seq.unit false))))
+(check-sat)
+(pop)
+
+(push)
+(declare-const il (Seq Int))
+(declare-const F (Array Int Int Bool))
+(assert (= (seq.mapi F 0 il) (seq.++ (seq.unit false) (seq.unit true) (seq.unit false))))
+(check-sat)
+(pop)
+
+(push)
+(declare-const f (Array Int Int Bool))
+(declare-const il_1 (Seq Int))
+(declare-const il_2 (Seq Int))
+(simplify (seq.mapi f 1 (as seq.empty (Seq Int))))
+(simplify (seq.mapi f 2 (seq.++ il_1 il_2)))
+(simplify (seq.mapi f 3 (seq.unit 4)))
+(pop)
+
+(push)
+(declare-fun f (Int Int) Bool)
+(declare-const il (Seq Int))
+(declare-const bl (Seq Bool))
+(assert (= (seq.mapi f 1 il) bl))
+(assert (> (seq.len il) 1))
+(check-sat)
+(pop)
+