smt_engine.h File Reference

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 "options/options.h"
#include "util/result.h"
#include "util/sexpr.h"
#include "util/hash.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)
ProofManager *	CVC4::smt::currentProofManager ()
StatisticsRegistry *	CVC4::stats::getStatisticsRegistry (SmtEngine *)

Detailed Description

SmtEngine: the main public entry point of libcvc4.

** Original author: Morgan Deters
** Major contributors: none
** Minor contributors (to current version): Martin Brain <>, Tim King, Clark Barrett, Christopher L. Conway, Andrew Reynolds, Kshitij Bansal, Dejan Jovanovic
** 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.

SmtEngine: the main public entry point of libcvc4.

Definition in file smt_engine.h.