Modifying emptyset.h and sexpr. Adding SetLanguage.

- Modifies expr/emptyset.h to use SetType only as an incomplete type within expr/emptyset.h. This breaks the include cycle between expr/emptyset.h, expr/expr.h and expr/type.h.
- Refactors SExpr to avoid a potentially infinite cycle. This is likely overkill, but it works.
- Moving Expr::setlanguage and related utilities out of the Expr class and into their own file. This allows files in util/ to know the output language set on an ostream.

1 files changed, 1 insertions, 1 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index f3bbc65cc..e6478440d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -579,7 +579,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
     }else{
       if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
         std::stringstream ss;
-        ss << Expr::setlanguage(options::outputLanguage());
+        ss << language::SetLanguage(options::outputLanguage());
         ss << "e_" << tn;
         mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
         Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;