'smt' Dialect

a dialect that models satisfiability modulo theories

Operations

smt.and (::llzk::smt::AndOp)

A boolean conjunction

Syntax:

operation ::= `smt.and` $inputs attr-dict

This operation performs a boolean conjunction. The semantics are equivalent to the 'and' operator in the Core theory. of the SMT-LIB Standard 2.7.

It supports a variadic number of operands, but requires at least two. This is because the operator is annotated with the :left-assoc attribute which means that op a b c is equivalent to (op (op a b) c).

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
inputs	variadic of

Results:

| Result | Description | | :-—: | --------— | | result |

smt.apply_func (::llzk::smt::ApplyFuncOp)

Apply a function

Syntax:

operation ::= `smt.apply_func` $func `(` $args `)` attr-dict `:` qualified(type($func))

This operation performs a function application as described in the SMT-LIB 2.7 standard. It is part of the language itself rather than a theory or logic.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | func | | args | variadic of any non-function SMT value type

Results:

Result	Description
result	any non-function SMT value type

smt.array.broadcast (::llzk::smt::ArrayBroadcastOp)

Construct an array with the given value stored at every index

Syntax:

operation ::= `smt.array.broadcast` $value attr-dict `:` qualified(type($result))

This operation represents a broadcast of the 'value' operand to all indices of the array. It is equivalent to

%0 = smt.declare_fun "array" : !smt.array<[!smt.int -> !smt.bool]>
%1 = smt.forall ["idx"] {
^bb0(%idx: !smt.int):
  %2 = smt.array.select %0[%idx] : !smt.array<[!smt.int -> !smt.bool]>
  %3 = smt.eq %value, %2 : !smt.bool
  smt.yield %3 : !smt.bool
}
smt.assert %1
// return %0

In SMT-LIB, this is frequently written as ((as const (Array Int Bool)) value).

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
value	any SMT value type

Results:

| Result | Description | | :-—: | --------— | | result |

smt.array.select (::llzk::smt::ArraySelectOp)

Get the value stored in the array at the given index

Syntax:

operation ::= `smt.array.select` $array `[` $index `]` attr-dict `:` qualified(type($array))

This operation is retuns the value stored in the given array at the given index. The semantics are equivalent to the select operator defined in the SMT ArrayEx theory of the SMT-LIB standard 2.7.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | array | | index | any SMT value type

Results:

Result	Description
result	any SMT value type

smt.array.store (::llzk::smt::ArrayStoreOp)

Stores a value at a given index and returns the new array

Syntax:

operation ::= `smt.array.store` $array `[` $index `]` `,` $value attr-dict `:` qualified(type($array))

This operation returns a new array which is the same as the 'array' operand except that the value at the given 'index' is changed to the given 'value'. The semantics are equivalent to the 'store' operator described in the SMT ArrayEx theory of the SMT-LIB standard 2.7.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | array | | index | any SMT value type | value | any SMT value type

Results:

| Result | Description | | :-—: | --------— | | result |

smt.assert (::llzk::smt::AssertOp)

Assert that a boolean expression holds

Syntax:

operation ::= `smt.assert` $input attr-dict

Operands:

| Operand | Description | | :--—: | --------— | | input |

smt.bv.add (::llzk::smt::BVAddOp)

Equivalent to bvadd in SMT-LIB

Syntax:

operation ::= `smt.bv.add` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs addition. The semantics are equivalent to the bvadd operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.and (::llzk::smt::BVAndOp)

Equivalent to bvand in SMT-LIB

Syntax:

operation ::= `smt.bv.and` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs bitwise AND. The semantics are equivalent to the bvand operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.ashr (::llzk::smt::BVAShrOp)

Equivalent to bvashr in SMT-LIB

Syntax:

operation ::= `smt.bv.ashr` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs arithmetic shift right. The semantics are equivalent to the bvashr operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.cmp (::llzk::smt::BVCmpOp)

Compare bit-vectors interpreted as signed or unsigned

Syntax:

operation ::= `smt.bv.cmp` $pred $lhs `,` $rhs attr-dict `:` qualified(type($lhs))

This operation compares bit-vector values, interpreting them as signed or unsigned values depending on the predicate. The semantics are equivalent to the bvslt, bvsle, bvsgt, bvsge, bvult, bvule, bvugt, or bvuge operator defined in the SMT-LIB 2.7 standard depending on the specified predicate. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameTypeOperands

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`pred`	llzk::smt::BVCmpPredicateAttr	smt bit-vector comparison predicate

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.concat (::llzk::smt::ConcatOp)

Bit-vector concatenation

Syntax:

