Implement bags rewriter (#5132)

This PR implements rewrite rules for bags. This PR focuses on rewrite rules for non constant nodes.
Rewriting nodes with constant children is delegated to bags::NormalForm class (future PR).

1 files changed, 35 insertions, 0 deletions

diff --git a/src/theory/bags/bags_statistics.cpp b/src/theory/bags/bags_statistics.cpp
new file mode 100644
index 000000000..ea3d3046e
--- /dev/null
+++ b/src/theory/bags/bags_statistics.cpp
@@ -0,0 +1,35 @@
+/*********************                                                        */
+/*! \file bags_statistics.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Statistics for the theory of bags
+ **/
+
+#include "theory/bags/bags_statistics.h"
+
+#include "smt/smt_statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+BagsStatistics::BagsStatistics() : d_rewrites("theory::bags::rewrites")
+{
+  smtStatisticsRegistry()->registerStat(&d_rewrites);
+}
+
+BagsStatistics::~BagsStatistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_rewrites);
+}
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4