diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-10-27 16:40:31 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-27 23:40:31 +0000 |
commit | 898290ddffe61d19588182cc01a8af39c9252156 (patch) | |
tree | 4d9d9e3fd2178db9c4fce777a6b3c8f05899e2eb /src/theory/arith | |
parent | 5ea33ca829d257d408a242974b28bd6defafff6e (diff) |
Add comments for arith type rules. (#7488)
Add comments for the arithmetic type rules.
Fixes cvc5/cvc5-projects#273.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.cpp | 6 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 26 |
2 files changed, 29 insertions, 3 deletions
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: |