From: Gereon Kremer 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 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: