9 #ifndef CIRCT_CONVERSION_SMTTOZ3LLVM_H
10 #define CIRCT_CONVERSION_SMTTOZ3LLVM_H
14 #include "mlir/Dialect/LLVMIR/LLVMDialect.h"
15 #include "llvm/ADT/StringRef.h"
20 #define GEN_PASS_DECL_LOWERSMTTOZ3LLVM
21 #include "circt/Conversion/Passes.h.inc"
41 mlir::LLVM::GlobalOp
ctx);
53 mlir::LLVM::GlobalOp
ctx);
59 const mlir::LLVM::GlobalOp
ctx;
62 DenseMap<StringAttr, mlir::LLVM::LLVMFuncOp>
funcMap;
75 RewritePatternSet &
patterns, TypeConverter &converter,
A namespace that is used to store existing names and generate new names in some scope within the IR.
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
void populateSMTToZ3LLVMTypeConverter(TypeConverter &converter)
Populate the given type converter with the SMT to LLVM type conversions.
void populateSMTToZ3LLVMConversionPatterns(RewritePatternSet &patterns, TypeConverter &converter, SMTGlobalsHandler &globals, const LowerSMTToZ3LLVMOptions &options)
Add the SMT to LLVM IR conversion patterns to 'patterns'.
A symbol cache for LLVM globals and functions relevant to SMT lowering patterns.
DenseMap< StringAttr, mlir::LLVM::GlobalOp > stringCache
DenseMap< StringAttr, mlir::LLVM::LLVMFuncOp > funcMap
DenseMap< Block *, Value > solverCache
static SMTGlobalsHandler create(OpBuilder &builder, ModuleOp module)
Creates the LLVM global operations to store the pointers to the solver and the context and returns a ...
SMTGlobalsHandler(ModuleOp module, mlir::LLVM::GlobalOp solver, mlir::LLVM::GlobalOp ctx)
Initializes the caches and keeps track of the given globals to store the pointers to the SMT solver a...
const mlir::LLVM::GlobalOp ctx
The global storing the pointer to the SMT context object currently active.
const mlir::LLVM::GlobalOp solver
The global storing the pointer to the SMT solver object currently active.
DenseMap< Block *, Value > ctxCache