From 4ae38ac43e7218c28e4dd0bb20902b2ce4268dfc Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 29 Apr 2022 13:49:21 -0700
Subject: [PATCH] Add simple type rule for real-or-int arguments (#8685)

This adds a simple type rule, ARealOrInteger, which checks whether the
argument of an operator is either a Real or and Int. Note that this
is currently equivalent to AReal, but the plan is to make AReal
strict in the future.
---
 src/expr/type_checker_util.h | 11 +++++++++++
 src/theory/arith/kinds       | 36 ++++++++++++++++++------------------
 2 files changed, 29 insertions(+), 18 deletions(-)

diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h
index cf23b4ea7..75317e6d1 100644
--- a/src/expr/type_checker_util.h
+++ b/src/expr/type_checker_util.h
@@ -112,6 +112,17 @@ struct AReal
   constexpr static const char* typeName = "real";
 };
 
+/** Argument is a real or an integer */
+struct ARealOrInteger
+{
+  static bool checkArg(TNode n, size_t arg)
+  {
+    TypeNode t = n[arg].getType(true);
+    return t.isRealOrInt();
+  }
+  constexpr static const char* typeName = "real or integer";
+};
+
 /** Argument is a regexp */
 struct ARegExp
 {
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index b70c6c61d..106b85898 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -140,10 +140,10 @@ typerule GEQ ::cvc5::internal::theory::arith::ArithRelationTypeRule
 typerule INDEXED_ROOT_PREDICATE_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule INDEXED_ROOT_PREDICATE ::cvc5::internal::theory::arith::IndexedRootPredicateTypeRule
 
-typerule TO_REAL ::cvc5::internal::theory::arith::ArithOperatorTypeRule
-typerule CAST_TO_REAL ::cvc5::internal::theory::arith::ArithOperatorTypeRule
-typerule TO_INTEGER ::cvc5::internal::theory::arith::ArithOperatorTypeRule
-typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>"
+typerule TO_REAL "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule CAST_TO_REAL "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule TO_INTEGER "SimpleTypeRule<RInteger, ARealOrInteger>"
+typerule IS_INTEGER "SimpleTypeRule<RBool, ARealOrInteger>"
 
 typerule ABS ::cvc5::internal::theory::arith::ArithOperatorTypeRule
 typerule INTS_DIVISION "SimpleTypeRule<RInteger, AInteger, AInteger>"
@@ -155,22 +155,22 @@ typerule DIVISION_TOTAL ::cvc5::internal::theory::arith::ArithOperatorTypeRule
 typerule INTS_DIVISION_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
 typerule INTS_MODULUS_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
 
-typerule EXPONENTIAL "SimpleTypeRule<RReal, AReal>"
-typerule SINE "SimpleTypeRule<RReal, AReal>"
-typerule COSINE "SimpleTypeRule<RReal, AReal>"
-typerule TANGENT "SimpleTypeRule<RReal, AReal>"
-typerule COSECANT "SimpleTypeRule<RReal, AReal>"
-typerule SECANT "SimpleTypeRule<RReal, AReal>"
-typerule COTANGENT "SimpleTypeRule<RReal, AReal>"
-typerule ARCSINE "SimpleTypeRule<RReal, AReal>"
-typerule ARCCOSINE "SimpleTypeRule<RReal, AReal>"
-typerule ARCTANGENT "SimpleTypeRule<RReal, AReal>"
-typerule ARCCOSECANT "SimpleTypeRule<RReal, AReal>"
-typerule ARCSECANT "SimpleTypeRule<RReal, AReal>"
-typerule ARCCOTANGENT "SimpleTypeRule<RReal, AReal>"
+typerule EXPONENTIAL "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule SINE "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule COSINE "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule TANGENT "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule COSECANT "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule SECANT "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule COTANGENT "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule ARCSINE "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule ARCCOSINE "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule ARCTANGENT "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule ARCCOSECANT "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule ARCSECANT "SimpleTypeRule<RReal, ARealOrInteger>"
+typerule ARCCOTANGENT "SimpleTypeRule<RReal, ARealOrInteger>"
 typerule POW2 "SimpleTypeRule<RInteger, AInteger>"
 
-typerule SQRT "SimpleTypeRule<RReal, AReal>"
+typerule SQRT "SimpleTypeRule<RReal, ARealOrInteger>"
 
 nullaryoperator PI "pi"
 
-- 
2.30.2