Skip to content

Commit

Permalink
[SMT] Add basic array operations
Browse files Browse the repository at this point in the history
  • Loading branch information
maerhart committed Mar 14, 2024
1 parent 9c4f721 commit 91a63aa
Show file tree
Hide file tree
Showing 4 changed files with 127 additions and 0 deletions.
1 change: 1 addition & 0 deletions include/circt/Dialect/SMT/SMT.td
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ include "circt/Dialect/SMT/SMTAttributes.td"
include "circt/Dialect/SMT/SMTDialect.td"
include "circt/Dialect/SMT/SMTTypes.td"
include "circt/Dialect/SMT/SMTOps.td"
include "circt/Dialect/SMT/SMTArrayOps.td"
include "circt/Dialect/SMT/SMTBitVectorOps.td"

#endif // CIRCT_DIALECT_SMT_SMT_TD
99 changes: 99 additions & 0 deletions include/circt/Dialect/SMT/SMTArrayOps.td
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
//===- SMTArrayOps.td - SMT array operations ---------------*- tablegen -*-===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//

#ifndef CIRCT_DIALECT_SMT_SMTARRAYOPS_TD
#define CIRCT_DIALECT_SMT_SMTARRAYOPS_TD

include "circt/Dialect/SMT/SMTDialect.td"
include "circt/Dialect/SMT/SMTAttributes.td"
include "circt/Dialect/SMT/SMTTypes.td"
include "mlir/Interfaces/SideEffectInterfaces.td"

class SMTArrayOp<string mnemonic, list<Trait> traits = []> :
SMTOp<"array." # mnemonic, traits>;

def ArrayStoreOp : SMTArrayOp<"store", [
Pure,
TypesMatchWith<"summary", "array", "index",
"cast<ArrayType>($_self).getDomainType()">,
TypesMatchWith<"summary", "array", "value",
"cast<ArrayType>($_self).getRangeType()">,
AllTypesMatch<["array", "result"]>,
]> {
let summary = "stores a value at a given index and returns the new array";
let description = [{
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](https://smtlib.cs.uiowa.edu/Theories/ArraysEx.smt2) of
the SMT-LIB standard 2.6.
}];

let arguments = (ins ArrayType:$array, AnySMTType:$index, AnySMTType:$value);
let results = (outs ArrayType:$result);

let assemblyFormat = [{
$array `[` $index `]` `,` $value attr-dict `:` qualified(type($array))
}];
}

def ArraySelectOp : SMTArrayOp<"select", [
Pure,
TypesMatchWith<"summary", "array", "index",
"cast<ArrayType>($_self).getDomainType()">,
TypesMatchWith<"summary", "array", "result",
"cast<ArrayType>($_self).getRangeType()">,
]> {
let summary = "get the value stored in the array at the given index";
let description = [{
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](https://smtlib.cs.uiowa.edu/Theories/ArraysEx.smt2) of
the SMT-LIB standard 2.6.
}];

let arguments = (ins ArrayType:$array, AnySMTType:$index);
let results = (outs AnySMTType:$result);

let assemblyFormat = [{
$array `[` $index `]` attr-dict `:` qualified(type($array))
}];
}

def ArrayBroadcastOp : SMTArrayOp<"broadcast", [
Pure,
TypesMatchWith<"summary", "result", "value",
"cast<ArrayType>($_self).getRangeType()">,
]> {
let summary = "construct an array with the given value stored at every index";
let description = [{
This operation represents a broadcast of the 'value' operand to all indices
of the array. It is equivalent to
```
%0 = smt.declare_const "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)`.
}];

let arguments = (ins AnySMTType:$value);
let results = (outs ArrayType:$result);

let assemblyFormat = "$value attr-dict `:` qualified(type($result))";
}

#endif // CIRCT_DIALECT_SMT_SMTARRAYOPS_TD
13 changes: 13 additions & 0 deletions include/circt/Dialect/SMT/SMTTypes.td
Original file line number Diff line number Diff line change
Expand Up @@ -35,4 +35,17 @@ def BitVectorType : SMTTypeDef<"BitVector"> {
let genVerifyDecl = true;
}

def ArrayType : SMTTypeDef<"Array"> {
let mnemonic = "array";
let description = [{
This type represents the `(Array X Y)` sort, where X and Y are any
sort/type, as described in the
[SMT ArrayEx theory](https://smtlib.cs.uiowa.edu/Theories/ArraysEx.smt2) of
the SMT-LIB standard 2.6.
}];

let parameters = (ins "mlir::Type":$domainType, "mlir::Type":$rangeType);
let assemblyFormat = "`<` `[` $domainType `->` $rangeType `]` `>`";
}

#endif // CIRCT_DIALECT_SMT_SMTTYPES_TD
14 changes: 14 additions & 0 deletions test/Dialect/SMT/array.mlir
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
// RUN: circt-opt %s | circt-opt | FileCheck %s

// CHECK-LABEL: func @arrayOperations
// CHECK-SAME: ([[A0:%.+]]: !smt.bool)
func.func @arrayOperations(%arg0: !smt.bool) {
// CHECK-NEXT: [[V0:%.+]] = smt.array.broadcast [[A0]] {smt.some_attr} : !smt.array<[!smt.int -> !smt.bool]>
%0 = smt.array.broadcast %arg0 {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
// CHECK-NEXT: [[V1:%.+]] = smt.array.select [[V0]][[[A0]]] {smt.some_attr} : !smt.array<[!smt.int -> !smt.bool]>
%1 = smt.array.select %0[%arg0] {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
// CHECK-NEXT: [[V2:%.+]] = smt.array.store [[V0]][[[A0]]], [[A0]] {smt.some_attr} : !smt.array<[!smt.int -> !smt.bool]>
%2 = smt.array.store %0[%arg0], %arg0 {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>

return
}

0 comments on commit 91a63aa

Please sign in to comment.