Skip to content

Commit c0ee019

Browse files
AnneKoziolekAnneKoziolek
committed
added Z3ConstraintSolver from Z3 branch
1 parent 19cb9ce commit c0ee019

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

43 files changed

+788
-173
lines changed

‎knarr-runtime/cp.txt‎

Lines changed: 1 addition & 1 deletion
Large diffs are not rendered by default.

‎knarr-runtime/execution_paths_automatic.json‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
"CreateAscetTaskRoutine:execute:userChoice_forTask_specialname==0"
1010
],
1111
"numConstraints": 2,
12-
"executionTimeMs": 23810
12+
"executionTimeMs": 21595
1313
},
1414
{
1515
"pathId": 2,
@@ -20,7 +20,7 @@
2020
"CreateAscetTaskRoutine:execute:userChoice_forTask_specialname==1"
2121
],
2222
"numConstraints": 1,
23-
"executionTimeMs": 144
23+
"executionTimeMs": 172
2424
},
2525
{
2626
"pathId": 3,
@@ -31,7 +31,7 @@
3131
"CreateAscetTaskRoutine:execute:userChoice_forTask_specialname==2"
3232
],
3333
"numConstraints": 1,
34-
"executionTimeMs": 162
34+
"executionTimeMs": 133
3535
},
3636
{
3737
"pathId": 4,
@@ -42,7 +42,7 @@
4242
"CreateAscetTaskRoutine:execute:userChoice_forTask_specialname==3"
4343
],
4444
"numConstraints": 1,
45-
"executionTimeMs": 165
45+
"executionTimeMs": 159
4646
},
4747
{
4848
"pathId": 5,
@@ -53,6 +53,6 @@
5353
"CreateAscetTaskRoutine:execute:userChoice_forTask_specialname==4"
5454
],
5555
"numConstraints": 1,
56-
"executionTimeMs": 87
56+
"executionTimeMs": 63
5757
}
5858
]

