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

diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index 7093d52fcf51578e6e9ce83243991091983040b2..b8f3b80c99c5cd5a2007a1c5211336faa8dca300 100644 (file)
--- 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 861aaf862b860333fbc4f73733f0d5ca96d56f62..4dffbdb00c8a846fe706af1a05148c03cb03e742 100644 (file)
--- 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<SkolemLemma>& 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<SkolemLemma>& 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 b4888f3b458e4da2b24abe6153f58e1ada6fe637..fd28482d4119ec7524cebdfbd228fd3fdeaf0e20 100644 (file)
--- 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<SkolemLemma>& lems);
+  /** expand the definition of bag.card operator */
+  TrustNode expandCardOperator(TNode n, std::vector<SkolemLemma>& 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 f4e9e287bf883dc5d4f4d0fe54171cacb74da20d..e11149df0c6106280002fb78edec59db4de1c76d 100644 (file)
--- 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 (file)
index 0000000..4ea5488
--- /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)