Add comments for arith type rules. (#7488)

Add comments for the arithmetic type rules.

Fixes cvc5/cvc5-projects#273.

diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp
index c9309a3d406b1dfea5726ba26bf9fb94cb468e23..9bcc6ca2b24a615ea0641b0f5c2ed5af41e3d544 100644 (file)
--- a/src/theory/arith/theory_arith_type_rules.cpp
+++ b/src/theory/arith/theory_arith_type_rules.cpp
@@ -104,7 +104,7 @@ TypeNode IAndOpTypeRule::computeType(NodeManager* nodeManager,
 {
   if (n.getKind() != kind::IAND_OP)
   {
-    InternalError() << "IAND_OP typerule invoked for IAND_OP kind";
+    InternalError() << "IAND_OP typerule invoked for " << n << " instead of IAND_OP kind";
   }
   TypeNode iType = nodeManager->integerType();
   std::vector<TypeNode> argTypes;
@@ -119,7 +119,7 @@ TypeNode IAndTypeRule::computeType(NodeManager* nodeManager,
 {
   if (n.getKind() != kind::IAND)
   {
-    InternalError() << "IAND typerule invoked for IAND kind";
+    InternalError() << "IAND typerule invoked for " << n << " instead of IAND kind";
   }
   if (check)
   {
@@ -139,7 +139,7 @@ TypeNode Pow2TypeRule::computeType(NodeManager* nodeManager,
 {
   if (n.getKind() != kind::POW2)
   {
-    InternalError() << "POW2 typerule invoked for POW2 kind";
+    InternalError() << "POW2 typerule invoked for " << n << " instead of POW2 kind";
   }
   if (check)
   {

diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 7bb623ad2207db3be4714588794b1d5e718bdb91..1fbd9664864021b421f9f1745ad5ed946867f7de 100644 (file)
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -25,42 +25,68 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
+/**
+ * Type rule for arithmetic values.
+ * Returns `integerType` or `realType` depending on the value.
+ */
 class ArithConstantTypeRule
 {
  public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for arithmetic operators.
+ * Takes care of mixed-integer operators, cases and (total) division.
+ */
 class ArithOperatorTypeRule
 {
  public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/** Type rule for nullary real operators. */
 class RealNullaryOperatorTypeRule
 {
  public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for the IAND operator kind.
+ * Always returns (integerType, integerType) -> integerType.
+ */
 class IAndOpTypeRule
 {
  public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for the IAND kind.
+ * Always returns integerType.
+ */
 class IAndTypeRule
 {
  public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for the POW2 operator.
+ * Always returns integerType.
+ */
 class Pow2TypeRule
 {
  public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for the IndexedRootPredicate operator.
+ * Checks that the two arguments are booleanType and realType, always returns
+ * booleanType.
+ */
 class IndexedRootPredicateTypeRule
 {
  public: