-
Notifications
You must be signed in to change notification settings - Fork 4
/
test.smt2
71 lines (71 loc) · 3.28 KB
/
test.smt2
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
(set-option :auto_config false)
(set-option :smt.phase_selection 5)
(set-option :smt.random-seed 73207424)
(declare-fun SL_0_1_2_3 () Int)
(declare-fun t32_tuesday_1000 () Int)
(declare-fun t33_tuesday_1030 () Int)
(declare-fun t34_tuesday_1100 () Int)
(declare-fun t35_tuesday_1130 () Int)
(declare-fun t40_tuesday_1400 () Int)
(declare-fun t41_tuesday_1430 () Int)
(declare-fun t42_tuesday_1500 () Int)
(declare-fun t43_tuesday_1530 () Int)
(declare-fun t36_tuesday_1200 () Int)
(declare-fun t37_tuesday_1230 () Int)
(declare-fun t38_tuesday_1300 () Int)
(declare-fun t39_tuesday_1330 () Int)
(declare-fun t16_monday_1600 () Int)
(declare-fun t17_monday_1630 () Int)
(declare-fun t18_monday_1700 () Int)
(declare-fun t19_monday_1730 () Int)
(declare-fun SL_1024 () Int)
(declare-fun t12_monday_1400 () Int)
(declare-fun t13_monday_1430 () Int)
(declare-fun t14_monday_1500 () Int)
(declare-fun t15_monday_1530 () Int)
(assert (or (= SL_0_1_2_3 0) (= SL_0_1_2_3 1) (= SL_0_1_2_3 2) (= SL_0_1_2_3 3)))
(assert (= (= SL_0_1_2_3 0) (= t32_tuesday_1000 0)))
(assert (= (= SL_0_1_2_3 0) (= t33_tuesday_1030 0)))
(assert (= (= SL_0_1_2_3 0) (= t34_tuesday_1100 0)))
(assert (= (= SL_0_1_2_3 0) (= t35_tuesday_1130 0)))
(assert (= (= SL_0_1_2_3 1) (= t40_tuesday_1400 1)))
(assert (= (= SL_0_1_2_3 1) (= t41_tuesday_1430 1)))
(assert (= (= SL_0_1_2_3 1) (= t42_tuesday_1500 1)))
(assert (= (= SL_0_1_2_3 1) (= t43_tuesday_1530 1)))
(assert (= (= SL_0_1_2_3 2) (= t36_tuesday_1200 2)))
(assert (= (= SL_0_1_2_3 2) (= t37_tuesday_1230 2)))
(assert (= (= SL_0_1_2_3 2) (= t38_tuesday_1300 2)))
(assert (= (= SL_0_1_2_3 2) (= t39_tuesday_1330 2)))
(assert (= (= SL_0_1_2_3 3) (= t16_monday_1600 3)))
(assert (= (= SL_0_1_2_3 3) (= t17_monday_1630 3)))
(assert (= (= SL_0_1_2_3 3) (= t18_monday_1700 3)))
(assert (= (= SL_0_1_2_3 3) (= t19_monday_1730 3)))
(assert (= SL_1024 1024))
(assert (= (= SL_1024 1024) (= t12_monday_1400 1024)))
(assert (= (= SL_1024 1024) (= t13_monday_1430 1024)))
(assert (= (= SL_1024 1024) (= t14_monday_1500 1024)))
(assert (= (= SL_1024 1024) (= t15_monday_1530 1024)))
(assert (or (= t32_tuesday_1000 0) (= t32_tuesday_1000 -1)))
(assert (or (= t33_tuesday_1030 0) (= t33_tuesday_1030 -1)))
(assert (or (= t34_tuesday_1100 0) (= t34_tuesday_1100 -1)))
(assert (or (= t35_tuesday_1130 0) (= t35_tuesday_1130 -1)))
(assert (or (= t40_tuesday_1400 1) (= t40_tuesday_1400 -1)))
(assert (or (= t41_tuesday_1430 1) (= t41_tuesday_1430 -1)))
(assert (or (= t42_tuesday_1500 1) (= t42_tuesday_1500 -1)))
(assert (or (= t43_tuesday_1530 1) (= t43_tuesday_1530 -1)))
(assert (or (= t36_tuesday_1200 2) (= t36_tuesday_1200 -1)))
(assert (or (= t37_tuesday_1230 2) (= t37_tuesday_1230 -1)))
(assert (or (= t38_tuesday_1300 2) (= t38_tuesday_1300 -1)))
(assert (or (= t39_tuesday_1330 2) (= t39_tuesday_1330 -1)))
(assert (or (= t16_monday_1600 3) (= t16_monday_1600 -1)))
(assert (or (= t17_monday_1630 3) (= t17_monday_1630 -1)))
(assert (or (= t18_monday_1700 3) (= t18_monday_1700 -1)))
(assert (or (= t19_monday_1730 3) (= t19_monday_1730 -1)))
(assert (or (= t12_monday_1400 1024) (= t12_monday_1400 -1)))
(assert (or (= t13_monday_1430 1024) (= t13_monday_1430 -1)))
(assert (or (= t14_monday_1500 1024) (= t14_monday_1500 -1)))
(assert (or (= t15_monday_1530 1024) (= t15_monday_1530 -1)))
(check-sat)
(get-model)
(get-objectives)
(exit)