expr_manager.h File Reference

expr_manager.h More...

#include "cvc4_public.h"
#include <vector>
#include "expr/kind.h"
#include "expr/type.h"
#include "expr/expr.h"
#include "util/subrange_bound.h"
#include "util/statistics.h"
#include "util/sexpr.h"
#include "util/uninterpreted_constant.h"
#include "util/abstract_value.h"
#include "util/chain.h"
#include "util/predicate.h"
#include "util/bool.h"
#include "util/divisible.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"

Go to the source code of this file.

Data Structures
class	CVC4::ExprManager

Namespaces
	CVC4
	CVC4::expr
	CVC4::expr::pickle
	CVC4::context
	CVC4::stats

Functions
StatisticsRegistry *	CVC4::stats::getStatisticsRegistry (ExprManager *)

Detailed Description

expr_manager.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_manager_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): Andrew Reynolds, 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 manager interface

Public-facing expression manager interface.

Definition in file expr_manager.h.