mirror of https://github.com/llvm/circt.git
138 lines
4.8 KiB
MLIR
138 lines
4.8 KiB
MLIR
// RUN: circt-translate --export-smtlib %s | FileCheck %s
|
|
// RUN: circt-translate --export-smtlib --smtlibexport-inline-single-use-values %s | FileCheck %s --check-prefix=CHECK-INLINED
|
|
|
|
smt.solver () : () -> () {
|
|
%c0_bv32 = smt.bv.constant #smt.bv<0> : !smt.bv<32>
|
|
%true = smt.constant true
|
|
%false = smt.constant false
|
|
|
|
// CHECK: (declare-const b (_ BitVec 32))
|
|
// CHECK: (assert (let (([[V0:.+]] (= #x00000000 b)))
|
|
// CHECK: [[V0]]))
|
|
|
|
// CHECK-INLINED: (declare-const b (_ BitVec 32))
|
|
// CHECK-INLINED: (assert (= #x00000000 b))
|
|
%21 = smt.declare_fun "b" : !smt.bv<32>
|
|
%23 = smt.eq %c0_bv32, %21 : !smt.bv<32>
|
|
smt.assert %23
|
|
|
|
// CHECK: (assert (let (([[V1:.+]] (distinct #x00000000 #x00000000)))
|
|
// CHECK: [[V1]]))
|
|
|
|
// CHECK-INLINED: (assert (distinct #x00000000 #x00000000))
|
|
%24 = smt.distinct %c0_bv32, %c0_bv32 : !smt.bv<32>
|
|
smt.assert %24
|
|
|
|
// CHECK: (declare-const a Bool)
|
|
// CHECK: (assert (let (([[V2:.+]] (ite a #x00000000 b)))
|
|
// CHECK: (let (([[V3:.+]] (= #x00000000 [[V2]])))
|
|
// CHECK: [[V3]])))
|
|
|
|
// CHECK-INLINED: (declare-const a Bool)
|
|
// CHECK-INLINED: (assert (= #x00000000 (ite a #x00000000 b)))
|
|
%20 = smt.declare_fun "a" : !smt.bool
|
|
%38 = smt.ite %20, %c0_bv32, %21 : !smt.bv<32>
|
|
%4 = smt.eq %c0_bv32, %38 : !smt.bv<32>
|
|
smt.assert %4
|
|
|
|
// CHECK: (assert (let (([[V4:.+]] (not true)))
|
|
// CHECK: (let (([[V5:.+]] (and [[V4]] true false)))
|
|
// CHECK: (let (([[V6:.+]] (or [[V5]] [[V4]] true)))
|
|
// CHECK: (let (([[V7:.+]] (xor [[V4]] [[V6]])))
|
|
// CHECK: (let (([[V8:.+]] (=> [[V7]] false)))
|
|
// CHECK: [[V8]]))))))
|
|
|
|
// CHECK-INLINED: (assert (let (([[V15:.+]] (not true)))
|
|
// CHECK-INLINED: (=> (xor [[V15]] (or (and [[V15]] true false) [[V15]] true)) false)))
|
|
%39 = smt.not %true
|
|
%40 = smt.and %39, %true, %false
|
|
%41 = smt.or %40, %39, %true
|
|
%42 = smt.xor %39, %41
|
|
%43 = smt.implies %42, %false
|
|
smt.assert %43
|
|
|
|
// CHECK: (declare-fun func1 (Bool Bool) Bool)
|
|
// CHECK: (assert (let (([[V9:.+]] (func1 true false)))
|
|
// CHECK: [[V9]]))
|
|
|
|
// CHECK-INLINED: (declare-fun func1 (Bool Bool) Bool)
|
|
// CHECK-INLINED: (assert (func1 true false))
|
|
%44 = smt.declare_fun "func1" : !smt.func<(!smt.bool, !smt.bool) !smt.bool>
|
|
%45 = smt.apply_func %44(%true, %false) : !smt.func<(!smt.bool, !smt.bool) !smt.bool>
|
|
smt.assert %45
|
|
|
|
// CHECK: (assert (let (([[V10:.+]] (forall (([[A:.+]] Int) ([[B:.+]] Int))
|
|
// CHECK: (let (([[V11:.+]] (= [[A]] [[B]])))
|
|
// CHECK: [[V11]]))))
|
|
// CHECK: [[V10]]))
|
|
|
|
// CHECK-INLINED: (assert (forall (([[A:.+]] Int) ([[B:.+]] Int))
|
|
// CHECK-INLINED: (= [[A]] [[B]])))
|
|
%1 = smt.forall ["a", "b"] {
|
|
^bb0(%arg2: !smt.int, %arg3: !smt.int):
|
|
%2 = smt.eq %arg2, %arg3 : !smt.int
|
|
smt.yield %2 : !smt.bool
|
|
}
|
|
smt.assert %1
|
|
|
|
// CHECK: (assert (let (([[V12:.+]] (exists (([[V13:.+]] Int) ([[V14:.+]] Int))
|
|
// CHECK: (let (([[V15:.+]] (= [[V13]] [[V14]])))
|
|
// CHECK: [[V15]]))))
|
|
// CHECK: [[V12]]))
|
|
|
|
// CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
|
|
// CHECK-INLINED: (= [[A]] [[B]])))
|
|
%2 = smt.exists {
|
|
^bb0(%arg2: !smt.int, %arg3: !smt.int):
|
|
%3 = smt.eq %arg2, %arg3 : !smt.int
|
|
smt.yield %3 : !smt.bool
|
|
}
|
|
smt.assert %2
|
|
|
|
// Test: make sure that open parens from outside quantifier bodies are not
|
|
// propagated into the body.
|
|
// CHECK: (assert (let (([[V15:.+]] (exists (([[V16:.+]] Int) ([[V17:.+]] Int)){{$}}
|
|
// CHECK: (let (([[V18:.+]] (= [[V16]] [[V17]]))){{$}}
|
|
// CHECK: [[V18]])))){{$}}
|
|
// CHECK: (let (([[V19:.+]] (exists (([[V20:.+]] Int) ([[V21:.+]] Int)){{$}}
|
|
// CHECK: (let (([[V22:.+]] (= [[V20]] [[V21]]))){{$}}
|
|
// CHECK: [[V22]])))){{$}}
|
|
// CHECK: (let (([[V23:.+]] (and [[V19]] [[V15]]))){{$}}
|
|
// CHECK: [[V23]])))){{$}}
|
|
%3 = smt.exists {
|
|
^bb0(%arg2: !smt.int, %arg3: !smt.int):
|
|
%5 = smt.eq %arg2, %arg3 : !smt.int
|
|
smt.yield %5 : !smt.bool
|
|
}
|
|
%5 = smt.exists {
|
|
^bb0(%arg2: !smt.int, %arg3: !smt.int):
|
|
%6 = smt.eq %arg2, %arg3 : !smt.int
|
|
smt.yield %6 : !smt.bool
|
|
}
|
|
%6 = smt.and %3, %5
|
|
smt.assert %6
|
|
|
|
// CHECK: (check-sat)
|
|
// CHECK-INLINED: (check-sat)
|
|
smt.check sat {} unknown {} unsat {}
|
|
|
|
// CHECK: (reset)
|
|
// CHECK-INLINED: (reset)
|
|
smt.reset
|
|
|
|
// CHECK: (push 1)
|
|
// CHECK-INLINED: (push 1)
|
|
smt.push 1
|
|
|
|
// CHECK: (pop 1)
|
|
// 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)
|
|
}
|