tests for smt2_solver
This commit is contained in:
parent
246472fb45
commit
ab688488e3
|
@ -11,6 +11,7 @@ DIRS = cbmc \
|
|||
strings-smoke-tests \
|
||||
cbmc-cover \
|
||||
goto-instrument-typedef \
|
||||
smt2_solver \
|
||||
strings \
|
||||
invariants \
|
||||
goto-diff \
|
||||
|
|
|
@ -0,0 +1,18 @@
|
|||
default: tests.log
|
||||
|
||||
test:
|
||||
@../test.pl -p -c ../../../src/solvers/smt2_solver
|
||||
|
||||
tests.log: ../test.pl
|
||||
@../test.pl -p -c ../../../src/solvers/smt2_solver
|
||||
|
||||
show:
|
||||
@for dir in *; do \
|
||||
if [ -d "$$dir" ]; then \
|
||||
vim -o "$$dir/*.c" "$$dir/*.out"; \
|
||||
fi; \
|
||||
done;
|
||||
|
||||
clean:
|
||||
find -name '*.out' -execdir $(RM) '{}' \;
|
||||
$(RM) tests.log
|
|
@ -0,0 +1,64 @@
|
|||
(set-logic QF_BV)
|
||||
|
||||
; From https://rise4fun.com/z3/tutorialcontent/guide
|
||||
|
||||
; Basic Bitvector Arithmetic
|
||||
(define-fun b01 () Bool (= (bvadd #x07 #x03) #x0a)) ; addition
|
||||
(define-fun b02 () Bool (= (bvsub #x07 #x03) #x04)) ; subtraction
|
||||
(define-fun b03 () Bool (= (bvneg #x07) #xf9)) ; unary minus
|
||||
(define-fun b04 () Bool (= (bvmul #x07 #x03) #x15)) ; multiplication
|
||||
(define-fun b05 () Bool (= (bvurem #x07 #x03) #x01)) ; unsigned remainder
|
||||
(define-fun b06 () Bool (= (bvsrem #x07 #x03) #x01)) ; signed remainder
|
||||
(define-fun b07 () Bool (= (bvsmod #x07 #x03) #x01)) ; signed modulo
|
||||
(define-fun b08 () Bool (= (bvshl #x07 #x03) #x38)) ; shift left
|
||||
(define-fun b09 () Bool (= (bvlshr #xf0 #x03) #x1e)) ; unsigned (logical) shift right
|
||||
(define-fun b10 () Bool (= (bvashr #xf0 #x03) #xfe)) ; signed (arithmetical) shift right#x0a
|
||||
|
||||
; Bitwise Operations
|
||||
|
||||
(define-fun w1 () Bool (= (bvor #x6 #x3) #x7)) ; bitwise or
|
||||
(define-fun w2 () Bool (= (bvand #x6 #x3) #x2)) ; bitwise and
|
||||
(define-fun w3 () Bool (= (bvnot #x6) #x9)) ; bitwise not
|
||||
(define-fun w4 () Bool (= (bvnand #x6 #x3) #xd)) ; bitwise nand
|
||||
(define-fun w5 () Bool (= (bvnor #x6 #x3) #x8)) ; bitwise nor
|
||||
(define-fun w6 () Bool (= (bvxnor #x6 #x3) #xa)) ; bitwise xnor
|
||||
|
||||
; We can prove a bitwise version of deMorgan's law
|
||||
|
||||
(declare-const x (_ BitVec 64))
|
||||
(declare-const y (_ BitVec 64))
|
||||
(define-fun d01 () Bool (= (bvand (bvnot x) (bvnot y)) (bvnot (bvor x y))))
|
||||
|
||||
; There is a fast way to check that fixed size numbers are powers of two
|
||||
|
||||
(define-fun is-power-of-two ((x (_ BitVec 4))) Bool
|
||||
(= #x0 (bvand x (bvsub x #x1))))
|
||||
(declare-const a (_ BitVec 4))
|
||||
(define-fun power-test () Bool
|
||||
(= (is-power-of-two a)
|
||||
(or (= a #x0)
|
||||
(= a #x1)
|
||||
(= a #x2)
|
||||
(= a #x4)
|
||||
(= a #x8))))
|
||||
|
||||
; Predicates over Bitvectors
|
||||
|
||||
(define-fun p1 () Bool (= (bvule #x0a #xf0) true)) ; unsigned less or equal
|
||||
(define-fun p2 () Bool (= (bvult #x0a #xf0) true)) ; unsigned less than
|
||||
(define-fun p3 () Bool (= (bvuge #x0a #xf0) false)) ; unsigned greater or equal
|
||||
(define-fun p4 () Bool (= (bvugt #x0a #xf0) false)) ; unsigned greater than
|
||||
(define-fun p5 () Bool (= (bvsle #x0a #xf0) false)) ; signed less or equal
|
||||
(define-fun p6 () Bool (= (bvslt #x0a #xf0) false)) ; signed less than
|
||||
(define-fun p7 () Bool (= (bvsge #x0a #xf0) true)) ; signed greater or equal
|
||||
(define-fun p8 () Bool (= (bvsgt #x0a #xf0) true)) ; signed greater than
|
||||
|
||||
; all must be true
|
||||
|
||||
(assert (not (and
|
||||
b01 b02 b03 b04 b05 b06 b07 b08 b09 b10
|
||||
d01
|
||||
power-test
|
||||
p1 p2 p3 p4 p5 p6 p7 p8)))
|
||||
|
||||
(check-sat)
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
basic-bv1.smt2
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^unsat$
|
||||
--
|
|
@ -0,0 +1,32 @@
|
|||
(set-logic QF_BV)
|
||||
|
||||
; try 'let' on bitvectors
|
||||
|
||||
(define-fun x () (_ BitVec 4) #x0)
|
||||
|
||||
; very simple
|
||||
(define-fun let0 () Bool (= (let ((x #x0)) #x1) #x1))
|
||||
|
||||
; let hides the function 'x'
|
||||
(define-fun let1 () Bool (= (let ((x #x1)) x) #x1))
|
||||
|
||||
; the binding isn't visible immediately
|
||||
(define-fun let2 () Bool (= (let ((x x)) x) #x0))
|
||||
|
||||
; parallel let
|
||||
(define-fun let3 () Bool (= (let ((x #x1) (y x)) y) #x0))
|
||||
|
||||
; limited scope
|
||||
(define-fun let4 () Bool (and (= (let ((x #x1)) x) #x1) (= x #x0)))
|
||||
|
||||
; all must be true
|
||||
|
||||
(assert (not (and
|
||||
let0
|
||||
let1
|
||||
let2
|
||||
let3
|
||||
let4
|
||||
)))
|
||||
|
||||
(check-sat)
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
let-with-bv1.smt2
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^unsat$
|
||||
--
|
|
@ -0,0 +1,30 @@
|
|||
(set-logic QF_BV)
|
||||
|
||||
(define-fun x () Bool false)
|
||||
|
||||
; very simple
|
||||
(define-fun let0 () Bool (let ((x false)) true))
|
||||
|
||||
; let hides the function 'x'
|
||||
(define-fun let1 () Bool (let ((x true)) x))
|
||||
|
||||
; the binding isn't visible immediately
|
||||
(define-fun let2 () Bool (not (let ((x x)) x)))
|
||||
|
||||
; parallel let
|
||||
(define-fun let3 () Bool (let ((x true) (y x)) (not y)))
|
||||
|
||||
; limited scope
|
||||
(define-fun let4 () Bool (and (let ((x true)) x) (not x)))
|
||||
|
||||
; all must be true
|
||||
|
||||
(assert (not (and
|
||||
let0
|
||||
let1
|
||||
let2
|
||||
let3
|
||||
let4
|
||||
)))
|
||||
|
||||
(check-sat)
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
let1.smt2
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^unsat$
|
||||
--
|
Loading…
Reference in New Issue