SMT.cpp File Reference

#include "mlir-c/Dialect/SMT.h"
#include "mlir/CAPI/Registration.h"
#include "mlir/Dialect/SMT/IR/SMTAttributes.h"
#include "mlir/Dialect/SMT/IR/SMTDialect.h"
#include "mlir/Dialect/SMT/IR/SMTTypes.h"

Go to the source code of this file.

Functions
bool	mlirSMTTypeIsAnyNonFuncSMTValueType (MlirType type)
	Checks if the given type is any non-func SMT value type.
bool	mlirSMTTypeIsAnySMTValueType (MlirType type)
	Checks if the given type is any SMT value type.
bool	mlirSMTTypeIsAArray (MlirType type)
	Checks if the given type is a smt::ArrayType.
MlirType	mlirSMTTypeGetArray (MlirContext ctx, MlirType domainType, MlirType rangeType)
	Creates an array type with the given domain and range types.
bool	mlirSMTTypeIsABitVector (MlirType type)
	Checks if the given type is a smt::BitVectorType.
MlirType	mlirSMTTypeGetBitVector (MlirContext ctx, int32_t width)
	Creates a smt::BitVectorType with the given width.
bool	mlirSMTTypeIsABool (MlirType type)
	Checks if the given type is a smt::BoolType.
MlirType	mlirSMTTypeGetBool (MlirContext ctx)
	Creates a smt::BoolType.
bool	mlirSMTTypeIsAInt (MlirType type)
	Checks if the given type is a smt::IntType.
MlirType	mlirSMTTypeGetInt (MlirContext ctx)
	Creates a smt::IntType.
bool	mlirSMTTypeIsASMTFunc (MlirType type)
	Checks if the given type is a smt::FuncType.
MlirType	mlirSMTTypeGetSMTFunc (MlirContext ctx, size_t numberOfDomainTypes, const MlirType *domainTypes, MlirType rangeType)
	Creates a smt::FuncType with the given domain and range types.
bool	mlirSMTTypeIsASort (MlirType type)
	Checks if the given type is a smt::SortType.
MlirType	mlirSMTTypeGetSort (MlirContext ctx, MlirIdentifier identifier, size_t numberOfSortParams, const MlirType *sortParams)
	Creates a smt::SortType with the given identifier and sort parameters.
bool	mlirSMTAttrCheckBVCmpPredicate (MlirContext ctx, MlirStringRef str)
	Checks if the given string is a valid smt::BVCmpPredicate.
bool	mlirSMTAttrCheckIntPredicate (MlirContext ctx, MlirStringRef str)
	Checks if the given string is a valid smt::IntPredicate.
bool	mlirSMTAttrIsASMTAttribute (MlirAttribute attr)
	Checks if the given attribute is a smt::SMTAttribute.
MlirAttribute	mlirSMTAttrGetBitVector (MlirContext ctx, uint64_t value, unsigned width)
	Creates a smt::BitVectorAttr with the given value and width.
MlirAttribute	mlirSMTAttrGetBVCmpPredicate (MlirContext ctx, MlirStringRef str)
	Creates a smt::BVCmpPredicateAttr with the given string.
MlirAttribute	mlirSMTAttrGetIntPredicate (MlirContext ctx, MlirStringRef str)
	Creates a smt::IntPredicateAttr with the given string.

Function Documentation

mlirSMTAttrCheckBVCmpPredicate()

bool mlirSMTAttrCheckBVCmpPredicate	(	MlirContext	ctx,
		MlirStringRef	str )

Checks if the given string is a valid smt::BVCmpPredicate.

Definition at line 98 of file SMT.cpp.

References unwrap().

mlirSMTAttrCheckIntPredicate()

bool mlirSMTAttrCheckIntPredicate	(	MlirContext	ctx,
		MlirStringRef	str )

Checks if the given string is a valid smt::IntPredicate.

Definition at line 102 of file SMT.cpp.

References unwrap().

mlirSMTAttrGetBitVector()

MlirAttribute mlirSMTAttrGetBitVector	(	MlirContext	ctx,
		uint64_t	value,
		unsigned	width )

Creates a smt::BitVectorAttr with the given value and width.

Definition at line 110 of file SMT.cpp.

References unwrap(), and wrap().

mlirSMTAttrGetBVCmpPredicate()

MlirAttribute mlirSMTAttrGetBVCmpPredicate	(	MlirContext	ctx,
		MlirStringRef	str )

Creates a smt::BVCmpPredicateAttr with the given string.

Definition at line 115 of file SMT.cpp.

References unwrap(), and wrap().

mlirSMTAttrGetIntPredicate()

