1 files changed, 21 insertions, 21 deletions

diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index 341798eb2..444878574 100644
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -42,8 +42,8 @@ BagSolver::BagSolver(Env& env,
       d_termReg(tr),
       d_mapCache(userContext())
 {
-  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
-  d_one = NodeManager::currentNM()->mkConst(Rational(1));
+  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+  d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
 }
@@ -69,14 +69,14 @@ void BagSolver::postCheck()
       Kind k = n.getKind();
       switch (k)
       {
-        case kind::EMPTYBAG: checkEmpty(n); break;
-        case kind::MK_BAG: checkMkBag(n); break;
-        case kind::UNION_DISJOINT: checkUnionDisjoint(n); break;
-        case kind::UNION_MAX: checkUnionMax(n); break;
-        case kind::INTERSECTION_MIN: checkIntersectionMin(n); break;
-        case kind::DIFFERENCE_SUBTRACT: checkDifferenceSubtract(n); break;
-        case kind::DIFFERENCE_REMOVE: checkDifferenceRemove(n); break;
-        case kind::DUPLICATE_REMOVAL: checkDuplicateRemoval(n); break;
+        case kind::BAG_EMPTY: checkEmpty(n); break;
+        case kind::BAG_MAKE: checkBagMake(n); break;
+        case kind::BAG_UNION_DISJOINT: checkUnionDisjoint(n); break;
+        case kind::BAG_UNION_MAX: checkUnionMax(n); break;
+        case kind::BAG_INTER_MIN: checkIntersectionMin(n); break;
+        case kind::BAG_DIFFERENCE_SUBTRACT: checkDifferenceSubtract(n); break;
+        case kind::BAG_DIFFERENCE_REMOVE: checkDifferenceRemove(n); break;
+        case kind::BAG_DUPLICATE_REMOVAL: checkDuplicateRemoval(n); break;
         case kind::BAG_MAP: checkMap(n); break;
         default: break;
       }
@@ -112,7 +112,7 @@ set<Node> BagSolver::getElementsForBinaryOperator(const Node& n)
 
 void BagSolver::checkEmpty(const Node& n)
 {
-  Assert(n.getKind() == EMPTYBAG);
+  Assert(n.getKind() == BAG_EMPTY);
   for (const Node& e : d_state.getElements(n))
   {
     InferInfo i = d_ig.empty(n, e);
@@ -122,7 +122,7 @@ void BagSolver::checkEmpty(const Node& n)
 
 void BagSolver::checkUnionDisjoint(const Node& n)
 {
-  Assert(n.getKind() == UNION_DISJOINT);
+  Assert(n.getKind() == BAG_UNION_DISJOINT);
   std::set<Node> elements = getElementsForBinaryOperator(n);
   for (const Node& e : elements)
   {
@@ -133,7 +133,7 @@ void BagSolver::checkUnionDisjoint(const Node& n)
 
 void BagSolver::checkUnionMax(const Node& n)
 {
-  Assert(n.getKind() == UNION_MAX);
+  Assert(n.getKind() == BAG_UNION_MAX);
   std::set<Node> elements = getElementsForBinaryOperator(n);
   for (const Node& e : elements)
   {
@@ -144,7 +144,7 @@ void BagSolver::checkUnionMax(const Node& n)
 
 void BagSolver::checkIntersectionMin(const Node& n)
 {
-  Assert(n.getKind() == INTERSECTION_MIN);
+  Assert(n.getKind() == BAG_INTER_MIN);
   std::set<Node> elements = getElementsForBinaryOperator(n);
   for (const Node& e : elements)
   {
@@ -155,7 +155,7 @@ void BagSolver::checkIntersectionMin(const Node& n)
 
 void BagSolver::checkDifferenceSubtract(const Node& n)
 {
-  Assert(n.getKind() == DIFFERENCE_SUBTRACT);
+  Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT);
   std::set<Node> elements = getElementsForBinaryOperator(n);
   for (const Node& e : elements)
   {
@@ -164,15 +164,15 @@ void BagSolver::checkDifferenceSubtract(const Node& n)
   }
 }
 
-void BagSolver::checkMkBag(const Node& n)
+void BagSolver::checkBagMake(const Node& n)
 {
-  Assert(n.getKind() == MK_BAG);
+  Assert(n.getKind() == BAG_MAKE);
   Trace("bags::BagSolver::postCheck")
-      << "BagSolver::checkMkBag Elements of " << n
+      << "BagSolver::checkBagMake Elements of " << n
       << " are: " << d_state.getElements(n) << std::endl;
   for (const Node& e : d_state.getElements(n))
   {
-    InferInfo i = d_ig.mkBag(n, e);
+    InferInfo i = d_ig.bagMake(n, e);
     d_im.lemmaTheoryInference(&i);
   }
 }
@@ -184,7 +184,7 @@ void BagSolver::checkNonNegativeCountTerms(const Node& bag, const Node& element)
 
 void BagSolver::checkDifferenceRemove(const Node& n)
 {
-  Assert(n.getKind() == DIFFERENCE_REMOVE);
+  Assert(n.getKind() == BAG_DIFFERENCE_REMOVE);
   std::set<Node> elements = getElementsForBinaryOperator(n);
   for (const Node& e : elements)
   {
@@ -195,7 +195,7 @@ void BagSolver::checkDifferenceRemove(const Node& n)
 
 void BagSolver::checkDuplicateRemoval(Node n)
 {
-  Assert(n.getKind() == DUPLICATE_REMOVAL);
+  Assert(n.getKind() == BAG_DUPLICATE_REMOVAL);
   set<Node> elements;
   const set<Node>& downwards = d_state.getElements(n);
   const set<Node>& upwards = d_state.getElements(n[0]);