cvc4-1.3
CVC4::SExpr Class Reference

A simple S-expression. More...

#include <sexpr.h>

Public Types

typedef SExprKeyword Keyword
 

Public Member Functions

 SExpr ()
 
 SExpr (const CVC4::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 std::string &value)
 
 SExpr (const char *value)
 This constructs a string expression from a const char* value. More...
 
 SExpr (bool value)
 This adds a convenience wrapper to SExpr to cast from bools. More...
 
 SExpr (const Keyword &value)
 
 SExpr (const std::vector< SExpr > &children)
 
bool isAtom () const
 Is this S-expression an atom? More...
 
bool isInteger () const
 Is this S-expression an integer? More...
 
bool isRational () const
 Is this S-expression a rational? More...
 
bool isString () const
 Is this S-expression a string? More...
 
bool isKeyword () const
 Is this S-expression a keyword? More...
 
std::string getValue () const
 Get the string value of this S-expression. More...
 
const CVC4::IntegergetIntegerValue () const
 Get the integer value of this S-expression. More...
 
const CVC4::RationalgetRationalValue () const
 Get the rational value of this S-expression. More...
 
const std::vector< SExpr > & getChildren () const
 Get the children of this S-expression. More...
 
bool operator== (const SExpr &s) const
 Is this S-expression equal to another? More...
 
bool operator!= (const SExpr &s) const
 Is this S-expression different from another? More...
 

Detailed Description

A simple S-expression.

An S-expression is either an atom with a string value, or a list of other S-expressions.

Definition at line 51 of file sexpr.h.

Member Typedef Documentation

Definition at line 75 of file sexpr.h.

Constructor & Destructor Documentation

CVC4::SExpr::SExpr ( )
inline

Definition at line 77 of file sexpr.h.

CVC4::SExpr::SExpr ( const CVC4::Integer value)
inline

Definition at line 85 of file sexpr.h.

CVC4::SExpr::SExpr ( int  value)
inline

Definition at line 93 of file sexpr.h.

CVC4::SExpr::SExpr ( long int  value)
inline

Definition at line 101 of file sexpr.h.

CVC4::SExpr::SExpr ( unsigned int  value)
inline

Definition at line 109 of file sexpr.h.

CVC4::SExpr::SExpr ( unsigned long int  value)
inline

Definition at line 117 of file sexpr.h.

CVC4::SExpr::SExpr ( const CVC4::Rational value)
inline

Definition at line 125 of file sexpr.h.

CVC4::SExpr::SExpr ( const std::string &  value)
inline

Definition at line 133 of file sexpr.h.

CVC4::SExpr::SExpr ( const char *  value)
inline

This constructs a string expression from a const char* value.

This cannot be removed in order to support SExpr("foo"). Given the other constructors this SExpr("foo") converts to bool. instead of SExpr(string("foo")).

Definition at line 147 of file sexpr.h.

CVC4::SExpr::SExpr ( bool  value)
inline

This adds a convenience wrapper to SExpr to cast from bools.

This is internally handled as the strings "true" and "false"

Definition at line 159 of file sexpr.h.

CVC4::SExpr::SExpr ( const Keyword value)
inline

Definition at line 167 of file sexpr.h.

CVC4::SExpr::SExpr ( const std::vector< SExpr > &  children)
inline

Definition at line 175 of file sexpr.h.

Member Function Documentation

const std::vector< SExpr > & CVC4::SExpr::getChildren ( ) const
inline

Get the children of this S-expression.

This will cause an error if this S-expression is not a list.

Definition at line 283 of file sexpr.h.

References CVC4::CheckArgument(), and isAtom().

const CVC4::Integer & CVC4::SExpr::getIntegerValue ( ) const
inline

Get the integer value of this S-expression.

This will cause an error if this S-expression is not an integer.

Definition at line 273 of file sexpr.h.

References CVC4::CheckArgument(), and isInteger().

const CVC4::Rational & CVC4::SExpr::getRationalValue ( ) const
inline

Get the rational value of this S-expression.

This will cause an error if this S-expression is not a rational.

Definition at line 278 of file sexpr.h.

References CVC4::CheckArgument(), and isRational().

std::string CVC4::SExpr::getValue ( ) const
inline

Get the string value of this S-expression.

This will cause an error if this S-expression is not an atom.

Definition at line 250 of file sexpr.h.

References CVC4::CheckArgument(), CVC4::Rational::getDouble(), isAtom(), and CVC4::Integer::toString().

bool CVC4::SExpr::isAtom ( ) const
inline

Is this S-expression an atom?

Definition at line 230 of file sexpr.h.

Referenced by getChildren(), and getValue().

bool CVC4::SExpr::isInteger ( ) const
inline

Is this S-expression an integer?

Definition at line 234 of file sexpr.h.

Referenced by getIntegerValue().

bool CVC4::SExpr::isKeyword ( ) const
inline

Is this S-expression a keyword?

Definition at line 246 of file sexpr.h.

bool CVC4::SExpr::isRational ( ) const
inline

Is this S-expression a rational?

Definition at line 238 of file sexpr.h.

Referenced by getRationalValue().

bool CVC4::SExpr::isString ( ) const
inline

Is this S-expression a string?

Definition at line 242 of file sexpr.h.

bool CVC4::SExpr::operator!= ( const SExpr s) const
inline

Is this S-expression different from another?

Definition at line 296 of file sexpr.h.

bool CVC4::SExpr::operator== ( const SExpr s) const
inline

Is this S-expression equal to another?

Definition at line 288 of file sexpr.h.


The documentation for this class was generated from the following file: