cvc4-1.4
expr.h File Reference

expr.h More...

#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"

Go to the source code of this file.

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

Copyright 2010-2014 New York University and The University of Iowa, and as below.

This file automatically generated by:

/builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/expr/mkexpr /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_template.h /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/booleans/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/uf/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/arrays/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/sets/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-redhat-linux-gnu/production-abc-proof/../../../src/theory/quantifiers/kinds /builddir/build/BUILD/cvc4-1.4/builds/powerpc64le-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.

Public-facing expression interface.

Definition in file expr.h.

Macro Definition Documentation

#define __CVC4__EXPR_H

Definition at line 88 of file expr.h.