From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 27 Oct 2021 23:40:31 +0000 (-0700)
Subject: Add comments for arith type rules. (#7488)
X-Git-Tag: cvc5-1.0.0~949
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=898290ddffe61d19588182cc01a8af39c9252156;p=cvc5.git

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 c9309a3d4..9bcc6ca2b 100644
--- 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 7bb623ad2..1fbd96648 100644
--- 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: