Add skeleton for theory of bags (multisets) (#5100)

This PR adds initial headers and mostly empty source files for the theory of bags (multisets).
It acts as a basis for future commits.
It includes straightforward implementation for typing rules an enumerator for bags.

5 files changed, 134 insertions, 0 deletions

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 7861bf7ae..8a4d878ef 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -48,6 +48,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkPredicateSort();
   void testMkRecordSort();
   void testMkSetSort();
+  void testMkBagSort();
   void testMkSequenceSort();
   void testMkSortConstructorSort();
   void testMkTupleSort();
@@ -59,6 +60,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkConst();
   void testMkConstArray();
   void testMkEmptySet();
+  void testMkEmptyBag();
   void testMkEmptySequence();
   void testMkFalse();
   void testMkFloatingPoint();
@@ -425,6 +427,16 @@ void SolverBlack::testMkSetSort()
                    CVC4ApiException&);
 }
 
+void SolverBlack::testMkBagSort()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->getBooleanSort()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->getIntegerSort()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->mkBitVectorSort(4)));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkBagSort(d_solver->mkBitVectorSort(4)),
+                   CVC4ApiException&);
+}
+
 void SolverBlack::testMkSequenceSort()
 {
   TS_ASSERT_THROWS_NOTHING(
@@ -596,6 +608,17 @@ void SolverBlack::testMkEmptySet()
   TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&);
 }
 
+void SolverBlack::testMkEmptyBag()
+{
+  Solver slv;
+  Sort s = d_solver->mkBagSort(d_solver->getBooleanSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptyBag(Sort()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptyBag(s));
+  TS_ASSERT_THROWS(d_solver->mkEmptyBag(d_solver->getBooleanSort()),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkEmptyBag(s), CVC4ApiException&);
+}
+
 void SolverBlack::testMkEmptySequence()
 {
   Solver slv;
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index a12bd969d..32108bf84 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -35,6 +35,7 @@ class SortBlack : public CxxTest::TestSuite
   void testGetArrayIndexSort();
   void testGetArrayElementSort();
   void testGetSetElementSort();
+  void testGetBagElementSort();
   void testGetSequenceElementSort();
   void testGetUninterpretedSortName();
   void testIsUninterpretedSortParameterized();
@@ -193,10 +194,22 @@ void SortBlack::testGetSetElementSort()
 {
   Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
   TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort());
+  Sort elementSort = setSort.getSetElementSort();
+  TS_ASSERT(elementSort == d_solver.getIntegerSort());
   Sort bvSort = d_solver.mkBitVectorSort(32);
   TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&);
 }
 
+void SortBlack::testGetBagElementSort()
+{
+  Sort bagSort = d_solver.mkBagSort(d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(bagSort.getBagElementSort());
+  Sort elementSort = bagSort.getBagElementSort();
+  TS_ASSERT(elementSort == d_solver.getIntegerSort());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getBagElementSort(), CVC4ApiException&);
+}
+
 void SortBlack::testGetSequenceElementSort()
 {
   Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort());
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index fed5de90b..f40d9658b 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -14,6 +14,7 @@ cvc4_add_unit_test_white(evaluator_white theory)
 cvc4_add_unit_test_white(logic_info_white theory)
 cvc4_add_unit_test_white(sequences_rewriter_white theory)
 cvc4_add_unit_test_white(theory_arith_white theory)
+cvc4_add_unit_test_white(theory_bags_type_rules_black theory)
 cvc4_add_unit_test_white(theory_bv_rewriter_white theory)
 cvc4_add_unit_test_white(theory_bv_white theory)
 cvc4_add_unit_test_white(theory_engine_white theory)
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 341b370c4..7990d9e54 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -538,6 +538,7 @@ public:
     TS_ASSERT( !info.isLocked() );
     info.disableTheory(THEORY_STRINGS);
     info.disableTheory(THEORY_SETS);
