#include "cvc4_public.h"
#include "util/uninterpreted_constant.h"
#include "util/abstract_value.h"
#include "expr/kind.h"
#include "util/chain.h"
#include "util/predicate.h"
#include "util/bool.h"
#include "util/divisible.h"
#include "util/subrange_bound.h"
#include "util/rational.h"
#include "util/bitvector.h"
#include "util/array_store_all.h"
#include "util/datatype.h"
#include "util/ascription_type.h"
#include "util/tuple.h"
#include "util/record.h"
#include "util/emptyset.h"
#include "util/regexp.h"
#include <string>
#include <iostream>
#include <iterator>
#include <stdint.h>
#include "util/exception.h"
#include "util/language.h"
#include "util/hash.h"
#include "expr/options.h"

Data Structures
class	CVC4::NodeTemplate< ref_count >

class	CVC4::TypeCheckingException
	Exception thrown in the case of type-checking errors. More...

class	CVC4::ExportUnsupportedException
	Exception thrown in case of failure to export. More...

struct	CVC4::ExprHashFunction

class	CVC4::Expr
	Class encapsulating CVC4 expressions and methods for constructing new expressions. More...

class	CVC4::Expr::const_iterator
	Iterator type for the children of an Expr. More...

class	CVC4::expr::ExprSetDepth
	IOStream manipulator to set the maximum depth of Exprs when pretty-printing. More...

class	CVC4::expr::ExprSetDepth::Scope
	Set the expression depth on the output stream for the current stack scope. More...

class	CVC4::expr::ExprPrintTypes
	IOStream manipulator to print type ascriptions or not. More...

class	CVC4::expr::ExprPrintTypes::Scope
	Set the print-types state on the output stream for the current stack scope. More...

class	CVC4::expr::ExprDag
	IOStream manipulator to print expressions as a dag (or not). More...

class	CVC4::expr::ExprDag::Scope
	Set the dag state on the output stream for the current stack scope. More...

class	CVC4::expr::ExprSetLanguage
	IOStream manipulator to set the output language for Exprs. More...

class	CVC4::expr::ExprSetLanguage::Scope
	Set a language on the output stream for the current stack scope. More...

Namespaces
	CVC4

	CVC4::expr

	CVC4::expr::pickle

	CVC4::prop

	CVC4::smt

Macros
#define	__CVC4__EXPR_H

Functions
std::ostream &	CVC4::operator<< (std::ostream &out, const TypeCheckingException &e)

std::ostream &	CVC4::operator<< (std::ostream &out, const Expr &e)
	Output operator for expressions. More...

template<>
::CVC4::UninterpretedConstant const &	CVC4::Expr::getConst< ::CVC4::UninterpretedConstant > () const

template<>
::CVC4::AbstractValue const &	CVC4::Expr::getConst< ::CVC4::AbstractValue > () const

template<>
::CVC4::Kind const &	CVC4::Expr::getConst< ::CVC4::Kind > () const

template<>
::CVC4::Chain const &	CVC4::Expr::getConst< ::CVC4::Chain > () const

template<>
::CVC4::TypeConstant const &	CVC4::Expr::getConst< ::CVC4::TypeConstant > () const

template<>
::CVC4::Predicate const &	CVC4::Expr::getConst< ::CVC4::Predicate > () const

template<>
::CVC4::Divisible const &	CVC4::Expr::getConst< ::CVC4::Divisible > () const

template<>
::CVC4::SubrangeBounds const &	CVC4::Expr::getConst< ::CVC4::SubrangeBounds > () const

template<>
::CVC4::Rational const &	CVC4::Expr::getConst< ::CVC4::Rational > () const

template<>
::CVC4::BitVectorSize const &	CVC4::Expr::getConst< ::CVC4::BitVectorSize > () const

template<>
::CVC4::BitVector const &	CVC4::Expr::getConst< ::CVC4::BitVector > () const

template<>
::CVC4::BitVectorBitOf const &	CVC4::Expr::getConst< ::CVC4::BitVectorBitOf > () const

template<>
::CVC4::BitVectorExtract const &	CVC4::Expr::getConst< ::CVC4::BitVectorExtract > () const

template<>
::CVC4::BitVectorRepeat const &	CVC4::Expr::getConst< ::CVC4::BitVectorRepeat > () const

template<>
::CVC4::BitVectorZeroExtend const &	CVC4::Expr::getConst< ::CVC4::BitVectorZeroExtend > () const

template<>
::CVC4::BitVectorSignExtend const &	CVC4::Expr::getConst< ::CVC4::BitVectorSignExtend > () const

template<>
::CVC4::BitVectorRotateLeft const &	CVC4::Expr::getConst< ::CVC4::BitVectorRotateLeft > () const

template<>
::CVC4::BitVectorRotateRight const &	CVC4::Expr::getConst< ::CVC4::BitVectorRotateRight > () const

template<>
::CVC4::IntToBitVector const &	CVC4::Expr::getConst< ::CVC4::IntToBitVector > () const

template<>
::CVC4::ArrayStoreAll const &	CVC4::Expr::getConst< ::CVC4::ArrayStoreAll > () const

template<>
::CVC4::Datatype const &	CVC4::Expr::getConst< ::CVC4::Datatype > () const

template<>
::CVC4::AscriptionType const &	CVC4::Expr::getConst< ::CVC4::AscriptionType > () const

template<>
::CVC4::TupleSelect const &	CVC4::Expr::getConst< ::CVC4::TupleSelect > () const

template<>
::CVC4::TupleUpdate const &	CVC4::Expr::getConst< ::CVC4::TupleUpdate > () const

template<>
::CVC4::Record const &	CVC4::Expr::getConst< ::CVC4::Record > () const

template<>
::CVC4::RecordSelect const &	CVC4::Expr::getConst< ::CVC4::RecordSelect > () const

template<>
::CVC4::RecordUpdate const &	CVC4::Expr::getConst< ::CVC4::RecordUpdate > () const

template<>
::CVC4::EmptySet const &	CVC4::Expr::getConst< ::CVC4::EmptySet > () const

template<>
::CVC4::String const &	CVC4::Expr::getConst< ::CVC4::String > () const

template<>
::CVC4::RegExp const &	CVC4::Expr::getConst< ::CVC4::RegExp > () const

std::ostream &	CVC4::expr::operator<< (std::ostream &out, ExprSetDepth sd)
	Sets the default depth when pretty-printing a Expr to an ostream. More...

std::ostream &	CVC4::expr::operator<< (std::ostream &out, ExprPrintTypes pt)
	Sets the default print-types setting when pretty-printing an Expr to an ostream. More...

std::ostream &	CVC4::expr::operator<< (std::ostream &out, ExprDag d)
	Sets the default dag setting when pretty-printing a Expr to an ostream. More...

std::ostream &	CVC4::expr::operator<< (std::ostream &out, ExprSetLanguage l)
	Sets the output language when pretty-printing a Expr to an ostream. More...

Detailed Description

expr.h

This file automatically generated by:

/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/expr/mkexpr /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_template.h /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/booleans/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/uf/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arrays/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/sets/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/quantifiers/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/idl/kinds

for the CVC4 project.

** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
** Minor contributors (to current version): Liana Hadarean, Kshitij Bansal, Tim King, Christopher L. Conway
** 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.

Public-facing expression interface.

Definition in file expr.h.

Macro Definition Documentation

#define __CVC4__EXPR_H

Definition at line 88 of file expr.h.

Data Structures

Namespaces

Macros

Functions

Detailed Description

Macro Definition Documentation