blob: 0c51e39af4f9a9b517ff56fae2a2701f44cd384c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
; COMMAND-LINE: --fmf-fun --no-check-models
; EXPECT: sat
(set-logic UFDTLIA)
(set-info :smt-lib-version 2.5)
(define-funs-rec
(
(validIdValue ((x Int)(v Int)) Bool)
)
(
(or
(and (= x 0) (< (- 10) v 10) )
(and (= x 1) (<= (- 100) v (- 10)) )
(and (= x 2) (<= 10 v 100) )
(and (= x 3) (< (- 1000) v (- 100)) )
(and (= x 4) (< 100 v 1000) )
(and (= x 5) (<= (- 1000) v) )
(and (= x 6) (<= v 1000) )
(validIdValue (- x 7) v)
)
)
)
(declare-datatypes (T) ( (List (Nil) (Cstr (head T) (tail List) ) ) ) )
(declare-datatypes (T S) ( (Pair (Pair (first T) (second S)) ) ) )
(define-funs-rec
(
(validList ((l (List (Pair Int Int)))) Bool)
)
(
(ite (= l (as Nil (List (Pair Int Int))) )
true
(let ((hd (head l))) (and (>= (first hd) 0)
(validIdValue (first hd) (second hd))
(validList (tail l))
)
)
)
)
)
(declare-const myList (List (Pair Int Int)))
(assert (distinct myList (as Nil (List (Pair Int Int)))))
(assert (validList myList))
(check-sat)
|
