aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath15
-rw-r--r--Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.gitignore2
-rw-r--r--Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.project28
-rw-r--r--Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/META-INF/MANIFEST.MF10
-rw-r--r--Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/build.properties4
-rw-r--r--Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/CMakeLists.txt23
-rw-r--r--Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.cpp261
-rw-r--r--Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.hpp16
-rwxr-xr-xSolvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.sobin0 -> 38248 bytes
-rw-r--r--Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcException.java30
-rw-r--r--Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcResult.java54
-rw-r--r--Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java71
-rw-r--r--Solvers/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF3
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend4
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend182
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend31
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend216
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend197
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 @@
1Manifest-Version: 1.0
2Bundle-ManifestVersion: 2
3Bundle-Name: Cbc
4Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.ilp.cbc
5Bundle-Version: 1.0.0.qualifier
6Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.ilp.cbc
7Export-Package: hu.bme.mit.inf.dslreasoner.ilp.cbc
8Bundle-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 @@
1source.. = src/
2output.. = bin/
3bin.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 @@
1cmake_minimum_required(VERSION 3.14.5)
2project(hu.bme.mit.inf.dslreasoner.ilp.cbc)
3
4set(CMAKE_CXX_STANDARD 17)
5
6find_package(JNI REQUIRED)
7find_package(PkgConfig REQUIRED)
8
9pkg_check_modules(CBC REQUIRED cbc)
10
11add_library(viatracbc SHARED viatracbc.cpp)
12
13target_link_libraries(viatracbc
14 ${JAVA_JVM_LIBRARY}
15 ${CBC_LIBRARIES})
16target_include_directories(viatracbc
17 PUBLIC ${JNI_INCLUDE_DIRS}
18 PRIVATE ${CBC_INCLUDE_DIRS})
19
20set(VIATRACBC_NATIVES_DIR ${CMAKE_SOURCE_DIR}/../lib)
21add_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
26static const char *const kCbcExceptionClassName = "hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcException";
27static const char *const kRuntimeExceptionClassName = "java/lang/RuntimeException";
28
29static const jint kCbcSolutionBounded = 0;
30static const jint kCbcSolutionUnbounded = 1;
31static const jint kCbcUnsat = 2;
32static const jint kCbcAbandoned = 3;
33static const jint kCbcTimeout = 4;
34static const jint kCbcError = 5;
35
36static CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray,
37 jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray,
38 jdoubleArray entriedArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray,
39 jdoubleArray objectiveArray);
40static void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray,
41 jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, CoinModel &build);
42static void CreateModelRows(JNIEnv *env, jintArray rowStartsArray, jintArray columnIndicesArray,
43 jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray,
44 CoinModel &build);
45static jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdouble &value);
46static void ThrowException(JNIEnv *env, const char *message);
47
48template <
49 typename Array,
50 typename Element,
51 Element *(JNIEnv::*GetElementsPtr)(Array, jboolean *),
52 void (JNIEnv::*ReleaseElementsPtr)(Array, Element *, jint)
53>
54class PinnedArray {
55public:
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
73private:
74 JNIEnv *env_;
75 Array array_;
76 Element *elements_;
77};
78
79using PinnedIntArray = PinnedArray<jintArray, jint, &JNIEnv::GetIntArrayElements, &JNIEnv::ReleaseIntArrayElements>;
80using PinnedDoubleArray = PinnedArray<jdoubleArray, jdouble, &JNIEnv::GetDoubleArrayElements, &JNIEnv::ReleaseDoubleArrayElements>;
81
82jint 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
106CoinModel 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
117void 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
130void 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
147jint 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
245void 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
6extern "C" {
7
8JNIEXPORT 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 @@
1package hu.bme.mit.inf.dslreasoner.ilp.cbc;
2
3public 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 @@
1package hu.bme.mit.inf.dslreasoner.ilp.cbc;
2
3public 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 @@
1package hu.bme.mit.inf.dslreasoner.ilp.cbc;
2
3public 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
9Bundle-NativeCode: lib/libz3.so; 9Bundle-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"
28Bundle-RequiredExecutionEnvironment: JavaSE-1.8 29Bundle-RequiredExecutionEnvironment: JavaSE-1.8
29Import-Package: org.apache.log4j 30Import-Package: org.apache.log4j
30Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery 31Automatic-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
4import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel 4import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
5import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 5import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
6import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery 6import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator 8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator 9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy 10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns 11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns
12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries 12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries
13import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider 13import 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality
2
3import com.google.common.collect.ImmutableMap
4import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult
5import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver
6import java.util.Map
7import org.eclipse.xtend.lib.annotations.Accessors
8import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
9
10@FinalFieldsConstructor
11class 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
24class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension
5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult
7import org.junit.Test
8
9import static org.junit.Assert.*
10
11class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint
5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSolver
9import org.junit.After
10import org.junit.Before
11import org.junit.Test
12
13import static org.junit.Assert.*
14
15abstract 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality
2 2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint
5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver 3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
9import org.junit.After
10import org.junit.Before
11import org.junit.Test
12 4
13import static org.junit.Assert.* 5class Z3PolyhedronSolverTest extends PolyhedronSolverTest {
14 6
15class 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}
generated by cgit v1.2.3-54-g00ecf (git 2.45.1) at 2024-05-29 11:32:23 +0000