From ebf4ff6cc2d93c59ef347f6db515bf3e44c036f3 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Tue, 11 Jan 2022 14:44:43 -0800
Subject: [PATCH] Adds a kind to hold RealAlgebraicNumber constants (#7908)

This PR adds a new kind that holds RealAlgebraicNumber constants. As it can not be a constant in the sense of isConst(), it is wrapped within an operator, similar to IAND or CARDINALITY_CONSTRAINT.
---
 src/theory/arith/kinds                       | 11 +++++++++++
 src/theory/arith/theory_arith_type_rules.cpp | 12 ++++++++++++
 src/theory/arith/theory_arith_type_rules.h   | 20 ++++++++++++++++++++
 3 files changed, 43 insertions(+)

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index e496cf335..4cd59c1a0 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -78,6 +78,14 @@ constant CONST_INTEGER \
     "util/rational.h" \
     "a multiple-precision integer constant; payload is an instance of the cvc5::Rational class"
 
+constant REAL_ALGEBRAIC_NUMBER_OP \
+    class \
+    RealAlgebraicNumber \
+    ::cvc5::RealAlgebraicNumberHashFunction \
+    "util/real_algebraic_number.h" \
+    "a real algebraic number constant; payload is an instance of the cvc5::RealAlgebraicNumber class"
+parameterized REAL_ALGEBRAIC_NUMBER REAL_ALGEBRAIC_NUMBER_OP 0 "a real algebraic number constant; payload is an instance of the cvc5::RealAlgebraicNumber class"
+
 enumerator REAL_TYPE \
     "::cvc5::theory::arith::RationalEnumerator" \
     "theory/arith/type_enumerator.h"
@@ -121,6 +129,9 @@ typerule POW ::cvc5::theory::arith::ArithOperatorTypeRule
 typerule CONST_RATIONAL ::cvc5::theory::arith::ArithConstantTypeRule
 typerule CONST_INTEGER ::cvc5::theory::arith::ArithConstantTypeRule
 
+typerule REAL_ALGEBRAIC_NUMBER_OP ::cvc5::theory::arith::ArithRealAlgebraicNumberOpTypeRule
+typerule REAL_ALGEBRAIC_NUMBER ::cvc5::theory::arith::ArithRealAlgebraicNumberTypeRule
+
 typerule LT ::cvc5::theory::arith::ArithRelationTypeRule
 typerule LEQ ::cvc5::theory::arith::ArithRelationTypeRule
 typerule GT ::cvc5::theory::arith::ArithRelationTypeRule
diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp
index 786b98196..c743639e0 100644
--- a/src/theory/arith/theory_arith_type_rules.cpp
+++ b/src/theory/arith/theory_arith_type_rules.cpp
@@ -36,6 +36,18 @@ TypeNode ArithConstantTypeRule::computeType(NodeManager* nodeManager,
   }
 }
 
+TypeNode ArithRealAlgebraicNumberOpTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  return nodeManager->realType();
+}
+TypeNode ArithRealAlgebraicNumberTypeRule::computeType(NodeManager* nodeManager,
+                                                       TNode n,
+                                                       bool check)
+{
+  return nodeManager->realType();
+}
+
 TypeNode ArithOperatorTypeRule::computeType(NodeManager* nodeManager,
                                             TNode n,
                                             bool check)
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 66b3ebedd..d1153f63f 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -35,6 +35,26 @@ class ArithConstantTypeRule
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for real algebraic numbers.
+ * Returns `realType`.
+ */
+class ArithRealAlgebraicNumberOpTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
+
+/**
+ * Type rule for real algebraic numbers.
+ * Returns `realType`.
+ */
+class ArithRealAlgebraicNumberTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
+
 /**
  * Type rule for arithmetic relations. Returns Boolean. Throws a type error
  * if the types of the children are not arithmetic or not comparable.
-- 
2.30.2