Commit 80a9c005 authored by Vladislav Kiselev's avatar Vladislav Kiselev

Улучшен интерфейс.

parent 3dfe2fe9
...@@ -13,6 +13,27 @@ import java.util.function.BiConsumer; ...@@ -13,6 +13,27 @@ import java.util.function.BiConsumer;
import java.util.stream.Collectors; import java.util.stream.Collectors;
public class Solver { public class Solver {
public enum SolverName {
Undefined(""),
Chuffed ("Chuffed"),
OrTools ("OrTools");
public final String text;
public static final String legalValues = "\"Chuffed\", \"OrTools\"";
SolverName(String text) {
this.text = text;
}
public static Solver.SolverName fromString(String text) {
for (Solver.SolverName t : Solver.SolverName.values()) {
if (t.text.equalsIgnoreCase(text)) {
return t;
}
}
return Undefined;
}
}
private final Lock lock = new ReentrantLock(); private final Lock lock = new ReentrantLock();
private final Condition condition = lock.newCondition(); private final Condition condition = lock.newCondition();
private Boolean isDestroyed; private Boolean isDestroyed;
...@@ -24,6 +45,7 @@ public class Solver { ...@@ -24,6 +45,7 @@ public class Solver {
private String tempDir = "temp_data"; private String tempDir = "temp_data";
private int timeLimitS; private int timeLimitS;
private String flatZincSolver = ""; private String flatZincSolver = "";
private SolverName solverName = SolverName.Undefined;
private String solverResults = ""; private String solverResults = "";
...@@ -42,6 +64,9 @@ public class Solver { ...@@ -42,6 +64,9 @@ public class Solver {
public void setFlatZincSolver(String flatZincSolver) { public void setFlatZincSolver(String flatZincSolver) {
this.flatZincSolver = flatZincSolver; this.flatZincSolver = flatZincSolver;
} }
public void setSolverName(String solverName) {
this.solverName = SolverName.fromString(solverName);
}
public String getFlatZincSolver() { public String getFlatZincSolver() {
return flatZincSolver; return flatZincSolver;
...@@ -102,34 +127,61 @@ public class Solver { ...@@ -102,34 +127,61 @@ public class Solver {
ProcessBuilder pb; ProcessBuilder pb;
boolean isResultsInOutput; boolean isResultsInOutput;
if (flatZincSolver.isEmpty()) { switch (solverName) {
pb = new ProcessBuilder("minizinc", case Chuffed: {
"--solver", "Chuffed", pb = new ProcessBuilder("minizinc",
constraints, minizincData, "--solver", "Chuffed",
"-o", solverResults); constraints, minizincData,
isResultsInOutput = false; "-o", solverResults);
} else { isResultsInOutput = false;
isResultsInOutput = true; break;
{ }
ProcessBuilder lPB = new ProcessBuilder("mzn2fzn", case OrTools: {
"-o", flatZincConstraints, isResultsInOutput = true;
constraints, {
minizincData); ProcessBuilder lPB = new ProcessBuilder("mzn2fzn",
Process process = lPB.start(); "-o", flatZincConstraints,
process.waitFor(); constraints,
minizincData);
BufferedReader br = new BufferedReader(new InputStreamReader(process.getInputStream())); Process process = lPB.start();
String output = br.lines().collect(Collectors.joining("\n")); process.waitFor();
if (output.trim().equals("=====UNSATISFIABLE=====")) { BufferedReader br = new BufferedReader(new InputStreamReader(process.getInputStream()));
task.setSolution(new ArrayList<>()); String output = br.lines().collect(Collectors.joining("\n"));
task.setSolution_result(-1);
return ""; 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);
} }
pb = new ProcessBuilder("external_tools/or-tools_flatzinc_Ubuntu-18.04-64bit_v7.2.6977/bin/fzn-or-tools", case Undefined: {
flatZincConstraints); if (flatZincSolver.isEmpty()) {
return "FlatZinc solver not defined!";
}
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(flatZincSolver, flatZincConstraints);
}
default:
return "Undefined solver.";
} }
lock.lock(); lock.lock();
......
package inport; package inport;
import java.io.*; import java.io.*;
import java.util.ArrayList; import java.util.*;
import java.util.Map; import java.util.function.Consumer;
import java.util.TreeMap;
import java.util.function.Supplier; import java.util.function.Supplier;
import static inport.Testing.*; import static inport.Testing.*;
import inport.ConversionUtils.MZnResultsResolver; import inport.ConversionUtils.*;
import inport.ConversionUtils.ParserException;
import inport.ConversionUtils.Solver;
import inport.ConversionUtils.Task;
import org.kohsuke.args4j.CmdLineException; import org.kohsuke.args4j.CmdLineException;
import org.kohsuke.args4j.CmdLineParser; import org.kohsuke.args4j.CmdLineParser;
...@@ -20,9 +16,6 @@ import org.kohsuke.args4j.Option; ...@@ -20,9 +16,6 @@ import org.kohsuke.args4j.Option;
public class Main { public class Main {
private static final int DEFAULT_TIME_LIMIT_S = 3600; private static final int DEFAULT_TIME_LIMIT_S = 3600;
@Option(name="-fzs", aliases="--flat_zinc_solver", usage="Path to executable file of flat zinc solver.")
private String flatZincSolver = "";
private enum ConversionType { private enum ConversionType {
Undefined ("", Testing::getTask_2_Solver), Undefined ("", Testing::getTask_2_Solver),
WithoutSplitting("Without splitting", Testing::getTask_2_Solver), WithoutSplitting("Without splitting", Testing::getTask_2_Solver),
...@@ -33,6 +26,8 @@ public class Main { ...@@ -33,6 +26,8 @@ public class Main {
private final String text; private final String text;
private final Supplier<Solver> solversGetter; private final Supplier<Solver> solversGetter;
static final String legalValues = "\"Without splitting\", \"With splitting\", \"Greedy\", \"Greedy v2\"";
ConversionType(String text, Supplier<Solver> solversGerrer) { ConversionType(String text, Supplier<Solver> solversGerrer) {
this.text = text; this.text = text;
this.solversGetter = solversGerrer; this.solversGetter = solversGerrer;
...@@ -59,58 +54,150 @@ public class Main { ...@@ -59,58 +54,150 @@ public class Main {
return s.toString(); return s.toString();
} }
private void doMain(final String[] args) throws IOException { private static class MainCommandsData {
final CmdLineParser parser = new CmdLineParser(this); Boolean isHidden;
if (args.length < 1) { String description;
parser.printUsage(System.out); Consumer<Collection<String>> command;
System.exit(-1);
MainCommandsData(Boolean isHidden, String description, Consumer<Collection<String>> command) {
this.isHidden = isHidden;
this.description = description;
this.command = command;
} }
/* TODO }
private void solve(Collection<String> args) {
try { try {
class Arguments {
@Option(name = "-fzs", aliases = "--flat_zinc_solver", usage = "Путь к исполняемому файлу flatZinc solver-а.", forbids = {"-s"})
private String flatZincSolver = "";
@Option(name = "-p", usage = "Путь к задаче.", required = true)
private String pathToTask = "";
@Option(name = "-ct", usage = "Тип сведения, один из " + ConversionType.legalValues + ".")
private String conversionType = ConversionType.WithoutSplitting.text;
@Option(name = "-s", aliases = "--solver", usage = "Тип solver-а из предопределённого списка : " + Solver.SolverName.legalValues + ".",
forbids = {"-fzs"})
private String solverName = Solver.SolverName.Chuffed.text;
}
Arguments arguments = new Arguments();
CmdLineParser parser = new CmdLineParser(arguments);
if (args.isEmpty()) {
parser.printUsage(System.out);
return;
}
parser.parseArgument(args); parser.parseArgument(args);
} catch (CmdLineException clEx) {
System.out.println("ERROR: Unable to parse command-line options: " + clEx);
}
*/
// flatZincSolver = "external_tools/or-tools_flatzinc_Ubuntu-18.04-64bit_v7.2.6977/bin/fzn-or-tools";
String type = args[0]; long start = System.currentTimeMillis();
switch (type) { TaskCase task = new TaskCase();
case "solve" : { task.deserialize(arguments.pathToTask);
String fileName = args[1];
long start = System.currentTimeMillis();
TaskCase task = new TaskCase(); Solver solver;
task.deserialize(fileName); if (! task.isTypified()) {
solver = getTask_2_Solver();
Solver solver; } else {
if (!task.isTypified()) { ConversionType t = ConversionType.fromString(arguments.conversionType);
solver = getTask_2_Solver(); if (t.equals(ConversionType.Undefined)) {
} else { System.out.println(undefinedTypeErrorMess(arguments.conversionType));
ConversionType t = (args.length == 2) ? ConversionType.WithoutSplitting return;
: ConversionType.fromString(args[2]);
if (t.equals(ConversionType.Undefined)) {
System.out.println(undefinedTypeErrorMess(args[2]));
return;
}
solver = t.solversGetter.get();
} }
solver = t.solversGetter.get();
}
solver.setTask(task); solver.setTask(task);
solver.setTimeLimitS(DEFAULT_TIME_LIMIT_S); solver.setTimeLimitS(DEFAULT_TIME_LIMIT_S);
solver.setTempDir("temp_data"); solver.setTempDir("temp_data");
String error = solver.solve(); if (arguments.flatZincSolver.isEmpty()) {
solver.setSolverName(arguments.solverName);
} else {
solver.setFlatZincSolver(arguments.flatZincSolver);
}
String error = solver.solve();
long finish = System.currentTimeMillis(); long finish = System.currentTimeMillis();
System.out.println((finish - start) + " milliseconds"); System.out.println((finish - start) + " milliseconds");
if (!error.isEmpty()) { if (!error.isEmpty()) {
System.out.println("Error : " + error); System.out.println("Error : " + error);
} else { } else {
task.serialize(fileName); task.serialize(arguments.pathToTask);
}
} catch (IOException ex) {
throw new UncheckedIOException(ex);
} catch (CmdLineException ex) {
System.out.println("Illegal arguments: " + ex.getLocalizedMessage());
}
}
private void doMain(final String[] args) throws IOException {
final CmdLineParser parser = new CmdLineParser(this);
Map<String, MainCommandsData> mainCommands = new TreeMap<>();
Consumer<Boolean> c = (Boolean b) -> {};
mainCommands.put("solve",
new MainCommandsData(false, "Решение задачи.", this::solve));
mainCommands.put("tippToMzn",
new MainCommandsData(
false
, "Сводит задачу к формату MiniZinc-а используя заданное сведение. " +
"Производит два файла - conversion.mzn и minizinc_data.dzn ."
, (Collection<String> a) ->
{
// try {
// // TODO реализовать
// } catch (IOException ex) {
// throw new UncheckedIOException(ex);
// }
}));
if (args.length < 1) {
System.out.println("usage: java -jar Conversion.jar <command> [<args>]");
System.out.println("Стандартные команды: ");
int maxLength = 0;
for (String name : mainCommands.keySet()) {
if (! mainCommands.get(name).isHidden) {
maxLength = Math.max(maxLength, name.length());
} }
}
for (String name : mainCommands.keySet()) {
MainCommandsData data = mainCommands.get(name);
if (! data.isHidden) {
System.out.print(name);
for (int i = maxLength - name.length(); i > 0; i--) {
System.out.print(" ");
}
System.out.println(" " + data.description);
}
}
return;
}
MainCommandsData data = mainCommands.get(args[0]);
if (data == null) {
System.out.println("Unknown type \"" + args[0] + "\"");
return;
}
data.command.accept(Arrays.asList(args).subList(1, args.length));
/*
String type = args[0];
// TODO переделать
switch (type) {
case "solve" : {
break; break;
} }
case "to_MiniZinc_0" : { case "to_MiniZinc_0" : {
...@@ -194,6 +281,7 @@ public class Main { ...@@ -194,6 +281,7 @@ public class Main {
default: default:
System.out.println("Unknown type \"" + type + "\""); System.out.println("Unknown type \"" + type + "\"");
} }
*/
} }
public static void main(String[] args) { public static void main(String[] args) {
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment