Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
C
Conversion
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Vladislav Kiselev
Conversion
Commits
fed0aba4
Commit
fed0aba4
authored
Aug 04, 2019
by
Vladislav Kiselev
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Решатель вынесен в отдельный класс, добавлена возможность подключения flatZinc-солверов.
parent
8aed7ccb
Changes
3
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
325 additions
and
248 deletions
+325
-248
src/inport/ConversionUtils/MZnResultsResolver.java
src/inport/ConversionUtils/MZnResultsResolver.java
+95
-54
src/inport/ConversionUtils/Solver.java
src/inport/ConversionUtils/Solver.java
+200
-0
src/inport/Testing.java
src/inport/Testing.java
+30
-194
No files found.
src/inport/ConversionUtils/MZnResultsResolver.java
View file @
fed0aba4
...
@@ -6,6 +6,86 @@ import java.io.*;
...
@@ -6,6 +6,86 @@ import java.io.*;
import
java.util.*
;
import
java.util.*
;
public
class
MZnResultsResolver
{
public
class
MZnResultsResolver
{
private
static
int
resolveDimension
(
String
str
)
{
str
=
str
.
trim
();
if
(
str
.
equals
(
"{}"
))
{
return
0
;
}
int
pos
=
str
.
indexOf
(
".."
);
int
lim1
=
Integer
.
parseInt
(
str
.
substring
(
0
,
pos
));
int
lim2
=
Integer
.
parseInt
(
str
.
substring
(
pos
+
2
,
str
.
length
()));
return
lim2
-
lim1
+
1
;
}
private
static
void
parseArray
(
Map
<
String
,
ArrayList
<
ArrayList
<
String
>>>
arrays
,
int
pos
,
String
line
,
TaskCase
taskCase
,
String
name
)
{
int
index
=
line
.
indexOf
(
"array"
,
pos
);
if
(
index
>=
pos
)
{
// Из flatzinc-а.
if
(
line
.
charAt
(
index
+
"array"
.
length
())
==
'2'
)
{
String
[]
values
=
line
.
substring
(
line
.
indexOf
(
'['
)
+
1
,
line
.
indexOf
(
']'
)).
split
(
","
);
String
[]
items
=
line
.
substring
(
line
.
indexOf
(
'('
,
pos
)
+
1
,
line
.
indexOf
(
'['
)).
split
(
","
);
int
dim1
=
resolveDimension
(
items
[
0
]);
int
dim2
=
resolveDimension
(
items
[
1
]);
ArrayList
<
ArrayList
<
String
>>
res
=
new
ArrayList
<>();
for
(
int
i
=
0
;
i
<
dim1
;
i
++)
{
res
.
add
(
new
ArrayList
<>());
for
(
int
j
=
0
;
j
<
dim2
;
j
++)
{
res
.
get
(
i
).
add
(
values
[
i
*
dim2
+
j
].
trim
());
}
}
arrays
.
put
(
name
,
res
);
}
}
else
{
// Из minizinc-а
while
((
pos
<
line
.
length
())
&&
(
line
.
charAt
(
pos
)
!=
'['
)
&&
(
line
.
charAt
(
pos
)
!=
'{'
))
{
pos
++;
}
int
arrayFirstDim
=
((
int
)
taskCase
.
getPlanningInterval
())
+
2
;
if
(
line
.
charAt
(
pos
)
==
'{'
)
{
pos
++;
int
nextPos
=
pos
;
while
(
line
.
charAt
(
nextPos
)
!=
'}'
)
{
nextPos
++;
}
String
[]
dimensions
=
line
.
substring
(
pos
,
nextPos
).
trim
().
split
(
" "
);
if
(
dimensions
.
length
>
0
)
{
arrayFirstDim
=
Integer
.
valueOf
(
dimensions
[
0
].
trim
());
}
pos
=
nextPos
+
1
;
while
(
line
.
charAt
(
pos
)
!=
'['
)
{
pos
++;
}
}
int
pos2
=
pos
;
while
((
pos2
<
line
.
length
())
&&
(
line
.
charAt
(
pos2
)
!=
']'
))
{
pos2
++;
}
String
values
=
line
.
substring
(
pos
+
1
,
pos2
);
ArrayList
<
String
>
elements
=
new
ArrayList
<>();
for
(
String
val
:
values
.
split
(
","
))
{
elements
.
add
(
val
.
trim
());
}
if
((
arrayFirstDim
!=
0
)
&&
(
elements
.
size
()
%
arrayFirstDim
==
0
))
{
ArrayList
<
ArrayList
<
String
>>
res
=
new
ArrayList
<>();
for
(
int
i
=
0
;
i
<
elements
.
size
();
i
+=
arrayFirstDim
)
{
ArrayList
<
String
>
subRes
=
new
ArrayList
<>();
for
(
int
j
=
0
;
j
<
arrayFirstDim
;
j
++)
{
subRes
.
add
(
elements
.
get
(
i
+
j
));
}
res
.
add
(
subRes
);
}
arrays
.
put
(
name
,
res
);
}
}
}
public
static
void
resolveMiniZincResults
(
TaskCase
taskCase
,
String
fileName
)
{
public
static
void
resolveMiniZincResults
(
TaskCase
taskCase
,
String
fileName
)
{
ArrayList
<
Operation
>
operations
=
null
;
ArrayList
<
Operation
>
operations
=
null
;
Integer
result
=
null
;
Integer
result
=
null
;
...
@@ -36,66 +116,14 @@ public class MZnResultsResolver {
...
@@ -36,66 +116,14 @@ public class MZnResultsResolver {
break
;
break
;
}
}
if
(
name
.
matches
(
"\\d+"
))
{
if
(
name
.
matches
(
"\\d+"
))
{
if
(
result
!=
null
)
{
continue
;
}
result
=
Integer
.
parseInt
(
name
);
continue
;
continue
;
}
}
parseArray
(
arrays
,
pos
,
line
,
taskCase
,
name
);
while
((
pos
<
line
.
length
())
&&
(
line
.
charAt
(
pos
)
!=
'['
)
&&
(
line
.
charAt
(
pos
)
!=
'{'
))
{
pos
++;
}
int
arrayFirstDim
=
((
int
)
taskCase
.
getPlanningInterval
())
+
2
;
if
(
line
.
charAt
(
pos
)
==
'{'
)
{
pos
++;
int
nextPos
=
pos
;
while
(
line
.
charAt
(
nextPos
)
!=
'}'
)
{
nextPos
++;
}
String
[]
dimensions
=
line
.
substring
(
pos
,
nextPos
).
trim
().
split
(
" "
);
if
(
dimensions
.
length
>
0
)
{
arrayFirstDim
=
Integer
.
valueOf
(
dimensions
[
0
].
trim
());
}
pos
=
nextPos
+
1
;
while
(
line
.
charAt
(
pos
)
!=
'['
)
{
pos
++;
}
}
int
pos2
=
pos
;
while
((
pos2
<
line
.
length
())
&&
(
line
.
charAt
(
pos2
)
!=
']'
))
{
pos2
++;
}
String
values
=
line
.
substring
(
pos
+
1
,
pos2
);
ArrayList
<
String
>
elements
=
new
ArrayList
<>();
for
(
String
val
:
values
.
split
(
","
))
{
elements
.
add
(
val
.
trim
());
}
if
((
arrayFirstDim
!=
0
)
&&
(
elements
.
size
()
%
arrayFirstDim
==
0
))
{
ArrayList
<
ArrayList
<
String
>>
res
=
new
ArrayList
<>();
for
(
int
i
=
0
;
i
<
elements
.
size
();
i
+=
arrayFirstDim
)
{
ArrayList
<
String
>
subRes
=
new
ArrayList
<>();
for
(
int
j
=
0
;
j
<
arrayFirstDim
;
j
++)
{
subRes
.
add
(
elements
.
get
(
i
+
j
));
}
res
.
add
(
subRes
);
}
arrays
.
put
(
name
,
res
);
}
}
if
(
result
==
null
)
{
throw
new
ParserException
(
"No result in input"
);
}
}
for
(
String
keyArray
:
Arrays
.
asList
(
"op_status"
,
"participation_as_resource"
))
{
for
(
String
keyArray
:
Arrays
.
asList
(
"op_status"
,
"participation_as_resource"
))
{
if
(!
arrays
.
containsKey
(
keyArray
))
{
if
(!
arrays
.
containsKey
(
keyArray
))
{
if
(
result
==
-
1
)
{
if
(
(
result
!=
null
)
&&
(
result
==
-
1
)
)
{
operations
=
new
ArrayList
<>();
operations
=
new
ArrayList
<>();
}
else
{
}
else
{
throw
new
ParserException
(
"No \""
+
keyArray
+
"\" in input"
);
throw
new
ParserException
(
"No \""
+
keyArray
+
"\" in input"
);
...
@@ -103,6 +131,19 @@ public class MZnResultsResolver {
...
@@ -103,6 +131,19 @@ public class MZnResultsResolver {
}
}
}
}
if
(
result
==
null
)
{
ArrayList
<
ArrayList
<
String
>>
opStatus
=
arrays
.
get
(
"op_status"
);
result
=
0
;
for
(
ArrayList
<
String
>
a
:
opStatus
)
{
for
(
int
i
=
0
;
i
<
a
.
size
();
i
++)
{
if
(
a
.
get
(
i
).
trim
().
equals
(
"true"
))
{
result
=
Math
.
max
(
result
,
i
);
}
}
}
}
if
(
result
!=
-
1
)
{
if
(
result
!=
-
1
)
{
Task
task
=
new
Task
(
taskCase
,
""
);
Task
task
=
new
Task
(
taskCase
,
""
);
...
...
src/inport/ConversionUtils/Solver.java
0 → 100644
View file @
fed0aba4
package
inport.ConversionUtils
;
import
inport.Main
;
import
inport.TaskCase
;
import
java.io.*
;
import
java.util.ArrayList
;
import
java.util.concurrent.TimeUnit
;
import
java.util.concurrent.locks.Condition
;
import
java.util.concurrent.locks.Lock
;
import
java.util.concurrent.locks.ReentrantLock
;
import
java.util.function.BiConsumer
;
import
java.util.stream.Collectors
;
public
class
Solver
{
private
final
Lock
lock
=
new
ReentrantLock
();
private
final
Condition
condition
=
lock
.
newCondition
();
private
Boolean
isDestroyed
;
private
TaskCase
task
;
private
final
String
constraintName
;
private
final
BiConsumer
<
TaskCase
,
String
>
converterToMinizincFormat
;
private
final
BiConsumer
<
TaskCase
,
String
>
interpreter
;
private
String
tempDir
=
"temp_data"
;
private
int
timeLimitS
;
private
String
flatZincSolver
=
""
;
public
void
setTask
(
TaskCase
task
)
{
this
.
task
=
task
;
}
public
void
setTempDir
(
String
tempDir
)
{
this
.
tempDir
=
tempDir
;
}
public
void
setTimeLimitS
(
int
timeLimitS
)
{
this
.
timeLimitS
=
timeLimitS
;
}
public
void
setFlatZincSolver
(
String
flatZincSolver
)
{
this
.
flatZincSolver
=
flatZincSolver
;
}
public
String
getFlatZincSolver
()
{
return
flatZincSolver
;
}
public
Solver
(
String
constraintName
,
BiConsumer
<
TaskCase
,
String
>
converterToMinizincFormat
,
BiConsumer
<
TaskCase
,
String
>
interpreter
)
{
this
.
constraintName
=
constraintName
;
this
.
converterToMinizincFormat
=
converterToMinizincFormat
;
this
.
interpreter
=
interpreter
;
}
public
String
solve
()
{
File
directory
=
new
File
(
tempDir
);
if
(!
directory
.
exists
())
{
directory
.
mkdir
();
}
tempDir
=
tempDir
+
"/"
;
String
minizincData
=
tempDir
+
"minizinc_data.dzn"
;
String
solverResults
=
tempDir
+
"solver_results.txt"
;
String
constraints
=
tempDir
+
"constraints.mzn"
;
String
flatZincConstraints
=
tempDir
+
"model.fzn"
;
try
{
try
(
FileWriter
res
=
new
FileWriter
(
constraints
))
{
BufferedReader
reader
=
new
BufferedReader
(
new
InputStreamReader
(
Main
.
class
.
getResourceAsStream
(
"/constraints/"
+
constraintName
)));
String
line
;
while
((
line
=
reader
.
readLine
())
!=
null
)
{
res
.
write
(
line
+
"\n"
);
}
}
converterToMinizincFormat
.
accept
(
task
,
minizincData
);
ProcessBuilder
pb
;
boolean
isResultsInOutput
;
if
(
flatZincSolver
.
isEmpty
())
{
pb
=
new
ProcessBuilder
(
"minizinc"
,
"--solver"
,
"Chuffed"
,
constraints
,
minizincData
,
"-o"
,
solverResults
);
isResultsInOutput
=
false
;
}
else
{
isResultsInOutput
=
true
;
{
ProcessBuilder
lPB
=
new
ProcessBuilder
(
"mzn2fzn"
,
"-o"
,
flatZincConstraints
,
constraints
,
minizincData
);
Process
process
=
lPB
.
start
();
process
.
waitFor
();
BufferedReader
br
=
new
BufferedReader
(
new
InputStreamReader
(
process
.
getInputStream
()));
String
output
=
br
.
lines
().
collect
(
Collectors
.
joining
(
"\n"
));
if
(
output
.
trim
().
equals
(
"=====UNSATISFIABLE====="
))
{
task
.
setSolution
(
new
ArrayList
<>());
task
.
setSolution_result
(-
1
);
return
""
;
}
}
pb
=
new
ProcessBuilder
(
"external_tools/or-tools_flatzinc_Ubuntu-18.04-64bit_v7.2.6977/bin/fzn-or-tools"
,
flatZincConstraints
);
}
lock
.
lock
();
isDestroyed
=
false
;
lock
.
unlock
();
final
Process
process
=
pb
.
start
();
Thread
killer
=
new
Thread
(()
->
{
lock
.
lock
();
long
start
=
System
.
currentTimeMillis
();
try
{
while
(
process
.
isAlive
())
{
long
currentTimeMillis
=
System
.
currentTimeMillis
();
if
(
currentTimeMillis
-
start
>
timeLimitS
*
1000
)
{
process
.
destroyForcibly
();
isDestroyed
=
true
;
break
;
}
condition
.
await
(
timeLimitS
*
1000
-
(
currentTimeMillis
-
start
),
TimeUnit
.
MILLISECONDS
);
}
}
catch
(
InterruptedException
ex
)
{
isDestroyed
=
true
;
process
.
destroyForcibly
();
}
finally
{
lock
.
unlock
();
}
});
killer
.
start
();
int
exitCode
=
process
.
waitFor
();
lock
.
lock
();
try
{
condition
.
signal
();
}
finally
{
lock
.
unlock
();
}
killer
.
join
();
assert
exitCode
==
0
;
lock
.
lock
();
try
{
if
(
isDestroyed
)
{
return
"Time limit exceeded."
;
}
}
finally
{
lock
.
unlock
();
}
if
(
isResultsInOutput
)
{
try
(
FileWriter
res
=
new
FileWriter
(
solverResults
))
{
BufferedReader
br
=
new
BufferedReader
(
new
InputStreamReader
(
process
.
getInputStream
()));
res
.
write
(
br
.
lines
().
collect
(
Collectors
.
joining
(
"\n"
)));
}
interpreter
.
accept
(
task
,
solverResults
);
}
else
{
BufferedReader
br
=
new
BufferedReader
(
new
InputStreamReader
(
process
.
getInputStream
()));
String
output
=
br
.
lines
().
collect
(
Collectors
.
joining
(
"\n"
));
// BufferedReader br2 = new BufferedReader(new InputStreamReader(process.getErrorStream()));
// String errors = br.lines().collect(Collectors.joining("\n"));
// System.out.println("output : " + output);
// System.out.println("errors : " + errors);
if
(
output
.
trim
().
equals
(
"=====UNSATISFIABLE====="
))
{
task
.
setSolution
(
new
ArrayList
<>());
task
.
setSolution_result
(-
1
);
}
else
{
interpreter
.
accept
(
task
,
solverResults
);
}
}
}
catch
(
UncheckedIOException
|
IOException
|
InterruptedException
|
ParserException
ex
)
{
return
ex
.
getMessage
();
}
finally
{
// removeDirectory(directory);
}
return
""
;
}
private
static
void
removeDirectory
(
File
dir
)
{
if
(
dir
.
isDirectory
())
{
File
[]
files
=
dir
.
listFiles
();
if
(
files
!=
null
&&
files
.
length
>
0
)
{
for
(
File
aFile
:
files
)
{
removeDirectory
(
aFile
);
}
}
}
dir
.
delete
();
}
}
src/inport/Testing.java
View file @
fed0aba4
This diff is collapsed.
Click to expand it.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment