diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-18 15:21:56 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-19 11:43:02 +0200 |
commit | b217dfc7e7bd7beb73c8cc23ad82383309ceb697 (patch) | |
tree | 965485702e311137a9ea865285ce1f409b99caed | |
parent | Transitive closure of type hierarchy in ScopePropagator (diff) | |
download | VIATRA-Generator-b217dfc7e7bd7beb73c8cc23ad82383309ceb697.tar.gz VIATRA-Generator-b217dfc7e7bd7beb73c8cc23ad82383309ceb697.tar.zst VIATRA-Generator-b217dfc7e7bd7beb73c8cc23ad82383309ceb697.zip |
Implement Coin-OR CBC polyhedron saturation operator
19 files changed, 952 insertions, 197 deletions
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath new file mode 100644 index 00000000..e19039ae --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath | |||
@@ -0,0 +1,15 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <classpath> | ||
3 | <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"> | ||
4 | <attributes> | ||
5 | <attribute name="module" value="true"/> | ||
6 | </attributes> | ||
7 | </classpathentry> | ||
8 | <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> | ||
9 | <classpathentry kind="src" path="src"> | ||
10 | <attributes> | ||
11 | <attribute name="org.eclipse.jdt.launching.CLASSPATH_ATTR_LIBRARY_PATH_ENTRY" value="hu.bme.mit.inf.dslreasoner.ilp.cbc/lib"/> | ||
12 | </attributes> | ||
13 | </classpathentry> | ||
14 | <classpathentry kind="output" path="bin"/> | ||
15 | </classpath> | ||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.gitignore b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.gitignore new file mode 100644 index 00000000..0cc6a59e --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.gitignore | |||
@@ -0,0 +1,2 @@ | |||
1 | /bin/ | ||
2 | /cpp/build/ | ||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.project b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.project new file mode 100644 index 00000000..6c32e464 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.project | |||
@@ -0,0 +1,28 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <projectDescription> | ||
3 | <name>hu.bme.mit.inf.dslreasoner.ilp.cbc</name> | ||
4 | <comment></comment> | ||
5 | <projects> | ||
6 | </projects> | ||
7 | <buildSpec> | ||
8 | <buildCommand> | ||
9 | <name>org.eclipse.jdt.core.javabuilder</name> | ||
10 | <arguments> | ||
11 | </arguments> | ||
12 | </buildCommand> | ||
13 | <buildCommand> | ||
14 | <name>org.eclipse.pde.ManifestBuilder</name> | ||
15 | <arguments> | ||
16 | </arguments> | ||
17 | </buildCommand> | ||
18 | <buildCommand> | ||
19 | <name>org.eclipse.pde.SchemaBuilder</name> | ||
20 | <arguments> | ||
21 | </arguments> | ||
22 | </buildCommand> | ||
23 | </buildSpec> | ||
24 | <natures> | ||
25 | <nature>org.eclipse.pde.PluginNature</nature> | ||
26 | <nature>org.eclipse.jdt.core.javanature</nature> | ||
27 | </natures> | ||
28 | </projectDescription> | ||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/META-INF/MANIFEST.MF b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/META-INF/MANIFEST.MF new file mode 100644 index 00000000..04478746 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/META-INF/MANIFEST.MF | |||
@@ -0,0 +1,10 @@ | |||
1 | Manifest-Version: 1.0 | ||
2 | Bundle-ManifestVersion: 2 | ||
3 | Bundle-Name: Cbc | ||
4 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.ilp.cbc | ||
5 | Bundle-Version: 1.0.0.qualifier | ||
6 | Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.ilp.cbc | ||
7 | Export-Package: hu.bme.mit.inf.dslreasoner.ilp.cbc | ||
8 | Bundle-NativeCode: libviatracbc.so; | ||
9 | osname=Linux; | ||
10 | processor=x86_64 | ||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/build.properties b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/build.properties new file mode 100644 index 00000000..34d2e4d2 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/build.properties | |||
@@ -0,0 +1,4 @@ | |||
1 | source.. = src/ | ||
2 | output.. = bin/ | ||
3 | bin.includes = META-INF/,\ | ||
4 | . | ||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/CMakeLists.txt b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/CMakeLists.txt new file mode 100644 index 00000000..5dbcb071 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/CMakeLists.txt | |||
@@ -0,0 +1,23 @@ | |||
1 | cmake_minimum_required(VERSION 3.14.5) | ||
2 | project(hu.bme.mit.inf.dslreasoner.ilp.cbc) | ||
3 | |||
4 | set(CMAKE_CXX_STANDARD 17) | ||
5 | |||
6 | find_package(JNI REQUIRED) | ||
7 | find_package(PkgConfig REQUIRED) | ||
8 | |||
9 | pkg_check_modules(CBC REQUIRED cbc) | ||
10 | |||
11 | add_library(viatracbc SHARED viatracbc.cpp) | ||
12 | |||
13 | target_link_libraries(viatracbc | ||
14 | ${JAVA_JVM_LIBRARY} | ||
15 | ${CBC_LIBRARIES}) | ||
16 | target_include_directories(viatracbc | ||
17 | PUBLIC ${JNI_INCLUDE_DIRS} | ||
18 | PRIVATE ${CBC_INCLUDE_DIRS}) | ||
19 | |||
20 | set(VIATRACBC_NATIVES_DIR ${CMAKE_SOURCE_DIR}/../lib) | ||
21 | add_custom_command(TARGET viatracbc POST_BUILD | ||
22 | COMMAND ${CMAKE_COMMAND} -E make_directory ${VIATRACBC_NATIVES_DIR} | ||
23 | COMMAND ${CMAKE_COMMAND} -E copy $<TARGET_FILE:viatracbc> ${VIATRACBC_NATIVES_DIR}) | ||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.cpp b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.cpp new file mode 100644 index 00000000..49994244 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.cpp | |||
@@ -0,0 +1,261 @@ | |||
1 | |||
2 | #include <cmath> | ||
3 | #include <cstdlib> | ||
4 | #include <iostream> | ||
5 | #include <stdexcept> | ||
6 | |||
7 | #include <jni.h> | ||
8 | |||
9 | #include "CbcBranchDefaultDecision.hpp" | ||
10 | #include "CbcCompareDefault.hpp" | ||
11 | #include "CbcHeuristic.hpp" | ||
12 | #include "CbcHeuristicLocal.hpp" | ||
13 | #include "CbcModel.hpp" | ||
14 | #include "CglClique.hpp" | ||
15 | #include "CglFlowCover.hpp" | ||
16 | #include "CglGomory.hpp" | ||
17 | #include "CglKnapsackCover.hpp" | ||
18 | #include "CglMixedIntegerRounding.hpp" | ||
19 | #include "CglOddHole.hpp" | ||
20 | #include "CglProbing.hpp" | ||
21 | #include "CoinModel.hpp" | ||
22 | #include "OsiClpSolverInterface.hpp" | ||
23 | |||
24 | #include "viatracbc.hpp" | ||
25 | |||
26 | static const char *const kCbcExceptionClassName = "hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcException"; | ||
27 | static const char *const kRuntimeExceptionClassName = "java/lang/RuntimeException"; | ||
28 | |||
29 | static const jint kCbcSolutionBounded = 0; | ||
30 | static const jint kCbcSolutionUnbounded = 1; | ||
31 | static const jint kCbcUnsat = 2; | ||
32 | static const jint kCbcAbandoned = 3; | ||
33 | static const jint kCbcTimeout = 4; | ||
34 | static const jint kCbcError = 5; | ||
35 | |||
36 | static CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, | ||
37 | jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, | ||
38 | jdoubleArray entriedArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, | ||
39 | jdoubleArray objectiveArray); | ||
40 | static void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, | ||
41 | jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, CoinModel &build); | ||
42 | static void CreateModelRows(JNIEnv *env, jintArray rowStartsArray, jintArray columnIndicesArray, | ||
43 | jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, | ||
44 | CoinModel &build); | ||
45 | static jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdouble &value); | ||
46 | static void ThrowException(JNIEnv *env, const char *message); | ||
47 | |||
48 | template < | ||
49 | typename Array, | ||
50 | typename Element, | ||
51 | Element *(JNIEnv::*GetElementsPtr)(Array, jboolean *), | ||
52 | void (JNIEnv::*ReleaseElementsPtr)(Array, Element *, jint) | ||
53 | > | ||
54 | class PinnedArray { | ||
55 | public: | ||
56 | PinnedArray(JNIEnv *env, Array array) | ||
57 | : env_{env}, array_{array}, elements_{(env->*GetElementsPtr)(array, nullptr)} { | ||
58 | if (elements_ == nullptr) { | ||
59 | throw std::runtime_error("Failed to pin array elements"); | ||
60 | } | ||
61 | } | ||
62 | PinnedArray(const PinnedArray &) = delete; | ||
63 | PinnedArray(PinnedArray &&) = delete; | ||
64 | PinnedArray &operator=(const PinnedArray &) = delete; | ||
65 | PinnedArray &operator=(PinnedArray &&) = delete; | ||
66 | ~PinnedArray() { | ||
67 | (env_->*ReleaseElementsPtr)(array_, elements_, 0); | ||
68 | } | ||
69 | |||
70 | operator Element *() { return elements_; } | ||
71 | operator const Element *() const { return elements_; } | ||
72 | |||
73 | private: | ||
74 | JNIEnv *env_; | ||
75 | Array array_; | ||
76 | Element *elements_; | ||
77 | }; | ||
78 | |||
79 | using PinnedIntArray = PinnedArray<jintArray, jint, &JNIEnv::GetIntArrayElements, &JNIEnv::ReleaseIntArrayElements>; | ||
80 | using PinnedDoubleArray = PinnedArray<jdoubleArray, jdouble, &JNIEnv::GetDoubleArrayElements, &JNIEnv::ReleaseDoubleArrayElements>; | ||
81 | |||
82 | jint Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIlpProblem( | ||
83 | JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, | ||
84 | jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, | ||
85 | jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, | ||
86 | jdoubleArray outputArray, jdouble timeoutSeconds, jboolean silent) { | ||
87 | try { | ||
88 | auto build = CreateModel(env, columnLowerBoundsArray, columnUpperBoundsArray, | ||
89 | rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, rowUpperBoundsArray, | ||
90 | objectiveArray); | ||
91 | double value; | ||
92 | jint result = SolveModel(build, timeoutSeconds, silent, value); | ||
93 | if (result == kCbcSolutionBounded) { | ||
94 | PinnedDoubleArray output{env, outputArray}; | ||
95 | *output = value; | ||
96 | } | ||
97 | return result; | ||
98 | } catch (const std::exception &e) { | ||
99 | ThrowException(env, e.what()); | ||
100 | } catch (...) { | ||
101 | ThrowException(env, "Unknown solver error"); | ||
102 | } | ||
103 | return kCbcError; | ||
104 | } | ||
105 | |||
106 | CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, | ||
107 | jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, | ||
108 | jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, | ||
109 | jdoubleArray objectiveArray) { | ||
110 | CoinModel build; | ||
111 | CreateModelColumns(env, columnLowerBoundsArray, columnUpperBoundsArray, objectiveArray, build); | ||
112 | CreateModelRows(env, rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, | ||
113 | rowUpperBoundsArray, build); | ||
114 | return build; | ||
115 | } | ||
116 | |||
117 | void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, | ||
118 | jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, CoinModel &build) { | ||
119 | int numColumns = env->GetArrayLength(columnLowerBoundsArray); | ||
120 | PinnedDoubleArray columnLowerBounds{env, columnLowerBoundsArray}; | ||
121 | PinnedDoubleArray columnUpperBounds{env, columnUpperBoundsArray}; | ||
122 | PinnedDoubleArray objective{env, objectiveArray}; | ||
123 | for (int i = 0; i < numColumns; i++) { | ||
124 | build.setColumnBounds(i, columnLowerBounds[i], columnUpperBounds[i]); | ||
125 | build.setObjective(i, objective[i]); | ||
126 | build.setInteger(i); | ||
127 | } | ||
128 | } | ||
129 | |||
130 | void CreateModelRows(JNIEnv *env, jintArray rowStartsArray, jintArray columnIndicesArray, | ||
131 | jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, | ||
132 | CoinModel &build) { | ||
133 | int numRows = env->GetArrayLength(rowLowerBoundsArray); | ||
134 | PinnedIntArray rowStarts{env, rowStartsArray}; | ||
135 | PinnedIntArray columnIndices{env, columnIndicesArray}; | ||
136 | PinnedDoubleArray entries{env, entriesArray}; | ||
137 | PinnedDoubleArray rowLowerBounds{env, rowLowerBoundsArray}; | ||
138 | PinnedDoubleArray rowUpperBounds{env, rowUpperBoundsArray}; | ||
139 | for (int i = 0; i < numRows; i++) { | ||
140 | int rowStart = rowStarts[i]; | ||
141 | int numbersInRow = rowStarts[i + 1] - rowStart; | ||
142 | build.addRow(numbersInRow, &columnIndices[rowStart], &entries[rowStart], | ||
143 | rowLowerBounds[i], rowUpperBounds[i]); | ||
144 | } | ||
145 | } | ||
146 | |||
147 | jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdouble &value) { | ||
148 | OsiClpSolverInterface solver; | ||
149 | solver.loadFromCoinModel(build); | ||
150 | CbcModel model{solver}; | ||
151 | |||
152 | model.setDblParam(CbcModel::CbcMaximumSeconds, timeoutSeconds); | ||
153 | if (silent == JNI_FALSE) { | ||
154 | model.messageHandler()->setLogLevel(2); | ||
155 | model.solver()->messageHandler()->setLogLevel(1); | ||
156 | } else { | ||
157 | model.solver()->setHintParam(OsiDoReducePrint, true, OsiHintTry); | ||
158 | model.messageHandler()->setLogLevel(0); | ||
159 | model.solver()->messageHandler()->setLogLevel(0); | ||
160 | } | ||
161 | |||
162 | // Cut generators and heuristics are used according to | ||
163 | // https://github.com/coin-or/Cbc/blob/6b977b6707f1755520c64fea57b95891c1f3ddc0/Cbc/examples/sample2.cpp | ||
164 | |||
165 | CglProbing probing; | ||
166 | probing.setUsingObjective(true); | ||
167 | probing.setMaxPass(1); | ||
168 | probing.setMaxPassRoot(5); | ||
169 | probing.setMaxProbe(10); | ||
170 | probing.setMaxProbeRoot(1000); | ||
171 | probing.setMaxLook(50); | ||
172 | probing.setMaxLookRoot(500); | ||
173 | probing.setMaxElements(200); | ||
174 | probing.setRowCuts(3); | ||
175 | model.addCutGenerator(&probing, -1, "Probing"); | ||
176 | |||
177 | CglGomory gomory; | ||
178 | gomory.setLimit(300); | ||
179 | model.addCutGenerator(&gomory, -1, "Gomory"); | ||
180 | |||
181 | CglKnapsackCover knapsackCover; | ||
182 | model.addCutGenerator(&knapsackCover, -1, "KnapsackCover"); | ||
183 | |||
184 | CglClique clique; | ||
185 | clique.setStarCliqueReport(false); | ||
186 | clique.setRowCliqueReport(false); | ||
187 | model.addCutGenerator(&clique, -1, "Clique"); | ||
188 | |||
189 | CglFlowCover flowCover; | ||
190 | model.addCutGenerator(&flowCover, -1, "FlowCover"); | ||
191 | |||
192 | CglMixedIntegerRounding mixedIntegerRounding; | ||
193 | model.addCutGenerator(&mixedIntegerRounding, -1, "MixedIntegerRounding"); | ||
194 | |||
195 | OsiClpSolverInterface *osiClp = dynamic_cast<OsiClpSolverInterface *>(model.solver()); | ||
196 | if (osiClp != nullptr) { | ||
197 | osiClp->setSpecialOptions(128); | ||
198 | osiClp->setupForRepeatedUse(0, 0); | ||
199 | } | ||
200 | |||
201 | CbcRounding rounding; | ||
202 | model.addHeuristic(&rounding); | ||
203 | |||
204 | CbcHeuristicLocal localHeuristic; | ||
205 | model.addHeuristic(&localHeuristic); | ||
206 | |||
207 | CbcBranchDefaultDecision branchDecision; | ||
208 | model.setBranchingMethod(&branchDecision); | ||
209 | |||
210 | CbcCompareDefault nodeComparison; | ||
211 | model.setNodeComparison(nodeComparison); | ||
212 | |||
213 | model.initialSolve(); | ||
214 | |||
215 | if (model.isInitialSolveProvenPrimalInfeasible()) { | ||
216 | return kCbcUnsat; | ||
217 | } | ||
218 | if (model.isInitialSolveAbandoned()) { | ||
219 | return kCbcTimeout; | ||
220 | } | ||
221 | |||
222 | model.setMinimumDrop(CoinMin(1.0, fabs(model.getMinimizationObjValue()) * 1.0e-3 + 1.0e-4)); | ||
223 | model.setMaximumCutPassesAtRoot(-100); | ||
224 | model.setNumberStrong(10); | ||
225 | model.solver()->setIntParam(OsiMaxNumIterationHotStart, 100); | ||
226 | |||
227 | model.branchAndBound(); | ||
228 | |||
229 | if (model.isProvenInfeasible()) { | ||
230 | return kCbcUnsat; | ||
231 | } | ||
232 | if (model.isProvenDualInfeasible()) { | ||
233 | return kCbcSolutionUnbounded; | ||
234 | } | ||
235 | if (model.isProvenOptimal()) { | ||
236 | value = model.getMinimizationObjValue(); | ||
237 | return kCbcSolutionBounded; | ||
238 | } | ||
239 | if (model.maximumSecondsReached()) { | ||
240 | return kCbcTimeout; | ||
241 | } | ||
242 | return kCbcAbandoned; | ||
243 | } | ||
244 | |||
245 | void ThrowException(JNIEnv *env, const char *message) { | ||
246 | jclass exceptionClass = env->FindClass(kCbcExceptionClassName); | ||
247 | if (exceptionClass == nullptr) { | ||
248 | std::cerr << "WARNING: " << kCbcExceptionClassName << " class was not found" << std::endl; | ||
249 | exceptionClass = env->FindClass(kRuntimeExceptionClassName); | ||
250 | if (exceptionClass == nullptr) { | ||
251 | std::cerr << "FATAL: " << kRuntimeExceptionClassName << " class was not found" << std::endl; | ||
252 | std::cerr << "FATAL: " << message << std::endl; | ||
253 | std::exit(EXIT_FAILURE); | ||
254 | } | ||
255 | } | ||
256 | if (env->ThrowNew(exceptionClass, message) < 0) { | ||
257 | std::cerr << "FATAL: Could not throw java exception" << std::endl; | ||
258 | std::cerr << "FATAL: " << message << std::endl; | ||
259 | std::exit(EXIT_FAILURE); | ||
260 | } | ||
261 | } | ||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.hpp b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.hpp new file mode 100644 index 00000000..c65f71e3 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.hpp | |||
@@ -0,0 +1,16 @@ | |||
1 | #ifndef HU_BME_MIT_INF_DSLREASONER_ILP_CBC_ | ||
2 | #define HU_BME_MIT_INF_DSLREASONER_ILP_CBC_ | ||
3 | |||
4 | #include <jni.h> | ||
5 | |||
6 | extern "C" { | ||
7 | |||
8 | JNIEXPORT jint JNICALL Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIlpProblem( | ||
9 | JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, | ||
10 | jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, | ||
11 | jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, | ||
12 | jdoubleArray outputArray, jdouble timeoutSeconds, jboolean silent); | ||
13 | |||
14 | } | ||
15 | |||
16 | #endif // HU_BME_MIT_INF_DSLREASONER_ILP_CBC_ | ||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so new file mode 100755 index 00000000..21fd2ff2 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so | |||
Binary files differ | |||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcException.java b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcException.java new file mode 100644 index 00000000..26846958 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcException.java | |||
@@ -0,0 +1,30 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.ilp.cbc; | ||
2 | |||
3 | public class CbcException extends RuntimeException { | ||
4 | |||
5 | /** | ||
6 | * | ||
7 | */ | ||
8 | private static final long serialVersionUID = 2691773509078511887L; | ||
9 | |||
10 | public CbcException() { | ||
11 | super(); | ||
12 | } | ||
13 | |||
14 | public CbcException(String message, Throwable cause, boolean enableSuppression, boolean writableStackTrace) { | ||
15 | super(message, cause, enableSuppression, writableStackTrace); | ||
16 | } | ||
17 | |||
18 | public CbcException(String message, Throwable cause) { | ||
19 | super(message, cause); | ||
20 | } | ||
21 | |||
22 | public CbcException(String message) { | ||
23 | super(message); | ||
24 | } | ||
25 | |||
26 | public CbcException(Throwable cause) { | ||
27 | super(cause); | ||
28 | } | ||
29 | |||
30 | } | ||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcResult.java b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcResult.java new file mode 100644 index 00000000..dae3a447 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcResult.java | |||
@@ -0,0 +1,54 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.ilp.cbc; | ||
2 | |||
3 | public abstract class CbcResult { | ||
4 | public static final CbcResult SOLUTION_UNBOUNDED = new CbcResult() { | ||
5 | }; | ||
6 | |||
7 | public static final CbcResult UNSAT = new CbcResult() { | ||
8 | }; | ||
9 | |||
10 | public static final CbcResult ABANDONED = new CbcResult() { | ||
11 | }; | ||
12 | |||
13 | public static final CbcResult TIMEOUT = new CbcResult() { | ||
14 | }; | ||
15 | |||
16 | private CbcResult() { | ||
17 | } | ||
18 | |||
19 | public static class SolutionBounded extends CbcResult { | ||
20 | public final double value; | ||
21 | |||
22 | public SolutionBounded(double value) { | ||
23 | this.value = value; | ||
24 | } | ||
25 | |||
26 | public double getValue() { | ||
27 | return value; | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public int hashCode() { | ||
32 | final int prime = 31; | ||
33 | int result = 1; | ||
34 | long temp; | ||
35 | temp = Double.doubleToLongBits(value); | ||
36 | result = prime * result + (int) (temp ^ (temp >>> 32)); | ||
37 | return result; | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public boolean equals(Object obj) { | ||
42 | if (this == obj) | ||
43 | return true; | ||
44 | if (obj == null) | ||
45 | return false; | ||
46 | if (getClass() != obj.getClass()) | ||
47 | return false; | ||
48 | SolutionBounded other = (SolutionBounded) obj; | ||
49 | if (Double.doubleToLongBits(value) != Double.doubleToLongBits(other.value)) | ||
50 | return false; | ||
51 | return true; | ||
52 | } | ||
53 | } | ||
54 | } | ||
diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java new file mode 100644 index 00000000..39b9d537 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java | |||
@@ -0,0 +1,71 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.ilp.cbc; | ||
2 | |||
3 | public class CbcSolver { | ||
4 | private static int CBC_SOLUTION_BOUNDED = 0; | ||
5 | private static int CBC_SOLUTION_UNBOUNDED = 1; | ||
6 | private static int CBC_UNSAT = 2; | ||
7 | private static int CBC_ABANDONED = 3; | ||
8 | private static int CBC_TIMEOUT = 4; | ||
9 | private static int CBC_ERROR = 5; | ||
10 | |||
11 | private static boolean nativesLoaded = false; | ||
12 | |||
13 | private CbcSolver() { | ||
14 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly."); | ||
15 | } | ||
16 | |||
17 | public static CbcResult solve(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, | ||
18 | int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, | ||
19 | double[] objective, double timeoutSeconds, boolean silent) { | ||
20 | loadNatives(); | ||
21 | validate(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, rowLowerBounds, | ||
22 | rowUpperBounds, objective); | ||
23 | double[] output = new double[1]; | ||
24 | int result = solveIlpProblem(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, | ||
25 | rowLowerBounds, rowUpperBounds, objective, output, timeoutSeconds, silent); | ||
26 | if (result == CBC_SOLUTION_BOUNDED) { | ||
27 | return new CbcResult.SolutionBounded(output[0]); | ||
28 | } else if (result == CBC_SOLUTION_UNBOUNDED) { | ||
29 | return CbcResult.SOLUTION_UNBOUNDED; | ||
30 | } else if (result == CBC_UNSAT) { | ||
31 | return CbcResult.UNSAT; | ||
32 | } else if (result == CBC_ABANDONED) { | ||
33 | return CbcResult.ABANDONED; | ||
34 | } else if (result == CBC_TIMEOUT) { | ||
35 | return CbcResult.TIMEOUT; | ||
36 | } else if (result == CBC_ERROR) { | ||
37 | throw new CbcException("Solver signalled error, but no exception was thrown"); | ||
38 | } else { | ||
39 | throw new CbcException("Unknown return value: " + result); | ||
40 | } | ||
41 | } | ||
42 | |||
43 | private static void loadNatives() { | ||
44 | if (!nativesLoaded) { | ||
45 | synchronized (CbcSolver.class) { | ||
46 | System.loadLibrary("viatracbc"); | ||
47 | nativesLoaded = true; | ||
48 | } | ||
49 | } | ||
50 | } | ||
51 | |||
52 | private static void validate(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, | ||
53 | int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, | ||
54 | double[] objective) { | ||
55 | int numColumns = columnLowerBounds.length; | ||
56 | if (columnUpperBounds.length != numColumns) { | ||
57 | throw new CbcException("Lengths of columnLowerBounds and columnUpperBounds must match"); | ||
58 | } | ||
59 | if (objective.length != numColumns) { | ||
60 | throw new CbcException("Lengths of columnLowerBounds and objective must match"); | ||
61 | } | ||
62 | int numRows = rowLowerBounds.length; | ||
63 | if (rowUpperBounds.length != numRows) { | ||
64 | throw new CbcException("Lengths of rowLowerBounds and rowUpperBounds must match"); | ||
65 | } | ||
66 | } | ||
67 | |||
68 | private static native int solveIlpProblem(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, | ||
69 | int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, double[] objective, | ||
70 | double[] output, double timeoutSeconds, boolean silent); | ||
71 | } | ||
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF b/Solvers/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF index 01faa2ad..401fa6cf 100644 --- a/Solvers/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF +++ b/Solvers/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF | |||
@@ -9,7 +9,7 @@ Bundle-ClassPath: com.microsoft.z3.jar | |||
9 | Bundle-NativeCode: lib/libz3.so; | 9 | Bundle-NativeCode: lib/libz3.so; |
10 | lib/libz3java.so; | 10 | lib/libz3java.so; |
11 | osname=Linux; | 11 | osname=Linux; |
12 | processor=x86_64; | 12 | processor=x86_64, |
13 | lib/libz3.dylib; | 13 | lib/libz3.dylib; |
14 | lib/libz3java.dylib; | 14 | lib/libz3java.dylib; |
15 | osname=MacOSX; | 15 | osname=MacOSX; |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF index 37495e50..f9090901 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF | |||
@@ -24,7 +24,8 @@ Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | |||
24 | org.eclipse.xtext;bundle-version="2.10.0", | 24 | org.eclipse.xtext;bundle-version="2.10.0", |
25 | org.eclipse.viatra.transformation.runtime.emf;bundle-version="1.5.0", | 25 | org.eclipse.viatra.transformation.runtime.emf;bundle-version="1.5.0", |
26 | org.eclipse.xtext.xbase;bundle-version="2.10.0", | 26 | org.eclipse.xtext.xbase;bundle-version="2.10.0", |
27 | com.microsoft.z3;bundle-version="4.8.5" | 27 | com.microsoft.z3;bundle-version="4.8.5", |
28 | hu.bme.mit.inf.dslreasoner.ilp.cbc;bundle-version="1.0.0" | ||
28 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 | 29 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 |
29 | Import-Package: org.apache.log4j | 30 | Import-Package: org.apache.log4j |
30 | Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery | 31 | Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index 0040dbcd..0ceb5b2e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend | |||
@@ -4,10 +4,10 @@ import com.google.common.collect.ImmutableMap | |||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | 6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider |
@@ -119,7 +119,7 @@ class ModelGenerationMethodProvider { | |||
119 | new ScopePropagator(emptySolution) | 119 | new ScopePropagator(emptySolution) |
120 | case PolyhedralTypeHierarchy: { | 120 | case PolyhedralTypeHierarchy: { |
121 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | 121 | val types = queries.refineObjectQueries.keySet.map[newType].toSet |
122 | val solver = new Z3PolyhedronSolver | 122 | val solver = new CbcPolyhedronSolver |
123 | new PolyhedronScopePropagator(emptySolution, types, solver) | 123 | new PolyhedronScopePropagator(emptySolution, types, solver) |
124 | } | 124 | } |
125 | default: | 125 | default: |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend new file mode 100644 index 00000000..1f6d4e8f --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend | |||
@@ -0,0 +1,182 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableMap | ||
4 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult | ||
5 | import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver | ||
6 | import java.util.Map | ||
7 | import org.eclipse.xtend.lib.annotations.Accessors | ||
8 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
9 | |||
10 | @FinalFieldsConstructor | ||
11 | class CbcPolyhedronSolver implements PolyhedronSolver { | ||
12 | val double timeoutSeconds | ||
13 | val boolean silent | ||
14 | |||
15 | new() { | ||
16 | this(10, true) | ||
17 | } | ||
18 | |||
19 | override createSaturationOperator(Polyhedron polyhedron) { | ||
20 | new CbcSaturationOperator(polyhedron, timeoutSeconds, silent) | ||
21 | } | ||
22 | } | ||
23 | |||
24 | class CbcSaturationOperator implements PolyhedronSaturationOperator { | ||
25 | @Accessors val Polyhedron polyhedron | ||
26 | val double timeoutSeconds | ||
27 | val boolean silent | ||
28 | val double[] columnLowerBounds | ||
29 | val double[] columnUpperBounds | ||
30 | val double[] objective | ||
31 | val Map<Dimension, Integer> dimensionsToIndicesMap | ||
32 | |||
33 | new(Polyhedron polyhedron, double timeoutSeconds, boolean silent) { | ||
34 | this.polyhedron = polyhedron | ||
35 | this.timeoutSeconds = timeoutSeconds | ||
36 | this.silent = silent | ||
37 | val numDimensions = polyhedron.dimensions.size | ||
38 | columnLowerBounds = newDoubleArrayOfSize(numDimensions) | ||
39 | columnUpperBounds = newDoubleArrayOfSize(numDimensions) | ||
40 | objective = newDoubleArrayOfSize(numDimensions) | ||
41 | dimensionsToIndicesMap = ImmutableMap.copyOf(polyhedron.dimensions.indexed.toMap([value], [key])) | ||
42 | } | ||
43 | |||
44 | override saturate() { | ||
45 | val numDimensions = polyhedron.dimensions.size | ||
46 | for (var int j = 0; j < numDimensions; j++) { | ||
47 | val dimension = polyhedron.dimensions.get(j) | ||
48 | columnLowerBounds.set(j, dimension.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) | ||
49 | columnUpperBounds.set(j, dimension.upperBound.toDouble(Double.POSITIVE_INFINITY)) | ||
50 | } | ||
51 | val numConstraints = polyhedron.constraints.size | ||
52 | val rowStarts = newIntArrayOfSize(numConstraints + 1) | ||
53 | val rowLowerBounds = newDoubleArrayOfSize(numConstraints) | ||
54 | val rowUpperBounds = newDoubleArrayOfSize(numConstraints) | ||
55 | val numEntries = polyhedron.constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0 | ||
56 | rowStarts.set(numConstraints, numEntries) | ||
57 | val columnIndices = newIntArrayOfSize(numEntries) | ||
58 | val entries = newDoubleArrayOfSize(numEntries) | ||
59 | var int index = 0 | ||
60 | for (var int i = 0; i < numConstraints; i++) { | ||
61 | rowStarts.set(i, index) | ||
62 | val constraint = polyhedron.constraints.get(i) | ||
63 | rowLowerBounds.set(i, constraint.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) | ||
64 | rowUpperBounds.set(i, constraint.upperBound.toDouble(Double.POSITIVE_INFINITY)) | ||
65 | if (!dimensionsToIndicesMap.keySet.containsAll(constraint.coefficients.keySet)) { | ||
66 | throw new IllegalArgumentException("Constrains has unknown dimensions") | ||
67 | } | ||
68 | for (var int j = 0; j < numDimensions; j++) { | ||
69 | val dimension = polyhedron.dimensions.get(j) | ||
70 | val coefficient = constraint.coefficients.get(dimension) | ||
71 | if (coefficient !== null && coefficient != 0) { | ||
72 | columnIndices.set(index, j) | ||
73 | entries.set(index, coefficient) | ||
74 | index++ | ||
75 | } | ||
76 | } | ||
77 | } | ||
78 | if (index != numEntries) { | ||
79 | throw new AssertionError("Last entry does not equal the number of entries in the constraint matrix") | ||
80 | } | ||
81 | for (expressionToSaturate : polyhedron.expressionsToSaturate) { | ||
82 | for (var int j = 0; j < numDimensions; j++) { | ||
83 | objective.set(j, 0) | ||
84 | } | ||
85 | switch (expressionToSaturate) { | ||
86 | Dimension: { | ||
87 | val j = getIndex(expressionToSaturate) | ||
88 | objective.set(j, 1) | ||
89 | } | ||
90 | LinearConstraint: { | ||
91 | for (pair : expressionToSaturate.coefficients.entrySet) { | ||
92 | val j = getIndex(pair.key) | ||
93 | objective.set(j, pair.value) | ||
94 | } | ||
95 | } | ||
96 | default: | ||
97 | throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate) | ||
98 | } | ||
99 | val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, | ||
100 | entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) | ||
101 | switch (minimizationResult) { | ||
102 | CbcResult.SolutionBounded: { | ||
103 | val value = Math.floor(minimizationResult.value) | ||
104 | expressionToSaturate.lowerBound = value as int | ||
105 | setBound(expressionToSaturate, value, columnLowerBounds, rowLowerBounds) | ||
106 | } | ||
107 | case CbcResult.SOLUTION_UNBOUNDED: { | ||
108 | expressionToSaturate.lowerBound = null | ||
109 | setBound(expressionToSaturate, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) | ||
110 | } | ||
111 | case CbcResult.UNSAT: | ||
112 | return PolyhedronSaturationResult.EMPTY | ||
113 | case CbcResult.ABANDONED, | ||
114 | case CbcResult.TIMEOUT: | ||
115 | return PolyhedronSaturationResult.UNKNOWN | ||
116 | default: | ||
117 | throw new RuntimeException("Unknown CbcResult: " + minimizationResult) | ||
118 | } | ||
119 | for (var int j = 0; j < numDimensions; j++) { | ||
120 | val objectiveCoefficient = objective.get(j) | ||
121 | objective.set(j, -objectiveCoefficient) | ||
122 | } | ||
123 | val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, | ||
124 | entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) | ||
125 | switch (maximizationResult) { | ||
126 | CbcResult.SolutionBounded: { | ||
127 | val value = Math.ceil(-maximizationResult.value) | ||
128 | expressionToSaturate.upperBound = value as int | ||
129 | setBound(expressionToSaturate, value, columnUpperBounds, rowUpperBounds) | ||
130 | } | ||
131 | case CbcResult.SOLUTION_UNBOUNDED: { | ||
132 | expressionToSaturate.upperBound = null | ||
133 | setBound(expressionToSaturate, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) | ||
134 | } | ||
135 | case CbcResult.UNSAT: | ||
136 | throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") | ||
137 | case CbcResult.ABANDONED, | ||
138 | case CbcResult.TIMEOUT: | ||
139 | return PolyhedronSaturationResult.UNKNOWN | ||
140 | default: | ||
141 | throw new RuntimeException("Unknown CbcResult: " + maximizationResult) | ||
142 | } | ||
143 | } | ||
144 | PolyhedronSaturationResult.SATURATED | ||
145 | } | ||
146 | |||
147 | private def toDouble(Integer nullableInt, double defaultValue) { | ||
148 | if (nullableInt === null) { | ||
149 | defaultValue | ||
150 | } else { | ||
151 | nullableInt.doubleValue | ||
152 | } | ||
153 | } | ||
154 | |||
155 | private def int getIndex(Dimension dimension) { | ||
156 | val index = dimensionsToIndicesMap.get(dimension) | ||
157 | if (index === null) { | ||
158 | throw new IllegalArgumentException("Unknown dimension: " + dimension) | ||
159 | } | ||
160 | index | ||
161 | } | ||
162 | |||
163 | private def void setBound(LinearBoundedExpression expression, double bound, double[] columnBounds, | ||
164 | double[] rowBounds) { | ||
165 | switch (expression) { | ||
166 | Dimension: { | ||
167 | val j = getIndex(expression) | ||
168 | columnBounds.set(j, bound) | ||
169 | } | ||
170 | LinearConstraint: { | ||
171 | val i = polyhedron.constraints.indexOf(expression) | ||
172 | if (i >= 0) { | ||
173 | rowBounds.set(i, bound) | ||
174 | } | ||
175 | } | ||
176 | } | ||
177 | } | ||
178 | |||
179 | override close() throws Exception { | ||
180 | // Nothing to close | ||
181 | } | ||
182 | } | ||
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend new file mode 100644 index 00000000..3d911bfb --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend | |||
@@ -0,0 +1,31 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult | ||
7 | import org.junit.Test | ||
8 | |||
9 | import static org.junit.Assert.* | ||
10 | |||
11 | class CbcPolyhedronSolverTest extends PolyhedronSolverTest { | ||
12 | |||
13 | override protected createSolver() { | ||
14 | new CbcPolyhedronSolver(10, false) | ||
15 | } | ||
16 | |||
17 | @Test | ||
18 | def void timeoutTest() { | ||
19 | val solver = new CbcPolyhedronSolver(0, false) | ||
20 | val x = new Dimension("x", 0, 1) | ||
21 | val polyhedron = new Polyhedron(#[x], #[], #[x]) | ||
22 | val operator = solver.createSaturationOperator(polyhedron) | ||
23 | try { | ||
24 | val result = operator.saturate | ||
25 | |||
26 | assertEquals(PolyhedronSaturationResult.UNKNOWN, result) | ||
27 | } finally { | ||
28 | operator.close() | ||
29 | } | ||
30 | } | ||
31 | } | ||
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend new file mode 100644 index 00000000..789018cb --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend | |||
@@ -0,0 +1,216 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSolver | ||
9 | import org.junit.After | ||
10 | import org.junit.Before | ||
11 | import org.junit.Test | ||
12 | |||
13 | import static org.junit.Assert.* | ||
14 | |||
15 | abstract class PolyhedronSolverTest { | ||
16 | var PolyhedronSolver solver | ||
17 | var PolyhedronSaturationOperator operator | ||
18 | |||
19 | protected def PolyhedronSolver createSolver() | ||
20 | |||
21 | @Before | ||
22 | def void setUp() { | ||
23 | solver = createSolver() | ||
24 | } | ||
25 | |||
26 | @After | ||
27 | def void tearDown() { | ||
28 | destroyOperatorIfExists() | ||
29 | } | ||
30 | |||
31 | @Test | ||
32 | def void singleDimensionTest() { | ||
33 | val x = new Dimension("x", 0, 1) | ||
34 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | ||
35 | |||
36 | val result = saturate() | ||
37 | |||
38 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
39 | assertEquals(0, x.lowerBound) | ||
40 | assertEquals(1, x.upperBound) | ||
41 | } | ||
42 | |||
43 | @Test | ||
44 | def void singleDimensionNegativeValueTest() { | ||
45 | val x = new Dimension("x", -2, -1) | ||
46 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | ||
47 | |||
48 | val result = saturate() | ||
49 | |||
50 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
51 | assertEquals(-2, x.lowerBound) | ||
52 | assertEquals(-1, x.upperBound) | ||
53 | } | ||
54 | |||
55 | @Test | ||
56 | def void singleDimensionConstraintTest() { | ||
57 | val x = new Dimension("x", null, null) | ||
58 | val constraint = new LinearConstraint(#{x -> 2}, 0, 2) | ||
59 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
60 | |||
61 | val result = saturate() | ||
62 | |||
63 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
64 | assertEquals(0, x.lowerBound) | ||
65 | assertEquals(1, x.upperBound) | ||
66 | } | ||
67 | |||
68 | @Test | ||
69 | def void singleDimensionConstraintUnitCoefficientTest() { | ||
70 | val x = new Dimension("x", null, null) | ||
71 | val constraint = new LinearConstraint(#{x -> 1}, 1, 3) | ||
72 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
73 | |||
74 | val result = saturate() | ||
75 | |||
76 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
77 | assertEquals(1, x.lowerBound) | ||
78 | assertEquals(3, x.upperBound) | ||
79 | } | ||
80 | |||
81 | @Test | ||
82 | def void singleDimensionConstraintIntegerTest() { | ||
83 | val x = new Dimension("x", null, null) | ||
84 | val constraint = new LinearConstraint(#{x -> 2}, 0, 3) | ||
85 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
86 | |||
87 | val result = saturate() | ||
88 | |||
89 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
90 | assertEquals(0, x.lowerBound) | ||
91 | assertEquals(1, x.upperBound) | ||
92 | } | ||
93 | |||
94 | @Test | ||
95 | def void singleDimensionUnboundedFromAboveTest() { | ||
96 | val x = new Dimension("x", 0, null) | ||
97 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | ||
98 | |||
99 | val result = saturate() | ||
100 | |||
101 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
102 | assertEquals(0, x.lowerBound) | ||
103 | assertEquals(null, x.upperBound) | ||
104 | } | ||
105 | |||
106 | @Test | ||
107 | def void singleDimensionUnboundedFromBelowTest() { | ||
108 | val x = new Dimension("x", null, 0) | ||
109 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | ||
110 | |||
111 | val result = saturate() | ||
112 | |||
113 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
114 | assertEquals(null, x.lowerBound) | ||
115 | assertEquals(0, x.upperBound) | ||
116 | } | ||
117 | |||
118 | @Test | ||
119 | def void singleDimensionUnsatisfiableTest() { | ||
120 | val x = new Dimension("x", 0, 1) | ||
121 | val constraint = new LinearConstraint(#{x -> 2}, -2, -1) | ||
122 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
123 | |||
124 | val result = saturate() | ||
125 | |||
126 | assertEquals(PolyhedronSaturationResult.EMPTY, result) | ||
127 | } | ||
128 | |||
129 | @Test | ||
130 | def void equalityConstraintTest() { | ||
131 | val x = new Dimension("x", null, null) | ||
132 | val y = new Dimension("y", 1, 2) | ||
133 | val constraint = new LinearConstraint(#{x -> 2, y -> 2}, 6, 6) | ||
134 | createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[x])) | ||
135 | |||
136 | val result = saturate() | ||
137 | |||
138 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
139 | assertEquals(1, x.lowerBound) | ||
140 | assertEquals(2, x.upperBound) | ||
141 | } | ||
142 | |||
143 | @Test | ||
144 | def void saturateConstraintTest() { | ||
145 | val x = new Dimension("x", 0, 2) | ||
146 | val y = new Dimension("y", 1, 2) | ||
147 | val constraint = new LinearConstraint(#{x -> 2, y -> 1}, 0, 8) | ||
148 | createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[constraint])) | ||
149 | |||
150 | val result = saturate() | ||
151 | |||
152 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
153 | assertEquals(1, constraint.lowerBound) | ||
154 | assertEquals(6, constraint.upperBound) | ||
155 | } | ||
156 | |||
157 | @Test(expected=IllegalArgumentException) | ||
158 | def void unknownVariableTest() { | ||
159 | val x = new Dimension("x", 0, 1) | ||
160 | val y = new Dimension("y", 0, 1) | ||
161 | val constraint = new LinearConstraint(#{y -> 2}, 0, 2) | ||
162 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
163 | |||
164 | saturate() | ||
165 | } | ||
166 | |||
167 | @Test | ||
168 | def void unsatisfiableMultipleInheritanceTest() { | ||
169 | val x = new Dimension("x", 0, 1) | ||
170 | val y = new Dimension("y", 0, 1) | ||
171 | val z = new Dimension("z", 0, 1) | ||
172 | createSaturationOperator(new Polyhedron( | ||
173 | #[x, y, z], | ||
174 | #[ | ||
175 | new LinearConstraint(#{x -> 1, y -> 1}, 1, 1), | ||
176 | new LinearConstraint(#{x -> 1, z -> 1}, 1, 1), | ||
177 | new LinearConstraint(#{y -> 1, z -> 1}, 1, 1) | ||
178 | ], | ||
179 | #[x, y, z] | ||
180 | )) | ||
181 | |||
182 | val result = saturate() | ||
183 | |||
184 | assertEquals(PolyhedronSaturationResult.EMPTY, result) | ||
185 | } | ||
186 | |||
187 | @Test | ||
188 | def void unboundedRelaxationWithNoIntegerSolutionTest() { | ||
189 | val x = new Dimension("x", 0, 1) | ||
190 | val y = new Dimension("y", 0, null) | ||
191 | createSaturationOperator(new Polyhedron( | ||
192 | #[x, y], | ||
193 | #[new LinearConstraint(#{x -> 2}, 1, 1)], | ||
194 | #[x, y] | ||
195 | )) | ||
196 | |||
197 | val result = saturate() | ||
198 | |||
199 | assertEquals(PolyhedronSaturationResult.EMPTY, result) | ||
200 | } | ||
201 | |||
202 | private def createSaturationOperator(Polyhedron polyhedron) { | ||
203 | destroyOperatorIfExists() | ||
204 | operator = solver.createSaturationOperator(polyhedron) | ||
205 | } | ||
206 | |||
207 | private def destroyOperatorIfExists() { | ||
208 | if (operator !== null) { | ||
209 | operator.close | ||
210 | } | ||
211 | } | ||
212 | |||
213 | private def saturate() { | ||
214 | operator.saturate | ||
215 | } | ||
216 | } | ||
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend index 2d159752..b6d9b3b2 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend | |||
@@ -1,199 +1,10 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | 3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver |
9 | import org.junit.After | ||
10 | import org.junit.Before | ||
11 | import org.junit.Test | ||
12 | 4 | ||
13 | import static org.junit.Assert.* | 5 | class Z3PolyhedronSolverTest extends PolyhedronSolverTest { |
14 | 6 | ||
15 | class Z3PolyhedronSolverTest { | 7 | override protected createSolver() { |
16 | var Z3PolyhedronSolver solver | 8 | new Z3PolyhedronSolver(false) |
17 | var PolyhedronSaturationOperator operator | ||
18 | |||
19 | @Before | ||
20 | def void setUp() { | ||
21 | solver = new Z3PolyhedronSolver(false) | ||
22 | } | ||
23 | |||
24 | @After | ||
25 | def void tearDown() { | ||
26 | destroyOperatorIfExists() | ||
27 | } | ||
28 | |||
29 | @Test | ||
30 | def void singleDimensionTest() { | ||
31 | val x = new Dimension("x", 0, 1) | ||
32 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | ||
33 | |||
34 | val result = saturate() | ||
35 | |||
36 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
37 | assertEquals(0, x.lowerBound) | ||
38 | assertEquals(1, x.upperBound) | ||
39 | } | ||
40 | |||
41 | @Test | ||
42 | def void singleDimensionNegativeValueTest() { | ||
43 | val x = new Dimension("x", -2, -1) | ||
44 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | ||
45 | |||
46 | val result = saturate() | ||
47 | |||
48 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
49 | assertEquals(-2, x.lowerBound) | ||
50 | assertEquals(-1, x.upperBound) | ||
51 | } | ||
52 | |||
53 | @Test | ||
54 | def void singleDimensionConstraintTest() { | ||
55 | val x = new Dimension("x", null, null) | ||
56 | val constraint = new LinearConstraint(#{x -> 2}, 0, 2) | ||
57 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
58 | |||
59 | val result = saturate() | ||
60 | |||
61 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
62 | assertEquals(0, x.lowerBound) | ||
63 | assertEquals(1, x.upperBound) | ||
64 | } | ||
65 | |||
66 | @Test | ||
67 | def void singleDimensionConstraintUnitCoefficientTest() { | ||
68 | val x = new Dimension("x", null, null) | ||
69 | val constraint = new LinearConstraint(#{x -> 1}, 1, 3) | ||
70 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
71 | |||
72 | val result = saturate() | ||
73 | |||
74 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
75 | assertEquals(1, x.lowerBound) | ||
76 | assertEquals(3, x.upperBound) | ||
77 | } | ||
78 | |||
79 | @Test | ||
80 | def void singleDimensionConstraintIntegerTest() { | ||
81 | val x = new Dimension("x", null, null) | ||
82 | val constraint = new LinearConstraint(#{x -> 2}, 0, 3) | ||
83 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
84 | |||
85 | val result = saturate() | ||
86 | |||
87 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
88 | assertEquals(0, x.lowerBound) | ||
89 | assertEquals(1, x.upperBound) | ||
90 | } | ||
91 | |||
92 | @Test | ||
93 | def void singleDimensionUnboundedFromAboveTest() { | ||
94 | val x = new Dimension("x", 0, null) | ||
95 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | ||
96 | |||
97 | val result = saturate() | ||
98 | |||
99 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
100 | assertEquals(0, x.lowerBound) | ||
101 | assertEquals(null, x.upperBound) | ||
102 | } | ||
103 | |||
104 | @Test | ||
105 | def void singleDimensionUnboundedFromBelowTest() { | ||
106 | val x = new Dimension("x", null, 0) | ||
107 | createSaturationOperator(new Polyhedron(#[x], #[], #[x])) | ||
108 | |||
109 | val result = saturate() | ||
110 | |||
111 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
112 | assertEquals(null, x.lowerBound) | ||
113 | assertEquals(0, x.upperBound) | ||
114 | } | ||
115 | |||
116 | @Test | ||
117 | def void singleDimensionUnsatisfiableTest() { | ||
118 | val x = new Dimension("x", 0, 1) | ||
119 | val constraint = new LinearConstraint(#{x -> 2}, -2, -1) | ||
120 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
121 | |||
122 | val result = saturate() | ||
123 | |||
124 | assertEquals(PolyhedronSaturationResult.EMPTY, result) | ||
125 | } | ||
126 | |||
127 | @Test | ||
128 | def void equalityConstraintTest() { | ||
129 | val x = new Dimension("x", null, null) | ||
130 | val y = new Dimension("y", 1, 2) | ||
131 | val constraint = new LinearConstraint(#{x -> 2, y -> 2}, 6, 6) | ||
132 | createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[x])) | ||
133 | |||
134 | val result = saturate() | ||
135 | |||
136 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
137 | assertEquals(1, x.lowerBound) | ||
138 | assertEquals(2, x.upperBound) | ||
139 | } | ||
140 | |||
141 | @Test | ||
142 | def void saturateConstraintTest() { | ||
143 | val x = new Dimension("x", 0, 2) | ||
144 | val y = new Dimension("y", 1, 2) | ||
145 | val constraint = new LinearConstraint(#{x -> 2, y -> 1}, 0, 8) | ||
146 | createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[constraint])) | ||
147 | |||
148 | val result = saturate() | ||
149 | |||
150 | assertEquals(PolyhedronSaturationResult.SATURATED, result) | ||
151 | assertEquals(1, constraint.lowerBound) | ||
152 | assertEquals(6, constraint.upperBound) | ||
153 | } | ||
154 | |||
155 | @Test(expected=IllegalArgumentException) | ||
156 | def void unknownVariableTest() { | ||
157 | val x = new Dimension("x", 0, 1) | ||
158 | val y = new Dimension("y", 0, 1) | ||
159 | val constraint = new LinearConstraint(#{y -> 2}, 0, 2) | ||
160 | createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) | ||
161 | |||
162 | saturate() | ||
163 | } | ||
164 | |||
165 | @Test | ||
166 | def void unsatisfiableMultipleInheritanceTest() { | ||
167 | val x = new Dimension("x", 0, 1) | ||
168 | val y = new Dimension("y", 0, 1) | ||
169 | val z = new Dimension("z", 0, 1) | ||
170 | createSaturationOperator(new Polyhedron( | ||
171 | #[x, y, z], | ||
172 | #[ | ||
173 | new LinearConstraint(#{x -> 1, y -> 1}, 1, 1), | ||
174 | new LinearConstraint(#{x -> 1, z -> 1}, 1, 1), | ||
175 | new LinearConstraint(#{y -> 1, z -> 1}, 1, 1) | ||
176 | ], | ||
177 | #[x, y, z] | ||
178 | )) | ||
179 | |||
180 | val result = saturate() | ||
181 | |||
182 | assertEquals(PolyhedronSaturationResult.EMPTY, result) | ||
183 | } | ||
184 | |||
185 | private def createSaturationOperator(Polyhedron polyhedron) { | ||
186 | destroyOperatorIfExists() | ||
187 | operator = solver.createSaturationOperator(polyhedron) | ||
188 | } | ||
189 | |||
190 | private def destroyOperatorIfExists() { | ||
191 | if (operator !== null) { | ||
192 | operator.close | ||
193 | } | ||
194 | } | ||
195 | |||
196 | private def saturate() { | ||
197 | operator.saturate | ||
198 | } | 9 | } |
199 | } | 10 | } |