From 1167e38030cbf3c746dcf5bdf09e0ebfa9d44672 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 9 Nov 2021 20:31:49 -0600 Subject: [PATCH] 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)) --- src/theory/bags/inference_generator.cpp | 47 ++++++++----------------- src/theory/bags/inference_generator.h | 11 +++--- src/theory/inference_id.cpp | 2 -- src/theory/inference_id.h | 2 -- test/regress/CMakeLists.txt | 1 + test/regress/regress1/bags/fuzzy6.smt2 | 13 +++++++ 6 files changed, 33 insertions(+), 43 deletions(-) create mode 100644 test/regress/regress1/bags/fuzzy6.smt2 diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 66c38ab86..a746a2cba 100644 --- 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 3f38d05b9..391a352bd 100644 --- 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 594834226..653762721 100644 --- 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 cebf02c9d..da2805df0 100644 --- 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 9574628a8..d9076c81b 100644 --- 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 index 000000000..2bcc024dd --- /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) -- 2.30.2