From b217dfc7e7bd7beb73c8cc23ad82383309ceb697 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 18 Jul 2019 15:21:56 +0200 Subject: Implement Coin-OR CBC polyhedron saturation operator --- .../hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath | 15 ++ .../hu.bme.mit.inf.dslreasoner.ilp.cbc/.gitignore | 2 + .../hu.bme.mit.inf.dslreasoner.ilp.cbc/.project | 28 +++ .../META-INF/MANIFEST.MF | 10 + .../build.properties | 4 + .../cpp/CMakeLists.txt | 23 ++ .../cpp/viatracbc.cpp | 261 +++++++++++++++++++++ .../cpp/viatracbc.hpp | 16 ++ .../lib/libviatracbc.so | Bin 0 -> 38248 bytes .../mit/inf/dslreasoner/ilp/cbc/CbcException.java | 30 +++ .../bme/mit/inf/dslreasoner/ilp/cbc/CbcResult.java | 54 +++++ .../bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java | 71 ++++++ 12 files changed, 514 insertions(+) create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.gitignore create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.project create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/META-INF/MANIFEST.MF create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/build.properties create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/CMakeLists.txt create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.cpp create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/viatracbc.hpp create mode 100755 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcException.java create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcResult.java create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/src/hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java (limited to 'Solvers/ILP-Solver') 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 @@ + + + + + + + + + + + + + + + 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 @@ +/bin/ +/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 @@ + + + hu.bme.mit.inf.dslreasoner.ilp.cbc + + + + + + org.eclipse.jdt.core.javabuilder + + + + + org.eclipse.pde.ManifestBuilder + + + + + org.eclipse.pde.SchemaBuilder + + + + + + org.eclipse.pde.PluginNature + org.eclipse.jdt.core.javanature + + 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 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: Cbc +Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.ilp.cbc +Bundle-Version: 1.0.0.qualifier +Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.ilp.cbc +Export-Package: hu.bme.mit.inf.dslreasoner.ilp.cbc +Bundle-NativeCode: libviatracbc.so; + osname=Linux; + 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 @@ +source.. = src/ +output.. = bin/ +bin.includes = META-INF/,\ + . 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 @@ +cmake_minimum_required(VERSION 3.14.5) +project(hu.bme.mit.inf.dslreasoner.ilp.cbc) + +set(CMAKE_CXX_STANDARD 17) + +find_package(JNI REQUIRED) +find_package(PkgConfig REQUIRED) + +pkg_check_modules(CBC REQUIRED cbc) + +add_library(viatracbc SHARED viatracbc.cpp) + +target_link_libraries(viatracbc + ${JAVA_JVM_LIBRARY} + ${CBC_LIBRARIES}) +target_include_directories(viatracbc + PUBLIC ${JNI_INCLUDE_DIRS} + PRIVATE ${CBC_INCLUDE_DIRS}) + +set(VIATRACBC_NATIVES_DIR ${CMAKE_SOURCE_DIR}/../lib) +add_custom_command(TARGET viatracbc POST_BUILD + COMMAND ${CMAKE_COMMAND} -E make_directory ${VIATRACBC_NATIVES_DIR} + COMMAND ${CMAKE_COMMAND} -E copy $ ${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 @@ + +#include +#include +#include +#include + +#include + +#include "CbcBranchDefaultDecision.hpp" +#include "CbcCompareDefault.hpp" +#include "CbcHeuristic.hpp" +#include "CbcHeuristicLocal.hpp" +#include "CbcModel.hpp" +#include "CglClique.hpp" +#include "CglFlowCover.hpp" +#include "CglGomory.hpp" +#include "CglKnapsackCover.hpp" +#include "CglMixedIntegerRounding.hpp" +#include "CglOddHole.hpp" +#include "CglProbing.hpp" +#include "CoinModel.hpp" +#include "OsiClpSolverInterface.hpp" + +#include "viatracbc.hpp" + +static const char *const kCbcExceptionClassName = "hu/bme/mit/inf/dslreasoner/ilp/cbc/CbcException"; +static const char *const kRuntimeExceptionClassName = "java/lang/RuntimeException"; + +static const jint kCbcSolutionBounded = 0; +static const jint kCbcSolutionUnbounded = 1; +static const jint kCbcUnsat = 2; +static const jint kCbcAbandoned = 3; +static const jint kCbcTimeout = 4; +static const jint kCbcError = 5; + +static CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, + jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, + jdoubleArray entriedArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, + jdoubleArray objectiveArray); +static void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, + jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, CoinModel &build); +static void CreateModelRows(JNIEnv *env, jintArray rowStartsArray, jintArray columnIndicesArray, + jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, + CoinModel &build); +static jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdouble &value); +static void ThrowException(JNIEnv *env, const char *message); + +template < + typename Array, + typename Element, + Element *(JNIEnv::*GetElementsPtr)(Array, jboolean *), + void (JNIEnv::*ReleaseElementsPtr)(Array, Element *, jint) +> +class PinnedArray { +public: + PinnedArray(JNIEnv *env, Array array) + : env_{env}, array_{array}, elements_{(env->*GetElementsPtr)(array, nullptr)} { + if (elements_ == nullptr) { + throw std::runtime_error("Failed to pin array elements"); + } + } + PinnedArray(const PinnedArray &) = delete; + PinnedArray(PinnedArray &&) = delete; + PinnedArray &operator=(const PinnedArray &) = delete; + PinnedArray &operator=(PinnedArray &&) = delete; + ~PinnedArray() { + (env_->*ReleaseElementsPtr)(array_, elements_, 0); + } + + operator Element *() { return elements_; } + operator const Element *() const { return elements_; } + +private: + JNIEnv *env_; + Array array_; + Element *elements_; +}; + +using PinnedIntArray = PinnedArray; +using PinnedDoubleArray = PinnedArray; + +jint Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIlpProblem( + JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, + jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, + jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, + jdoubleArray outputArray, jdouble timeoutSeconds, jboolean silent) { + try { + auto build = CreateModel(env, columnLowerBoundsArray, columnUpperBoundsArray, + rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, rowUpperBoundsArray, + objectiveArray); + double value; + jint result = SolveModel(build, timeoutSeconds, silent, value); + if (result == kCbcSolutionBounded) { + PinnedDoubleArray output{env, outputArray}; + *output = value; + } + return result; + } catch (const std::exception &e) { + ThrowException(env, e.what()); + } catch (...) { + ThrowException(env, "Unknown solver error"); + } + return kCbcError; +} + +CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, + jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, + jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, + jdoubleArray objectiveArray) { + CoinModel build; + CreateModelColumns(env, columnLowerBoundsArray, columnUpperBoundsArray, objectiveArray, build); + CreateModelRows(env, rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, + rowUpperBoundsArray, build); + return build; +} + +void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, + jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, CoinModel &build) { + int numColumns = env->GetArrayLength(columnLowerBoundsArray); + PinnedDoubleArray columnLowerBounds{env, columnLowerBoundsArray}; + PinnedDoubleArray columnUpperBounds{env, columnUpperBoundsArray}; + PinnedDoubleArray objective{env, objectiveArray}; + for (int i = 0; i < numColumns; i++) { + build.setColumnBounds(i, columnLowerBounds[i], columnUpperBounds[i]); + build.setObjective(i, objective[i]); + build.setInteger(i); + } +} + +void CreateModelRows(JNIEnv *env, jintArray rowStartsArray, jintArray columnIndicesArray, + jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, + CoinModel &build) { + int numRows = env->GetArrayLength(rowLowerBoundsArray); + PinnedIntArray rowStarts{env, rowStartsArray}; + PinnedIntArray columnIndices{env, columnIndicesArray}; + PinnedDoubleArray entries{env, entriesArray}; + PinnedDoubleArray rowLowerBounds{env, rowLowerBoundsArray}; + PinnedDoubleArray rowUpperBounds{env, rowUpperBoundsArray}; + for (int i = 0; i < numRows; i++) { + int rowStart = rowStarts[i]; + int numbersInRow = rowStarts[i + 1] - rowStart; + build.addRow(numbersInRow, &columnIndices[rowStart], &entries[rowStart], + rowLowerBounds[i], rowUpperBounds[i]); + } +} + +jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdouble &value) { + OsiClpSolverInterface solver; + solver.loadFromCoinModel(build); + CbcModel model{solver}; + + model.setDblParam(CbcModel::CbcMaximumSeconds, timeoutSeconds); + if (silent == JNI_FALSE) { + model.messageHandler()->setLogLevel(2); + model.solver()->messageHandler()->setLogLevel(1); + } else { + model.solver()->setHintParam(OsiDoReducePrint, true, OsiHintTry); + model.messageHandler()->setLogLevel(0); + model.solver()->messageHandler()->setLogLevel(0); + } + + // Cut generators and heuristics are used according to + // https://github.com/coin-or/Cbc/blob/6b977b6707f1755520c64fea57b95891c1f3ddc0/Cbc/examples/sample2.cpp + + CglProbing probing; + probing.setUsingObjective(true); + probing.setMaxPass(1); + probing.setMaxPassRoot(5); + probing.setMaxProbe(10); + probing.setMaxProbeRoot(1000); + probing.setMaxLook(50); + probing.setMaxLookRoot(500); + probing.setMaxElements(200); + probing.setRowCuts(3); + model.addCutGenerator(&probing, -1, "Probing"); + + CglGomory gomory; + gomory.setLimit(300); + model.addCutGenerator(&gomory, -1, "Gomory"); + + CglKnapsackCover knapsackCover; + model.addCutGenerator(&knapsackCover, -1, "KnapsackCover"); + + CglClique clique; + clique.setStarCliqueReport(false); + clique.setRowCliqueReport(false); + model.addCutGenerator(&clique, -1, "Clique"); + + CglFlowCover flowCover; + model.addCutGenerator(&flowCover, -1, "FlowCover"); + + CglMixedIntegerRounding mixedIntegerRounding; + model.addCutGenerator(&mixedIntegerRounding, -1, "MixedIntegerRounding"); + + OsiClpSolverInterface *osiClp = dynamic_cast(model.solver()); + if (osiClp != nullptr) { + osiClp->setSpecialOptions(128); + osiClp->setupForRepeatedUse(0, 0); + } + + CbcRounding rounding; + model.addHeuristic(&rounding); + + CbcHeuristicLocal localHeuristic; + model.addHeuristic(&localHeuristic); + + CbcBranchDefaultDecision branchDecision; + model.setBranchingMethod(&branchDecision); + + CbcCompareDefault nodeComparison; + model.setNodeComparison(nodeComparison); + + model.initialSolve(); + + if (model.isInitialSolveProvenPrimalInfeasible()) { + return kCbcUnsat; + } + if (model.isInitialSolveAbandoned()) { + return kCbcTimeout; + } + + model.setMinimumDrop(CoinMin(1.0, fabs(model.getMinimizationObjValue()) * 1.0e-3 + 1.0e-4)); + model.setMaximumCutPassesAtRoot(-100); + model.setNumberStrong(10); + model.solver()->setIntParam(OsiMaxNumIterationHotStart, 100); + + model.branchAndBound(); + + if (model.isProvenInfeasible()) { + return kCbcUnsat; + } + if (model.isProvenDualInfeasible()) { + return kCbcSolutionUnbounded; + } + if (model.isProvenOptimal()) { + value = model.getMinimizationObjValue(); + return kCbcSolutionBounded; + } + if (model.maximumSecondsReached()) { + return kCbcTimeout; + } + return kCbcAbandoned; +} + +void ThrowException(JNIEnv *env, const char *message) { + jclass exceptionClass = env->FindClass(kCbcExceptionClassName); + if (exceptionClass == nullptr) { + std::cerr << "WARNING: " << kCbcExceptionClassName << " class was not found" << std::endl; + exceptionClass = env->FindClass(kRuntimeExceptionClassName); + if (exceptionClass == nullptr) { + std::cerr << "FATAL: " << kRuntimeExceptionClassName << " class was not found" << std::endl; + std::cerr << "FATAL: " << message << std::endl; + std::exit(EXIT_FAILURE); + } + } + if (env->ThrowNew(exceptionClass, message) < 0) { + std::cerr << "FATAL: Could not throw java exception" << std::endl; + std::cerr << "FATAL: " << message << std::endl; + std::exit(EXIT_FAILURE); + } +} 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 @@ +#ifndef HU_BME_MIT_INF_DSLREASONER_ILP_CBC_ +#define HU_BME_MIT_INF_DSLREASONER_ILP_CBC_ + +#include + +extern "C" { + +JNIEXPORT jint JNICALL Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIlpProblem( + JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, + jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, + jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, + jdoubleArray outputArray, jdouble timeoutSeconds, jboolean silent); + +} + +#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 Binary files /dev/null and b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so 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 @@ +package hu.bme.mit.inf.dslreasoner.ilp.cbc; + +public class CbcException extends RuntimeException { + + /** + * + */ + private static final long serialVersionUID = 2691773509078511887L; + + public CbcException() { + super(); + } + + public CbcException(String message, Throwable cause, boolean enableSuppression, boolean writableStackTrace) { + super(message, cause, enableSuppression, writableStackTrace); + } + + public CbcException(String message, Throwable cause) { + super(message, cause); + } + + public CbcException(String message) { + super(message); + } + + public CbcException(Throwable cause) { + super(cause); + } + +} 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 @@ +package hu.bme.mit.inf.dslreasoner.ilp.cbc; + +public abstract class CbcResult { + public static final CbcResult SOLUTION_UNBOUNDED = new CbcResult() { + }; + + public static final CbcResult UNSAT = new CbcResult() { + }; + + public static final CbcResult ABANDONED = new CbcResult() { + }; + + public static final CbcResult TIMEOUT = new CbcResult() { + }; + + private CbcResult() { + } + + public static class SolutionBounded extends CbcResult { + public final double value; + + public SolutionBounded(double value) { + this.value = value; + } + + public double getValue() { + return value; + } + + @Override + public int hashCode() { + final int prime = 31; + int result = 1; + long temp; + temp = Double.doubleToLongBits(value); + result = prime * result + (int) (temp ^ (temp >>> 32)); + return result; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + SolutionBounded other = (SolutionBounded) obj; + if (Double.doubleToLongBits(value) != Double.doubleToLongBits(other.value)) + return false; + return true; + } + } +} 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 @@ +package hu.bme.mit.inf.dslreasoner.ilp.cbc; + +public class CbcSolver { + private static int CBC_SOLUTION_BOUNDED = 0; + private static int CBC_SOLUTION_UNBOUNDED = 1; + private static int CBC_UNSAT = 2; + private static int CBC_ABANDONED = 3; + private static int CBC_TIMEOUT = 4; + private static int CBC_ERROR = 5; + + private static boolean nativesLoaded = false; + + private CbcSolver() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly."); + } + + public static CbcResult solve(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, + int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, + double[] objective, double timeoutSeconds, boolean silent) { + loadNatives(); + validate(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, rowLowerBounds, + rowUpperBounds, objective); + double[] output = new double[1]; + int result = solveIlpProblem(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, + rowLowerBounds, rowUpperBounds, objective, output, timeoutSeconds, silent); + if (result == CBC_SOLUTION_BOUNDED) { + return new CbcResult.SolutionBounded(output[0]); + } else if (result == CBC_SOLUTION_UNBOUNDED) { + return CbcResult.SOLUTION_UNBOUNDED; + } else if (result == CBC_UNSAT) { + return CbcResult.UNSAT; + } else if (result == CBC_ABANDONED) { + return CbcResult.ABANDONED; + } else if (result == CBC_TIMEOUT) { + return CbcResult.TIMEOUT; + } else if (result == CBC_ERROR) { + throw new CbcException("Solver signalled error, but no exception was thrown"); + } else { + throw new CbcException("Unknown return value: " + result); + } + } + + private static void loadNatives() { + if (!nativesLoaded) { + synchronized (CbcSolver.class) { + System.loadLibrary("viatracbc"); + nativesLoaded = true; + } + } + } + + private static void validate(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, + int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, + double[] objective) { + int numColumns = columnLowerBounds.length; + if (columnUpperBounds.length != numColumns) { + throw new CbcException("Lengths of columnLowerBounds and columnUpperBounds must match"); + } + if (objective.length != numColumns) { + throw new CbcException("Lengths of columnLowerBounds and objective must match"); + } + int numRows = rowLowerBounds.length; + if (rowUpperBounds.length != numRows) { + throw new CbcException("Lengths of rowLowerBounds and rowUpperBounds must match"); + } + } + + private static native int solveIlpProblem(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, + int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, double[] objective, + double[] output, double timeoutSeconds, boolean silent); +} -- cgit v1.2.3-54-g00ecf From b4bf8d387e430600790f6b30d9e88ec785148cd7 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 29 Jul 2019 14:21:36 +0200 Subject: Make CbcPolyhedronSolver more robust --- .../cpp/viatracbc.cpp | 54 +++++--- .../cpp/viatracbc.hpp | 2 +- .../lib/libviatracbc.so | Bin 38248 -> 33944 bytes .../bme/mit/inf/dslreasoner/ilp/cbc/CbcSolver.java | 8 +- .../cardinality/CbcPolyhedronSolver.xtend | 154 +++++++++++++-------- .../cardinality/CbcPolyhedronSolverTest.xtend | 14 +- .../tests/cardinality/PolyhedronSolverTest.xtend | 107 ++++++++++++-- 7 files changed, 240 insertions(+), 99 deletions(-) (limited to 'Solvers/ILP-Solver') 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 index 49994244..ffd35759 100644 --- 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 @@ -36,9 +36,10 @@ static const jint kCbcError = 5; static CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriedArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, - jdoubleArray objectiveArray); + jdoubleArray objectiveArray, jboolean lpRelaxation); static void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, - jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, CoinModel &build); + jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, jboolean lpRelaxation, + CoinModel &build); static void CreateModelRows(JNIEnv *env, jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, CoinModel &build); @@ -83,11 +84,11 @@ jint Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIlpProblem( JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, - jdoubleArray outputArray, jdouble timeoutSeconds, jboolean silent) { + jdoubleArray outputArray, jboolean lpRelaxation, jdouble timeoutSeconds, jboolean silent) { try { auto build = CreateModel(env, columnLowerBoundsArray, columnUpperBoundsArray, rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, rowUpperBoundsArray, - objectiveArray); + objectiveArray, lpRelaxation); double value; jint result = SolveModel(build, timeoutSeconds, silent, value); if (result == kCbcSolutionBounded) { @@ -106,16 +107,18 @@ jint Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIlpProblem( CoinModel CreateModel(JNIEnv *env, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, - jdoubleArray objectiveArray) { + jdoubleArray objectiveArray, jboolean lpRelaxation) { CoinModel build; - CreateModelColumns(env, columnLowerBoundsArray, columnUpperBoundsArray, objectiveArray, build); + CreateModelColumns(env, columnLowerBoundsArray, columnUpperBoundsArray, objectiveArray, + lpRelaxation, build); CreateModelRows(env, rowStartsArray, columnIndicesArray, entriesArray, rowLowerBoundsArray, rowUpperBoundsArray, build); return build; } void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, - jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, CoinModel &build) { + jdoubleArray columnUpperBoundsArray, jdoubleArray objectiveArray, jboolean lpRelaxation, + CoinModel &build) { int numColumns = env->GetArrayLength(columnLowerBoundsArray); PinnedDoubleArray columnLowerBounds{env, columnLowerBoundsArray}; PinnedDoubleArray columnUpperBounds{env, columnUpperBoundsArray}; @@ -123,7 +126,9 @@ void CreateModelColumns(JNIEnv *env, jdoubleArray columnLowerBoundsArray, for (int i = 0; i < numColumns; i++) { build.setColumnBounds(i, columnLowerBounds[i], columnUpperBounds[i]); build.setObjective(i, objective[i]); - build.setInteger(i); + if (!lpRelaxation) { + build.setInteger(i); + } } } @@ -215,6 +220,9 @@ jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdoub if (model.isInitialSolveProvenPrimalInfeasible()) { return kCbcUnsat; } + if (model.isInitialSolveProvenDualInfeasible()) { + return kCbcSolutionUnbounded; + } if (model.isInitialSolveAbandoned()) { return kCbcTimeout; } @@ -226,20 +234,26 @@ jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdoub model.branchAndBound(); - if (model.isProvenInfeasible()) { - return kCbcUnsat; - } - if (model.isProvenDualInfeasible()) { - return kCbcSolutionUnbounded; - } - if (model.isProvenOptimal()) { - value = model.getMinimizationObjValue(); - return kCbcSolutionBounded; - } - if (model.maximumSecondsReached()) { + switch (model.status()) { + case 0: + if (model.isProvenInfeasible()) { + return kCbcUnsat; + } + if (model.isProvenDualInfeasible()) { + return kCbcSolutionUnbounded; + } + if (model.isProvenOptimal()) { + value = model.getMinimizationObjValue(); + return kCbcSolutionBounded; + } + throw std::runtime_error("CBC status is 0, but no solution is found"); + case 1: return kCbcTimeout; + case 2: + return kCbcAbandoned; + default: + throw std::runtime_error("Unknown CBC status"); } - return kCbcAbandoned; } void ThrowException(JNIEnv *env, const char *message) { 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 index c65f71e3..12198c8b 100644 --- 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 @@ -9,7 +9,7 @@ JNIEXPORT jint JNICALL Java_hu_bme_mit_inf_dslreasoner_ilp_cbc_CbcSolver_solveIl JNIEnv *env, jclass klazz, jdoubleArray columnLowerBoundsArray, jdoubleArray columnUpperBoundsArray, jintArray rowStartsArray, jintArray columnIndicesArray, jdoubleArray entriesArray, jdoubleArray rowLowerBoundsArray, jdoubleArray rowUpperBoundsArray, jdoubleArray objectiveArray, - jdoubleArray outputArray, jdouble timeoutSeconds, jboolean silent); + jdoubleArray outputArray, jboolean lpRelaxation, jdouble timeoutSeconds, jboolean silent); } 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 index 21fd2ff2..4eae7de6 100755 Binary files a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so and b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so differ 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 index 39b9d537..085d4448 100644 --- 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 @@ -15,14 +15,14 @@ public class CbcSolver { } public static CbcResult solve(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, - int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, - double[] objective, double timeoutSeconds, boolean silent) { + int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, double[] objective, + boolean lpRelaxation, double timeoutSeconds, boolean silent) { loadNatives(); validate(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, rowLowerBounds, rowUpperBounds, objective); double[] output = new double[1]; int result = solveIlpProblem(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, entries, - rowLowerBounds, rowUpperBounds, objective, output, timeoutSeconds, silent); + rowLowerBounds, rowUpperBounds, objective, output, lpRelaxation, timeoutSeconds, silent); if (result == CBC_SOLUTION_BOUNDED) { return new CbcResult.SolutionBounded(output[0]); } else if (result == CBC_SOLUTION_UNBOUNDED) { @@ -67,5 +67,5 @@ public class CbcSolver { private static native int solveIlpProblem(double[] columnLowerBounds, double[] columnUpperBounds, int[] rowStarts, int[] columnIndices, double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, double[] objective, - double[] output, double timeoutSeconds, boolean silent); + double[] output, boolean lpRelaxation, double timeoutSeconds, boolean silent); } 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 index 7753e68e..4bd46fbf 100644 --- 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 @@ -1,27 +1,32 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality +import com.google.common.collect.ImmutableList import com.google.common.collect.ImmutableMap import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcResult import hu.bme.mit.inf.dslreasoner.ilp.cbc.CbcSolver +import java.util.HashSet import java.util.List import java.util.Map +import java.util.Set import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor @FinalFieldsConstructor class CbcPolyhedronSolver implements PolyhedronSolver { + val boolean lpRelaxation val double timeoutSeconds val boolean silent new() { - this(10, true) + this(false, -1, true) } override createSaturationOperator(Polyhedron polyhedron) { - new CbcSaturationOperator(polyhedron, timeoutSeconds, silent) + new CbcSaturationOperator(polyhedron, lpRelaxation, timeoutSeconds, silent) } } class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { + val boolean lpRelaxation val double timeoutSeconds val boolean silent val double[] columnLowerBounds @@ -29,8 +34,9 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { val double[] objective val Map dimensionsToIndicesMap - new(Polyhedron polyhedron, double timeoutSeconds, boolean silent) { + new(Polyhedron polyhedron, boolean lpRelaxation, double timeoutSeconds, boolean silent) { super(polyhedron) + this.lpRelaxation = lpRelaxation this.timeoutSeconds = timeoutSeconds this.silent = silent val numDimensions = polyhedron.dimensions.size @@ -56,6 +62,12 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { rowStarts.set(numConstraints, numEntries) val columnIndices = newIntArrayOfSize(numEntries) val entries = newDoubleArrayOfSize(numEntries) + val unconstrainedDimensions = new HashSet + for (dimension : polyhedron.dimensions) { + if (dimension.lowerBound === null && dimension.upperBound === null) { + unconstrainedDimensions += dimension + } + } var int index = 0 for (var int i = 0; i < numConstraints; i++) { rowStarts.set(i, index) @@ -69,6 +81,7 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { val dimension = polyhedron.dimensions.get(j) val coefficient = constraint.coefficients.get(dimension) if (coefficient !== null && coefficient != 0) { + unconstrainedDimensions -= dimension columnIndices.set(index, j) entries.set(index, coefficient) index++ @@ -79,71 +92,94 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator { throw new AssertionError("Last entry does not equal the number of entries in the constraint matrix") } for (expressionToSaturate : polyhedron.expressionsToSaturate) { - for (var int j = 0; j < numDimensions; j++) { - objective.set(j, 0) + val result = saturate(expressionToSaturate, rowStarts, columnIndices, entries, rowLowerBounds, + rowUpperBounds, unconstrainedDimensions, constraints) + if (result != PolyhedronSaturationResult.SATURATED) { + return result } - switch (expressionToSaturate) { - Dimension: { - val j = getIndex(expressionToSaturate) - objective.set(j, 1) + } + PolyhedronSaturationResult.SATURATED + } + + protected def saturate(LinearBoundedExpression expressionToSaturate, int[] rowStarts, int[] columnIndices, + double[] entries, double[] rowLowerBounds, double[] rowUpperBounds, Set unconstrainedDimensions, + ImmutableList constraints) { + val numDimensions = objective.size + for (var int j = 0; j < numDimensions; j++) { + objective.set(j, 0) + } + switch (expressionToSaturate) { + Dimension: { + // CBC will return nonsensical results or call free() with invalid arguments if + // it is passed a fully unconstrained (-Inf lower and +Int upper bound, no inequalities) variable + // in the objective function. + if (unconstrainedDimensions.contains(expressionToSaturate)) { + return PolyhedronSaturationResult.SATURATED } - LinearConstraint: { - for (pair : expressionToSaturate.coefficients.entrySet) { - val j = getIndex(pair.key) - objective.set(j, pair.value) + val j = getIndex(expressionToSaturate) + objective.set(j, 1) + } + LinearConstraint: { + for (pair : expressionToSaturate.coefficients.entrySet) { + val dimension = pair.key + // We also have to check for unconstrained dimensions here to avoid crashing. + if (unconstrainedDimensions.contains(dimension)) { + expressionToSaturate.lowerBound = null + expressionToSaturate.upperBound = null + return PolyhedronSaturationResult.SATURATED } + val j = getIndex(dimension) + objective.set(j, pair.value) } - default: - throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate) } - val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, - entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) - switch (minimizationResult) { - CbcResult.SolutionBounded: { - val value = Math.floor(minimizationResult.value) - expressionToSaturate.lowerBound = value as int - setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds) - } - case CbcResult.SOLUTION_UNBOUNDED: { - expressionToSaturate.lowerBound = null - setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, - rowLowerBounds) - } - case CbcResult.UNSAT: - return PolyhedronSaturationResult.EMPTY - case CbcResult.ABANDONED, - case CbcResult.TIMEOUT: - return PolyhedronSaturationResult.UNKNOWN - default: - throw new RuntimeException("Unknown CbcResult: " + minimizationResult) + default: + throw new IllegalArgumentException("Unknown expression: " + expressionToSaturate) + } + val minimizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, + entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) + switch (minimizationResult) { + CbcResult.SolutionBounded: { + val value = Math.floor(minimizationResult.value) + expressionToSaturate.lowerBound = value as int + setBound(expressionToSaturate, constraints, value, columnLowerBounds, rowLowerBounds) } - for (var int j = 0; j < numDimensions; j++) { - val objectiveCoefficient = objective.get(j) - objective.set(j, -objectiveCoefficient) + case CbcResult.SOLUTION_UNBOUNDED: { + expressionToSaturate.lowerBound = null + setBound(expressionToSaturate, constraints, Double.NEGATIVE_INFINITY, columnLowerBounds, rowLowerBounds) } - val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, - entries, rowLowerBounds, rowUpperBounds, objective, timeoutSeconds, silent) - switch (maximizationResult) { - CbcResult.SolutionBounded: { - val value = Math.ceil(-maximizationResult.value) - expressionToSaturate.upperBound = value as int - setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds) - } - case CbcResult.SOLUTION_UNBOUNDED: { - expressionToSaturate.upperBound = null - setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, - rowUpperBounds) - } - case CbcResult.UNSAT: - throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") - case CbcResult.ABANDONED, - case CbcResult.TIMEOUT: - return PolyhedronSaturationResult.UNKNOWN - default: - throw new RuntimeException("Unknown CbcResult: " + maximizationResult) + case CbcResult.UNSAT: + return PolyhedronSaturationResult.EMPTY + case CbcResult.ABANDONED, + case CbcResult.TIMEOUT: + return PolyhedronSaturationResult.UNKNOWN + default: + throw new RuntimeException("Unknown CbcResult: " + minimizationResult) + } + for (var int j = 0; j < numDimensions; j++) { + val objectiveCoefficient = objective.get(j) + objective.set(j, -objectiveCoefficient) + } + val maximizationResult = CbcSolver.solve(columnLowerBounds, columnUpperBounds, rowStarts, columnIndices, + entries, rowLowerBounds, rowUpperBounds, objective, lpRelaxation, timeoutSeconds, silent) + switch (maximizationResult) { + CbcResult.SolutionBounded: { + val value = Math.ceil(-maximizationResult.value) + expressionToSaturate.upperBound = value as int + setBound(expressionToSaturate, constraints, value, columnUpperBounds, rowUpperBounds) } + case CbcResult.SOLUTION_UNBOUNDED: { + expressionToSaturate.upperBound = null + setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds) + } + case CbcResult.UNSAT: + throw new RuntimeException("Minimization was SAT, but maximization is UNSAT") + case CbcResult.ABANDONED, + case CbcResult.TIMEOUT: + return PolyhedronSaturationResult.UNKNOWN + default: + throw new RuntimeException("Unknown CbcResult: " + maximizationResult) } - PolyhedronSaturationResult.SATURATED + return PolyhedronSaturationResult.SATURATED } private def toDouble(Integer nullableInt, double defaultValue) { 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 index a51aa082..b22e2a20 100644 --- 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 @@ -7,11 +7,19 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedr import org.junit.Test import static org.junit.Assert.* +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint class CbcPolyhedronSolverTest extends IntegerPolyhedronSolverTest { override protected createSolver() { - new CbcPolyhedronSolver(10, true) + new CbcPolyhedronSolver(false, 10, true) + } +} + +class RelaxedCbcPolyhedronSolverTest extends RelaxedPolyhedronSolverTest { + + override protected createSolver() { + new CbcPolyhedronSolver(true, 10, true) } } @@ -19,9 +27,9 @@ class CbcPolyhedronSolverTimeoutTest { @Test def void timeoutTest() { - val solver = new CbcPolyhedronSolver(0, true) + val solver = new CbcPolyhedronSolver(false, 0, true) val x = new Dimension("x", 0, 1) - val polyhedron = new Polyhedron(#[x], #[], #[x]) + val polyhedron = new Polyhedron(#[x], #[new LinearConstraint(#{x -> 1}, null, 0)], #[x]) val operator = solver.createSaturationOperator(polyhedron) try { val result = operator.saturate 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 index 1b2dcb00..47534618 100644 --- 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 @@ -80,26 +80,52 @@ abstract class PolyhedronSolverTest { @Test def void singleDimensionUnboundedFromAboveTest() { - val x = new Dimension("x", 0, null) + val x = new Dimension("x", -2, null) createSaturationOperator(new Polyhedron(#[x], #[], #[x])) val result = saturate() assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(0, x.lowerBound) + assertEquals(-2, x.lowerBound) assertEquals(null, x.upperBound) } @Test def void singleDimensionUnboundedFromBelowTest() { - val x = new Dimension("x", null, 0) + val x = new Dimension("x", null, 2) createSaturationOperator(new Polyhedron(#[x], #[], #[x])) val result = saturate() assertEquals(PolyhedronSaturationResult.SATURATED, result) assertEquals(null, x.lowerBound) - assertEquals(0, x.upperBound) + assertEquals(2, x.upperBound) + } + + @Test + def void singleDimensionUnboundedTest() { + val x = new Dimension("x", null, null) + createSaturationOperator(new Polyhedron(#[x], #[], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(null, x.lowerBound) + assertEquals(null, x.upperBound) + } + + @Test + def void singleDimensionUnboundedObjectiveTest() { + val x = new Dimension("x", null, null) + val y = new Dimension("y", 0, 1) + val objective = new LinearConstraint(#{x -> 1, y -> 1}, null, null) + createSaturationOperator(new Polyhedron(#[x, y], #[], #[objective])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(null, objective.lowerBound) + assertEquals(null, objective.upperBound) } @Test @@ -174,6 +200,25 @@ abstract class PolyhedronSolverTest { assertEquals(PolyhedronSaturationResult.EMPTY, result) } + + @Test + def void unboundedRelaxationWithIntegerSolutionTest() { + val x = new Dimension("x", 1, 3) + val y = new Dimension("y", null, null) + createSaturationOperator(new Polyhedron( + #[x, y], + #[new LinearConstraint(#{x -> 2}, 2, 6)], + #[x, y] + )) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, x.lowerBound) + assertEquals(3, x.upperBound) + assertEquals(null, y.lowerBound) + assertEquals(null, y.upperBound) + } protected def createSaturationOperator(Polyhedron polyhedron) { destroyOperatorIfExists() @@ -228,7 +273,7 @@ abstract class IntegerPolyhedronSolverTest extends PolyhedronSolverTest { @Test def void unboundedRelaxationWithNoIntegerSolutionTest() { val x = new Dimension("x", 0, 1) - val y = new Dimension("y", 0, null) + val y = new Dimension("y", null, null) createSaturationOperator(new Polyhedron( #[x, y], #[new LinearConstraint(#{x -> 2}, 1, 1)], @@ -282,21 +327,59 @@ abstract class RelaxedPolyhedronSolverTest extends PolyhedronSolverTest { } @Test - def void unboundedRelaxationWithNoIntegerSolutionTest() { - val x = new Dimension("x", 0, 1) - val y = new Dimension("y", 0, null) + def void unboundedRelaxationWithNoIntegerSolutionUnconstrainedVariableTest() { + val x = new Dimension("x", 1, 2) + val y = new Dimension("y", null, null) createSaturationOperator(new Polyhedron( #[x, y], - #[new LinearConstraint(#{x -> 2}, 1, 1)], + #[new LinearConstraint(#{x -> 2}, 3, 3)], #[x, y] )) val result = saturate() assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(0, x.lowerBound) - assertEquals(1, x.upperBound) - assertEquals(0, y.lowerBound) + assertEquals(1, x.lowerBound) + assertEquals(2, x.upperBound) + assertEquals(null, y.lowerBound) assertEquals(null, y.upperBound) } + + @Test + def void unboundedRelaxationWithNoIntegerSolutionConstrainedVariableTest() { + val x = new Dimension("x", 1, 2) + val y = new Dimension("y", null, null) + createSaturationOperator(new Polyhedron( + #[x, y], + #[new LinearConstraint(#{x -> 2}, 3, 3), new LinearConstraint(#{y -> 1}, null, 1)], + #[x, y] + )) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, x.lowerBound) + assertEquals(2, x.upperBound) + assertEquals(null, y.lowerBound) + assertEquals(1, y.upperBound) + } + + @Test + def void unboundedRelaxationWithNoIntegerSolutionBoundedVariableTest() { + val x = new Dimension("x", 1, 2) + val y = new Dimension("y", null, 1) + createSaturationOperator(new Polyhedron( + #[x, y], + #[new LinearConstraint(#{x -> 2}, 3, 3)], + #[x, y] + )) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, x.lowerBound) + assertEquals(2, x.upperBound) + assertEquals(null, y.lowerBound) + assertEquals(1, y.upperBound) + } } -- cgit v1.2.3-54-g00ecf From 83f8384f66ddb1d86567c928bdb102174c70cba0 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 29 Jul 2019 15:36:28 +0200 Subject: Fix CBC timeout --- .../cpp/viatracbc.cpp | 4 +++- .../lib/libviatracbc.so | Bin 33944 -> 33944 bytes .../cardinality/PolyhedronScopePropagator.xtend | 2 +- .../reasoner/ViatraReasonerConfiguration.xtend | 2 +- 4 files changed, 5 insertions(+), 3 deletions(-) (limited to 'Solvers/ILP-Solver') 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 index ffd35759..34cab1dd 100644 --- 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 @@ -154,7 +154,9 @@ jint SolveModel(CoinModel &build, jdouble timeoutSeconds, jboolean silent, jdoub solver.loadFromCoinModel(build); CbcModel model{solver}; - model.setDblParam(CbcModel::CbcMaximumSeconds, timeoutSeconds); + if (timeoutSeconds >= 0) { + model.setDblParam(CbcModel::CbcMaximumSeconds, timeoutSeconds); + } if (silent == JNI_FALSE) { model.messageHandler()->setLogLevel(2); model.solver()->messageHandler()->setLogLevel(1); 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 index 4eae7de6..96289216 100755 Binary files a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so and b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so differ diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend index 3fd50071..a3977653 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend @@ -63,6 +63,7 @@ class PolyhedronScopePropagator extends ScopePropagator { populatePolyhedronFromScope() // println(polyhedron) val result = operator.saturate() +// println(polyhedron) if (result == PolyhedronSaturationResult.EMPTY) { throw new IllegalStateException("Scope bounds cannot be satisfied") } else { @@ -71,7 +72,6 @@ class PolyhedronScopePropagator extends ScopePropagator { super.propagateAllScopeConstraints() } } -// println(polyhedron) } def resetBounds() { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index 3c9ef74c..7a3a2d67 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend @@ -51,7 +51,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { */ public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint - public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.PolyhedralRelations + public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.PolyhedralTypeHierarchy public var List costObjectives = newArrayList } -- cgit v1.2.3-54-g00ecf From 51f3e80dabc0c500cf9154a25a7d4a1c55760707 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 1 Aug 2019 00:58:50 +0200 Subject: Build Cbc wrapper under Ubuntu 18.04 --- .../ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/cpp/CMakeLists.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Solvers/ILP-Solver') 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 index 5dbcb071..6169ae8f 100644 --- 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 @@ -1,7 +1,7 @@ -cmake_minimum_required(VERSION 3.14.5) +cmake_minimum_required(VERSION 3.10.2) project(hu.bme.mit.inf.dslreasoner.ilp.cbc) -set(CMAKE_CXX_STANDARD 17) +set(CMAKE_CXX_STANDARD 14) find_package(JNI REQUIRED) find_package(PkgConfig REQUIRED) -- cgit v1.2.3-54-g00ecf From 957082776dbb7efed53a783c5e5be6b443a9bb86 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sat, 27 Jun 2020 17:56:46 +0200 Subject: Fix scope + numerical propagation WIP --- .../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes .../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2526 -> 2526 bytes .../.SolverSemanticHighlightCalculator.xtendbin | Bin 5334 -> 5334 bytes .../.SolverSemanticTextAttributeProvider.xtendbin | Bin 4902 -> 4902 bytes .../validation/.SolverLanguageValidator.xtendbin | Bin 1717 -> 1717 bytes ....SolverLanguageTokenDefInjectingParser.xtendbin | Bin 2742 -> 2742 bytes ...nguageSyntheticTokenSyntacticSequencer.xtendbin | Bin 2758 -> 2758 bytes .../hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath | 6 +- .../.settings/org.eclipse.jdt.core.prefs | 8 ++ .../lib/libviatracbc.so | Bin 33944 -> 46416 bytes .../MultiplicityGoalConstraintCalculator.xtend | 15 +-- .../cardinality/PolyhedronScopePropagator.xtend | 8 +- .../logic2viatra/cardinality/ScopePropagator.xtend | 14 +- .../rules/GoalConstraintProvider.xtend | 3 +- .../rules/RefinementRuleProvider.xtend | 150 ++++++++++++--------- .../PartialInterpretationInitialiser.xtend | 29 ++-- .../reasoner/ViatraReasonerConfiguration.xtend | 5 +- .../dse/BestFirstStrategyForModelGeneration.java | 22 +-- .../dse/ModelGenerationCompositeObjective.xtend | 2 +- .../viatrasolver/reasoner/dse/ScopeObjective.xtend | 2 +- .../case.study.familyTree.run/bin/.gitignore | 1 - .../inputs/SatelliteInstance.xmi | 2 +- .../src/run/RunGeneratorConfig.xtend | 6 +- 23 files changed, 136 insertions(+), 137 deletions(-) create mode 100644 Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs delete mode 100644 Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore (limited to 'Solvers/ILP-Solver') diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin index b5a7c99c..94c786eb 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin index 9274eee0..46ab9b95 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin index 8e8e8c70..27dc1dd4 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin index 741776d1..d71f4f21 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin index 73356e7f..801783da 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin index 24f61d80..30c2ff9e 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin index eae3bd77..261f466c 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin differ 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 index e19039ae..93829d26 100644 --- a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.classpath @@ -1,10 +1,6 @@ - - - - - + diff --git a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..9f6ece88 --- /dev/null +++ b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,8 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.release=disabled +org.eclipse.jdt.core.compiler.source=1.8 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 index 96289216..ba3cdc06 100755 Binary files a/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so and b/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib/libviatracbc.so differ diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend index 034420d6..b28cd584 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend @@ -10,15 +10,13 @@ class MultiplicityGoalConstraintCalculator { val String targetRelationName val IQuerySpecification querySpecification var ViatraQueryMatcher matcher - val int minValue val boolean containment val int cost - public new(String targetRelationName, IQuerySpecification querySpecification, int minValue, boolean containment, int cost) { + public new(String targetRelationName, IQuerySpecification querySpecification, boolean containment, int cost) { this.targetRelationName = targetRelationName this.querySpecification = querySpecification this.matcher = null - this.minValue = minValue this.containment = containment this.cost = cost } @@ -27,7 +25,6 @@ class MultiplicityGoalConstraintCalculator { this.targetRelationName = other.targetRelationName this.querySpecification = other.querySpecification this.matcher = null - this.minValue = other.minValue this.containment = other.containment this.cost = other.cost } @@ -49,14 +46,8 @@ class MultiplicityGoalConstraintCalculator { var res = 0 val allMatches = this.matcher.allMatches for(match : allMatches) { - val existingMultiplicity = match.get(4) as Integer - if(existingMultiplicity < this.minValue) { - val missingMultiplicity = this.minValue-existingMultiplicity - res += missingMultiplicity - } -// if(missingMultiplicity!=0) { -// println(targetRelationName+ " missing multiplicity: "+missingMultiplicity) -// } + val missingMultiplicity = match.get(2) as Integer + res += missingMultiplicity } // if(res>0) // println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost) diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend index 120fb18a..9b4dff0f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend @@ -88,6 +88,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { val result = operator.saturate() if (result == PolyhedronSaturationResult.EMPTY) { cache.put(signature, PolyhedronSignature.EMPTY) +// println("INVALID") setScopesInvalid() } else { val resultSignature = polyhedron.createSignature @@ -110,11 +111,8 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { } } - override propagateAdditionToRelation(Relation r) { - super.propagateAdditionToRelation(r) - if (relevantRelations.contains(r)) { - propagateAllScopeConstraints() - } + override isPropagationNeededAfterAdditionToRelation(Relation r) { + relevantRelations.contains(r) || super.isPropagationNeededAfterAdditionToRelation(r) } def resetBounds() { diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend index 8f3a5bb0..8350c7f4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend @@ -114,21 +114,21 @@ class ScopePropagator { } } - def void propagateAdditionToRelation(Relation r) { - // Nothing to propagate. + def isPropagationNeededAfterAdditionToRelation(Relation r) { + false } private def removeOne(Scope scope) { - if (scope.maxNewElements === 0) { - throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') - } else if (scope.maxNewElements > 0) { - scope.maxNewElements = scope.maxNewElements - 1 - } if (scope.minNewElements > 0) { scope.minNewElements = scope.minNewElements - 1 } if (scope.minNewElementsHeuristic > 0) { scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1 } + if (scope.maxNewElements > 0) { + scope.maxNewElements = scope.maxNewElements - 1 + } else if (scope.maxNewElements === 0) { + setScopesInvalid() + } } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index 238ade5b..d2ee80dc 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend @@ -15,9 +15,8 @@ class GoalConstraintProvider { val queries = entry.value val targetRelationName = constraint.relation.name val query = queries.unfinishedMultiplicityQuery - val minValue = constraint.lowerBound val containment = constraint.containment - res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, minValue, containment, 1) + res += new MultiplicityGoalConstraintCalculator(targetRelationName, query, containment, 1) } } return res diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index 0b8a9019..863ee18b 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend @@ -32,9 +32,12 @@ import java.util.LinkedHashMap import java.util.LinkedList import java.util.List import java.util.Map +import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine import org.eclipse.viatra.query.runtime.api.GenericPatternMatch import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.viatra.query.runtime.emf.EMFScope import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory import org.eclipse.xtend.lib.annotations.Data @@ -45,6 +48,8 @@ class RefinementRuleProvider { val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE + var AdvancedViatraQueryEngine queryEngine + def canonizeName(String name) { return name.replace(' ','_') } @@ -60,6 +65,7 @@ class RefinementRuleProvider { { val res = new LinkedHashMap val recursiveObjectCreation = recursiveObjectCreation(p,i) + queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine for(LHSEntry: patterns.refineObjectQueries.entrySet) { val containmentRelation = LHSEntry.key.containmentRelation val inverseRelation = LHSEntry.key.inverseContainment @@ -90,8 +96,7 @@ class RefinementRuleProvider { if(inverseRelation!== null) { ruleBuilder.action[match | statistics.incrementTransformationCount -// println(name) - val startTime = System.nanoTime +// println(name) //val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation @@ -99,79 +104,89 @@ class RefinementRuleProvider { val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation val container = match.get(5) as DefinedElement - createObjectActionWithContainmentAndInverse( - nameNewElement, - interpretation, - typeInterpretation, - container, - relationInterpretation, - inverseRelationInterpretation, - [createDefinedElement], - recursiceObjectCreations, - scopePropagator - ) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createObjectActionWithContainmentAndInverse( + nameNewElement, + interpretation, + typeInterpretation, + container, + relationInterpretation, + inverseRelationInterpretation, + [createDefinedElement], + recursiceObjectCreations, + scopePropagator + ) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] ] } else { ruleBuilder.action[match | statistics.incrementTransformationCount // println(name) - val startTime = System.nanoTime //val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val relationInterpretation = match.get(2) as PartialRelationInterpretation val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation val container = match.get(4) as DefinedElement - createObjectActionWithContainment( - nameNewElement, - interpretation, - typeInterpretation, - container, - relationInterpretation, - [createDefinedElement], - recursiceObjectCreations, - scopePropagator - ) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createObjectActionWithContainment( + nameNewElement, + interpretation, + typeInterpretation, + container, + relationInterpretation, + [createDefinedElement], + recursiceObjectCreations, + scopePropagator + ) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] ] } } else { ruleBuilder.action[match | statistics.incrementTransformationCount // println(name) - val startTime = System.nanoTime //val problem = match.get(0) as LogicProblem val interpretation = match.get(1) as PartialInterpretation val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation - createObjectAction( - nameNewElement, - interpretation, - typeInterpretation, - [createDefinedElement], - recursiceObjectCreations, - scopePropagator - ) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createObjectAction( + nameNewElement, + interpretation, + typeInterpretation, + [createDefinedElement], + recursiceObjectCreations, + scopePropagator + ) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] ] } return ruleBuilder.build @@ -342,7 +357,7 @@ class RefinementRuleProvider { if (inverseRelation === null) { ruleBuilder.action [ match | statistics.incrementTransformationCount - val startTime = System.nanoTime + // println(name) // val problem = match.get(0) as LogicProblem // val interpretation = match.get(1) as PartialInterpretation @@ -350,19 +365,24 @@ class RefinementRuleProvider { val src = match.get(3) as DefinedElement val trg = match.get(4) as DefinedElement - createRelationLinkAction(src, trg, relationInterpretation) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createRelationLinkAction(src, trg, relationInterpretation) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAdditionToRelation(declaration) - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] + } ] } else { ruleBuilder.action [ match | statistics.incrementTransformationCount - val startTime = System.nanoTime // println(name) // val problem = match.get(0) as LogicProblem // val interpretation = match.get(1) as PartialInterpretation @@ -371,14 +391,20 @@ class RefinementRuleProvider { val src = match.get(4) as DefinedElement val trg = match.get(5) as DefinedElement - createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) - - val propagatorStartTime = System.nanoTime - statistics.addExecutionTime(propagatorStartTime-startTime) + queryEngine.delayUpdatePropagation [ + val startTime = System.nanoTime + createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) + statistics.addExecutionTime(System.nanoTime-startTime) + ] // Scope propagation - scopePropagator.propagateAdditionToRelation(declaration) - statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { + queryEngine.delayUpdatePropagation [ + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) + ] + } ] } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend index d37acb6d..20ff58f2 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend @@ -2,19 +2,24 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStar import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partial2logicannotations.PartialModelRelation2Assertion -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.NaryRelationLink import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialIntegerInterpretation @@ -22,10 +27,10 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRealInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.UnaryElementRelationLink import java.math.BigDecimal import java.util.HashMap import java.util.Map @@ -35,14 +40,6 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope import org.eclipse.xtend.lib.annotations.Data import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition @Data class Problem2PartialInterpretationTrace { Map type2Interpretation @@ -194,7 +191,7 @@ class PartialInterpretationInitialiser { interpretation.minNewElements = minNewElements interpretation.maxNewElements = maxNewElements // elements from problem are included - if(maxNewElements>0) { + if(maxNewElements != 0) { val newElements = createDefinedElement => [it.name = "New Objects"] interpretation.openWorldElements += newElements } @@ -213,12 +210,8 @@ class PartialInterpretationInitialiser { def private initialiseTypeScope(PartialTypeInterpratation interpretation, Integer min, Integer max) { val res = createScope res.targetTypeInterpretation = interpretation - if(min !== null) { - res.minNewElements = min - } - if(max !== null) { - res.maxNewElements = max - } + res.minNewElements = min ?: 0 + res.maxNewElements = max ?: -1 return res } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index ddd25aac..e33a2590 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend @@ -58,13 +58,14 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { public var runIntermediateNumericalConsistencyChecks = true public var punishSize = true - public var scopeWeight = 1 - public var conaintmentWeight = 2 + public var scopeWeight = 2 + public var conaintmentWeight = 1 public var nonContainmentWeight = 1 public var unfinishedWFWeight = 1 public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) +// public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.BasicTypeHierarchy public var List hints = newArrayList diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index e529892c..09575384 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java @@ -18,6 +18,7 @@ import java.util.List; import java.util.PriorityQueue; import java.util.Random; +import org.apache.log4j.Level; import org.apache.log4j.Logger; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.util.EcoreUtil; @@ -76,7 +77,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { private volatile boolean isInterrupted = false; private ModelResult modelResultByInternalSolver = null; private Random random = new Random(); - //private Collection> matchers; +// private Collection> matchers; public ActivationSelector activationSelector = new EvenActivationSelector(random); public ViatraReasonerSolutionSaver solutionSaver; public NumericSolver numericSolver; @@ -100,7 +101,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { this.method = method; this.solutionSaver = solutionSaver; this.numericSolver = numericSolver; - //logger.setLevel(Level.DEBUG); +// logger.setLevel(Level.DEBUG); } public int getNumberOfStatecoderFail() { @@ -136,7 +137,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { // ViatraQueryEngine engine = context.getQueryEngine(); // matchers = new LinkedList>(); // for(IQuerySpecification> p : this.method.getAllPatterns()) { -// //System.out.println(p.getSimpleName()); // ViatraQueryMatcher matcher = p.getMatcher(engine); // matchers.add(matcher); // } @@ -154,13 +154,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { @Override public void explore() { -// System.out.println("press enter"); -// try { -// new BufferedReader(new InputStreamReader(System.in)).readLine(); -// } catch (IOException e) { -// // TODO Auto-generated catch block -// e.printStackTrace(); -// } this.explorationStarted=System.nanoTime(); if (!checkGlobalConstraints()) { logger.info("Global contraint is not satisifed in the first state. Terminate."); @@ -219,10 +212,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { while (!isInterrupted && !configuration.progressMonitor.isCancelled() && iterator.hasNext()) { final Object nextActivation = iterator.next(); -// if (!iterator.hasNext()) { -// logger.debug("Last untraversed activation of the state."); -// trajectoiresToExplore.remove(currentTrajectoryWithfitness); -// } logger.debug("Executing new activation: " + nextActivation); context.executeAcitvationId(nextActivation); method.getStatistics().incrementDecisionCount(); @@ -230,10 +219,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { visualiseCurrentState(); // for(ViatraQueryMatcher matcher : matchers) { // int c = matcher.countMatches(); -// if(c>=100) { +// if(c>=1) { // System.out.println(c+ " " +matcher.getPatternName()); -// } -// +// } // } boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness); diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend index d2faaa65..481f4ce1 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend @@ -112,7 +112,7 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective { override isHardObjective() { true } - override satisifiesHardObjective(Double fitness) { fitness <= 0.001 } + override satisifiesHardObjective(Double fitness) { fitness <= 0.9 } override setComparator(Comparator comparator) { throw new UnsupportedOperationException("Model generation objective comparator cannot be set.") diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend index 69a734f8..7abc5cb8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend @@ -25,7 +25,7 @@ class ScopeObjective implements IObjective{ val interpretation = context.model as PartialInterpretation var res = interpretation.minNewElementsHeuristic.doubleValue for(scope : interpretation.scopes) { - res += scope.minNewElementsHeuristic*2 + res += scope.minNewElementsHeuristic } return res } diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore deleted file mode 100644 index 7050a7e3..00000000 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/queries/ diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi index 3d07a199..66512878 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/SatelliteInstance.xmi @@ -4,4 +4,4 @@ xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:satellite="http://www.example.org/satellite" - xsi:schemaLocation="http://www.example.org/satellite ../model/satellite.ecore"/> + xsi:schemaLocation="http://www.example.org/satellite ../../hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore"/> diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend index 20eed2e2..e4d6fe9f 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend @@ -12,7 +12,9 @@ import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.RuntimeEn import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ScopeSpecification import hu.bme.mit.inf.dslreasoner.application.execution.ScriptExecutor import hu.bme.mit.inf.dslreasoner.application.execution.StandaloneScriptExecutor +import hu.bme.mit.inf.dslreasoner.application.execution.StandardOutputBasedScriptConsole import java.io.File +import java.io.PrintWriter import java.text.SimpleDateFormat import java.util.Date import org.apache.commons.cli.BasicParser @@ -23,8 +25,6 @@ import org.apache.commons.cli.Option import org.apache.commons.cli.Options import org.apache.commons.cli.ParseException import org.eclipse.core.runtime.NullProgressMonitor -import com.google.common.io.Files -import java.io.PrintWriter class RunGeneratorConfig { static var SIZE_LB = 20 @@ -102,7 +102,7 @@ class RunGeneratorConfig { val SimpleDateFormat format = new SimpleDateFormat("dd-HHmm") val formattedDate = format.format(date) - val executor = new ScriptExecutor + val executor = new ScriptExecutor(StandardOutputBasedScriptConsole.FACTORY) val path = "config//generic" + DOMAIN + ".vsconfig" var ConfigurationScript config = StandaloneScriptExecutor.loadScript(path) -- cgit v1.2.3-54-g00ecf