Set incomplete if not applying ho extensionality (#6281)

[cvc5.git] / src / util / sexpr.cpp

diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index 91ef8a2718dd6d2e039694d9c33d7a5c663d93cf..85dd038bb43414eac777712ac0a9037db50cfbe2 100644 (file)
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -33,7 +33,7 @@
 #include "util/ostream_util.h"
 #include "util/smt2_quote_string.h"
 
-namespace CVC4 {
+namespace cvc5 {
 
 const int PrettySExprs::s_iosIndex = std::ios_base::xalloc();
 
@@ -90,12 +90,14 @@ SExpr::SExpr(const SExpr& other)
   Assert((d_children == NULL) == isAtom());
 }
 
-SExpr::SExpr(const CVC4::Integer& value)
+SExpr::SExpr(const cvc5::Integer& value)
     : d_sexprType(SEXPR_INTEGER),
       d_integerValue(value),
       d_rationalValue(0),
       d_stringValue(""),
-      d_children(NULL) {}
+      d_children(NULL)
+{
+}
 
 SExpr::SExpr(int value)
     : d_sexprType(SEXPR_INTEGER),
@@ -125,12 +127,14 @@ SExpr::SExpr(unsigned long int value)
       d_stringValue(""),
       d_children(NULL) {}
 
-SExpr::SExpr(const CVC4::Rational& value)
+SExpr::SExpr(const cvc5::Rational& value)
     : d_sexprType(SEXPR_RATIONAL),
       d_integerValue(0),
       d_rationalValue(value),
       d_stringValue(""),
-      d_children(NULL) {}
+      d_children(NULL)
+{
+}
 
 SExpr::SExpr(const std::string& value)
     : d_sexprType(SEXPR_STRING),
@@ -304,12 +308,14 @@ std::string SExpr::getValue() const {
   return std::string();
 }
 
-const CVC4::Integer& SExpr::getIntegerValue() const {
+const cvc5::Integer& SExpr::getIntegerValue() const
+{
   PrettyCheckArgument(isInteger(), this);
   return d_integerValue;
 }
 
-const CVC4::Rational& SExpr::getRationalValue() const {
+const cvc5::Rational& SExpr::getRationalValue() const
+{
   PrettyCheckArgument(isRational(), this);
   return d_rationalValue;
 }
@@ -377,4 +383,4 @@ SExpr SExpr::parseListOfListOfAtoms(
   return SExpr(parsedListsOfAtoms);
 }
 
-} /* CVC4 namespace */
+}  // namespace cvc5