Consolidate language types (#7065)

This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.

8 files changed, 32 insertions, 46 deletions

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index feacc8837..31a22b44a 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -898,7 +898,7 @@ const std::vector<std::shared_ptr<DTypeConstructor> >& DType::getConstructors()
 std::ostream& operator<<(std::ostream& os, const DType& dt)
 {
   // can only output datatypes in the cvc5 native language
-  language::SetLanguage::Scope ls(os, language::output::LANG_CVC);
+  language::SetLanguage::Scope ls(os, Language::LANG_CVC);
   dt.toStream(os);
   return os;
 }
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index b71f49e87..3603c776a 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -685,7 +685,7 @@ void DTypeConstructor::toStream(std::ostream& out) const
 std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor)
 {
   // can only output datatypes in the cvc5 native language
-  language::SetLanguage::Scope ls(os, language::output::LANG_CVC);
+  language::SetLanguage::Scope ls(os, Language::LANG_CVC);
   ctor.toStream(os);
   return os;
 }
diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp
index c8497433b..1898a4186 100644
--- a/src/expr/dtype_selector.cpp
+++ b/src/expr/dtype_selector.cpp
@@ -84,7 +84,7 @@ void DTypeSelector::toStream(std::ostream& out) const
 std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg)
 {
   // can only output datatypes in the cvc5 native language
-  language::SetLanguage::Scope ls(os, language::output::LANG_CVC);
+  language::SetLanguage::Scope ls(os, Language::LANG_CVC);
   arg.toStream(os);
   return os;
 }
diff --git a/src/expr/node.h b/src/expr/node.h
index a406b3d13..1ce915472 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -826,11 +826,10 @@ public:
    * print it fully
    * @param language the language in which to output
    */
