Add inference for count map (#7264)

6 files changed, 49 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5b3f3b729..c248d2231 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1569,9 +1569,14 @@ set(regress_1_tests
   regress1/bags/duplicate_removal1.smt2
   regress1/bags/duplicate_removal2.smt2
   regress1/bags/emptybag1.smt2
+  regress1/bags/fuzzy1.smt2
+  regress1/bags/fuzzy2.smt2
   regress1/bags/intersection_min1.smt2
   regress1/bags/intersection_min2.smt2
   regress1/bags/issue5759.smt2
+  regress1/bags/map1.smt2
+  regress1/bags/map2.smt2
+  regress1/bags/map3.smt2
   regress1/bags/subbag1.smt2
   regress1/bags/subbag2.smt2
   regress1/bags/union_disjoint.smt2
diff --git a/test/regress/regress1/bags/fuzzy1.smt2 b/test/regress/regress1/bags/fuzzy1.smt2
new file mode 100644
index 000000000..f9fee0ec4
--- /dev/null
+++ b/test/regress/regress1/bags/fuzzy1.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Bag (Tuple Int Int)))
+(declare-fun b () (Bag (Tuple Int Int)))
+(declare-fun c () Int) ; c here is zero
+(assert
+  (and
+    (= b (difference_subtract b a)) ; b is empty
+    (= a (bag (tuple c 0) 1)))) ; a = {|(<0, 0>, 1)|}
+(check-sat)
diff --git a/test/regress/regress1/bags/fuzzy2.smt2 b/test/regress/regress1/bags/fuzzy2.smt2
new file mode 100644
index 000000000..31da47f53
--- /dev/null
+++ b/test/regress/regress1/bags/fuzzy2.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Bag (Tuple Int Int)))
+(declare-fun b () (Bag (Tuple Int Int)))
+(declare-fun c () Int)
+(declare-fun d () (Tuple Int Int))
+(assert
+  (let ((D (bag d c))) ; when c = zero, then D is empty
+    (and
+      (= a (bag (tuple 1 1) c)) ; when c = zero, then a is empty
+      (= a (union_max a D))
+      (= a (difference_subtract a (bag d 1)))
+      (= a (union_disjoint a D))
+      (= a (intersection_min a D)))))
+(check-sat)
diff --git a/test/regress/regress1/bags/map.smt2 b/test/regress/regress1/bags/map1.smt2
index 54d671415..54d671415 100644
--- a/test/regress/regress1/bags/map.smt2
+++ b/test/regress/regress1/bags/map1.smt2
diff --git a/test/regress/regress1/bags/map2.smt2 b/test/regress/regress1/bags/map2.smt2
new file mode 100644
index 000000000..faed04caa
--- /dev/null
+++ b/test/regress/regress1/bags/map2.smt2
@@ -0,0 +1,9 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(set-option :fmf-bound true)
+(declare-fun A () (Bag Int))
+(declare-fun B () (Bag Int))
+(declare-fun f (Int) Int)
+(assert (= B (bag.map f A)))
+(assert (= (bag.count (- 2) B) 57))
+(check-sat)
diff --git a/test/regress/regress1/bags/map3.smt2 b/test/regress/regress1/bags/map3.smt2
new file mode 100644
index 000000000..637815fa5
--- /dev/null
+++ b/test/regress/regress1/bags/map3.smt2
@@ -0,0 +1,10 @@
+(set-logic HO_ALL)
+(set-info :status unsat)
+(set-option :fmf-bound true)
+(declare-fun A () (Bag Int))
+(declare-fun B () (Bag Int))
+(define-fun f ((x Int)) Int (+ x 1))
+(assert (= B (bag.map f A)))
+(assert (= (bag.count (- 2) B) 57))
+(assert (= A (as emptybag (Bag Int)) ))
+(check-sat)