‎knarr-runtime/execution_paths_multivar.json‎

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -8,175 +8,175 @@
88
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 0, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 0},
99
"constraints": ["(0<=CreateAscetTaskRoutine:execute:userChoice_forTask_task1)&&(CreateAscetTaskRoutine:execute:userChoice_forTask_task1<5)", "CreateAscetTaskRoutine:execute:userChoice_forTask_task1==0", "(0<=CreateAscetTaskRoutine:execute:userChoice_forTask_task2)&&(CreateAscetTaskRoutine:execute:userChoice_forTask_task2<5)", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==0"],
1010
"num_constraints": 4,
11-
"execution_time_ms": 51206
11+
"execution_time_ms": 22352
1212
},
1313
{
1414
"path_id": 1,
1515
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 1, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 0},
1616
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==0", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==1"],
1717
"num_constraints": 2,
18-
"execution_time_ms": 326
18+
"execution_time_ms": 193
1919
},
2020
{
2121
"path_id": 2,
2222
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 2, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 0},
2323
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==0", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==2"],
2424
"num_constraints": 2,
25-
"execution_time_ms": 234
25+
"execution_time_ms": 238
2626
},
2727
{
2828
"path_id": 3,
2929
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 3, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 0},
3030
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==0", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==3"],
3131
"num_constraints": 2,
32-
"execution_time_ms": 229
32+
"execution_time_ms": 181
3333
},
3434
{
3535
"path_id": 4,
3636
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 4, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 0},
3737
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==0", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==4"],
3838
"num_constraints": 2,
39-
"execution_time_ms": 183
39+
"execution_time_ms": 106
4040
},
4141
{
4242
"path_id": 5,
4343
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 0, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 1},
4444
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==1", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==0"],
4545
"num_constraints": 2,
46-
"execution_time_ms": 188
46+
"execution_time_ms": 127
4747
},
4848
{
4949
"path_id": 6,
5050
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 1, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 1},
5151
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==1", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==1"],
5252
"num_constraints": 2,
53-
"execution_time_ms": 139
53+
"execution_time_ms": 138
5454
},
5555
{
5656
"path_id": 7,
5757
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 2, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 1},
5858
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==1", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==2"],
5959
"num_constraints": 2,
60-
"execution_time_ms": 195
60+
"execution_time_ms": 155
6161
},
6262
{
6363
"path_id": 8,
6464
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 3, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 1},
6565
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==1", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==3"],
6666
"num_constraints": 2,
67-
"execution_time_ms": 113
67+
"execution_time_ms": 111
6868
},
6969
{
7070
"path_id": 9,
7171
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 4, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 1},
7272
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==1", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==4"],
7373
"num_constraints": 2,
74-
"execution_time_ms": 111
74+
"execution_time_ms": 112
7575
},
7676
{
7777
"path_id": 10,
7878
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 0, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 2},
7979
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==2", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==0"],
8080
"num_constraints": 2,
81-
"execution_time_ms": 136
81+
"execution_time_ms": 156
8282
},
8383
{
8484
"path_id": 11,
8585
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 1, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 2},
8686
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==2", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==1"],
8787
"num_constraints": 2,
88-
"execution_time_ms": 104
88+
"execution_time_ms": 122
8989
},
9090
{
9191
"path_id": 12,
9292
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 2, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 2},
9393
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==2", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==2"],
9494
"num_constraints": 2,
95-
"execution_time_ms": 111
95+
"execution_time_ms": 179
9696
},
9797
{
9898
"path_id": 13,
9999
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 3, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 2},
100100
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==2", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==3"],
101101
"num_constraints": 2,
102-
"execution_time_ms": 104
102+
"execution_time_ms": 114
103103
},
104104
{
105105
"path_id": 14,
106106
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 4, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 2},
107107
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==2", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==4"],
108108
"num_constraints": 2,
109-
"execution_time_ms": 139
109+
"execution_time_ms": 125
110110
},
111111
{
112112
"path_id": 15,
113113
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 0, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 3},
114114
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==3", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==0"],
115115
"num_constraints": 2,
116-
"execution_time_ms": 132
116+
"execution_time_ms": 134
117117
},
118118
{
119119
"path_id": 16,
120120
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 1, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 3},
121121
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==3", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==1"],
122122
"num_constraints": 2,
123-
"execution_time_ms": 105
123+
"execution_time_ms": 103
124124
},
125125
{
126126
"path_id": 17,
127127
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 2, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 3},
128128
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==3", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==2"],
129129
"num_constraints": 2,
130-
"execution_time_ms": 121
130+
"execution_time_ms": 126
131131
},
132132
{
133133
"path_id": 18,
134134
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 3, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 3},
135135
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==3", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==3"],
136136
"num_constraints": 2,
137-
"execution_time_ms": 185
137+
"execution_time_ms": 159
138138
},
139139
{
140140
"path_id": 19,
141141
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 4, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 3},
142142
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==3", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==4"],
143143
"num_constraints": 2,
144-
"execution_time_ms": 103
144+
"execution_time_ms": 95
145145
},
146146
{
147147
"path_id": 20,
148148
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 0, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 4},
149149
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==4", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==0"],
150150
"num_constraints": 2,
151-
"execution_time_ms": 100
151+
"execution_time_ms": 87
152152
},
153153
{
154154
"path_id": 21,
155155
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 1, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 4},
156156
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==4", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==1"],
157157
"num_constraints": 2,
158-
"execution_time_ms": 162
158+
"execution_time_ms": 120
159159
},
160160
{
161161
"path_id": 22,
162162
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 2, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 4},
163163
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==4", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==2"],
164164
"num_constraints": 2,
165-
"execution_time_ms": 113
165+
"execution_time_ms": 97
166166
},
167167
{
168168
"path_id": 23,
169169
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 3, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 4},
170170
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==4", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==3"],
171171
"num_constraints": 2,
172-
"execution_time_ms": 125
172+
"execution_time_ms": 107
173173
},
174174
{
175175
"path_id": 24,
176176
"inputs": {"CreateAscetTaskRoutine:execute:userChoice_forTask_task2": 4, "CreateAscetTaskRoutine:execute:userChoice_forTask_task1": 4},
177177
"constraints": ["CreateAscetTaskRoutine:execute:userChoice_forTask_task1==4", "CreateAscetTaskRoutine:execute:userChoice_forTask_task2==4"],
178178
"num_constraints": 2,
179-
"execution_time_ms": 127
179+
"execution_time_ms": 86
180180
}
181181
]
182182
}

‎knarr-runtime/galette-output-automatic-0/example.model2‎

Lines changed: 0 additions & 4 deletions
This file was deleted.

‎knarr-runtime/galette-output-automatic-0/galette-test-output/vsum-output.xmi‎

Lines changed: 0 additions & 9 deletions
This file was deleted.

‎knarr-runtime/galette-output-automatic-0/vsum/correspondences.correspondence‎

Lines changed: 0 additions & 11 deletions
This file was deleted.

‎knarr-runtime/galette-output-automatic-0/vsum/models.models‎

Lines changed: 0 additions & 2 deletions
This file was deleted.

‎knarr-runtime/galette-output-automatic-0/vsum/uuid.uuid‎

Lines changed: 0 additions & 4 deletions
This file was deleted.

‎knarr-runtime/galette-output-automatic-1/example.model‎

Lines changed: 0 additions & 4 deletions
This file was deleted.

‎knarr-runtime/galette-output-automatic-1/example.model2‎

Lines changed: 0 additions & 4 deletions
This file was deleted.

0 commit comments

Comments
 (0)