cvc4-1.3
|
SmtEngine: the main public entry point of libcvc4. More...
#include "cvc4_public.h"
#include <string>
#include <vector>
#include "context/cdlist_forward.h"
#include "context/cdhashmap_forward.h"
#include "context/cdhashset_forward.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "util/proof.h"
#include "smt/modal_exception.h"
#include "smt/logic_exception.h"
#include "util/hash.h"
#include "options/options.h"
#include "util/result.h"
#include "util/sexpr.h"
#include "util/statistics.h"
#include "theory/logic_info.h"
Go to the source code of this file.
Data Structures | |
class | CVC4::NodeTemplate< ref_count > |
class | CVC4::SmtEngine |
Namespaces | |
CVC4 | |
CVC4::context | |
CVC4::prop | |
CVC4::smt | |
CVC4::theory | |
CVC4::stats | |
Typedefs | |
typedef NodeTemplate< true > | CVC4::Node |
typedef NodeTemplate< false > | CVC4::TNode |
typedef context::CDList < Command *, CommandCleanup > | CVC4::smt::CommandList |
Functions | |
void | CVC4::smt::beforeSearch (std::string, bool, SmtEngine *) throw (ModalException) |
StatisticsRegistry * | CVC4::stats::getStatisticsRegistry (SmtEngine *) |
SmtEngine: the main public entry point of libcvc4.
** Original author: Morgan Deters ** Major contributors: none ** Minor contributors (to current version): Andrew Reynolds, Tim King, Clark Barrett, Christopher L. Conway, Kshitij Bansal, Dejan Jovanovic ** This file is part of the CVC4 project. ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.
SmtEngine: the main public entry point of libcvc4.
Definition in file smt_engine.h.