operation ::= `smt.bv.concat` $lhs `,` $rhs attr-dict `:` qualified(type(operands))

This operation concatenates bit-vector values with semantics equivalent to the concat operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Note that the following equivalences hold:

smt.bv.concat a, b : !smt.bv<4>, !smt.bv<4> is equivalent to (concat a b) in SMT-LIB
(= (concat #xf #x0) #xf0)

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.constant (::llzk::smt::BVConstantOp)

Produce a constant bit-vector

Syntax:

operation ::= `smt.bv.constant` qualified($value) attr-dict

This operation produces an SSA value equal to the bit-vector constant specified by the 'value' attribute. Refer to the BitVectorAttr documentation for more information about the semantics of bit-vector constants, their format, and associated sort. The result type always matches the attribute's type.

Examples:

%c92_bv8 = smt.bv.constant #smt.bv<92> : !smt.bv<8>

%c5_bv4 = smt.bv.constant #smt.bv<5> : !smt.bv<4>

Traits: AlwaysSpeculatableImplTrait, ConstantLike, FirstAttrDerivedResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface), OpAsmOpInterface

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`value`	::llzk::smt::BitVectorAttr

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.extract (::llzk::smt::ExtractOp)

Bit-vector extraction

Syntax:

operation ::= `smt.bv.extract` $input `from` $lowBit attr-dict `:` functional-type($input, $result)

This operation extracts the range of bits starting at the 'lowBit' index (inclusive) up to the 'lowBit' + result-width index (exclusive). The semantics are equivalent to the extract operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Note that smt.bv.extract bv from 2 : (!smt.bv<32>) -> !smt.bv<16> is equivalent to ((_ extract 17 2) bv), i.e., the SMT-LIB operator takes the low and high indices where both are inclusive. The following equivalence holds: (= ((_ extract 3 0) #x0f) #xf)

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`lowBit`	::mlir::IntegerAttr	32-bit signless integer attribute

Operands:

| Operand | Description | | :--—: | --------— | | input |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.lshr (::llzk::smt::BVLShrOp)

Equivalent to bvlshr in SMT-LIB

Syntax:

operation ::= `smt.bv.lshr` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs logical shift right. The semantics are equivalent to the bvlshr operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.mul (::llzk::smt::BVMulOp)

Equivalent to bvmul in SMT-LIB

Syntax:

operation ::= `smt.bv.mul` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs multiplication. The semantics are equivalent to the bvmul operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.neg (::llzk::smt::BVNegOp)

Equivalent to bvneg in SMT-LIB

Syntax:

operation ::= `smt.bv.neg` $input attr-dict `:` qualified(type($result))

This operation performs two's complement unary minus. The semantics are equivalent to the bvneg operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | input |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.not (::llzk::smt::BVNotOp)

Equivalent to bvnot in SMT-LIB

Syntax:

operation ::= `smt.bv.not` $input attr-dict `:` qualified(type($result))

This operation performs bitwise negation. The semantics are equivalent to the bvnot operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | input |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.or (::llzk::smt::BVOrOp)

Equivalent to bvor in SMT-LIB

Syntax:

operation ::= `smt.bv.or` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs bitwise OR. The semantics are equivalent to the bvor operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.repeat (::llzk::smt::RepeatOp)

Repeated bit-vector concatenation of one value

This operation is a shorthand for repeated concatenation of the same bit-vector value, i.e.,

smt.bv.repeat 5 times %a : !smt.bv<4>
// is the same as
%0 = smt.bv.repeat 4 times %a : !smt.bv<4>
smt.bv.concat %a, %0 : !smt.bv<4>, !smt.bv<16>
// or also 
%0 = smt.bv.repeat 4 times %a : !smt.bv<4>
smt.bv.concat %0, %a : !smt.bv<16>, !smt.bv<4>

The semantics are equivalent to the repeat operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | input |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.sdiv (::llzk::smt::BVSDivOp)

Equivalent to bvsdiv in SMT-LIB

Syntax:

operation ::= `smt.bv.sdiv` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs two's complement signed division. The semantics are equivalent to the bvsdiv operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.shl (::llzk::smt::BVShlOp)

Equivalent to bvshl in SMT-LIB

Syntax:

operation ::= `smt.bv.shl` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs shift left. The semantics are equivalent to the bvshl operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.smod (::llzk::smt::BVSModOp)

Equivalent to bvsmod in SMT-LIB

Syntax:

operation ::= `smt.bv.smod` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs two's complement signed remainder (sign follows divisor). The semantics are equivalent to the bvsmod operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.srem (::llzk::smt::BVSRemOp)

Equivalent to bvsrem in SMT-LIB

Syntax:

operation ::= `smt.bv.srem` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs two's complement signed remainder (sign follows dividend). The semantics are equivalent to the bvsrem operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.udiv (::llzk::smt::BVUDivOp)

Equivalent to bvudiv in SMT-LIB

Syntax:

operation ::= `smt.bv.udiv` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs unsigned division (rounded towards zero). The semantics are equivalent to the bvudiv operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.urem (::llzk::smt::BVURemOp)

Equivalent to bvurem in SMT-LIB

Syntax:

operation ::= `smt.bv.urem` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs unsigned remainder. The semantics are equivalent to the bvurem operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv.xor (::llzk::smt::BVXOrOp)

Equivalent to bvxor in SMT-LIB

Syntax:

operation ::= `smt.bv.xor` $lhs `,` $rhs attr-dict `:` qualified(type($result))

This operation performs bitwise exclusive OR. The semantics are equivalent to the bvxor operator defined in the SMT-LIB 2.7 standard. More precisely in the theory of FixedSizeBitVectors and the QF_BV logic describing closed quantifier-free formulas over the theory of fixed-size bit-vectors.

Traits: AlwaysSpeculatableImplTrait, SameOperandsAndResultType

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.bv2int (::llzk::smt::BV2IntOp)

Convert an SMT bit-vector to an SMT integer.

Syntax:

operation ::= `smt.bv2int` $input (`signed` $is_signed^)? attr-dict `:`

qualified(type($input))

Create an integer from the bit-vector argument input. If is_signed is present, the bit-vector is treated as two's complement signed. Otherwise, it is treated as an unsigned integer in the range [0..2^N-1], where N is the number of bits in input.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`is_signed`	::mlir::UnitAttr	unit attribute

Operands:

| Operand | Description | | :--—: | --------— | | input |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.check (::llzk::smt::CheckOp)

Check if the current set of assertions is satisfiable

Syntax:

operation ::= `smt.check` attr-dict `sat` $satRegion `unknown` $unknownRegion `unsat` $unsatRegion

(`->` qualified(type($results))^ )?

This operation checks if all the assertions in the solver defined by the nearest ancestor operation of type smt.solver are consistent. The outcome an be 'satisfiable', 'unknown', or 'unsatisfiable' and the corresponding region will be executed. It is the corresponding construct to the check-sat in SMT-LIB.

Example:

%0 = smt.check sat {
  %c1_i32 = arith.constant 1 : i32
  smt.yield %c1_i32 : i32
} unknown {
  %c0_i32 = arith.constant 0 : i32
  smt.yield %c0_i32 : i32
} unsat {
  %c-1_i32 = arith.constant -1 : i32
  smt.yield %c-1_i32 : i32
} -> i32

Traits: NoRegionArguments, SingleBlockImplicitTerminator<smt::YieldOp>, SingleBlock

Results:

Result	Description
results	variadic of any type

smt.constant (::llzk::smt::BoolConstantOp)

Produce a constant boolean

Syntax:

operation ::= `smt.constant` $value attr-dict

Produces the constant expressions 'true' and 'false' as described in the Core theory of the SMT-LIB Standard 2.7.

Traits: AlwaysSpeculatableImplTrait, ConstantLike

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface), OpAsmOpInterface

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`value`	::mlir::BoolAttr	bool attribute

Results:

| Result | Description | | :-—: | --------— | | result |

smt.declare_fun (::llzk::smt::DeclareFunOp)

Declare a symbolic value of a given sort

Syntax:

operation ::= `smt.declare_fun` ($namePrefix^)? attr-dict `:` qualified(type($result))

This operation declares a symbolic value just as the declare-const and declare-fun statements in SMT-LIB 2.7. The result type determines the SMT sort of the symbolic value. The returned value can then be used to refer to the symbolic value instead of using the identifier like in SMT-LIB.

The optionally provided string will be used as a prefix for the newly generated identifier (useful for easier readability when exporting to SMT-LIB). Each declare will always provide a unique new symbolic value even if the identifier strings are the same.

Note that there does not exist a separate operation equivalent to SMT-LIBs define-fun since

(define-fun f (a Int) Int (-a))

is only syntactic sugar for

%f = smt.declare_fun : !smt.func<(!smt.int) !smt.int>
%0 = smt.forall {
^bb0(%arg0: !smt.int):
  %1 = smt.apply_func %f(%arg0) : !smt.func<(!smt.int) !smt.int>
  %2 = smt.int.neg %arg0
  %3 = smt.eq %1, %2 : !smt.int
  smt.yield %3 : !smt.bool
}
smt.assert %0

Note that this operation cannot be marked as Pure since two operations (even with the same identifier string) could then be CSEd, leading to incorrect behavior.

Interfaces: OpAsmOpInterface

Attributes:

Attribute	MLIR Type	Description
`namePrefix`	::mlir::StringAttr	string attribute

Results:

Result	Description
result	any SMT value type

smt.distinct (::llzk::smt::DistinctOp)

Returns true iff all operands are not identical to any other

This operation compares the operands and returns true iff all operands are not identical to any of the other operands. The semantics are equivalent to the distinct operator defined in the SMT-LIB Standard 2.7 in the Core theory.

Any SMT sort/type is allowed for the operands and it supports a variadic number of operands, but requires at least two. This is because the distinct operator is annotated with :pairwise which means that distinct a b c d is equivalent to

and (distinct a b) (distinct a c) (distinct a d)
    (distinct b c) (distinct b d)
    (distinct c d)

where and is annotated :left-assoc, i.e., it can be further rewritten to

(and (and (and (and (and (distinct a b)
                         (distinct a c))
                    (distinct a d))
               (distinct b c))
          (distinct b d))
     (distinct c d)

Traits: AlwaysSpeculatableImplTrait, SameTypeOperands

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
inputs	variadic of any non-function SMT value type

Results:

| Result | Description | | :-—: | --------— | | result |

smt.eq (::llzk::smt::EqOp)

Returns true iff all operands are identical

This operation compares the operands and returns true iff all operands are identical. The semantics are equivalent to the = operator defined in the SMT-LIB Standard 2.7 in the Core theory.

Any SMT sort/type is allowed for the operands and it supports a variadic number of operands, but requires at least two. This is because the = operator is annotated with :chainable which means that = a b c d is equivalent to and (= a b) (= b c) (= c d) where and is annotated :left-assoc, i.e., it can be further rewritten to and (and (= a b) (= b c)) (= c d).

Traits: AlwaysSpeculatableImplTrait, SameTypeOperands

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
inputs	variadic of any non-function SMT value type

Results:

| Result | Description | | :-—: | --------— | | result |

smt.exists (::llzk::smt::ExistsOp)

Exists quantifier

Syntax:

operation ::= `smt.exists` ($boundVarNames^)? (`no_pattern` $noPattern^)? (`weight` $weight^)?

attr-dict-with-keyword $body (`patterns` $patterns^)?

This operation represents the exists quantifier as described in the SMT-LIB 2.7 standard. It is part of the language itself rather than a theory or logic.

The operation specifies the name prefixes (as an optional attribute) and types (as the types of the block arguments of the regions) of bound variables that may be used in the 'body' of the operation. If a 'patterns' region is specified, the block arguments must match the ones of the 'body' region and (other than there) must be used at least once in the 'patterns' region. It may also not contain any operations that bind variables, such as quantifiers. While the 'body' region must always yield exactly one !smt.bool-typed value, the 'patterns' region can yield an arbitrary number (but at least one) of SMT values.

The bound variables can be any SMT type except of functions, since SMT only supports first-order logic.

The 'no_patterns' attribute is only allowed when no 'patterns' region is specified and forbids the solver to generate and use patterns for this quantifier.

The 'weight' attribute indicates the importance of this quantifier being instantiated compared to other quantifiers that may be present. The default value is zero.

Both the 'no_patterns' and 'weight' attributes are annotations to the quantifiers body term. Annotations and attributes are described in the standard in sections 3.4, and 3.6 (specifically 3.6.5). SMT-LIB allows adding custom attributes to provide solvers with additional metadata, e.g., hints such as above mentioned attributes. They are not part of the standard themselves, but supported by common SMT solvers (e.g., Z3).

Traits: RecursiveMemoryEffects, RecursivelySpeculatableImplTrait, SingleBlockImplicitTerminator<smt::YieldOp>, SingleBlock

Interfaces: ConditionallySpeculatable, InferTypeOpInterface

Attributes:

Attribute	MLIR Type	Description
`weight`	::mlir::IntegerAttr	32-bit signless integer attribute
`noPattern`	::mlir::UnitAttr	unit attribute
`boundVarNames`	::mlir::ArrayAttr	string array attribute

Results:

| Result | Description | | :-—: | --------— | | result |

smt.forall (::llzk::smt::ForallOp)

Forall quantifier

Syntax:

operation ::= `smt.forall` ($boundVarNames^)? (`no_pattern` $noPattern^)? (`weight` $weight^)?

attr-dict-with-keyword $body (`patterns` $patterns^)?

This operation represents the forall quantifier as described in the SMT-LIB 2.7 standard. It is part of the language itself rather than a theory or logic.

The operation specifies the name prefixes (as an optional attribute) and types (as the types of the block arguments of the regions) of bound variables that may be used in the 'body' of the operation. If a 'patterns' region is specified, the block arguments must match the ones of the 'body' region and (other than there) must be used at least once in the 'patterns' region. It may also not contain any operations that bind variables, such as quantifiers. While the 'body' region must always yield exactly one !smt.bool-typed value, the 'patterns' region can yield an arbitrary number (but at least one) of SMT values.

The bound variables can be any SMT type except of functions, since SMT only supports first-order logic.

The 'no_patterns' attribute is only allowed when no 'patterns' region is specified and forbids the solver to generate and use patterns for this quantifier.

The 'weight' attribute indicates the importance of this quantifier being instantiated compared to other quantifiers that may be present. The default value is zero.

Both the 'no_patterns' and 'weight' attributes are annotations to the quantifiers body term. Annotations and attributes are described in the standard in sections 3.4, and 3.6 (specifically 3.6.5). SMT-LIB allows adding custom attributes to provide solvers with additional metadata, e.g., hints such as above mentioned attributes. They are not part of the standard themselves, but supported by common SMT solvers (e.g., Z3).

Traits: RecursiveMemoryEffects, RecursivelySpeculatableImplTrait, SingleBlockImplicitTerminator<smt::YieldOp>, SingleBlock

Interfaces: ConditionallySpeculatable, InferTypeOpInterface

Attributes:

Attribute	MLIR Type	Description
`weight`	::mlir::IntegerAttr	32-bit signless integer attribute
`noPattern`	::mlir::UnitAttr	unit attribute
`boundVarNames`	::mlir::ArrayAttr	string array attribute

Results:

| Result | Description | | :-—: | --------— | | result |

smt.implies (::llzk::smt::ImpliesOp)

Boolean implication

Syntax:

operation ::= `smt.implies` $lhs `,` $rhs attr-dict

This operation performs a boolean implication. The semantics are equivalent to the '=>' operator in the Core theory of the SMT-LIB Standard 2.7.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.int.abs (::llzk::smt::IntAbsOp)

The absolute value of an Int

Syntax:

operation ::= `smt.int.abs` $input attr-dict

This operation represents the absolute value function for the Int sort. The semantics are equivalent to the abs operator as described in the SMT Ints theory of the SMT-LIB 2.7 standard.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | input |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.int.add (::llzk::smt::IntAddOp)

Integer addition

Syntax:

operation ::= `smt.int.add` $inputs attr-dict

This operation represents (infinite-precision) integer addition. The semantics are equivalent to the corresponding operator described in the SMT Ints theory of the SMT-LIB 2.7 standard.

Traits: AlwaysSpeculatableImplTrait, Commutative

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
inputs	variadic of

Results:

| Result | Description | | :-—: | --------— | | result |

smt.int.cmp (::llzk::smt::IntCmpOp)

Integer comparison

Syntax:

operation ::= `smt.int.cmp` $pred $lhs `,` $rhs attr-dict

This operation represents the comparison of (infinite-precision) integers. The semantics are equivalent to the <= (le), < (lt), >= (ge), or > (gt) operator depending on the predicate (indicated in parentheses) as described in the SMT Ints theory of the SMT-LIB 2.7 standard.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`pred`	llzk::smt::IntPredicateAttr	smt comparison predicate for integers

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.int.constant (::llzk::smt::IntConstantOp)

Produce a constant (infinite-precision) integer

This operation represents (infinite-precision) integer literals of the Int sort. The set of values for the sort Int consists of all numerals and all terms of the form -nwhere n is a numeral other than 0. For more information refer to the SMT Ints theory of the SMT-LIB 2.7 standard.

Traits: AlwaysSpeculatableImplTrait, ConstantLike

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface), OpAsmOpInterface

Effects: MemoryEffects::Effect{}

Attributes:

Attribute	MLIR Type	Description
`value`	::mlir::IntegerAttr	arbitrary integer attribute

Results:

| Result | Description | | :-—: | --------— | | result |

smt.int.div (::llzk::smt::IntDivOp)

Integer division

Syntax:

operation ::= `smt.int.div` $lhs `,` $rhs attr-dict

This operation represents (infinite-precision) integer division. The semantics are equivalent to the corresponding operator described in the SMT Ints theory of the SMT-LIB 2.7 standard.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.int.mod (::llzk::smt::IntModOp)

Integer remainder

Syntax:

operation ::= `smt.int.mod` $lhs `,` $rhs attr-dict

This operation represents (infinite-precision) integer remainder. The semantics are equivalent to the corresponding operator described in the SMT Ints theory of the SMT-LIB 2.7 standard.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.int.mul (::llzk::smt::IntMulOp)

Integer multiplication

Syntax:

operation ::= `smt.int.mul` $inputs attr-dict

This operation represents (infinite-precision) integer multiplication. The semantics are equivalent to the corresponding operator described in the SMT Ints theory of the SMT-LIB 2.7 standard.

Traits: AlwaysSpeculatableImplTrait, Commutative

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
inputs	variadic of

Results:

| Result | Description | | :-—: | --------— | | result |

smt.int.neg (::llzk::smt::IntNegOp)

The negation of an Int

Syntax:

operation ::= `smt.int.neg` $input attr-dict

This operation represents unary negation for the Int sort.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | input |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.int.sub (::llzk::smt::IntSubOp)

Integer subtraction

Syntax:

operation ::= `smt.int.sub` $lhs `,` $rhs attr-dict

This operation represents (infinite-precision) integer subtraction. The semantics are equivalent to the corresponding operator described in the SMT Ints theory of the SMT-LIB 2.7 standard.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | lhs | | rhs |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.int2bv (::llzk::smt::Int2BVOp)

Convert an integer to an inferred-width bitvector.

Syntax:

operation ::= `smt.int2bv` $input attr-dict `:` qualified(type($result))

Designed to lower directly to an operation of the same name in Z3. The Z3 C API describes the semantics as follows: Create an n bit bit-vector from the integer argument t1. The resulting bit-vector has n bits, where the i'th bit (counting from 0 to n-1) is 1 if (t1 div 2^i) mod 2 is 1. The node t1 must have integer sort.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | input |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.ite (::llzk::smt::IteOp)

An if-then-else function

Syntax:

operation ::= `smt.ite` $cond `,` $thenValue `,` $elseValue attr-dict `:` qualified(type($result))

This operation returns its second operand or its third operand depending on whether its first operand is true or not. The semantics are equivalent to the ite operator defined in the Core theory of the SMT-LIB 2.7 standard.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | cond | | thenValue | any SMT value type | elseValue | any SMT value type

Results:

Result	Description
result	any SMT value type

smt.not (::llzk::smt::NotOp)

A boolean negation

Syntax:

operation ::= `smt.not` $input attr-dict

This operation performs a boolean negation. The semantics are equivalent to the 'not' operator in the Core theory of the SMT-LIB Standard 2.7.

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

| Operand | Description | | :--—: | --------— | | input |

Results:

| Result | Description | | :-—: | --------— | | result |

smt.or (::llzk::smt::OrOp)

A boolean disjunction

Syntax:

operation ::= `smt.or` $inputs attr-dict

This operation performs a boolean disjunction. The semantics are equivalent to the 'or' operator in the Core theory. of the SMT-LIB Standard 2.7.

It supports a variadic number of operands, but requires at least two. This is because the operator is annotated with the :left-assoc attribute which means that op a b c is equivalent to (op (op a b) c).

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
inputs	variadic of

Results:

| Result | Description | | :-—: | --------— | | result |

smt.pop (::llzk::smt::PopOp)

Pop a given number of levels from the assertion stack

Syntax:

operation ::= `smt.pop` $count attr-dict

Attributes:

Attribute	MLIR Type	Description
`count`	::mlir::IntegerAttr	32-bit signless integer attribute whose value is non-negative

smt.push (::llzk::smt::PushOp)

Push a given number of levels onto the assertion stack

Syntax:

operation ::= `smt.push` $count attr-dict

Attributes:

Attribute	MLIR Type	Description
`count`	::mlir::IntegerAttr	32-bit signless integer attribute whose value is non-negative

smt.reset (::llzk::smt::ResetOp)

Reset the solver

Syntax:

operation ::= `smt.reset` attr-dict

smt.set_info (::llzk::smt::SetInfoOp)

Attach SMT-LIB set-info metadata to the script

This operation models SMT-LIB's (set-info ...) command directly. It is a generic script-level metadata mechanism and can be used for standardized keys such as :status as well as tool-specific keys such as :llzk-stage.

Example:

smt.set_info ":llzk-stage" "pre"
smt.set_info ":status" sat
smt.set_info ":notes" ("phase1" ok :custom)

Attributes:

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

smt.set_logic (::llzk::smt::SetLogicOp)

Set the logic for the SMT solver

Syntax:

operation ::= `smt.set_logic` $logic attr-dict

Traits: HasParent<smt::SolverOp>

Attributes:

Attribute	MLIR Type	Description
`logic`	::mlir::StringAttr	string attribute

smt.solver (::llzk::smt::SolverOp)

Create a solver instance within a lifespan

Syntax:

operation ::= `smt.solver` `(` $inputs `)` attr-dict `:` functional-type($inputs, $results) $bodyRegion

This operation defines an SMT context with a solver instance. SMT operations are only valid when being executed between the start and end of the region of this operation. Any invocation outside is undefined. However, they do not have to be direct children of this operation. For example, it is allowed to have SMT operations in a func.func which is only called from within this region. No SMT value may enter or exit the lifespan of this region (such that no value created from another SMT context can be used in this scope and the solver can deallocate all state required to keep track of SMT values at the end).

As a result, the region is comparable to an entire SMT-LIB script, but allows for concrete operations and control-flow. Concrete values may be passed in and returned to influence the computations after the smt.solver operation.

Example:

%0:2 = smt.solver (%in) {smt.some_attr} : (i8) -> (i8, i32) {
^bb0(%arg0: i8):
  %c = smt.declare_fun "c" : !smt.bool
  smt.assert %c
  %1 = smt.check sat {
    %c1_i32 = arith.constant 1 : i32
    smt.yield %c1_i32 : i32
  } unknown {
    %c0_i32 = arith.constant 0 : i32
    smt.yield %c0_i32 : i32
  } unsat {
    %c-1_i32 = arith.constant -1 : i32
    smt.yield %c-1_i32 : i32
  } -> i32
  smt.yield %arg0, %1 : i8, i32
}

Traits: IsolatedFromAbove, SingleBlockImplicitTerminator<smt::YieldOp>, SingleBlock

Operands:

Operand	Description
inputs	variadic of any non-smt type

Results:

Result	Description
results	variadic of any non-smt type

smt.xor (::llzk::smt::XOrOp)

A boolean exclusive OR

Syntax:

operation ::= `smt.xor` $inputs attr-dict

This operation performs a boolean exclusive OR. The semantics are equivalent to the 'xor' operator in the Core theory. of the SMT-LIB Standard 2.7.

It supports a variadic number of operands, but requires at least two. This is because the operator is annotated with the :left-assoc attribute which means that op a b c is equivalent to (op (op a b) c).

Traits: AlwaysSpeculatableImplTrait

Interfaces: ConditionallySpeculatable, InferTypeOpInterface, NoMemoryEffect (MemoryEffectOpInterface)

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
inputs	variadic of

Results:

| Result | Description | | :-—: | --------— | | result |

smt.yield (::llzk::smt::YieldOp)

Terminator operation for various regions of SMT operations

Syntax:

operation ::= `smt.yield` ($values^ `:` qualified(type($values)))? attr-dict

Traits: AlwaysSpeculatableImplTrait, HasParent<smt::SolverOp, smt::CheckOp, smt::ForallOp, smt::ExistsOp>, ReturnLike, Terminator

Interfaces: ConditionallySpeculatable, NoMemoryEffect (MemoryEffectOpInterface), RegionBranchTerminatorOpInterface

Effects: MemoryEffects::Effect{}

Operands:

Operand	Description
values	variadic of any type

Attributes

BitVectorAttr

This attribute represents a constant value of the (_ BitVec width) sort as described in the SMT bit-vector theory.

The constant is as #bX (binary) or #xX (hexadecimal) in SMT-LIB where X is the value in the corresponding format without any further prefixing. Here, the bit-vector constant is given as a regular non-negative integer literal and the associated bit-vector type indicating the bit-width.

Examples:

#smt.bv<5> : !smt.bv<4>

#smt.bv<92> : !smt.bv<8>

The explicit type-suffix is mandatory to uniquely represent the attribute, i.e., this attribute should always be used in the extended form (using the quantified keyword in the operation assembly format string).

The bit-width must be greater than zero (i.e., at least one digit has to be present).

Parameters:

Parameter	C++ type	Description
value	::llvm::APInt

KeywordAttr

an SMT-LIB keyword

Represents a bare SMT-LIB keyword such as :status or :produce-models. These values are used by operations such as smt.set_info that need the structured surface syntax of the SMT-LIB language rather than quoted strings.

Parameters:

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

SymbolAttr

an SMT-LIB bare symbol

Represents a bare SMT-LIB symbol, for example sat, unknown, or a user-defined identifier used inside an SMT-LIB set-info payload.

Parameters:

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

Types

ArrayType

Syntax:

!smt.array<
  mlir::Type,   # domainType
  mlir::Type   # rangeType
>

This type represents the (Array X Y) sort, where X and Y are any sort/type, as described in the SMT ArrayEx theory of the SMT-LIB standard 2.7.

Parameters:

Parameter	C++ type	Description
domainType	mlir::Type
rangeType	mlir::Type

BitVectorType

Syntax:

!smt.bv<
  int64_t   # width
>

This type represents the (_ BitVec width) sort as described in the SMT bit-vector theory.

The bit-width must be strictly greater than zero.

Parameters:

Parameter	C++ type	Description
width	int64_t

BoolType

Syntax: !smt.bool

IntType

Syntax: !smt.int

This type represents the Int sort as described in the SMT Ints theory of the SMT-LIB 2.7 standard.

SMTFuncType

Syntax:

!smt.func<
  ::llvm::ArrayRef<mlir::Type>,   # domainTypes
  mlir::Type   # rangeType
>

This type represents the SMT function sort as described in the SMT-LIB 2.7 standard. It is part of the language itself rather than a theory or logic.

A function in SMT can have an arbitrary domain size, but always has exactly one range sort.

Since SMT only supports first-order logic, it is not possible to nest function types.

Example: !smt.func<(!smt.bool, !smt.int) !smt.bool> is equivalent to ((Bool Int) Bool) in SMT-LIB.

Parameters:

Parameter	C++ type	Description
domainTypes	::llvm::ArrayRef<mlir::Type>	domain types
rangeType	mlir::Type

SortType

Syntax:

!smt.sort<
  mlir::StringAttr,   # identifier
  ::llvm::ArrayRef<mlir::Type>   # sortParams
>

This type represents uninterpreted sorts. The usage of a type like !smt.sort<"sort_name"[!smt.bool, !smt.sort<"other_sort">]> implies a declare-sort sort_name 2 and a declare-sort other_sort 0 in SMT-LIB. This type represents concrete use-sites of such declared sorts, in this particular case it would be equivalent to (sort_name Bool other_sort) in SMT-LIB. More details about the semantics can be found in the SMT-LIB 2.7 standard.

Parameters:

Parameter	C++ type	Description
identifier	mlir::StringAttr
sortParams	::llvm::ArrayRef<mlir::Type>	sort parameters

Enums

BVCmpPredicate

smt bit-vector comparison predicate

Cases:

Symbol	Value	String
slt	0	slt
sle	1	sle
sgt	2	sgt
sge	3	sge
ult	4	ult
ule	5	ule
ugt	6	ugt
uge	7	uge

IntPredicate

smt comparison predicate for integers

Cases:

Symbol	Value	String
lt	0	lt
le	1	le
gt	2	gt
ge	3	ge

Table of Contents

'smt' Dialect

Operations

smt.and (::llzk::smt::AndOp)

Operands:

Results:

smt.apply_func (::llzk::smt::ApplyFuncOp)

Operands:

Results:

smt.array.broadcast (::llzk::smt::ArrayBroadcastOp)

Operands:

Results:

smt.array.select (::llzk::smt::ArraySelectOp)

Operands:

Results:

smt.array.store (::llzk::smt::ArrayStoreOp)

Operands:

Results:

smt.assert (::llzk::smt::AssertOp)

Operands:

smt.bv.add (::llzk::smt::BVAddOp)

Operands:

Results:

smt.bv.and (::llzk::smt::BVAndOp)

Operands:

Results:

smt.bv.ashr (::llzk::smt::BVAShrOp)

Operands:

Results:

smt.bv.cmp (::llzk::smt::BVCmpOp)

Attributes:

Operands:

Results:

smt.bv.concat (::llzk::smt::ConcatOp)

Operands:

Results:

smt.bv.constant (::llzk::smt::BVConstantOp)

Attributes:

Results:

smt.bv.extract (::llzk::smt::ExtractOp)

Attributes:

Operands:

Results:

smt.bv.lshr (::llzk::smt::BVLShrOp)

Operands:

Results:

smt.bv.mul (::llzk::smt::BVMulOp)

Operands:

Results:

smt.bv.neg (::llzk::smt::BVNegOp)

Operands:

Results:

smt.bv.not (::llzk::smt::BVNotOp)

Operands:

Results:

smt.bv.or (::llzk::smt::BVOrOp)

Operands:

Results:

smt.bv.repeat (::llzk::smt::RepeatOp)

Operands:

Results:

smt.bv.sdiv (::llzk::smt::BVSDivOp)

Operands:

Results:

smt.bv.shl (::llzk::smt::BVShlOp)

Operands:

Results:

smt.bv.smod (::llzk::smt::BVSModOp)

Operands:

Results:

smt.bv.srem (::llzk::smt::BVSRemOp)

Operands:

Results:

smt.bv.udiv (::llzk::smt::BVUDivOp)

Operands:

Results:

smt.bv.urem (::llzk::smt::BVURemOp)

Operands:

Results:

smt.bv.xor (::llzk::smt::BVXOrOp)