SMT.h File Reference

#include "mlir-c/IR.h"

Go to the source code of this file.

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

Function Documentation

MLIR_DECLARE_CAPI_DIALECT_REGISTRATION()

MLIR_DECLARE_CAPI_DIALECT_REGISTRATION	(	SMT	,
		smt
	)

mlirSMTAttrCheckBVCmpPredicate()

MLIR_CAPI_EXPORTED 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()

MLIR_CAPI_EXPORTED 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()

MLIR_CAPI_EXPORTED 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 mlir::get(), unwrap(), and wrap().

mlirSMTAttrGetBVCmpPredicate()

MLIR_CAPI_EXPORTED MlirAttribute mlirSMTAttrGetBVCmpPredicate	(	MlirContext	ctx,
		MlirStringRef	str
	)

Creates a smt::BVCmpPredicateAttr with the given string.

Definition at line 115 of file SMT.cpp.

References mlir::get(), unwrap(), and wrap().

mlirSMTAttrGetIntPredicate()

MLIR_CAPI_EXPORTED MlirAttribute mlirSMTAttrGetIntPredicate	(	MlirContext	ctx,
		MlirStringRef	str
	)

Creates a smt::IntPredicateAttr with the given string.

Definition at line 122 of file SMT.cpp.

References mlir::get(), unwrap(), and wrap().

mlirSMTAttrIsASMTAttribute()

MLIR_CAPI_EXPORTED bool mlirSMTAttrIsASMTAttribute

(

MlirAttribute

attr

)

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

Definition at line 106 of file SMT.cpp.

References unwrap().

mlirSMTTypeGetArray()

MLIR_CAPI_EXPORTED 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 mlir::get(), unwrap(), and wrap().

mlirSMTTypeGetBitVector()

MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetBitVector	(	MlirContext	ctx,
		int32_t	width
	)

Creates a smt::BitVectorType with the given width.

Definition at line 48 of file SMT.cpp.

References mlir::get(), unwrap(), and wrap().

mlirSMTTypeGetBool()

MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetBool

(

MlirContext

ctx

)

Creates a smt::BoolType.

Definition at line 54 of file SMT.cpp.

References mlir::get(), unwrap(), and wrap().

mlirSMTTypeGetInt()

MLIR_CAPI_EXPORTED MlirType mlirSMTTypeGetInt

(

MlirContext

ctx

)

Creates a smt::IntType.

Definition at line 60 of file SMT.cpp.

References mlir::get(), unwrap(), and wrap().

mlirSMTTypeGetSMTFunc()

MLIR_CAPI_EXPORTED 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 mlir::get(), unwrap(), and wrap().

mlirSMTTypeGetSort()

MLIR_CAPI_EXPORTED 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 mlir::get(), unwrap(), and wrap().

mlirSMTTypeIsAArray()

MLIR_CAPI_EXPORTED bool mlirSMTTypeIsAArray

(

MlirType

type

)

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

Definition at line 36 of file SMT.cpp.

References unwrap().

mlirSMTTypeIsABitVector()

MLIR_CAPI_EXPORTED bool mlirSMTTypeIsABitVector

(

MlirType

type

)

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

Definition at line 44 of file SMT.cpp.

References unwrap().

mlirSMTTypeIsABool()

MLIR_CAPI_EXPORTED bool mlirSMTTypeIsABool

(

MlirType

type

)

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

Definition at line 52 of file SMT.cpp.

References unwrap().

mlirSMTTypeIsAInt()

MLIR_CAPI_EXPORTED bool mlirSMTTypeIsAInt

(

MlirType

type

)

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

Definition at line 58 of file SMT.cpp.

References unwrap().

mlirSMTTypeIsAnyNonFuncSMTValueType()

MLIR_CAPI_EXPORTED 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(), and unwrap().

mlirSMTTypeIsAnySMTValueType()

MLIR_CAPI_EXPORTED 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()

MLIR_CAPI_EXPORTED bool mlirSMTTypeIsASMTFunc

(

MlirType

type

)

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

Definition at line 64 of file SMT.cpp.

References unwrap().

mlirSMTTypeIsASort()

MLIR_CAPI_EXPORTED bool mlirSMTTypeIsASort

(

MlirType

type

)

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

Definition at line 80 of file SMT.cpp.

References unwrap().