LLVM 19.0.0git
Classes | Namespaces | Typedefs | Functions
SMTAPI.h File Reference
#include "llvm/ADT/APFloat.h"
#include "llvm/ADT/APSInt.h"
#include "llvm/ADT/FoldingSet.h"
#include "llvm/Support/raw_ostream.h"
#include <memory>

Go to the source code of this file.


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...


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


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.


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