SMTOps.cpp File Reference

#include "mlir/Dialect/SMT/IR/SMTOps.h"
#include "mlir/IR/Builders.h"
#include "mlir/IR/OpImplementation.h"
#include "llvm/ADT/APSInt.h"
#include "mlir/Dialect/SMT/IR/SMT.cpp.inc"

Go to the source code of this file.

Macros
#define	GET_OP_CLASSES

Functions
static LogicalResult	parseSameOperandTypeVariadicToBoolOp (OpAsmParser &parser, OperationState &result)
template<typename QuantifierOp>
static LogicalResult	verifyQuantifierRegions (QuantifierOp op)
template<typename Properties>
static void	buildQuantifier (OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes, function_ref< Value(OpBuilder &, Location, ValueRange)> bodyBuilder, std::optional< ArrayRef< StringRef > > boundVarNames, function_ref< ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder, uint32_t weight, bool noPattern)

Macro Definition Documentation

GET_OP_CLASSES

#define GET_OP_CLASSES

Definition at line 471 of file SMTOps.cpp.

Function Documentation

buildQuantifier()

template<typename Properties>

void buildQuantifier ( OpBuilder & odsBuilder, OperationState & odsState, TypeRange boundVarTypes, function_ref< Value(OpBuilder &, Location, ValueRange)> bodyBuilder, std::optional< ArrayRef< StringRef > > boundVarNames, function_ref< ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder, uint32_t weight, bool noPattern )

static

Definition at line 379 of file SMTOps.cpp.

References mlir::Block::addArguments(), mlir::OperationState::addRegion(), mlir::OperationState::addTypes(), mlir::OpBuilder::createBlock(), mlir::Block::getArguments(), mlir::Builder::getArrayAttr(), mlir::Builder::getContext(), mlir::Builder::getIntegerAttr(), mlir::Builder::getIntegerType(), mlir::OperationState::getOrAddProperties(), mlir::Builder::getStringAttr(), mlir::Builder::getUnitAttr(), and mlir::OperationState::location.

parseSameOperandTypeVariadicToBoolOp()

LogicalResult parseSameOperandTypeVariadicToBoolOp ( OpAsmParser & parser, OperationState & result )

static

Definition at line 95 of file SMTOps.cpp.

References mlir::AsmParser::getContext(), mlir::AsmParser::getCurrentLocation(), mlir::AsmParser::parseColon(), mlir::OpAsmParser::parseOperandList(), mlir::AsmParser::parseOptionalAttrDict(), mlir::AsmParser::parseType(), mlir::OpAsmParser::resolveOperands(), result, and success().

verifyQuantifierRegions()

template<typename QuantifierOp>

LogicalResult verifyQuantifierRegions ( QuantifierOp op )

static

Definition at line 321 of file SMTOps.cpp.

References mlir::WalkResult::advance(), diag(), mlir::Region::front(), mlir::Region::getArgumentTypes(), mlir::Operation::getDialect(), mlir::Operation::getLoc(), mlir::Operation::getNumOperands(), mlir::Block::getTerminator(), mlir::WalkResult::interrupt(), mlir::smt::isAnyNonFuncSMTValueType(), result, success(), and mlir::Region::walk().