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.

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index e496cf335fdc20b9348a40853d2951d44732fea4..4cd59c1a08c6e91dfc85b075e49a0857bb417abe 100644 (file)
--- 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 786b98196f665869aabc7dbfd0da928bdb90bcb2..c743639e0f7dedc93812aa5995744cbbcec95469 100644 (file)
--- 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 66b3ebedd783031891b274e57e04976a355a73fe..d1153f63f1ec1c0f500f57b7a37f1b22067640de 100644 (file)
--- 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.