Fix soundness issue of missing premises for count bag lemmas (#7615)

This PR fixes soundness issues found by cvc5 fuzzy sygus when it answers unsat for sat problems.
The error is related to a previous fix which did not include the required antecedent in the two lemmas:

(=>  (= e x)
        (=
              (bag.count e (bag x c))
             (ite (>= c 1) c 0)))

and

(=>  (distinct x e))  (= (bag.count e (bag x c)) 0))

diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index 66c38ab869561149ad2f04b6e409fbaeb33d9211..a746a2cbaf77a31a2a187957e57e9fe1d4fa1e15 100644 (file)
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -58,41 +58,24 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e)
   Assert(n.getKind() == MK_BAG);
   Assert(e.getType() == n.getType().getBagElementType());
 
+  /*
+   * (ite (and (= e x) (>= c 1))
+   *   (= (bag.count e skolem) c)
+   *   (= (bag.count e skolem) 0))
+   */
   Node x = n[0];
   Node c = n[1];
+  InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG);
+  Node same = d_nm->mkNode(EQUAL, e, x);
   Node geq = d_nm->mkNode(GEQ, c, d_one);
-  if (d_state->areEqual(e, x))
-  {
-    // (= (bag.count e skolem) (ite (>= c 1) c 0)))
-    InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG_SAME_ELEMENT);
-    Node skolem = getSkolem(n, inferInfo);
-    Node count = getMultiplicityTerm(e, skolem);
-    Node ite = d_nm->mkNode(ITE, geq, c, d_zero);
-    inferInfo.d_conclusion = count.eqNode(ite);
-    return inferInfo;
-  }
-  if (d_state->areDisequal(e, x))
-  {
-    //(= (bag.count e skolem) 0))
-    InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG_SAME_ELEMENT);
-    Node skolem = getSkolem(n, inferInfo);
-    Node count = getMultiplicityTerm(e, skolem);
-    inferInfo.d_conclusion = count.eqNode(d_zero);
-    return inferInfo;
-  }
-  else
-  {
-    // (= (bag.count e skolem) (ite (and (= e x) (>= c 1)) c 0)))
-    InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG);
-    Node skolem = getSkolem(n, inferInfo);
-    Node count = getMultiplicityTerm(e, skolem);
-    Node same = d_nm->mkNode(EQUAL, e, x);
-    Node andNode = same.andNode(geq);
-    Node ite = d_nm->mkNode(ITE, andNode, c, d_zero);
-    Node equal = count.eqNode(ite);
-    inferInfo.d_conclusion = equal;
-    return inferInfo;
-  }
+  Node andNode = same.andNode(geq);
+  Node skolem = getSkolem(n, inferInfo);
+  Node count = getMultiplicityTerm(e, skolem);
+  Node equalC = d_nm->mkNode(EQUAL, count, c);
+  Node equalZero = d_nm->mkNode(EQUAL, count, d_zero);
+  Node ite = d_nm->mkNode(ITE, andNode, equalC, equalZero);
+  inferInfo.d_conclusion = ite;
+  return inferInfo;
 }
 
 /**

diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h
index 3f38d05b9ab737829e52655bdf863d37f3cdf831..391a352bd718a66421a7e5d88ae6c20fa72df414 100644 (file)
--- a/src/theory/bags/inference_generator.h
+++ b/src/theory/bags/inference_generator.h
@@ -50,13 +50,10 @@ class InferenceGenerator
   /**
    * @param n is (bag x c) of type (Bag E)
    * @param e is a node of type E
-   * @return an inference that represents the following cases:
-   * 1- e, x are in the same equivalent class, then we infer:
-   *    (= (bag.count e skolem) (ite (>= c 1) c 0)))
-   * 2- e, x are known to be disequal, then we infer:
-   *    (= (bag.count e skolem) 0))
-   * 3- if neither holds, we infer:
-   *    (= (bag.count e skolem) (ite (and (= e x) (>= c 1)) c 0)))
+   * @return an inference that represents the following lemma:
+   * (ite (and (= e x) (>= c 1))
+   *   (= (bag.count e skolem) c)
+   *   (= (bag.count e skolem) 0))
    * where skolem = (bag x c) is a fresh variable
    */
   InferInfo mkBag(Node n, Node e);

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 594834226be26b1f3b977fc8e1390cee6ac29700..653762721d63033e163e58977966f2caafb37baf 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -104,8 +104,6 @@ const char* toString(InferenceId i)
     case InferenceId::ARRAYS_EQ_TAUTOLOGY: return "ARRAYS_EQ_TAUTOLOGY";
 
     case InferenceId::BAGS_NON_NEGATIVE_COUNT: return "BAGS_NON_NEGATIVE_COUNT";
-    case InferenceId::BAGS_MK_BAG_DIFFERENT_ELEMENT: return "BAGS_MK_BAG_DIFFERENT_ELEMENT";
-    case InferenceId::BAGS_MK_BAG_SAME_ELEMENT: return "BAGS_MK_BAG_SAME_ELEMENT";
     case InferenceId::BAGS_MK_BAG: return "BAGS_MK_BAG";
     case InferenceId::BAGS_EQUALITY: return "BAGS_EQUALITY";
     case InferenceId::BAGS_DISEQUALITY: return "BAGS_DISEQUALITY";

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index cebf02c9d33a8c28dfdb794df96da8b2048ca863..da2805df0c8a563e7bc1ffb6ba48c3d83cb65a2a 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -169,8 +169,6 @@ enum class InferenceId
 
   // ---------------------------------- bags theory
   BAGS_NON_NEGATIVE_COUNT,
-  BAGS_MK_BAG_DIFFERENT_ELEMENT,
-  BAGS_MK_BAG_SAME_ELEMENT,
   BAGS_MK_BAG,
   BAGS_EQUALITY,
   BAGS_DISEQUALITY,

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9574628a8b1c3358d3feda64a9f6d323dfed3090..d9076c81b2a4a3b675dad6c59cb78eee5c793948 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1600,6 +1600,7 @@ set(regress_1_tests
   regress1/bags/fuzzy3.smt2
   regress1/bags/fuzzy4.smt2
   regress1/bags/fuzzy5.smt2
+  regress1/bags/fuzzy6.smt2
   regress1/bags/intersection_min1.smt2
   regress1/bags/intersection_min2.smt2
   regress1/bags/issue5759.smt2

diff --git a/test/regress/regress1/bags/fuzzy6.smt2 b/test/regress/regress1/bags/fuzzy6.smt2
new file mode 100644 (file)
index 0000000..2bcc024
--- /dev/null
+++ b/test/regress/regress1/bags/fuzzy6.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+(set-info :status sat)
+(set-option :produce-models true)
+(declare-fun A () (Bag (Tuple Int Int)))
+(declare-fun c () Int)
+(declare-fun d () (Tuple Int Int))
+(assert
+ (let ((double_c (+ c c)))
+   (let ((formula (= A (bag (tuple c double_c) c))))
+     (and (not (= formula (= A (bag (tuple c c) c))))
+          (not (= formula (= A (bag (tuple 0 c) double_c))))))))
+
+(check-sat)