MlirAttribute mlirSMTAttrGetIntPredicate	(	MlirContext	ctx,
		MlirStringRef	str )

Creates a smt::IntPredicateAttr with the given string.

Definition at line 122 of file SMT.cpp.

References unwrap(), and wrap().

mlirSMTAttrIsASMTAttribute()

bool mlirSMTAttrIsASMTAttribute

(

MlirAttribute

attr

)

Checks if the given attribute is a smt::SMTAttribute.

Definition at line 106 of file SMT.cpp.

References unwrap().

mlirSMTTypeGetArray()

MlirType mlirSMTTypeGetArray	(	MlirContext	ctx,
		MlirType	domainType,
		MlirType	rangeType )

Creates an array type with the given domain and range types.

Definition at line 38 of file SMT.cpp.

References unwrap(), and wrap().

mlirSMTTypeGetBitVector()

MlirType mlirSMTTypeGetBitVector	(	MlirContext	ctx,
		int32_t	width )

Creates a smt::BitVectorType with the given width.

Definition at line 48 of file SMT.cpp.

References unwrap(), and wrap().

Referenced by populateDialectSMTSubmodule().

mlirSMTTypeGetBool()

MlirType mlirSMTTypeGetBool

(

MlirContext

ctx

)

Creates a smt::BoolType.

Definition at line 54 of file SMT.cpp.

References unwrap(), and wrap().

Referenced by populateDialectSMTSubmodule().

mlirSMTTypeGetInt()

MlirType mlirSMTTypeGetInt

(

MlirContext

ctx

)

Creates a smt::IntType.

Definition at line 60 of file SMT.cpp.

References unwrap(), and wrap().

Referenced by populateDialectSMTSubmodule().

mlirSMTTypeGetSMTFunc()

MlirType mlirSMTTypeGetSMTFunc	(	MlirContext	ctx,
		size_t	numberOfDomainTypes,
		const MlirType *	domainTypes,
		MlirType	rangeType )

Creates a smt::FuncType with the given domain and range types.

Definition at line 68 of file SMT.cpp.

References unwrap(), and wrap().

mlirSMTTypeGetSort()

MlirType mlirSMTTypeGetSort	(	MlirContext	ctx,
		MlirIdentifier	identifier,
		size_t	numberOfSortParams,
		const MlirType *	sortParams )

Creates a smt::SortType with the given identifier and sort parameters.

Definition at line 82 of file SMT.cpp.

References unwrap(), and wrap().

mlirSMTTypeIsAArray()

bool mlirSMTTypeIsAArray

(

MlirType

type

)

Checks if the given type is a smt::ArrayType.

Definition at line 36 of file SMT.cpp.

References unwrap().

mlirSMTTypeIsABitVector()

bool mlirSMTTypeIsABitVector

(

MlirType

type

)

Checks if the given type is a smt::BitVectorType.

Definition at line 44 of file SMT.cpp.

References unwrap().

Referenced by populateDialectSMTSubmodule().

mlirSMTTypeIsABool()

bool mlirSMTTypeIsABool

(

MlirType

type

)

Checks if the given type is a smt::BoolType.

Definition at line 52 of file SMT.cpp.

References unwrap().

Referenced by populateDialectSMTSubmodule().

mlirSMTTypeIsAInt()

bool mlirSMTTypeIsAInt

(

MlirType

type

)

Checks if the given type is a smt::IntType.

Definition at line 58 of file SMT.cpp.

References unwrap().

Referenced by populateDialectSMTSubmodule().

mlirSMTTypeIsAnyNonFuncSMTValueType()

bool mlirSMTTypeIsAnyNonFuncSMTValueType

(

MlirType

type

)

Checks if the given type is any non-func SMT value type.

Definition at line 28 of file SMT.cpp.

References mlir::smt::isAnyNonFuncSMTValueType(), mlirSMTTypeIsAnyNonFuncSMTValueType(), and unwrap().

Referenced by mlirSMTTypeIsAnyNonFuncSMTValueType().

mlirSMTTypeIsAnySMTValueType()

bool mlirSMTTypeIsAnySMTValueType

(

MlirType

type

)

Checks if the given type is any SMT value type.

Definition at line 32 of file SMT.cpp.

References mlir::smt::isAnySMTValueType(), and unwrap().

mlirSMTTypeIsASMTFunc()

bool mlirSMTTypeIsASMTFunc

(

MlirType

type

)

Checks if the given type is a smt::FuncType.

Definition at line 64 of file SMT.cpp.

References unwrap().

mlirSMTTypeIsASort()

bool mlirSMTTypeIsASort

(

MlirType

type

)

Checks if the given type is a smt::SortType.

Definition at line 80 of file SMT.cpp.

References unwrap().