[SMT] Add set_logic operation (#7927)

llvm · Nov 30, 2024 · c9b5ba9 · c9b5ba9
1 parent 44a38c4
commit c9b5ba9
Show file tree

Hide file tree

Showing 6 changed files with 42 additions and 1 deletion.
diff --git a/include/circt/Dialect/SMT/SMTOps.td b/include/circt/Dialect/SMT/SMTOps.td
@@ -147,6 +147,12 @@ def SolverOp : SMTOp<"solver", [
   let hasRegionVerifier = true;
 }
 
+def SetLogicOp : SMTOp<"set_logic", []> {
+  let summary = "set the logic for the SMT solver";
+  let arguments = (ins StrAttr:$logic);
+  let assemblyFormat = "$logic attr-dict";
+}
+
 def AssertOp : SMTOp<"assert", []> {
   let summary = "assert that a boolean expression holds";
   let arguments = (ins BoolType:$input);

diff --git a/include/circt/Dialect/SMT/SMTVisitors.h b/include/circt/Dialect/SMT/SMTVisitors.h
@@ -44,7 +44,7 @@ class SMTOpVisitor {
             // Variable/symbol declaration
             DeclareFunOp, ApplyFuncOp,
             // solver interaction
-            SolverOp, AssertOp, ResetOp, PushOp, PopOp, CheckOp,
+            SolverOp, AssertOp, ResetOp, PushOp, PopOp, CheckOp, SetLogicOp,
             // Boolean logic
             NotOp, AndOp, OrOp, XOrOp, ImpliesOp,
             // Arrays
@@ -128,6 +128,7 @@ class SMTOpVisitor {
   HANDLE(PushOp, Unhandled);
   HANDLE(PopOp, Unhandled);
   HANDLE(CheckOp, Unhandled);
+  HANDLE(SetLogicOp, Unhandled);
 
   // Boolean logic operations
   HANDLE(NotOp, Unhandled);

diff --git a/integration_test/Target/ExportSMTLIB/basic.mlir b/integration_test/Target/ExportSMTLIB/basic.mlir
@@ -172,3 +172,20 @@ smt.solver () : () -> () {
 // CHECK-NOT: error
 // CHECK-NOT: unsat
 // CHECK: sat
+
+smt.solver () : () -> () {
+  smt.set_logic "HORN"
+  %c = smt.declare_fun : !smt.int
+  %c4 = smt.int.constant 4
+  %eq = smt.eq %c, %c4 : !smt.int
+  smt.assert %eq
+  smt.check sat {} unknown {} unsat {}
+}
+
+// CHECK-NOT: WARNING
+// CHECK-NOT: warning
+// CHECK-NOT: ERROR
+// CHECK-NOT: error
+// CHECK-NOT: unsat
+// CHECK-NOT: sat
+// CHECK: unknown
diff --git a/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp b/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp
@@ -592,6 +592,12 @@ struct StatementVisitor
     return success();
   }
 
+  LogicalResult visitSMTOp(SetLogicOp op, mlir::raw_indented_ostream &stream,
+                           ValueMap &valueMap) {
+    stream << "(set-logic " << op.getLogic() << ")\n";
+    return success();
+  }
+
   LogicalResult visitUnhandledSMTOp(Operation *op,
                                     mlir::raw_indented_ostream &stream,
                                     ValueMap &valueMap) {

diff --git a/test/Dialect/SMT/basic.mlir b/test/Dialect/SMT/basic.mlir
@@ -65,6 +65,13 @@ func.func @core(%in: i8) {
   // CHECK-NEXT: }
   smt.solver() : () -> () { }
 
+  // CHECK: smt.solver() : () -> () {
+  // CHECK-NEXT: smt.set_logic "AUFLIA"
+  // CHECK-NEXT: }
+  smt.solver() : () -> () {
+    smt.set_logic "AUFLIA"
+  }
+
   //      CHECK: smt.check sat {
   // CHECK-NEXT: } unknown {
   // CHECK-NEXT: } unsat {

diff --git a/test/Target/ExportSMTLIB/core.mlir b/test/Target/ExportSMTLIB/core.mlir
@@ -128,6 +128,10 @@ smt.solver () : () -> () {
   // CHECK-INLINED: (pop 1)
   smt.pop 1
 
+  // CHECK: (set-logic AUFLIA)
+  // CHECK-INLINED: (set-logic AUFLIA)
+  smt.set_logic "AUFLIA"
+
   // CHECK: (reset)
   // CHECK-INLINED: (reset)
 }