Skip to content

Commit

Permalink
[SMT] Add integration tests for smt.reset (#7874)
Browse files Browse the repository at this point in the history
  • Loading branch information
TaoBi22 authored Nov 22, 2024
1 parent cd7b8b3 commit f59bc61
Show file tree
Hide file tree
Showing 2 changed files with 42 additions and 0 deletions.
15 changes: 15 additions & 0 deletions integration_test/Dialect/SMT/basic.mlir
Original file line number Diff line number Diff line change
Expand Up @@ -168,6 +168,21 @@ func.func @entry() {
smt.yield
}

// CHECK: unsat
// CHECK: Res: -1
// CHECK: sat
// CHECK: Res: 1
smt.solver () : () -> () {
%c3 = smt.int.constant 3
%c4 = smt.int.constant 4
%unsat_eq = smt.eq %c3, %c4 : !smt.int
func.call @check(%unsat_eq) : (!smt.bool) -> ()
smt.reset
%sat_eq = smt.eq %c3, %c3 : !smt.int
func.call @check(%sat_eq) : (!smt.bool) -> ()
smt.yield
}

return
}

Expand Down
27 changes: 27 additions & 0 deletions integration_test/Target/ExportSMTLIB/basic.mlir
Original file line number Diff line number Diff line change
Expand Up @@ -145,3 +145,30 @@ smt.solver () : () -> () {
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat

// Reset
smt.solver () : () -> () {
%three = smt.int.constant 3
%four = smt.int.constant 4
%unsat_eq = smt.eq %three, %four : !smt.int
%sat_eq = smt.eq %three, %three : !smt.int

smt.assert %unsat_eq
smt.check sat {} unknown {} unsat {}
smt.reset
smt.assert %sat_eq
smt.check sat {} unknown {} unsat {}
}

// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: sat
// CHECK: unsat
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat

0 comments on commit f59bc61

Please sign in to comment.