SMT Backend

Table of Contents

• 'smt_info' Dialect
  • Operations
    • smt_info.set (llzk::smt_info::SMTInfoSetOp)
      • Attributes:
  • Attributes
    • KeywordAttr
      • Parameters:
    • SymbolAttr
      • Parameters:

LLZK uses the upstream SMT dialect for solver operations and terms. On top of that, LLZK defines the smt extensions below.

'smt_info' Dialect

SMT-LIB script metadata retained through emission

Operations

smt_info.set (::llzk::smt_info::SMTInfoSetOp)

Attach SMT-LIB set-info metadata to a script

Attributes:

Attribute	MLIR Type	Description
key	::llzk::smt_info::KeywordAttr	an SMT-LIB keyword
value	::mlir::Attribute	any attribute

Attributes

KeywordAttr

An SMT-LIB keyword

Parameters:

Parameter	C++ type	Description
value	::llvm::StringRef	The keyword text

SymbolAttr

An SMT-LIB bare symbol

Parameters:

Parameter	C++ type	Description
value	::llvm::StringRef	The symbol text

Felt literals are reduced to [0, p) before being emitted as SMT integer constants, including signed literals. A specified source field determines p; for fieldless literals, the field selected by the lowering pass determines p.