SMT Dialect
This dialect provides types and operations modeling the SMT (Satisfiability Modulo Theories) operations and datatypes commonly found in SMT-LIB and SMT solvers.
Rationale ¶
This dialect aims to provide a unified interface for expressing SMT problems directly within MLIR, enabling seamless integration with other MLIR dialects and optimization passes. It models the SMT-LIB standard 2.6, but may also include features of commonly used SMT solvers that are not part of the standard. In particular, the IR constructs are designed to enable more interactive communication with the solver (allowing if-statements, etc. to react on solver feedback).
The SMT dialect is motivated by the following advantages over directly printing SMT-LIB or exporting to a solver:
- Reuse MLIR’s infrastructure: passes and pass managers to select different SMT encodings, operation builders and rewrite patterns to build SMT formulae (and hide the solver’s API in a provided lowering pass), common textual format to share rather than dumping the solver’s state, etc.
- No need to add a link-dependency on SMT solvers to CIRCT (just provide the path to the library as an argument to the JIT runner or manually link the produced binary against it).
- Using an SMT dialect as intermediary allows it to be mixed with concrete computations, the debug dialect, etc. This is complicated to achieve and reason about when building the external solver’s state directly.
- Enable easy addition of new backends
- Have a common representation and infrastructure for all SMT related efforts, such that people don’t have to build their own isolated tools.
The dialect follows these design principles:
- Solver-independent: don’t model one particular solver’s API
- Seemless interoperability with other dialects. E.g., to allow using the debug dialect to back-propagate counter examples
- Small surface for errors: try to keep the SMT dialect and its lowerings simple to avoid mistakes, implement optimizations defensively or prove them formally; since higher-level dialects will be lowered through the SMT dialect to construct formal proofs it is essential that this dialect does not introduce bugs
- Interactive: the IR should be designed such that it can be interleaved with operations (from other dialects) that take the current feedback of the solver to steer the execution of further SMT operations. It shouldn’t just model the very rigid SMT-LIB.
- Don’t heavily integrate the dialect itself with CIRCT to make potential upstreaming easy
Dialect Structure ¶
The SMT dialect is structured into multiple “sub-dialects”, one for each of the following theories (this separation is also made clear in the prefix of operation and type names as indicated in parentheses):
- Core boolean logic including quantifiers and solver interaction (
smt.*
) - Bit-vectors (
smt.bv.*
) - Arbitrary-precision integers (
smt.int.*
) - Arrays (
smt.array.*
) - Floating-point numbers (
smt.real.*
)
Several operations in the core part (e.g., quantifiers, equality, etc.) allow operands of any SMT type (including bit-vectors, arrays, etc.). Therefore, all type and attribute declarations are part of the core.
Certain arithmetic, bitwise, and comparison operations exist for multiple theories. For example, there exists an AND operation for booleans and one for bit-vectors, or there exists and ADD operation for integers and bit-vectors. In such cases, each “sub-dialect” defines its own operation specific to its datatypes. This simplifies the operations such that an optimization or conversion pass only using bit-vectors does not have to take care of other potentially supported datatypes.
Optimizations ¶
The primary purpose of the SMT dialect is not to optimize SMT formulae. However, SMT solvers can exhibit significant differences in runtime, even with slight changes in input. Improving solver performance by implementing rewrite patterns that slightly restructure the SMT formulae may be possible.
Moreover, SMT solvers may differ in terms of built-in operators. If a solver lacks support for advanced operators, the problem can be simplified before passing it to the solver.
Backends ¶
Having an SMT dialect instead of directly interpreting the IR and building an SMT expression enables multiple different backends to be used in addition to the application of SMT dialect level optimizations that rewrite the formulae for faster and more predictable runtime performance of the solver backend (e.g., Z3).
In the following, we outline the different backend lowerings and their advantages and disadvantages.
LLVM IR ¶
Lowering to LLVM IR that calls the C API of a given SMT solver is practical for a few reasons:
- enables using LLVM JIT or compilation to a standalone binary
- easy to mix with Debug dialect to report back nice counter examples
- allows mixing concrete and symbolic executions (e.g., for dynamic BMC upper bounds, or more dynamic interaction with the solver such as extraction of multiple/all possible models)
However, it is solver-dependent and more complicated to implement than an SMT-LIB printer.
SMT-LIB ¶
The SMT-LIB format is a standardized format supported by practically all SMT solvers and thus an ideal target to support as many solver backends as possible. However,
- this format is quite static and does not allow easy interaction with the solver, in particular, it is not easily possible to make future asserts dependent on current solver outputs,
- providing good counter-examples to the user would mean parsing the textual model output of the solver and mapping it to an CIRCT-internal datastructure.
- it is impossible to mix symbolic and concrete executions, as well as debug constructs (see Debug Dialect).
- it is impossible to just use the LLVM JIT compiler to directly get a result, but instead the external solver has to be called directly, either by adding a compile-time dependency, or using a shell call.
C/C++ ¶
A C/C++ exporter that produces code which calls the C/C++ API of a given solver could allow for easier debugging and allows to support solvers without C API without the restrictions of SMT-LIB. However, this means the JIT compilation flow would not be available.
Handling counter-examples ¶
SMT solvers check formulae for satisfiability. Typically, there are three kinds of output a solver may give:
- Satisfiable: In this case a model (counter-example) can be provided by the solver. However, it may not be feasible to evaluate/interpret this model for a given SMT constant to get a constant value. This is, in particular, the case when the SMT encoding contains quantifiers which can lead to the model containing quantifiers as well. Solvers (e.g., Z3) usually don’t evaluate quantifiers in models (even if they are closed). If constants can be evaluated, a counter example can be provided and back-propagated to the source-code, e.g., using the debug dialect.
- Unsatisfiable: formal verification problems are typically encoded such that this output indicates correctness; a proof can be provided by the solver, but is often not needed
- Unknown: there can be various reasons why the result is unknown; a common one is the use of symbolic functions to represent operators and encode, e.g., a LEC problem as a rewrite task of patterns of function applications. This is a frequent application and the unknown result is just treated like a satisfiable result without counter example.
Non-Goals ¶
- The SMT Dialect does not aim to include any operations or types that model verification constructs not specific to SMT, i.e., things that could also be lowered to other kind of verification systems such as inductive theorem provers (e.g., Lean4).
Operations ¶
smt.and
(circt::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.6.
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
(circt::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.6 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
(circt::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 "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
(circt::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.6.
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
(circt::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.6.
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
(circt::smt::AssertOp) ¶
Assert that a boolean expression holds
Syntax:
operation ::= `smt.assert` $input attr-dict
Operands: ¶
Operand | Description |
---|---|
input |
smt.bv.ashr
(circt::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.6
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.add
(circt::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.6
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
(circt::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.6
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
(circt::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.6 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 | circt::smt::BVCmpPredicateAttr | smt bit-vector comparison predicate |
Operands: ¶
Operand | Description |
---|---|
lhs | |
rhs |
Results: ¶
Result | Description |
---|---|
result |
smt.bv.constant
(circt::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 | circt::smt::BitVectorAttr |
Results: ¶
Result | Description |
---|---|
result |
smt.bv.lshr
(circt::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.6
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
(circt::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.6
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
(circt::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.6
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
(circt::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.6
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
(circt::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.6
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.sdiv
(circt::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.6
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
(circt::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.6
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
(circt::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.6
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
(circt::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.6
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
(circt::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.6
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
(circt::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.6
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
(circt::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.6
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.constant
(circt::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.6.
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.check
(circt::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.bv.concat
(circt::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.6 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.declare_fun
(circt::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-func
statements in SMT-LIB 2.6. 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
(circt::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.6 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
(circt::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.6 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
(circt::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.6 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.bv.extract
(circt::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.6 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.forall
(circt::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.6 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
(circt::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.6.
Traits: AlwaysSpeculatableImplTrait
Interfaces: ConditionallySpeculatable
, InferTypeOpInterface
, NoMemoryEffect (MemoryEffectOpInterface)
Effects: MemoryEffects::Effect{}
Operands: ¶
Operand | Description |
---|---|
lhs | |
rhs |
Results: ¶
Result | Description |
---|---|
result |
smt.int.abs
(circt::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.6 standard.
Traits: AlwaysSpeculatableImplTrait
Interfaces: ConditionallySpeculatable
, InferTypeOpInterface
, NoMemoryEffect (MemoryEffectOpInterface)
Effects: MemoryEffects::Effect{}
Operands: ¶
Operand | Description |
---|---|
input |
Results: ¶
Result | Description |
---|---|
result |
smt.int.add
(circt::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.6 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
(circt::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.6 standard.
Traits: AlwaysSpeculatableImplTrait
Interfaces: ConditionallySpeculatable
, InferTypeOpInterface
, NoMemoryEffect (MemoryEffectOpInterface)
Effects: MemoryEffects::Effect{}
Attributes: ¶
Attribute | MLIR Type | Description |
---|---|---|
pred | circt::smt::IntPredicateAttr | smt comparison predicate for integers |
Operands: ¶
Operand | Description |
---|---|
lhs | |
rhs |
Results: ¶
Result | Description |
---|---|
result |
smt.int.constant
(circt::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 -n
where n is a numeral other than 0. For more
information refer to the
SMT Ints theory of the
SMT-LIB 2.6 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
(circt::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.6 standard.
Traits: AlwaysSpeculatableImplTrait
Interfaces: ConditionallySpeculatable
, InferTypeOpInterface
, NoMemoryEffect (MemoryEffectOpInterface)
Effects: MemoryEffects::Effect{}
Operands: ¶
Operand | Description |
---|---|
lhs | |
rhs |
Results: ¶
Result | Description |
---|---|
result |
smt.int.mod
(circt::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.6 standard.
Traits: AlwaysSpeculatableImplTrait
Interfaces: ConditionallySpeculatable
, InferTypeOpInterface
, NoMemoryEffect (MemoryEffectOpInterface)
Effects: MemoryEffects::Effect{}
Operands: ¶
Operand | Description |
---|---|
lhs | |
rhs |
Results: ¶
Result | Description |
---|---|
result |
smt.int.mul
(circt::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.6 standard.
Traits: AlwaysSpeculatableImplTrait
, Commutative
Interfaces: ConditionallySpeculatable
, InferTypeOpInterface
, NoMemoryEffect (MemoryEffectOpInterface)
Effects: MemoryEffects::Effect{}
Operands: ¶
Operand | Description |
---|---|
inputs | variadic of |
Results: ¶
Result | Description |
---|---|
result |
smt.int.sub
(circt::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.6 standard.
Traits: AlwaysSpeculatableImplTrait
Interfaces: ConditionallySpeculatable
, InferTypeOpInterface
, NoMemoryEffect (MemoryEffectOpInterface)
Effects: MemoryEffects::Effect{}
Operands: ¶
Operand | Description |
---|---|
lhs | |
rhs |
Results: ¶
Result | Description |
---|---|
result |
smt.ite
(circt::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.6 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
(circt::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.6.
Traits: AlwaysSpeculatableImplTrait
Interfaces: ConditionallySpeculatable
, InferTypeOpInterface
, NoMemoryEffect (MemoryEffectOpInterface)
Effects: MemoryEffects::Effect{}
Operands: ¶
Operand | Description |
---|---|
input |
Results: ¶
Result | Description |
---|---|
result |
smt.or
(circt::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.6.
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.bv.repeat
(circt::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.6 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.solver
(circt::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
}
TODO: solver configuration attributes
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
(circt::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.6.
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
(circt::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 |
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.6.
Parameters: ¶
Parameter | C++ type | Description |
---|---|---|
domainType | mlir::Type | |
rangeType | mlir::Type |
BitVectorType ¶
Syntax:
!smt.bv<
uint64_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 | uint64_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.6 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.6 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.6 standard.
Parameters: ¶
Parameter | C++ type | Description |
---|---|---|
identifier | mlir::StringAttr | |
sortParams | ::llvm::ArrayRef<mlir::Type> | sort parameters |