+    info.disableTheory(THEORY_BAGS);
     info.arithOnlyLinear();
     info.disableIntegers();
     info.lock();
@@ -546,6 +547,7 @@ public:
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
     info.disableQuantifiers();
+    info.disableTheory(THEORY_BAGS);
     info.lock();
     TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA");
 
@@ -553,6 +555,7 @@ public:
     TS_ASSERT( !info.isLocked() );
     info.disableTheory(THEORY_BV);
     info.disableTheory(THEORY_DATATYPES);
+    info.disableTheory(THEORY_BAGS);
     info.enableIntegers();
     info.disableReals();
     info.lock();
@@ -564,6 +567,7 @@ public:
     info.disableTheory(THEORY_UF);
     info.disableTheory(THEORY_FP);
     info.disableTheory(THEORY_SEP);
+    info.disableTheory(THEORY_BAGS);
     info.lock();
     TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" );
     TS_ASSERT( info.isPure( THEORY_ARRAYS ) );
diff --git a/test/unit/theory/theory_bags_type_rules_black.h b/test/unit/theory/theory_bags_type_rules_black.h
new file mode 100644
index 000000000..e5ec60154
--- /dev/null
+++ b/test/unit/theory/theory_bags_type_rules_black.h
@@ -0,0 +1,93 @@
+/*********************                                                        */
+/*! \file theory_bags_type_rules_black.h
+ ** \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 Black box testing of bags typing rules
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "expr/dtype.h"
+#include "smt/smt_engine.h"
+#include "theory/bags/theory_bags_type_rules.h"
+#include "theory/strings/type_enumerator.h"
+
+using namespace CVC4;
+using namespace CVC4::smt;
+using namespace CVC4::theory;
+using namespace CVC4::kind;
+using namespace CVC4::theory::bags;
+using namespace std;
+
+typedef expr::Attribute<Node, Node> attribute;
+
+class BagsTypeRuleBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override
+  {
+    d_em.reset(new ExprManager());
+    d_smt.reset(new SmtEngine(d_em.get()));
+    d_nm.reset(NodeManager::fromExprManager(d_em.get()));
+    d_smt->finishInit();
+  }
+
+  void tearDown() override
+  {
+    d_smt.reset();
+    d_nm.release();
+    d_em.reset();
+  }
+
+  std::vector<Node> getNStrings(size_t n)
+  {
+    std::vector<Node> elements(n);
+    CVC4::theory::strings::StringEnumerator enumerator(d_nm->stringType());
+
+    for (size_t i = 0; i < n; i++)
+    {
+      ++enumerator;
+      elements[i] = *enumerator;
+    }
+
+    return elements;
+  }
+
+  void testCountOperator()
+  {
+    vector<Node> elements = getNStrings(1);
+    Node bag = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(100)));
+
+    Node count = d_nm->mkNode(BAG_COUNT, elements[0], bag);
+    Node node = d_nm->mkConst(Rational(10));
+
+    // node of type Int is not compatible with bag of type (Bag String)
+    TS_ASSERT_THROWS(d_nm->mkNode(BAG_COUNT, node, bag),
+                     TypeCheckingExceptionPrivate&);
+  }
+
+  void testMkBagOperator()
+  {
+    vector<Node> elements = getNStrings(1);
+    Node negative = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(-1)));
+    Node zero = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(0)));
+    Node positive = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(1)));
+
+    // only positive multiplicity are constants
+    TS_ASSERT(! MkBagTypeRule::computeIsConst(d_nm.get(), negative));
+    TS_ASSERT(! MkBagTypeRule::computeIsConst(d_nm.get(), zero));
+    TS_ASSERT(MkBagTypeRule::computeIsConst(d_nm.get(), positive));
+  }
+
+ private:
+  std::unique_ptr<ExprManager> d_em;
+  std::unique_ptr<SmtEngine> d_smt;
+  std::unique_ptr<NodeManager> d_nm;
+}; /* class BagsTypeRuleBlack */