From 85900254c193c7205afc6f67158459d0940b7426 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Mar 2022 20:11:12 -0500 Subject: [PATCH] Simplify reductions for set and bag choose (#8304) Ensures that the reductions are deterministic, thus fixes cvc5/cvc5-projects#493. The reductions can be further simplified to not introduce UF. This will be addressed in a later PR. --- src/theory/bags/theory_bags.cpp | 22 +++++++------------ src/theory/sets/theory_sets_private.cpp | 20 ++++++----------- src/theory/skolem_lemma.cpp | 15 ------------- src/theory/skolem_lemma.h | 10 --------- test/regress/CMakeLists.txt | 1 + .../sets/proj-issue493-choose-det.smt2 | 8 +++++++ 6 files changed, 24 insertions(+), 52 deletions(-) create mode 100644 test/regress/regress0/sets/proj-issue493-choose-det.smt2 diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 37b6415e0..39b5a7e3c 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -110,17 +110,14 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node, { Assert(node.getKind() == BAG_CHOOSE); - // (bag.choose A) is expanded as - // (witness ((x elementType)) - // (ite - // (= A (as bag.empty (Bag E))) - // (= x (uf A)) - // (and (>= (bag.count x A) 1) (= x (uf A))) + // (bag.choose A) is eliminated to k, with lemma + // (and (= k (uf A)) (or (= A (as bag.empty (Bag E))) (>= (bag.count k A) 1))) // where uf: (Bag E) -> E is a skolem function, and E is the type of elements // of A NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); + Node x = sm->mkPurifySkolem(node, "bagChoose"); Node A = node[0]; TypeNode bagType = A.getType(); TypeNode ufType = nm->mkFunctionType(bagType, bagType.getBagElementType()); @@ -128,21 +125,18 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node, Node uf = sm->mkSkolemFunction(SkolemFunId::BAGS_CHOOSE, ufType, Node()); Node ufA = NodeManager::currentNM()->mkNode(APPLY_UF, uf, A); - Node x = nm->mkBoundVar(bagType.getBagElementType()); - Node equal = x.eqNode(ufA); Node emptyBag = nm->mkConst(EmptyBag(bagType)); Node isEmpty = A.eqNode(emptyBag); Node count = nm->mkNode(BAG_COUNT, x, A); Node one = nm->mkConstInt(Rational(1)); Node geqOne = nm->mkNode(GEQ, count, one); - Node geqOneAndEqual = geqOne.andNode(equal); - Node ite = nm->mkNode(ITE, isEmpty, equal, geqOneAndEqual); - Node ret = sm->mkSkolem(x, ite, "kBagChoose"); - lems.push_back(SkolemLemma(ret, nullptr)); + Node lem = nm->mkNode(AND, equal, nm->mkNode(OR, isEmpty, geqOne)); + TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr); + lems.push_back(SkolemLemma(tlem, x)); Trace("TheoryBags::ppRewrite") - << "ppRewrite(" << node << ") = " << ret << std::endl; - return TrustNode::mkTrustRewrite(node, ret, nullptr); + << "ppRewrite(" << node << ") = " << x << std::endl; + return TrustNode::mkTrustRewrite(node, x, nullptr); } void TheoryBags::postCheck(Effort effort) diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 37215458f..6bc582700 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1366,17 +1366,14 @@ TrustNode TheorySetsPrivate::expandChooseOperator( { Assert(node.getKind() == SET_CHOOSE); - // (choose A) is expanded as - // (witness ((x elementType)) - // (ite - // (= A (as emptyset (Set E))) - // (= x (uf A)) - // (and (member x A) (= x uf(A))) + // (choose A) is eliminated to k, with lemma + // (and (= k (uf A)) (or (= A (as set.empty (Set E))) (set.member k A))) // where uf: (Set E) -> E is a skolem function, and E is the type of elements // of A NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); + Node x = sm->mkPurifySkolem(node, "setChoose"); Node A = node[0]; TypeNode setType = A.getType(); ensureFirstClassSetType(setType); @@ -1385,17 +1382,14 @@ TrustNode TheorySetsPrivate::expandChooseOperator( Node uf = sm->mkSkolemFunction(SkolemFunId::SETS_CHOOSE, ufType, Node()); Node ufA = NodeManager::currentNM()->mkNode(APPLY_UF, uf, A); - Node x = nm->mkBoundVar(setType.getSetElementType()); - Node equal = x.eqNode(ufA); Node emptySet = nm->mkConst(EmptySet(setType)); Node isEmpty = A.eqNode(emptySet); Node member = nm->mkNode(SET_MEMBER, x, A); - Node memberAndEqual = member.andNode(equal); - Node ite = nm->mkNode(ITE, isEmpty, equal, memberAndEqual); - Node ret = sm->mkSkolem(x, ite, "kSetChoose"); - lems.push_back(SkolemLemma(ret, nullptr)); - return TrustNode::mkTrustRewrite(node, ret, nullptr); + Node lem = nm->mkNode(AND, equal, nm->mkNode(OR, isEmpty, member)); + TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr); + lems.push_back(SkolemLemma(tlem, x)); + return TrustNode::mkTrustRewrite(node, x, nullptr); } TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node) diff --git a/src/theory/skolem_lemma.cpp b/src/theory/skolem_lemma.cpp index af4d09492..b0b59b7e4 100644 --- a/src/theory/skolem_lemma.cpp +++ b/src/theory/skolem_lemma.cpp @@ -25,22 +25,7 @@ SkolemLemma::SkolemLemma(TrustNode lem, Node k) : d_lemma(lem), d_skolem(k) Assert(lem.getKind() == TrustNodeKind::LEMMA); } -SkolemLemma::SkolemLemma(Node k, ProofGenerator* pg) : d_lemma(), d_skolem(k) -{ - Node lem = getSkolemLemmaFor(k); - d_lemma = TrustNode::mkTrustLemma(lem, pg); -} - Node SkolemLemma::getProven() const { return d_lemma.getProven(); } -Node SkolemLemma::getSkolemLemmaFor(Node k) -{ - Node w = SkolemManager::getWitnessForm(k); - Assert(w.getKind() == kind::WITNESS); - TNode tx = w[0][0]; - TNode tk = k; - return w[1].substitute(tx, tk); -} - } // namespace theory } // namespace cvc5 diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h index 4f17ed9d3..0e78427f8 100644 --- a/src/theory/skolem_lemma.h +++ b/src/theory/skolem_lemma.h @@ -41,11 +41,6 @@ class SkolemLemma * Make skolem from trust node lem of kind LEMMA and skolem k. */ SkolemLemma(TrustNode lem, Node k); - /** - * Make skolem lemma from witness form of skolem k. If non-null, pg is - * proof generator that can generator a proof for getSkolemLemmaFor(k). - */ - SkolemLemma(Node k, ProofGenerator* pg); /** The lemma, a trust node of kind LEMMA */ TrustNode d_lemma; @@ -54,11 +49,6 @@ class SkolemLemma /** Get proven from the lemma */ Node getProven() const; - /** - * Get the lemma for skolem k based on its witness form. If k has witness - * form (witness ((x T)) (P x)), this is the formula (P k). - */ - static Node getSkolemLemmaFor(Node k); }; } // namespace theory diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 67073033d..84aebd5ae 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1254,6 +1254,7 @@ set(regress_0_tests regress0/sets/pre-proc-univ.smt2 regress0/sets/proj-issue177.smt2 regress0/sets/proj-issue486-sets-split-eq.smt2 + regress0/sets/proj-issue493-choose-det.smt2 regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 regress0/sets/setel-eq.smt2 regress0/sets/sets-deq-dd.smt2 diff --git a/test/regress/regress0/sets/proj-issue493-choose-det.smt2 b/test/regress/regress0/sets/proj-issue493-choose-det.smt2 new file mode 100644 index 000000000..16f8e1d34 --- /dev/null +++ b/test/regress/regress0/sets/proj-issue493-choose-det.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status unsat) +(set-option :sets-ext true) +(declare-const x Bool) +(declare-const x3 Bool) +(declare-const x4 Bool) +(assert (forall ((x2 Bool)) (ite (not (set.choose (set.complement (set.insert x3 x4 false false (set.singleton x))))) (set.choose (set.complement (set.insert x3 x4 x2 false (set.singleton x)))) false))) +(check-sat) -- 2.30.2