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