#include <vector>
#include <string>
+#include "util/integer.h"
+#include "util/rational.h"
#include "util/Assert.h"
namespace CVC4 {
friend std::ostream &operator<<(std::ostream&, SexprTypes);
/** The value of an atomic integer-valued S-expression. */
- Integer d_integerValue;
+ CVC4::Integer d_integerValue;
/** The value of an atomic rational-valued S-expression. */
- Rational d_rationalValue;
+ CVC4::Rational d_rationalValue;
/** The value of an atomic S-expression. */
std::string d_stringValue;
d_children() {
}
- SExpr(const Integer& value) :
+ SExpr(const CVC4::Integer& value) :
d_sexprType(SEXPR_INTEGER),
d_integerValue(value),
d_rationalValue(0),
d_children() {
}
- SExpr(const Rational& value) :
+ SExpr(const CVC4::Rational& value) :
d_sexprType(SEXPR_RATIONAL),
d_integerValue(0),
d_rationalValue(value),
* Get the integer value of this S-expression. This will cause an
* error if this S-expression is not an integer.
*/
- const Integer& getIntegerValue() const;
+ const CVC4::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 Rational& getRationalValue() const;
+ const CVC4::Rational& getRationalValue() const;
/**
* Get the children of this S-expression. This will cause an error
return d_stringValue;
}
-inline const Integer& SExpr::getIntegerValue() const {
+inline const CVC4::Integer& SExpr::getIntegerValue() const {
AlwaysAssert( isInteger() );
return d_integerValue;
}
-inline const Rational& SExpr::getRationalValue() const {
+inline const CVC4::Rational& SExpr::getRationalValue() const {
AlwaysAssert( isRational() );
return d_rationalValue;
}