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