cvc4-1.3
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 "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 *)
 

Detailed Description

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.