C# でパラメタライズド テストを自動生成するための基礎 - The road to Pex/Code Digger/IntelliTest -：03. SMT-LIB 標準形式

661425685-03.lisp

(push)
(echo "#1. v == null -----------------------------------------------")
(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
(declare-const v SystemInt32Array)
(assert (= v null))
(check-sat)
(get-model)
(pop)

(push)
(echo "#2. !(v == null) && !(v.Length > 0) -------------------------")
(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
(declare-const v SystemInt32Array)
(assert (not (= v null)))
(assert (not (> (seq.len (value v)) 0)))
(check-sat)
(get-model)
(pop)

(push)
(echo "#3. !(v == null) && v.Length > 0 && v[0] == 1234567890 ------")
(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
(declare-const v SystemInt32Array)
(assert (not (= v null)))
(assert (> (seq.len (value v)) 0))
(assert (= (seq.at (value v) 0) (seq.unit 1234567890)))
(check-sat)
(get-model)
(pop)

(push)
(echo "#4. !(v == null) && v.Length > 0 && !(v[0] == 1234567890) ---")
(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
(declare-const v SystemInt32Array)
(assert (not (= v null)))
(assert (> (seq.len (value v)) 0))
(assert (not (= (seq.at (value v) 0) (seq.unit 1234567890))))
(check-sat)
(get-model)
(pop)

; #1. v == null -----------------------------------------------
; sat
; (model 
;   (define-fun v () SystemInt32Array
;     null)
; )
; #2. !(v == null) && !(v.Length > 0) -------------------------
; sat
; (model 
;   (define-fun v () SystemInt32Array
;     (SystemInt32Array 1 (as seq.empty (Seq Int))))
; )
; #3. !(v == null) && v.Length > 0 && v[0] == 1234567890 ------
; sat
; (model 
;   (define-fun v () SystemInt32Array
;     (SystemInt32Array 4 (seq.unit 1234567890)))
; )
; #4. !(v == null) && v.Length > 0 && !(v[0] == 1234567890) ---
; sat
; (model 
;   (define-fun v () SystemInt32Array
;     (SystemInt32Array 3 (seq.unit 5)))
; )