cvc4-1.4
sexpr.h File Reference

Simple representation of S-expressions. More...

#include "cvc4_public.h"
#include <vector>
#include <string>
#include <iomanip>
#include <sstream>
#include "util/integer.h"
#include "util/rational.h"
#include "util/exception.h"

Go to the source code of this file.

Data Structures

class  CVC4::SExprKeyword
 
class  CVC4::SExpr
 A simple S-expression. More...
 

Namespaces

 CVC4
 

Functions

std::ostream & CVC4::operator<< (std::ostream &out, const SExpr &sexpr)
 

Detailed Description

Simple representation of S-expressions.

** Original author: Christopher L. Conway
** Major contributors: Tim King, Morgan Deters
** Minor contributors (to current version): Dejan Jovanovic
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014  New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.

Simple representation of S-expressions. These are used when a simple, and obvious interface for basic expressions is appropraite.

These are quite ineffecient. These are totally disconnected from any ExprManager. These keep unique copies of all of their children. These are VERY overly verbose and keep much more data than is needed.

Definition in file sexpr.h.