summaryrefslogtreecommitdiff
path: root/src/util/sexpr.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/sexpr.h')
-rw-r--r--src/util/sexpr.h16
1 files changed, 8 insertions, 8 deletions
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index aabbf473d..f4eaca663 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -35,7 +35,7 @@
#include "util/integer.h"
#include "util/rational.h"
-namespace CVC4 {
+namespace CVC5 {
class SExprKeyword
{
@@ -61,14 +61,14 @@ class CVC4_EXPORT SExpr
SExpr& operator=(const SExpr& other);
~SExpr();
- SExpr(const CVC4::Integer& value);
+ SExpr(const CVC5::Integer& value);
SExpr(int value);
SExpr(long int value);
SExpr(unsigned int value);
SExpr(unsigned long int value);
- SExpr(const CVC4::Rational& value);
+ SExpr(const CVC5::Rational& value);
SExpr(const std::string& value);
@@ -120,13 +120,13 @@ class CVC4_EXPORT SExpr
* Get the integer value of this S-expression. This will cause an
* error if this S-expression is not an integer.
*/
- const CVC4::Integer& getIntegerValue() const;
+ const CVC5::Integer& getIntegerValue() const;
/**
* Get the rational value of this S-expression. This will cause an
* error if this S-expression is not a rational.
*/
- const CVC4::Rational& getRationalValue() const;
+ const CVC5::Rational& getRationalValue() const;
/**
* Get the children of this S-expression. This will cause an error
@@ -211,10 +211,10 @@ class CVC4_EXPORT SExpr
} d_sexprType;
/** The value of an atomic integer-valued S-expression. */
- CVC4::Integer d_integerValue;
+ CVC5::Integer d_integerValue;
/** The value of an atomic rational-valued S-expression. */
- CVC4::Rational d_rationalValue;
+ CVC5::Rational d_rationalValue;
/** The value of an atomic S-expression. */
std::string d_stringValue;
@@ -301,6 +301,6 @@ class CVC4_EXPORT PrettySExprs
*/
std::ostream& operator<<(std::ostream& out, PrettySExprs ps);
-} /* CVC4 namespace */
+} // namespace CVC5
#endif /* CVC4__SEXPR_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback