188 lines · cpp
1//===- QuantifierTest.cpp - SMT quantifier operation unit tests -----------===//2//3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.4// See https://llvm.org/LICENSE.txt for license information.5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception6//7//===----------------------------------------------------------------------===//8 9#include "mlir/Dialect/SMT/IR/SMTOps.h"10#include "gtest/gtest.h"11 12using namespace mlir;13using namespace smt;14 15namespace {16 17//===----------------------------------------------------------------------===//18// Test custom builders of ExistsOp19//===----------------------------------------------------------------------===//20 21TEST(QuantifierTest, ExistsBuilderWithPattern) {22 MLIRContext context;23 context.loadDialect<SMTDialect>();24 Location loc(UnknownLoc::get(&context));25 26 OpBuilder builder(&context);27 auto boolTy = BoolType::get(&context);28 29 OwningOpRef<ExistsOp> existsOp = ExistsOp::create(30 builder, loc, TypeRange{boolTy, boolTy},31 [](OpBuilder &builder, Location loc, ValueRange boundVars) {32 return AndOp::create(builder, loc, boundVars);33 },34 std::nullopt,35 [](OpBuilder &builder, Location loc, ValueRange boundVars) {36 return boundVars;37 },38 /*weight=*/2);39 40 SmallVector<char, 1024> buffer;41 llvm::raw_svector_ostream stream(buffer);42 existsOp->print(stream);43 44 ASSERT_STREQ(45 stream.str().str().c_str(),46 "%0 = smt.exists weight 2 {\n^bb0(%arg0: !smt.bool, "47 "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield %0 : "48 "!smt.bool\n} patterns {\n^bb0(%arg0: !smt.bool, %arg1: !smt.bool):\n "49 "smt.yield %arg0, %arg1 : !smt.bool, !smt.bool\n}\n");50}51 52TEST(QuantifierTest, ExistsBuilderNoPattern) {53 MLIRContext context;54 context.loadDialect<SMTDialect>();55 Location loc(UnknownLoc::get(&context));56 57 OpBuilder builder(&context);58 auto boolTy = BoolType::get(&context);59 60 OwningOpRef<ExistsOp> existsOp = ExistsOp::create(61 builder, loc, TypeRange{boolTy, boolTy},62 [](OpBuilder &builder, Location loc, ValueRange boundVars) {63 return AndOp::create(builder, loc, boundVars);64 },65 ArrayRef<StringRef>{"a", "b"}, nullptr, /*weight=*/0, /*noPattern=*/true);66 67 SmallVector<char, 1024> buffer;68 llvm::raw_svector_ostream stream(buffer);69 existsOp->print(stream);70 71 ASSERT_STREQ(stream.str().str().c_str(),72 "%0 = smt.exists [\"a\", \"b\"] no_pattern {\n^bb0(%arg0: "73 "!smt.bool, %arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n "74 "smt.yield %0 : !smt.bool\n}\n");75}76 77TEST(QuantifierTest, ExistsBuilderDefault) {78 MLIRContext context;79 context.loadDialect<SMTDialect>();80 Location loc(UnknownLoc::get(&context));81 82 OpBuilder builder(&context);83 auto boolTy = BoolType::get(&context);84 85 OwningOpRef<ExistsOp> existsOp = ExistsOp::create(86 builder, loc, TypeRange{boolTy, boolTy},87 [](OpBuilder &builder, Location loc, ValueRange boundVars) {88 return AndOp::create(builder, loc, boundVars);89 },90 ArrayRef<StringRef>{"a", "b"});91 92 SmallVector<char, 1024> buffer;93 llvm::raw_svector_ostream stream(buffer);94 existsOp->print(stream);95 96 ASSERT_STREQ(stream.str().str().c_str(),97 "%0 = smt.exists [\"a\", \"b\"] {\n^bb0(%arg0: !smt.bool, "98 "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield "99 "%0 : !smt.bool\n}\n");100}101 102//===----------------------------------------------------------------------===//103// Test custom builders of ForallOp104//===----------------------------------------------------------------------===//105 106TEST(QuantifierTest, ForallBuilderWithPattern) {107 MLIRContext context;108 context.loadDialect<SMTDialect>();109 Location loc(UnknownLoc::get(&context));110 111 OpBuilder builder(&context);112 auto boolTy = BoolType::get(&context);113 114 OwningOpRef<ForallOp> forallOp = ForallOp::create(115 builder, loc, TypeRange{boolTy, boolTy},116 [](OpBuilder &builder, Location loc, ValueRange boundVars) {117 return AndOp::create(builder, loc, boundVars);118 },119 ArrayRef<StringRef>{"a", "b"},120 [](OpBuilder &builder, Location loc, ValueRange boundVars) {121 return boundVars;122 },123 /*weight=*/2);124 125 SmallVector<char, 1024> buffer;126 llvm::raw_svector_ostream stream(buffer);127 forallOp->print(stream);128 129 ASSERT_STREQ(130 stream.str().str().c_str(),131 "%0 = smt.forall [\"a\", \"b\"] weight 2 {\n^bb0(%arg0: !smt.bool, "132 "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield %0 : "133 "!smt.bool\n} patterns {\n^bb0(%arg0: !smt.bool, %arg1: !smt.bool):\n "134 "smt.yield %arg0, %arg1 : !smt.bool, !smt.bool\n}\n");135}136 137TEST(QuantifierTest, ForallBuilderNoPattern) {138 MLIRContext context;139 context.loadDialect<SMTDialect>();140 Location loc(UnknownLoc::get(&context));141 142 OpBuilder builder(&context);143 auto boolTy = BoolType::get(&context);144 145 OwningOpRef<ForallOp> forallOp = ForallOp::create(146 builder, loc, TypeRange{boolTy, boolTy},147 [](OpBuilder &builder, Location loc, ValueRange boundVars) {148 return AndOp::create(builder, loc, boundVars);149 },150 ArrayRef<StringRef>{"a", "b"}, nullptr, /*weight=*/0, /*noPattern=*/true);151 152 SmallVector<char, 1024> buffer;153 llvm::raw_svector_ostream stream(buffer);154 forallOp->print(stream);155 156 ASSERT_STREQ(stream.str().str().c_str(),157 "%0 = smt.forall [\"a\", \"b\"] no_pattern {\n^bb0(%arg0: "158 "!smt.bool, %arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n "159 "smt.yield %0 : !smt.bool\n}\n");160}161 162TEST(QuantifierTest, ForallBuilderDefault) {163 MLIRContext context;164 context.loadDialect<SMTDialect>();165 Location loc(UnknownLoc::get(&context));166 167 OpBuilder builder(&context);168 auto boolTy = BoolType::get(&context);169 170 OwningOpRef<ForallOp> forallOp = ForallOp::create(171 builder, loc, TypeRange{boolTy, boolTy},172 [](OpBuilder &builder, Location loc, ValueRange boundVars) {173 return AndOp::create(builder, loc, boundVars);174 },175 std::nullopt);176 177 SmallVector<char, 1024> buffer;178 llvm::raw_svector_ostream stream(buffer);179 forallOp->print(stream);180 181 ASSERT_STREQ(stream.str().str().c_str(),182 "%0 = smt.forall {\n^bb0(%arg0: !smt.bool, "183 "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield "184 "%0 : !smt.bool\n}\n");185}186 187} // namespace188