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 >

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  )

static

Definition at line 379 of file SMTOps.cpp.

References mlir::Block::addArguments(), mlir::OperationState::addRegion(), mlir::OperationState::addTypes(), mlir::OpBuilder::create(), mlir::OpBuilder::createBlock(), mlir::get(), 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()

static LogicalResult parseSameOperandTypeVariadicToBoolOp ( OpAsmParser &  parser, OperationState &  result  )

static

Definition at line 95 of file SMTOps.cpp.

References mlir::OperationState::addTypes(), mlir::OperationState::attributes, mlir::get(), mlir::AsmParser::getContext(), mlir::AsmParser::getCurrentLocation(), mlir::OperationState::operands, mlir::AsmParser::parseColon(), mlir::OpAsmParser::parseOperandList(), mlir::AsmParser::parseOptionalAttrDict(), mlir::AsmParser::parseType(), and mlir::OpAsmParser::resolveOperands().

verifyQuantifierRegions()

template<typename QuantifierOp >

static LogicalResult verifyQuantifierRegions ( QuantifierOp  op )

static

Definition at line 321 of file SMTOps.cpp.

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