blob: 72ec634a8db4c77d6c038340cab5eaac41953641 (
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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
; COMMAND-LINE: -mi
; EXPECT: sat
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
; must make parts 1 through 6 with different deadlines
; part 1 must be available for part 2
; parts 3 and 4 must be available for part 5
; all parts must be available for part 6
; start/complete is the timestep when a part is started/finished
(declare-fun start (Int) Int)
(declare-fun complete (Int) Int)
(define-fun before ((i Int) (j Int)) Bool (< (complete i) (start j)))
(assert (before 1 2))
(assert (before 3 5))
(assert (before 4 5))
(assert (before 1 6))
(assert (before 2 6))
(assert (before 3 6))
(assert (before 4 6))
(assert (before 5 6))
; part 1 takes 2 units of time
; part 2 takes 3
; part 3 takes 3
; part 4 takes 1
; part 5 takes 2
; part 6 takes 1
(define-fun requires ((i Int) (j Int)) Bool (= (complete i) (+ (start i) j)))
(assert (requires 1 2))
(assert (requires 2 3))
(assert (requires 3 3))
(assert (requires 4 1))
(assert (requires 5 2))
(assert (requires 6 1))
(assert (>= (start 1) 0))
(assert (>= (start 2) 0))
(assert (>= (start 3) 0))
(assert (>= (start 4) 0))
(assert (>= (start 5) 0))
(assert (>= (start 6) 0))
(define-fun cost () Int (complete 6))
(define-fun parallel ((t Int)) Int
(+ (ite (<= (start 1) t (complete 1)) 1 0)
(ite (<= (start 2) t (complete 2)) 1 0)
(ite (<= (start 3) t (complete 3)) 1 0)
(ite (<= (start 4) t (complete 4)) 1 0)
(ite (<= (start 5) t (complete 5)) 1 0)
(ite (<= (start 6) t (complete 6)) 1 0)))
(declare-fun cost2 () Int)
(assert (= cost2 cost))
(declare-fun max-parallel () Int)
(assert (forall ((t Int)) (=> (<= 0 t cost2) (>= max-parallel (parallel t)))))
(check-sat)
;(get-model)
;(get-value (cost2))
;(get-value ((parallel 1)))
;(get-value ((=> (<= 0 1 cost2) (>= max-parallel (parallel 1)))))
(assert (< cost 8))
(check-sat)
|