-  inline void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dagThreshold = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const
+  inline void toStream(std::ostream& out,
+                       int toDepth = -1,
+                       size_t dagThreshold = 1,
+                       Language language = Language::LANG_AUTO) const
   {
     assertTNodeNotExpired();
     d_nv->toStream(out, toDepth, dagThreshold, language);
@@ -1483,17 +1482,13 @@ Node NodeTemplate<ref_count>::substitute(
  * to meet. A cleaner solution is welcomed.
  */
 static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) {
-  Warning() << Node::setdepth(-1)
-            << Node::dag(true)
-            << Node::setlanguage(language::output::LANG_AST)
-            << n << std::endl;
+  Warning() << Node::setdepth(-1) << Node::dag(true)
+            << Node::setlanguage(Language::LANG_AST) << n << std::endl;
   Warning().flush();
 }
 static void __attribute__((used)) debugPrintNodeNoDag(const NodeTemplate<true>& n) {
-  Warning() << Node::setdepth(-1)
-            << Node::dag(false)
-            << Node::setlanguage(language::output::LANG_AST)
-            << n << std::endl;
+  Warning() << Node::setdepth(-1) << Node::dag(false)
+            << Node::setlanguage(Language::LANG_AST) << n << std::endl;
   Warning().flush();
 }
 static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) {
@@ -1502,17 +1497,13 @@ static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n)
 }
 
 static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) {
-  Warning() << Node::setdepth(-1)
-            << Node::dag(true)
-            << Node::setlanguage(language::output::LANG_AST)
-            << n << std::endl;
+  Warning() << Node::setdepth(-1) << Node::dag(true)
+            << Node::setlanguage(Language::LANG_AST) << n << std::endl;
   Warning().flush();
 }
 static void __attribute__((used)) debugPrintTNodeNoDag(const NodeTemplate<false>& n) {
-  Warning() << Node::setdepth(-1)
-            << Node::dag(false)
-            << Node::setlanguage(language::output::LANG_AST)
-            << n << std::endl;
+  Warning() << Node::setdepth(-1) << Node::dag(false)
+            << Node::setlanguage(Language::LANG_AST) << n << std::endl;
   Warning().flush();
 }
 static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& n) {
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 10e32ac71..46ba3d191 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -37,8 +37,8 @@ namespace expr {
 string NodeValue::toString() const {
   stringstream ss;
 
-  OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO
-                                             : options::outputLanguage();
+  Language outlang =
+      (this == &null()) ? Language::LANG_AUTO : options::outputLanguage();
   toStream(ss, -1, false, outlang);
   return ss.str();
 }
@@ -46,7 +46,7 @@ string NodeValue::toString() const {
 void NodeValue::toStream(std::ostream& out,
                          int toDepth,
                          size_t dag,
-                         OutputLanguage language) const
+                         Language language) const
 {
   // Ensure that this node value is live for the length of this call.
   // It really breaks things badly if we don't have a nonzero ref
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index c86651648..ba30dc8fb 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -233,7 +233,7 @@ class NodeValue
   void toStream(std::ostream& out,
                 int toDepth = -1,
                 size_t dag = 1,
-                OutputLanguage = language::output::LANG_AUTO) const;
+                Language = Language::LANG_AUTO) const;
 
   void printAst(std::ostream& out, int indent = 0) const;
 
@@ -525,17 +525,13 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
  * flushes the stream.
  */
 static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) {
-  Warning() << Node::setdepth(-1)
-            << Node::dag(true)
-            << Node::setlanguage(language::output::LANG_AST)
-            << *nv << std::endl;
+  Warning() << Node::setdepth(-1) << Node::dag(true)
+            << Node::setlanguage(Language::LANG_AST) << *nv << std::endl;
   Warning().flush();
 }
 static void __attribute__((used)) debugPrintNodeValueNoDag(const expr::NodeValue* nv) {
-  Warning() << Node::setdepth(-1)
-            << Node::dag(false)
-            << Node::setlanguage(language::output::LANG_AST)
-            << *nv << std::endl;
+  Warning() << Node::setdepth(-1) << Node::dag(false)
+            << Node::setlanguage(Language::LANG_AST) << *nv << std::endl;
   Warning().flush();
 }
 static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* nv) {
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 52a21040e..fa6a56c99 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -660,7 +660,8 @@ bool TypeNode::isSygusDatatype() const
 
 std::string TypeNode::toString() const {
   std::stringstream ss;
-  OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage();
+  Language outlang =
+      (this == &s_null) ? Language::LANG_AUTO : options::outputLanguage();
   d_nv->toStream(ss, -1, 0, outlang);
   return ss.str();
 }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 21e7b4d28..2f854f581 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -374,7 +374,9 @@ private:
    * @param out the stream to serialize this node to
    * @param language the language in which to output
    */
-  inline void toStream(std::ostream& out, OutputLanguage language = language::output::LANG_AUTO) const {
+  inline void toStream(std::ostream& out,
+                       Language language = Language::LANG_AUTO) const
+  {
     d_nv->toStream(out, -1, 0, language);
   }
 
@@ -1029,17 +1031,13 @@ inline unsigned TypeNode::getFloatingPointSignificandSize() const {
  * to meet. A cleaner solution is welcomed.
  */
 static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) {
-  Warning() << Node::setdepth(-1)
-            << Node::dag(true)
-            << Node::setlanguage(language::output::LANG_AST)
-            << n << std::endl;
+  Warning() << Node::setdepth(-1) << Node::dag(true)
+            << Node::setlanguage(Language::LANG_AST) << n << std::endl;
   Warning().flush();
 }
 static void __attribute__((used)) debugPrintTypeNodeNoDag(const TypeNode& n) {
-  Warning() << Node::setdepth(-1)
-            << Node::dag(false)
-            << Node::setlanguage(language::output::LANG_AST)
-            << n << std::endl;
+  Warning() << Node::setdepth(-1) << Node::dag(false)
+            << Node::setlanguage(Language::LANG_AST) << n << std::endl;
   Warning().flush();
 }
 static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) {