Add documentation for theory_bags_type_rules.h (#6268)

1 files changed, 38 insertions, 0 deletions

diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
index f48001c5e..909f607a9 100644
--- a/src/theory/bags/theory_bags_type_rules.h
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -27,58 +27,96 @@ class NodeManager;
 namespace theory {
 namespace bags {
 
+/**
+ * Type rule for binary operators (union_max, union_disjoint, intersection_min
+ * difference_subtract, difference_remove)
+ * to check if the two arguments are of the same sort.
+ */
 struct BinaryOperatorTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
   static bool computeIsConst(NodeManager* nodeManager, TNode n);
 }; /* struct BinaryOperatorTypeRule */
 
+/**
+ * Type rule for binary operator subbag to check if the two arguments have the
+ * same sort.
+ */
 struct SubBagTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct SubBagTypeRule */
 
+/**
+ * Type rule for binary operator bag.count to check the sort of the first
+ * argument matches the element sort of the given bag.
+ */
 struct CountTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct CountTypeRule */
 
+/**
+ * Type rule for duplicate_removal to check the argument is of a bag.
+ */
 struct DuplicateRemovalTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct DuplicateRemovalTypeRule */
 
+/**
+ * Type rule for (bag op e) operator to check the sort of e matches the sort
+ * stored in op.
+ */
 struct MkBagTypeRule
 {
   static TypeNode computeType(NodeManager* nm, TNode n, bool check);
   static bool computeIsConst(NodeManager* nodeManager, TNode n);
 }; /* struct MkBagTypeRule */
 
+/**
+ * Type rule for bag.is_singleton to check the argument is of a bag.
+ */
 struct IsSingletonTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct IsMkBagTypeRule */
 
+/**
+ * Type rule for (as emptybag (Bag ...))
+ */
 struct EmptyBagTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct EmptyBagTypeRule */
 
+/**
+ * Type rule for (bag.card ..) to check the argument is of a bag.
+ */
 struct CardTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct CardTypeRule */
 
+/**
+ * Type rule for (bag.choose ..) to check the argument is of a bag.
+ */
 struct ChooseTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct ChooseTypeRule */
 
+/**
+ * Type rule for (bag.from_set ..) to check the argument is of a set.
+ */
 struct FromSetTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct FromSetTypeRule */
 
+/**
+ * Type rule for (bag.to_set ..) to check the argument is of a bag.
+ */
 struct ToSetTypeRule
 {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);