SMTAPI.h File Reference

#include "llvm/ADT/APFloat.h"
#include "llvm/ADT/APSInt.h"
#include "llvm/ADT/FoldingSet.h"
#include "llvm/Support/Compiler.h"
#include "llvm/Support/raw_ostream.h"
#include <memory>

Go to the source code of this file.

Classes
class	llvm::SMTSort
	Generic base class for SMT sorts. More...
class	llvm::SMTExpr
	Generic base class for SMT exprs. More...
class	llvm::SMTSolverStatistics
class	llvm::SMTSolver
	Generic base class for SMT Solvers. More...

Namespaces
namespace	llvm
	This is an optimization pass for GlobalISel generic memory operations.

Typedefs
using	llvm::SMTSortRef = const SMTSort *
	Shared pointer for SMTSorts, used by SMTSolver API.
using	llvm::SMTExprRef = const SMTExpr *
	Shared pointer for SMTExprs, used by SMTSolver API.
using	llvm::SMTSolverRef = std::shared_ptr<SMTSolver>
	Shared pointer for SMTSolvers.

Functions
LLVM_ABI SMTSolverRef	llvm::CreateZ3Solver ()
	Convenience method to create and Z3Solver object.