From 51f7733bec4ab2c9666173848b81cab8744359da Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 23 Nov 2021 12:10:37 -0600 Subject: [PATCH] Add rewrite rule for bag.card operator using bag.map and lambda (#7643) Add rewrite rule for bag.card operator using bag.map and lambda --- src/theory/bags/bags_rewriter.cpp | 1 - src/theory/bags/theory_bags.cpp | 25 ++++++++++++++++++++++++- src/theory/bags/theory_bags.h | 2 ++ test/regress/CMakeLists.txt | 1 + test/regress/regress1/bags/card1.smt2 | 7 +++++++ 5 files changed, 34 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/bags/card1.smt2 diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 7093d52fc..b8f3b80c9 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -449,7 +449,6 @@ BagsRewriteResponse BagsRewriter::rewriteCard(const TNode& n) const Node plus = d_nm->mkNode(PLUS, A, B); return BagsRewriteResponse(plus, Rewrite::CARD_DISJOINT); } - return BagsRewriteResponse(n, Rewrite::NONE); } diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 861aaf862..4dffbdb00 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -86,6 +86,7 @@ TrustNode TheoryBags::ppRewrite(TNode atom, std::vector& lems) switch (atom.getKind()) { case kind::BAG_CHOOSE: return expandChooseOperator(atom, lems); + case kind::BAG_CARD: return expandCardOperator(atom, lems); default: return TrustNode::null(); } } @@ -125,9 +126,32 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node, Node ite = nm->mkNode(ITE, isEmpty, equal, geqOneAndEqual); Node ret = sm->mkSkolem(x, ite, "kBagChoose"); lems.push_back(SkolemLemma(ret, nullptr)); + Trace("TheoryBags::ppRewrite") + << "ppRewrite(" << node << ") = " << ret << std::endl; return TrustNode::mkTrustRewrite(node, ret, nullptr); } +TrustNode TheoryBags::expandCardOperator(TNode n, + std::vector& vector) +{ + if (d_env.getLogicInfo().isHigherOrder()) + { + // (bag.card A) = (bag.count 1 (bag.map (lambda ((x E)) 1) A)), + // where E is the type of elements of A + NodeManager* nm = NodeManager::currentNM(); + Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + TypeNode type = n[0].getType().getBagElementType(); + Node x = nm->mkBoundVar("x", type); + Node lambda = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, x), one); + Node map = nm->mkNode(kind::BAG_MAP, lambda, n[0]); + Node countOne = nm->mkNode(kind::BAG_COUNT, one, map); + Trace("TheoryBags::ppRewrite") + << "ppRewrite(" << n << ") = " << countOne << std::endl; + return TrustNode::mkTrustRewrite(n, countOne, nullptr); + } + return TrustNode::null(); +} + void TheoryBags::postCheck(Effort effort) { d_im.doPendingFacts(); @@ -253,7 +277,6 @@ void TheoryBags::preRegisterTerm(TNode n) Trace("bags::TheoryBags::preRegisterTerm") << n << std::endl; switch (n.getKind()) { - case BAG_CARD: case BAG_FROM_SET: case BAG_TO_SET: case BAG_IS_SINGLETON: diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index b4888f3b4..fd28482d4 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -92,6 +92,8 @@ class TheoryBags : public Theory /** expand the definition of the bag.choose operator */ TrustNode expandChooseOperator(const Node& node, std::vector& lems); + /** expand the definition of bag.card operator */ + TrustNode expandCardOperator(TNode n, std::vector& lems); /** The state of the bags solver at full effort */ SolverState d_state; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f4e9e287b..e11149df0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1592,6 +1592,7 @@ set(regress_1_tests regress1/bug681.smt2 regress1/bug694-Unapply1.scala-0.smt2 regress1/bug800.smt2 + regress1/bags/card1.smt2 regress1/bags/choose1.smt2 regress1/bags/choose2.smt2 regress1/bags/choose3.smt2 diff --git a/test/regress/regress1/bags/card1.smt2 b/test/regress/regress1/bags/card1.smt2 new file mode 100644 index 000000000..4ea5488d2 --- /dev/null +++ b/test/regress/regress1/bags/card1.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --fmf-bound --uf-lazy-ll +; EXPECT: sat +(set-logic HO_ALL) +(define-fun f ((x String)) Int 1) +(declare-fun A () (Bag String)) +(assert (= (bag.card A) 20)) +(check-sat) -- 2.30.2