cvc4-1.4
|
#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 | |
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/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.
Public-facing expression interface.
Definition in file expr.h.