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.

diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h
index cf23b4ea7c3ca3b26b1a74e5f40acf5179344a9c..75317e6d175f51ebeb08656a10bdae075d7afd47 100644 (file)
--- 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 b70c6c61d7e881704eabead86c2884b60348cb55..106b858984d15f1863bf75784464d59fabefb3d0 100644 (file)
--- 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"