LowerSMTToZ3LLVM.cpp File Reference

#include "circt/Conversion/SMTToZ3LLVM.h"
#include "circt/Dialect/SMT/SMTOps.h"
#include "circt/Support/Namespace.h"
#include "mlir/Conversion/ArithToLLVM/ArithToLLVM.h"
#include "mlir/Conversion/ControlFlowToLLVM/ControlFlowToLLVM.h"
#include "mlir/Conversion/FuncToLLVM/ConvertFuncToLLVM.h"
#include "mlir/Conversion/LLVMCommon/ConversionTarget.h"
#include "mlir/Conversion/LLVMCommon/TypeConverter.h"
#include "mlir/Conversion/SCFToControlFlow/SCFToControlFlow.h"
#include "mlir/Dialect/ControlFlow/IR/ControlFlow.h"
#include "mlir/Dialect/Func/IR/FuncOps.h"
#include "mlir/Dialect/LLVMIR/FunctionCallUtils.h"
#include "mlir/Dialect/LLVMIR/LLVMAttrs.h"
#include "mlir/Dialect/LLVMIR/LLVMDialect.h"
#include "mlir/Dialect/SCF/IR/SCF.h"
#include "mlir/IR/BuiltinDialect.h"
#include "mlir/Pass/Pass.h"
#include "mlir/Transforms/DialectConversion.h"
#include "llvm/ADT/TypeSwitch.h"
#include "llvm/Support/Debug.h"
#include "circt/Conversion/Passes.h.inc"

Include dependency graph for LowerSMTToZ3LLVM.cpp:

Go to the source code of this file.

Namespaces
	circt
	The InstanceGraph op interface, see InstanceGraphInterface.td for more details.

Macros
#define	DEBUG_TYPE   "lower-smt-to-z3-llvm"
#define	GEN_PASS_DEF_LOWERSMTTOZ3LLVM
#define	ADD_VARIADIC_PATTERN(OP, APINAME, MIN_NUM_ARGS)
#define	ADD_ONE_TO_ONE_PATTERN(OP, APINAME, NUM_ARGS)

Macro Definition Documentation

ADD_ONE_TO_ONE_PATTERN

#define ADD_ONE_TO_ONE_PATTERN	(		OP,
			APINAME,
			NUM_ARGS
	)

Value:

  patterns.add<OneToOneSMTPattern<OP>>(/*NOLINT(bugprone-macro-parentheses)*/  \
                                       converter, patterns.getContext(),       \
                                       globals, options, APINAME, NUM_ARGS);

ADD_VARIADIC_PATTERN

#define ADD_VARIADIC_PATTERN	(		OP,
			APINAME,
			MIN_NUM_ARGS
	)

Value:

  patterns.add<VariadicSMTPattern<OP>>(/*NOLINT(bugprone-macro-parentheses)*/  \
                                       converter, patterns.getContext(),       \
                                       globals, options, APINAME,              \
                                       MIN_NUM_ARGS);

DEBUG_TYPE

#define DEBUG_TYPE   "lower-smt-to-z3-llvm"

Definition at line 30 of file LowerSMTToZ3LLVM.cpp.

GEN_PASS_DEF_LOWERSMTTOZ3LLVM

#define GEN_PASS_DEF_LOWERSMTTOZ3LLVM

Definition at line 33 of file LowerSMTToZ3LLVM.cpp.