From 7f7f934fe6ad11df96906d009eec68583fd46660 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 5 Feb 2019 23:54:03 +0100 Subject: [Stochastic] Fault tree transformation langauge --- ...ure (hu.bme.mit.inf.dslreasoner.smt.language).launch | 17 ----------------- 1 file changed, 17 deletions(-) delete mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch (limited to 'Solvers/SMT-Solver') diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch deleted file mode 100644 index e448edbe..00000000 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch +++ /dev/null @@ -1,17 +0,0 @@ - - - - - - - - - - - - - - - - - -- cgit v1.2.3-54-g00ecf From fc505b6b171a2d54c3bad6078031b028b55131d3 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sun, 14 Jul 2019 00:56:19 +0200 Subject: Polyhedron abstraction with Z3 for cardinality propagation --- Solvers/SMT-Solver/com.microsoft.z3/.classpath | 15 ++ Solvers/SMT-Solver/com.microsoft.z3/.gitignore | 1 + Solvers/SMT-Solver/com.microsoft.z3/.project | 28 +++ .../com.microsoft.z3/META-INF/MANIFEST.MF | 22 +++ .../SMT-Solver/com.microsoft.z3/build.properties | 3 + Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dll | Bin 0 -> 13731840 bytes .../SMT-Solver/com.microsoft.z3/lib/libz3.dylib | Bin 0 -> 20880828 bytes Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so | Bin 0 -> 23841920 bytes .../SMT-Solver/com.microsoft.z3/lib/libz3java.dll | Bin 0 -> 97280 bytes .../com.microsoft.z3/lib/libz3java.dylib | Bin 0 -> 165680 bytes .../SMT-Solver/com.microsoft.z3/lib/libz3java.so | Bin 0 -> 270824 bytes .../META-INF/MANIFEST.MF | 4 +- .../ModelGenerationMethodProvider.xtend | 24 ++- .../logic2viatra/ScopePropagator.xtend | 156 ---------------- .../cardinality/PolyhedronScopePropagator.xtend | 153 +++++++++++++++ .../cardinality/PolyhedronSolver.xtend | 115 ++++++++++++ .../logic2viatra/cardinality/ScopePropagator.xtend | 149 +++++++++++++++ .../cardinality/Z3PolyhedronSolver.xtend | 206 +++++++++++++++++++++ .../rules/RefinementRuleProvider.xtend | 2 +- .../viatrasolver/reasoner/ViatraReasoner.xtend | 7 +- .../reasoner/ViatraReasonerConfiguration.xtend | 3 + .../META-INF/MANIFEST.MF | 2 + .../tests/cardinality/Z3PolyhedronSolverTest.xtend | 199 ++++++++++++++++++++ 23 files changed, 925 insertions(+), 164 deletions(-) create mode 100644 Solvers/SMT-Solver/com.microsoft.z3/.classpath create mode 100644 Solvers/SMT-Solver/com.microsoft.z3/.gitignore create mode 100644 Solvers/SMT-Solver/com.microsoft.z3/.project create mode 100644 Solvers/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF create mode 100644 Solvers/SMT-Solver/com.microsoft.z3/build.properties create mode 100644 Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dll create mode 100755 Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dylib create mode 100755 Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so create mode 100644 Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dll create mode 100755 Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dylib create mode 100755 Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so delete mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend (limited to 'Solvers/SMT-Solver') diff --git a/Solvers/SMT-Solver/com.microsoft.z3/.classpath b/Solvers/SMT-Solver/com.microsoft.z3/.classpath new file mode 100644 index 00000000..ffdc022a --- /dev/null +++ b/Solvers/SMT-Solver/com.microsoft.z3/.classpath @@ -0,0 +1,15 @@ + + + + + + + + + + + + + + + diff --git a/Solvers/SMT-Solver/com.microsoft.z3/.gitignore b/Solvers/SMT-Solver/com.microsoft.z3/.gitignore new file mode 100644 index 00000000..ae3c1726 --- /dev/null +++ b/Solvers/SMT-Solver/com.microsoft.z3/.gitignore @@ -0,0 +1 @@ +/bin/ diff --git a/Solvers/SMT-Solver/com.microsoft.z3/.project b/Solvers/SMT-Solver/com.microsoft.z3/.project new file mode 100644 index 00000000..ec5bbc58 --- /dev/null +++ b/Solvers/SMT-Solver/com.microsoft.z3/.project @@ -0,0 +1,28 @@ + + + com.microsoft.z3 + + + + + + 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/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF b/Solvers/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF new file mode 100644 index 00000000..01faa2ad --- /dev/null +++ b/Solvers/SMT-Solver/com.microsoft.z3/META-INF/MANIFEST.MF @@ -0,0 +1,22 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: Z3 +Bundle-SymbolicName: com.microsoft.z3 +Bundle-Version: 4.8.5.qualifier +Bundle-Vendor: Microsoft +Automatic-Module-Name: com.microsoft.z3 +Bundle-ClassPath: com.microsoft.z3.jar +Bundle-NativeCode: lib/libz3.so; + lib/libz3java.so; + osname=Linux; + processor=x86_64; + lib/libz3.dylib; + lib/libz3java.dylib; + osname=MacOSX; + processor=x86_64, + lib/libz3.dll; + lib/libz3java.dll; + osname=win32; + processor=x86_64 +Export-Package: com.microsoft.z3, + com.microsoft.z3.enumerations diff --git a/Solvers/SMT-Solver/com.microsoft.z3/build.properties b/Solvers/SMT-Solver/com.microsoft.z3/build.properties new file mode 100644 index 00000000..87f4e73f --- /dev/null +++ b/Solvers/SMT-Solver/com.microsoft.z3/build.properties @@ -0,0 +1,3 @@ +bin.includes = META-INF/,\ + lib/,\ + com.microsoft.z3.jar diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dll b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dll new file mode 100644 index 00000000..0b518988 Binary files /dev/null and b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dll differ diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dylib b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dylib new file mode 100755 index 00000000..7884a0e7 Binary files /dev/null and b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dylib differ diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so new file mode 100755 index 00000000..5beffe36 Binary files /dev/null and b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so differ diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dll b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dll new file mode 100644 index 00000000..5e8dbc9b Binary files /dev/null and b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dll differ diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dylib b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dylib new file mode 100755 index 00000000..2d9116ac Binary files /dev/null and b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dylib differ diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so new file mode 100755 index 00000000..e2d2618d Binary files /dev/null and b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so differ 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 b2ee3981..37495e50 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 @@ -4,6 +4,7 @@ Bundle-Name: Logic2viatra Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;singleton:=true Bundle-Version: 1.0.0.qualifier Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra, + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality, hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval, hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators, hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, @@ -22,7 +23,8 @@ Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", com.google.inject;bundle-version="3.0.0", org.eclipse.xtext;bundle-version="2.10.0", org.eclipse.viatra.transformation.runtime.emf;bundle-version="1.5.0", - org.eclipse.xtext.xbase;bundle-version="2.10.0" + org.eclipse.xtext.xbase;bundle-version="2.10.0", + com.microsoft.z3;bundle-version="4.8.5" Bundle-RequiredExecutionEnvironment: JavaSE-1.8 Import-Package: org.apache.log4j Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index b6918294..0040dbcd 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,6 +4,11 @@ import com.google.common.collect.ImmutableMap import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider @@ -63,7 +68,7 @@ class ModelGenerationMethodProvider { ReasonerWorkspace workspace, boolean nameNewElements, TypeInferenceMethod typeInferenceMethod, - ScopePropagator scopePropagator, + ScopePropagatorStrategy scopePropagatorStrategy, DocumentationLevel debugLevel ) { val statistics = new ModelGenerationStatistics @@ -74,6 +79,8 @@ class ModelGenerationMethodProvider { val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, workspace, typeInferenceMethod, writeFiles) + val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries) + scopePropagator.propagateAllScopeConstraints val // LinkedHashMap, BatchTransformationRule>> objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, nameNewElements, statistics) @@ -104,4 +111,19 @@ class ModelGenerationMethodProvider { queries.allQueries ) } + + private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, + PartialInterpretation emptySolution, GeneratedPatterns queries) { + switch (scopePropagatorStrategy) { + case BasicTypeHierarchy: + new ScopePropagator(emptySolution) + case PolyhedralTypeHierarchy: { + val types = queries.refineObjectQueries.keySet.map[newType].toSet + val solver = new Z3PolyhedronSolver + new PolyhedronScopePropagator(emptySolution, types, solver) + } + default: + throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) + } + } } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend deleted file mode 100644 index 38633c07..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend +++ /dev/null @@ -1,156 +0,0 @@ -package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra - -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope -import java.util.HashMap -import java.util.Map -import java.util.Set -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation -import java.util.HashSet - -class ScopePropagator { - PartialInterpretation partialInterpretation - Map type2Scope - - val Map> superScopes - val Map> subScopes - - public new(PartialInterpretation p) { - partialInterpretation = p - type2Scope = new HashMap - for(scope : p.scopes) { - type2Scope.put(scope.targetTypeInterpretation,scope) - } - - superScopes = new HashMap - subScopes = new HashMap - for(scope : p.scopes) { - superScopes.put(scope,new HashSet) - subScopes.put(scope,new HashSet) - } - - for(scope : p.scopes) { - val target = scope.targetTypeInterpretation - if(target instanceof PartialComplexTypeInterpretation) { - val supertypeInterpretations = target.supertypeInterpretation - for(supertypeInterpretation : supertypeInterpretations) { - val supertypeScope = type2Scope.get(supertypeInterpretation) - superScopes.get(scope).add(supertypeScope) - subScopes.get(supertypeScope).add(scope) - } - } - } - } - - def public propagateAllScopeConstraints() { - var boolean hadChanged - do{ - hadChanged = false - for(superScopeEntry : superScopes.entrySet) { - val sub = superScopeEntry.key - hadChanged = propagateLowerLimitUp(sub,partialInterpretation) || hadChanged - hadChanged = propagateUpperLimitDown(sub,partialInterpretation) || hadChanged - for(sup: superScopeEntry.value) { - hadChanged = propagateLowerLimitUp(sub,sup) || hadChanged - hadChanged = propagateUpperLimitDown(sub,sup) || hadChanged - } - } - } while(hadChanged) -// println('''All constraints are propagated.''') - } - - def public propagateAdditionToType(PartialTypeInterpratation t) { -// println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') - val targetScope = type2Scope.get(t) - targetScope.removeOne - val sups = superScopes.get(targetScope) - sups.forEach[removeOne] - if(this.partialInterpretation.minNewElements > 0) { - this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1 - } - if(this.partialInterpretation.maxNewElements > 0) { - this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1 - } else if(this.partialInterpretation.maxNewElements === 0) { - throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') - } - -// subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)] -// for(sup: sups) { -// subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)] -// } -// for(scope : type2Scope.values) { -// propagateUpperLimitDown(scope,partialInterpretation) -// } - - propagateAllScopeConstraints - -// println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') -// println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') -// this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] -// println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') - } - - private def propagateLowerLimitUp(Scope subScope, Scope superScope) { - if(subScope.minNewElements>superScope.minNewElements) { -// println(''' -// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -// superScope.minNewElements «superScope.minNewElements» = subScope.minNewElements «subScope.minNewElements» -// ''') - superScope.minNewElements = subScope.minNewElements - return true - } else { - return false - } - } - - private def propagateUpperLimitDown(Scope subScope, Scope superScope) { - if(superScope.maxNewElements>=0 && (superScope.maxNewElements «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -// subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» -// ''') - subScope.maxNewElements = superScope.maxNewElements - return true - } else { - return false - } - } - - private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { - if(subScope.minNewElements>p.minNewElements) { -// println(''' -// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes -// p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» -// ''') - p.minNewElements = subScope.minNewElements - return true - } else { - return false - } - } - - private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { - if(p.maxNewElements>=0 && (p.maxNewElements nodes -// subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» -// ''') - subScope.maxNewElements = p.maxNewElements - return true - } else { - return 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 - } - } -} - \ No newline at end of file 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 new file mode 100644 index 00000000..8f210ffb --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend @@ -0,0 +1,153 @@ +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.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope +import java.util.ArrayDeque +import java.util.HashMap +import java.util.HashSet +import java.util.Map +import java.util.Set + +class PolyhedronScopePropagator extends ScopePropagator { + val Map scopeBounds + val LinearConstraint topLevelBounds + val PolyhedronSaturationOperator operator + + new(PartialInterpretation p, Set possibleNewDynamicTypes, PolyhedronSolver solver) { + super(p) + val instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] + val primitiveDimensions = new HashMap + val constraintsBuilder = ImmutableList.builder + val scopeBoundsBuilder = ImmutableMap.builder + // Dimensions for instantiable types were created according to the type analysis, + // but for any possible primitive types, we create them on demand, + // as there is no Type directly associated with a PartialPrimitiveInterpretation. + for (scope : p.scopes) { + switch (targetTypeInterpretation : scope.targetTypeInterpretation) { + PartialPrimitiveInterpretation: { + val dimension = primitiveDimensions.computeIfAbsent(targetTypeInterpretation) [ interpretation | + new Dimension(interpretation.eClass.name, 0, null) + ] + scopeBoundsBuilder.put(scope, dimension) + } + PartialComplexTypeInterpretation: { + val complexType = targetTypeInterpretation.interpretationOf + val dimensions = findSubtypeDimensions(complexType, instanceCounts) + switch (dimensions.size) { + case 0: + if (scope.minNewElements > 0) { + throw new IllegalArgumentException("Found scope for " + complexType.name + + ", but the type cannot be instantiated") + } + case 1: + scopeBoundsBuilder.put(scope, dimensions.head) + default: { + val constraint = new LinearConstraint(dimensions.toInvertedMap[1], null, null) + constraintsBuilder.add(constraint) + scopeBoundsBuilder.put(scope, constraint) + } + } + } + default: + throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + targetTypeInterpretation) + } + } + val allDimensions = ImmutableList.builder.addAll(instanceCounts.values).addAll(primitiveDimensions.values).build + scopeBounds = scopeBoundsBuilder.build + topLevelBounds = new LinearConstraint(allDimensions.toInvertedMap[1], null, null) + constraintsBuilder.add(topLevelBounds) + val expressionsToSaturate = ImmutableList.builder.addAll(scopeBounds.values).add(topLevelBounds).build + val polyhedron = new Polyhedron(allDimensions, constraintsBuilder.build, expressionsToSaturate) + operator = solver.createSaturationOperator(polyhedron) + } + + private def findSubtypeDimensions(Type type, Map instanceCounts) { + val subtypes = new HashSet + val dimensions = new HashSet + val stack = new ArrayDeque + stack.addLast(type) + while (!stack.empty) { + val subtype = stack.removeLast + if (subtypes.add(subtype)) { + val dimension = instanceCounts.get(subtype) + if (dimension !== null) { + dimensions.add(dimension) + } + stack.addAll(subtype.subtypes) + } + } + dimensions + } + + override void propagateAllScopeConstraints() { + populatePolyhedronFromScope() + val result = operator.saturate() + if (result == PolyhedronSaturationResult.EMPTY) { + throw new IllegalStateException("Scope bounds cannot be satisfied") + } else { + populateScopesFromPolyhedron() + if (result != PolyhedronSaturationResult.SATURATED) { + super.propagateAllScopeConstraints() + } + } + } + + private def populatePolyhedronFromScope() { + topLevelBounds.lowerBound = partialInterpretation.minNewElements + if (partialInterpretation.maxNewElements >= 0) { + topLevelBounds.upperBound = partialInterpretation.maxNewElements + } + for (pair : scopeBounds.entrySet) { + val scope = pair.key + val bounds = pair.value + bounds.lowerBound = scope.minNewElements + if (scope.maxNewElements >= 0) { + bounds.upperBound = scope.maxNewElements + } + } + } + + private def populateScopesFromPolyhedron() { + checkFiniteBounds(topLevelBounds) + if (partialInterpretation.minNewElements > topLevelBounds.lowerBound) { + throw new IllegalArgumentException('''Lower bound of «topLevelBounds» smaller than top-level scope: «partialInterpretation.minNewElements»''') + } else if (partialInterpretation.minNewElements != topLevelBounds.lowerBound) { + partialInterpretation.minNewElements = topLevelBounds.lowerBound + } + if (partialInterpretation.maxNewElements >= 0 && + partialInterpretation.maxNewElements < topLevelBounds.upperBound) { + throw new IllegalArgumentException('''Upper bound of «topLevelBounds» larger than top-level scope: «partialInterpretation.maxNewElements»''') + } else if (partialInterpretation.maxNewElements != topLevelBounds.upperBound) { + partialInterpretation.maxNewElements = topLevelBounds.upperBound + } + for (pair : scopeBounds.entrySet) { + val scope = pair.key + val bounds = pair.value + checkFiniteBounds(bounds) + if (scope.minNewElements > bounds.lowerBound) { + throw new IllegalArgumentException('''Lower bound of «bounds» smaller than «scope.targetTypeInterpretation» scope: «scope.minNewElements»''') + } else if (scope.minNewElements != bounds.lowerBound) { + scope.minNewElements = bounds.lowerBound + } + if (scope.maxNewElements >= 0 && scope.maxNewElements < bounds.upperBound) { + throw new IllegalArgumentException('''Upper bound of «bounds» larger than «scope.targetTypeInterpretation» scope: «scope.maxNewElements»''') + } else if (scope.maxNewElements != bounds.upperBound) { + scope.maxNewElements = bounds.upperBound + } + } + } + + private def checkFiniteBounds(LinearBoundedExpression bounds) { + if (bounds.lowerBound === null) { + throw new IllegalArgumentException("Infinite lower bound: " + bounds) + } + if (bounds.upperBound === null) { + throw new IllegalArgumentException("Infinite upper bound: " + bounds) + } + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend new file mode 100644 index 00000000..08bf25b9 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend @@ -0,0 +1,115 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import java.util.List +import java.util.Map +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +interface PolyhedronSolver { + def PolyhedronSaturationOperator createSaturationOperator(Polyhedron polyhedron) +} + +enum PolyhedronSaturationResult { + SATURATED, + EMPTY, + UNKNOWN +} + +interface PolyhedronSaturationOperator extends AutoCloseable { + def Polyhedron getPolyhedron() + + def PolyhedronSaturationResult saturate() +} + +@FinalFieldsConstructor +@Accessors +class Polyhedron { + /** + * The list of dimensions (variables) for this polyhedron. + * + * This list must not be modified after the polyhedron was created. + * However, lower and upper bounds of the dimensions may be changed. + * + * Names of dimensions in this list are assumed to be unique. + */ + val List dimensions + + /** + * The list of constraints defining this polyhedron. + * + * The list and its elements may be freely modified. + */ + val List constraints + + /** + * The list of constraints that should be saturated (tightened) + * when a {@link PolyhedronSaturationOperator} is invoked. + * + * This list may be freely modified. + * + * Place all dimensions and constraints here to saturate all the bounds. + */ + val List expressionsToSaturate + + override toString() ''' + Dimensions: + «FOR dimension : dimensions» + «dimension» + «ENDFOR» + Constraints: + «FOR constraint : constraints» + «constraint» + «ENDFOR» +««« Saturate: +««« «FOR expression : expressionsToSaturate» +««« «IF expression instanceof Dimension»dimension«ELSEIF expression instanceof LinearConstraint»constraint«ELSE»unknown«ENDIF» «expression» +««« «ENDFOR» + ''' + +} + +@Accessors +abstract class LinearBoundedExpression { + var Integer lowerBound + var Integer upperBound +} + +@Accessors +class Dimension extends LinearBoundedExpression { + val String name + + @FinalFieldsConstructor + new() { + } + + new(String name, Integer lowerBound, Integer upperBound) { + this(name) + this.lowerBound = lowerBound + this.upperBound = upperBound + } + + override toString() { + '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«name»«IF upperBound !== null» <= «upperBound»«ENDIF»''' + } + +} + +@Accessors +class LinearConstraint extends LinearBoundedExpression { + val Map coefficients + + @FinalFieldsConstructor + new() { + } + + new(Map coefficients, Integer lowerBound, Integer upperBound) { + this(coefficients) + this.lowerBound = lowerBound + this.upperBound = upperBound + } + + override toString() { + '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«FOR pair : coefficients.entrySet SEPARATOR " + "»«IF pair.value != 1»«pair.value» * «ENDIF»«pair.key.name»«ENDFOR»«IF upperBound !== null» <= «upperBound»«ENDIF»''' + } + +} 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 new file mode 100644 index 00000000..c8fb3409 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend @@ -0,0 +1,149 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope +import java.util.HashMap +import java.util.HashSet +import java.util.Map +import java.util.Set +import org.eclipse.xtend.lib.annotations.Accessors + +enum ScopePropagatorStrategy { + BasicTypeHierarchy, + PolyhedralTypeHierarchy +} + +class ScopePropagator { + @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation + Map type2Scope + + val Map> superScopes + val Map> subScopes + + new(PartialInterpretation p) { + partialInterpretation = p + type2Scope = new HashMap + for (scope : p.scopes) { + type2Scope.put(scope.targetTypeInterpretation, scope) + } + + superScopes = new HashMap + subScopes = new HashMap + for (scope : p.scopes) { + superScopes.put(scope, new HashSet) + subScopes.put(scope, new HashSet) + } + + for (scope : p.scopes) { + val target = scope.targetTypeInterpretation + if (target instanceof PartialComplexTypeInterpretation) { + val supertypeInterpretations = target.supertypeInterpretation + for (supertypeInterpretation : supertypeInterpretations) { + val supertypeScope = type2Scope.get(supertypeInterpretation) + superScopes.get(scope).add(supertypeScope) + subScopes.get(supertypeScope).add(scope) + } + } + } + } + + def propagateAllScopeConstraints() { + var boolean hadChanged + do { + hadChanged = false + for (superScopeEntry : superScopes.entrySet) { + val sub = superScopeEntry.key + hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged + hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged + for (sup : superScopeEntry.value) { + hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged + hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged + } + } + } while (hadChanged) + } + + def propagateAdditionToType(PartialTypeInterpratation t) { +// println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') + val targetScope = type2Scope.get(t) + targetScope.removeOne + val sups = superScopes.get(targetScope) + sups.forEach[removeOne] + if (this.partialInterpretation.minNewElements > 0) { + this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 + } + if (this.partialInterpretation.maxNewElements > 0) { + this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 + } else if (this.partialInterpretation.maxNewElements === 0) { + throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') + } + propagateAllScopeConstraints + +// println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') +// println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') +// this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] +// println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') + } + + private def propagateLowerLimitUp(Scope subScope, Scope superScope) { + if (subScope.minNewElements > superScope.minNewElements) { + superScope.minNewElements = subScope.minNewElements + return true + } else { + return false + } + } + + private def propagateUpperLimitDown(Scope subScope, Scope superScope) { + if (superScope.maxNewElements >= 0 && + (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { +// println(''' +// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» +// subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» +// ''') + subScope.maxNewElements = superScope.maxNewElements + return true + } else { + return false + } + } + + private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { + if (subScope.minNewElements > p.minNewElements) { +// println(''' +// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes +// p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» +// ''') + p.minNewElements = subScope.minNewElements + return true + } else { + return false + } + } + + private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { + if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { +// println(''' +// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes +// subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» +// ''') + subScope.maxNewElements = p.maxNewElements + return true + } else { + return 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 + } + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend new file mode 100644 index 00000000..f1a84f2d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend @@ -0,0 +1,206 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import com.microsoft.z3.ArithExpr +import com.microsoft.z3.Context +import com.microsoft.z3.Expr +import com.microsoft.z3.IntNum +import com.microsoft.z3.Optimize +import com.microsoft.z3.Status +import com.microsoft.z3.Symbol +import java.util.Map +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +class Z3PolyhedronSolver implements PolyhedronSolver { + val boolean lpRelaxation + + @FinalFieldsConstructor + new() { + } + + new() { + this(true) + } + + override createSaturationOperator(Polyhedron polyhedron) { + new Z3SaturationOperator(polyhedron, lpRelaxation) + } +} + +class Z3SaturationOperator implements PolyhedronSaturationOperator { + static val INFINITY_SYMBOL_NAME = "oo" + static val MULT_SYMBOL_NAME = "*" + + extension val Context context + val Symbol infinitySymbol + val Symbol multSymbol + @Accessors val Polyhedron polyhedron + val Map variables + + new(Polyhedron polyhedron, boolean lpRelaxation) { + context = new Context + infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) + multSymbol = context.mkSymbol(MULT_SYMBOL_NAME) + this.polyhedron = polyhedron + variables = polyhedron.dimensions.toInvertedMap [ dimension | + val name = dimension.name + if (lpRelaxation) { + mkRealConst(name) + } else { + mkIntConst(name) + } + ] + } + + override saturate() { + val status = doSaturate() + convertStatusToSaturationResult(status) + } + + private def convertStatusToSaturationResult(Status status) { + switch (status) { + case SATISFIABLE: + PolyhedronSaturationResult.SATURATED + case UNSATISFIABLE: + PolyhedronSaturationResult.EMPTY + case UNKNOWN: + PolyhedronSaturationResult.UNKNOWN + default: + throw new IllegalArgumentException("Unknown Status: " + status) + } + } + + private def doSaturate() { + for (expressionToSaturate : polyhedron.expressionsToSaturate) { + val expr = expressionToSaturate.toExpr + val lowerResult = saturateLowerBound(expr, expressionToSaturate) + if (lowerResult != Status.SATISFIABLE) { + return lowerResult + } + val upperResult = saturateUpperBound(expr, expressionToSaturate) + if (upperResult != Status.SATISFIABLE) { + return upperResult + } + } + Status.SATISFIABLE + } + + private def saturateLowerBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { + val optimize = prepareOptimize + val handle = optimize.MkMinimize(expr) + val status = optimize.Check() + if (status == Status.SATISFIABLE) { + val value = switch (resultExpr : handle.lower) { + IntNum: + resultExpr.getInt() + default: + if (isNegativeInfinity(resultExpr)) { + null + } else { + throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) + } + } + expressionToSaturate.lowerBound = value + } + status + } + + private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { + val optimize = prepareOptimize + val handle = optimize.MkMaximize(expr) + val status = optimize.Check() + if (status == Status.SATISFIABLE) { + val value = switch (resultExpr : handle.upper) { + IntNum: + resultExpr.getInt() + default: + if (isPositiveInfinity(resultExpr)) { + null + } else { + throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) + } + } + expressionToSaturate.upperBound = value + } + status + } + + private def isPositiveInfinity(Expr expr) { + expr.app && expr.getFuncDecl.name == infinitySymbol + } + + private def isNegativeInfinity(Expr expr) { + // Negative infinity is represented as (* (- 1) oo) + if (!expr.app || expr.getFuncDecl.name != multSymbol || expr.numArgs != 2) { + return false + } + isPositiveInfinity(expr.args.get(1)) + } + + private def prepareOptimize() { + val optimize = mkOptimize() + assertConstraints(optimize) + optimize + } + + private def assertConstraints(Optimize it) { + for (pair : variables.entrySet) { + assertBounds(pair.value, pair.key) + } + for (constraint : polyhedron.constraints) { + val expr = createLinearCombination(constraint.coefficients) + assertBounds(expr, constraint) + } + } + + private def assertBounds(Optimize it, ArithExpr expression, LinearBoundedExpression bounds) { + val lowerBound = bounds.lowerBound + val upperBound = bounds.upperBound + if (lowerBound == upperBound) { + if (lowerBound === null) { + return + } + Assert(mkEq(expression, mkInt(lowerBound))) + } else { + if (lowerBound !== null) { + Assert(mkGe(expression, mkInt(lowerBound))) + } + if (upperBound !== null) { + Assert(mkLe(expression, mkInt(upperBound))) + } + } + } + + private def toExpr(LinearBoundedExpression linearBoundedExpression) { + switch (linearBoundedExpression) { + Dimension: variables.get(linearBoundedExpression) + LinearConstraint: createLinearCombination(linearBoundedExpression.coefficients) + default: throw new IllegalArgumentException("Unknown linear bounded expression:" + linearBoundedExpression) + } + } + + private def createLinearCombination(Map coefficients) { + val size = coefficients.size + val array = newArrayOfSize(size) + var int i = 0 + for (pair : coefficients.entrySet) { + val variable = variables.get(pair.key) + if (variable === null) { + throw new IllegalArgumentException("Unknown dimension: " + pair.key.name) + } + val coefficient = pair.value + val term = if (coefficient == 1) { + variable + } else { + mkMul(mkInt(coefficient), variable) + } + array.set(i, term) + i++ + } + mkAdd(array) + } + + override close() throws Exception { + context.close() + } +} 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 20d24b77..5fefa551 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 @@ -6,7 +6,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ScopePropagator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ObjectCreationPrecondition import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index 701eb054..101f0a3e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend @@ -12,7 +12,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ScopePropagator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage @@ -71,16 +71,13 @@ class ViatraReasoner extends LogicReasoner { } emptySolution.problemConainer = problem - val ScopePropagator scopePropagator = new ScopePropagator(emptySolution) - scopePropagator.propagateAllScopeConstraints - val method = modelGenerationMethodProvider.createModelGenerationMethod( problem, emptySolution, workspace, viatraConfig.nameNewElements, viatraConfig.typeInferenceMethod, - scopePropagator, + viatraConfig.scopePropagatorStrategy, viatraConfig.documentationLevel ) 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 99decdd9..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 @@ -6,6 +6,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold @@ -49,6 +50,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { * Configuration for cutting search space. */ public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint + + public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.PolyhedralTypeHierarchy public var List costObjectives = newArrayList } diff --git a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF index 76c113c1..43e40319 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF +++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/META-INF/MANIFEST.MF @@ -11,3 +11,5 @@ Require-Bundle: com.google.guava, org.eclipse.xtend.lib, org.eclipse.xtend.lib.macro, hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery +Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality, + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.interval 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 new file mode 100644 index 00000000..2d159752 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/Z3PolyhedronSolverTest.xtend @@ -0,0 +1,199 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality + +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver +import org.junit.After +import org.junit.Before +import org.junit.Test + +import static org.junit.Assert.* + +class Z3PolyhedronSolverTest { + var Z3PolyhedronSolver solver + var PolyhedronSaturationOperator operator + + @Before + def void setUp() { + solver = new Z3PolyhedronSolver(false) + } + + @After + def void tearDown() { + destroyOperatorIfExists() + } + + @Test + def void singleDimensionTest() { + val x = new Dimension("x", 0, 1) + createSaturationOperator(new Polyhedron(#[x], #[], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(0, x.lowerBound) + assertEquals(1, x.upperBound) + } + + @Test + def void singleDimensionNegativeValueTest() { + val x = new Dimension("x", -2, -1) + createSaturationOperator(new Polyhedron(#[x], #[], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(-2, x.lowerBound) + assertEquals(-1, x.upperBound) + } + + @Test + def void singleDimensionConstraintTest() { + val x = new Dimension("x", null, null) + val constraint = new LinearConstraint(#{x -> 2}, 0, 2) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(0, x.lowerBound) + assertEquals(1, x.upperBound) + } + + @Test + def void singleDimensionConstraintUnitCoefficientTest() { + val x = new Dimension("x", null, null) + val constraint = new LinearConstraint(#{x -> 1}, 1, 3) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, x.lowerBound) + assertEquals(3, x.upperBound) + } + + @Test + def void singleDimensionConstraintIntegerTest() { + val x = new Dimension("x", null, null) + val constraint = new LinearConstraint(#{x -> 2}, 0, 3) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(0, x.lowerBound) + assertEquals(1, x.upperBound) + } + + @Test + def void singleDimensionUnboundedFromAboveTest() { + val x = new Dimension("x", 0, null) + createSaturationOperator(new Polyhedron(#[x], #[], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(0, x.lowerBound) + assertEquals(null, x.upperBound) + } + + @Test + def void singleDimensionUnboundedFromBelowTest() { + val x = new Dimension("x", null, 0) + createSaturationOperator(new Polyhedron(#[x], #[], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(null, x.lowerBound) + assertEquals(0, x.upperBound) + } + + @Test + def void singleDimensionUnsatisfiableTest() { + val x = new Dimension("x", 0, 1) + val constraint = new LinearConstraint(#{x -> 2}, -2, -1) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.EMPTY, result) + } + + @Test + def void equalityConstraintTest() { + val x = new Dimension("x", null, null) + val y = new Dimension("y", 1, 2) + val constraint = new LinearConstraint(#{x -> 2, y -> 2}, 6, 6) + createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, x.lowerBound) + assertEquals(2, x.upperBound) + } + + @Test + def void saturateConstraintTest() { + val x = new Dimension("x", 0, 2) + val y = new Dimension("y", 1, 2) + val constraint = new LinearConstraint(#{x -> 2, y -> 1}, 0, 8) + createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[constraint])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, constraint.lowerBound) + assertEquals(6, constraint.upperBound) + } + + @Test(expected=IllegalArgumentException) + def void unknownVariableTest() { + val x = new Dimension("x", 0, 1) + val y = new Dimension("y", 0, 1) + val constraint = new LinearConstraint(#{y -> 2}, 0, 2) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) + + saturate() + } + + @Test + def void unsatisfiableMultipleInheritanceTest() { + val x = new Dimension("x", 0, 1) + val y = new Dimension("y", 0, 1) + val z = new Dimension("z", 0, 1) + createSaturationOperator(new Polyhedron( + #[x, y, z], + #[ + new LinearConstraint(#{x -> 1, y -> 1}, 1, 1), + new LinearConstraint(#{x -> 1, z -> 1}, 1, 1), + new LinearConstraint(#{y -> 1, z -> 1}, 1, 1) + ], + #[x, y, z] + )) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.EMPTY, result) + } + + private def createSaturationOperator(Polyhedron polyhedron) { + destroyOperatorIfExists() + operator = solver.createSaturationOperator(polyhedron) + } + + private def destroyOperatorIfExists() { + if (operator !== null) { + operator.close + } + } + + private def saturate() { + operator.saturate + } +} -- cgit v1.2.3-54-g00ecf 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 ++++++ .../com.microsoft.z3/META-INF/MANIFEST.MF | 2 +- .../META-INF/MANIFEST.MF | 3 +- .../ModelGenerationMethodProvider.xtend | 4 +- .../cardinality/CbcPolyhedronSolver.xtend | 182 ++++++++++++++ .../cardinality/CbcPolyhedronSolverTest.xtend | 31 +++ .../tests/cardinality/PolyhedronSolverTest.xtend | 216 +++++++++++++++++ .../tests/cardinality/Z3PolyhedronSolverTest.xtend | 197 +--------------- 19 files changed, 952 insertions(+), 197 deletions(-) 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 create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/CbcPolyhedronSolverTest.xtend create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/tests/cardinality/PolyhedronSolverTest.xtend (limited to 'Solvers/SMT-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); +} 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 Bundle-NativeCode: lib/libz3.so; lib/libz3java.so; osname=Linux; - processor=x86_64; + processor=x86_64, lib/libz3.dylib; lib/libz3java.dylib; 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", org.eclipse.xtext;bundle-version="2.10.0", org.eclipse.viatra.transformation.runtime.emf;bundle-version="1.5.0", org.eclipse.xtext.xbase;bundle-version="2.10.0", - com.microsoft.z3;bundle-version="4.8.5" + com.microsoft.z3;bundle-version="4.8.5", + hu.bme.mit.inf.dslreasoner.ilp.cbc;bundle-version="1.0.0" Bundle-RequiredExecutionEnvironment: JavaSE-1.8 Import-Package: org.apache.log4j Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index 0040dbcd..0ceb5b2e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend @@ -4,10 +4,10 @@ import com.google.common.collect.ImmutableMap import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider @@ -119,7 +119,7 @@ class ModelGenerationMethodProvider { new ScopePropagator(emptySolution) case PolyhedralTypeHierarchy: { val types = queries.refineObjectQueries.keySet.map[newType].toSet - val solver = new Z3PolyhedronSolver + val solver = new CbcPolyhedronSolver new PolyhedronScopePropagator(emptySolution, types, solver) } 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 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +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.Map +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +@FinalFieldsConstructor +class CbcPolyhedronSolver implements PolyhedronSolver { + val double timeoutSeconds + val boolean silent + + new() { + this(10, true) + } + + override createSaturationOperator(Polyhedron polyhedron) { + new CbcSaturationOperator(polyhedron, timeoutSeconds, silent) + } +} + +class CbcSaturationOperator implements PolyhedronSaturationOperator { + @Accessors val Polyhedron polyhedron + val double timeoutSeconds + val boolean silent + val double[] columnLowerBounds + val double[] columnUpperBounds + val double[] objective + val Map dimensionsToIndicesMap + + new(Polyhedron polyhedron, double timeoutSeconds, boolean silent) { + this.polyhedron = polyhedron + this.timeoutSeconds = timeoutSeconds + this.silent = silent + val numDimensions = polyhedron.dimensions.size + columnLowerBounds = newDoubleArrayOfSize(numDimensions) + columnUpperBounds = newDoubleArrayOfSize(numDimensions) + objective = newDoubleArrayOfSize(numDimensions) + dimensionsToIndicesMap = ImmutableMap.copyOf(polyhedron.dimensions.indexed.toMap([value], [key])) + } + + override saturate() { + val numDimensions = polyhedron.dimensions.size + for (var int j = 0; j < numDimensions; j++) { + val dimension = polyhedron.dimensions.get(j) + columnLowerBounds.set(j, dimension.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) + columnUpperBounds.set(j, dimension.upperBound.toDouble(Double.POSITIVE_INFINITY)) + } + val numConstraints = polyhedron.constraints.size + val rowStarts = newIntArrayOfSize(numConstraints + 1) + val rowLowerBounds = newDoubleArrayOfSize(numConstraints) + val rowUpperBounds = newDoubleArrayOfSize(numConstraints) + val numEntries = polyhedron.constraints.map[coefficients.size].reduce[a, b|a + b] ?: 0 + rowStarts.set(numConstraints, numEntries) + val columnIndices = newIntArrayOfSize(numEntries) + val entries = newDoubleArrayOfSize(numEntries) + var int index = 0 + for (var int i = 0; i < numConstraints; i++) { + rowStarts.set(i, index) + val constraint = polyhedron.constraints.get(i) + rowLowerBounds.set(i, constraint.lowerBound.toDouble(Double.NEGATIVE_INFINITY)) + rowUpperBounds.set(i, constraint.upperBound.toDouble(Double.POSITIVE_INFINITY)) + if (!dimensionsToIndicesMap.keySet.containsAll(constraint.coefficients.keySet)) { + throw new IllegalArgumentException("Constrains has unknown dimensions") + } + for (var int j = 0; j < numDimensions; j++) { + val dimension = polyhedron.dimensions.get(j) + val coefficient = constraint.coefficients.get(dimension) + if (coefficient !== null && coefficient != 0) { + columnIndices.set(index, j) + entries.set(index, coefficient) + index++ + } + } + } + if (index != numEntries) { + 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) + } + switch (expressionToSaturate) { + Dimension: { + val j = getIndex(expressionToSaturate) + objective.set(j, 1) + } + LinearConstraint: { + for (pair : expressionToSaturate.coefficients.entrySet) { + val j = getIndex(pair.key) + 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, value, columnLowerBounds, rowLowerBounds) + } + case CbcResult.SOLUTION_UNBOUNDED: { + expressionToSaturate.lowerBound = null + setBound(expressionToSaturate, 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) + } + 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, timeoutSeconds, silent) + switch (maximizationResult) { + CbcResult.SolutionBounded: { + val value = Math.ceil(-maximizationResult.value) + expressionToSaturate.upperBound = value as int + setBound(expressionToSaturate, value, columnUpperBounds, rowUpperBounds) + } + case CbcResult.SOLUTION_UNBOUNDED: { + expressionToSaturate.upperBound = null + setBound(expressionToSaturate, 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 + } + + private def toDouble(Integer nullableInt, double defaultValue) { + if (nullableInt === null) { + defaultValue + } else { + nullableInt.doubleValue + } + } + + private def int getIndex(Dimension dimension) { + val index = dimensionsToIndicesMap.get(dimension) + if (index === null) { + throw new IllegalArgumentException("Unknown dimension: " + dimension) + } + index + } + + private def void setBound(LinearBoundedExpression expression, double bound, double[] columnBounds, + double[] rowBounds) { + switch (expression) { + Dimension: { + val j = getIndex(expression) + columnBounds.set(j, bound) + } + LinearConstraint: { + val i = polyhedron.constraints.indexOf(expression) + if (i >= 0) { + rowBounds.set(i, bound) + } + } + } + } + + override close() throws Exception { + // Nothing to close + } +} 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 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality + +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult +import org.junit.Test + +import static org.junit.Assert.* + +class CbcPolyhedronSolverTest extends PolyhedronSolverTest { + + override protected createSolver() { + new CbcPolyhedronSolver(10, false) + } + + @Test + def void timeoutTest() { + val solver = new CbcPolyhedronSolver(0, false) + val x = new Dimension("x", 0, 1) + val polyhedron = new Polyhedron(#[x], #[], #[x]) + val operator = solver.createSaturationOperator(polyhedron) + try { + val result = operator.saturate + + assertEquals(PolyhedronSaturationResult.UNKNOWN, result) + } finally { + operator.close() + } + } +} 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 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality + +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult +import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSolver +import org.junit.After +import org.junit.Before +import org.junit.Test + +import static org.junit.Assert.* + +abstract class PolyhedronSolverTest { + var PolyhedronSolver solver + var PolyhedronSaturationOperator operator + + protected def PolyhedronSolver createSolver() + + @Before + def void setUp() { + solver = createSolver() + } + + @After + def void tearDown() { + destroyOperatorIfExists() + } + + @Test + def void singleDimensionTest() { + val x = new Dimension("x", 0, 1) + createSaturationOperator(new Polyhedron(#[x], #[], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(0, x.lowerBound) + assertEquals(1, x.upperBound) + } + + @Test + def void singleDimensionNegativeValueTest() { + val x = new Dimension("x", -2, -1) + createSaturationOperator(new Polyhedron(#[x], #[], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(-2, x.lowerBound) + assertEquals(-1, x.upperBound) + } + + @Test + def void singleDimensionConstraintTest() { + val x = new Dimension("x", null, null) + val constraint = new LinearConstraint(#{x -> 2}, 0, 2) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(0, x.lowerBound) + assertEquals(1, x.upperBound) + } + + @Test + def void singleDimensionConstraintUnitCoefficientTest() { + val x = new Dimension("x", null, null) + val constraint = new LinearConstraint(#{x -> 1}, 1, 3) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, x.lowerBound) + assertEquals(3, x.upperBound) + } + + @Test + def void singleDimensionConstraintIntegerTest() { + val x = new Dimension("x", null, null) + val constraint = new LinearConstraint(#{x -> 2}, 0, 3) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(0, x.lowerBound) + assertEquals(1, x.upperBound) + } + + @Test + def void singleDimensionUnboundedFromAboveTest() { + val x = new Dimension("x", 0, null) + createSaturationOperator(new Polyhedron(#[x], #[], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(0, x.lowerBound) + assertEquals(null, x.upperBound) + } + + @Test + def void singleDimensionUnboundedFromBelowTest() { + val x = new Dimension("x", null, 0) + createSaturationOperator(new Polyhedron(#[x], #[], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(null, x.lowerBound) + assertEquals(0, x.upperBound) + } + + @Test + def void singleDimensionUnsatisfiableTest() { + val x = new Dimension("x", 0, 1) + val constraint = new LinearConstraint(#{x -> 2}, -2, -1) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.EMPTY, result) + } + + @Test + def void equalityConstraintTest() { + val x = new Dimension("x", null, null) + val y = new Dimension("y", 1, 2) + val constraint = new LinearConstraint(#{x -> 2, y -> 2}, 6, 6) + createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[x])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, x.lowerBound) + assertEquals(2, x.upperBound) + } + + @Test + def void saturateConstraintTest() { + val x = new Dimension("x", 0, 2) + val y = new Dimension("y", 1, 2) + val constraint = new LinearConstraint(#{x -> 2, y -> 1}, 0, 8) + createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[constraint])) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.SATURATED, result) + assertEquals(1, constraint.lowerBound) + assertEquals(6, constraint.upperBound) + } + + @Test(expected=IllegalArgumentException) + def void unknownVariableTest() { + val x = new Dimension("x", 0, 1) + val y = new Dimension("y", 0, 1) + val constraint = new LinearConstraint(#{y -> 2}, 0, 2) + createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) + + saturate() + } + + @Test + def void unsatisfiableMultipleInheritanceTest() { + val x = new Dimension("x", 0, 1) + val y = new Dimension("y", 0, 1) + val z = new Dimension("z", 0, 1) + createSaturationOperator(new Polyhedron( + #[x, y, z], + #[ + new LinearConstraint(#{x -> 1, y -> 1}, 1, 1), + new LinearConstraint(#{x -> 1, z -> 1}, 1, 1), + new LinearConstraint(#{y -> 1, z -> 1}, 1, 1) + ], + #[x, y, z] + )) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.EMPTY, result) + } + + @Test + def void unboundedRelaxationWithNoIntegerSolutionTest() { + val x = new Dimension("x", 0, 1) + val y = new Dimension("y", 0, null) + createSaturationOperator(new Polyhedron( + #[x, y], + #[new LinearConstraint(#{x -> 2}, 1, 1)], + #[x, y] + )) + + val result = saturate() + + assertEquals(PolyhedronSaturationResult.EMPTY, result) + } + + private def createSaturationOperator(Polyhedron polyhedron) { + destroyOperatorIfExists() + operator = solver.createSaturationOperator(polyhedron) + } + + private def destroyOperatorIfExists() { + if (operator !== null) { + operator.close + } + } + + private def saturate() { + operator.saturate + } +} 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 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.tests.cardinality -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Dimension -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearConstraint -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Polyhedron -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationOperator -import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronSaturationResult import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver -import org.junit.After -import org.junit.Before -import org.junit.Test -import static org.junit.Assert.* - -class Z3PolyhedronSolverTest { - var Z3PolyhedronSolver solver - var PolyhedronSaturationOperator operator - - @Before - def void setUp() { - solver = new Z3PolyhedronSolver(false) - } - - @After - def void tearDown() { - destroyOperatorIfExists() - } - - @Test - def void singleDimensionTest() { - val x = new Dimension("x", 0, 1) - createSaturationOperator(new Polyhedron(#[x], #[], #[x])) - - val result = saturate() - - assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(0, x.lowerBound) - assertEquals(1, x.upperBound) - } - - @Test - def void singleDimensionNegativeValueTest() { - val x = new Dimension("x", -2, -1) - createSaturationOperator(new Polyhedron(#[x], #[], #[x])) - - val result = saturate() - - assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(-2, x.lowerBound) - assertEquals(-1, x.upperBound) - } - - @Test - def void singleDimensionConstraintTest() { - val x = new Dimension("x", null, null) - val constraint = new LinearConstraint(#{x -> 2}, 0, 2) - createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) - - val result = saturate() - - assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(0, x.lowerBound) - assertEquals(1, x.upperBound) - } - - @Test - def void singleDimensionConstraintUnitCoefficientTest() { - val x = new Dimension("x", null, null) - val constraint = new LinearConstraint(#{x -> 1}, 1, 3) - createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) - - val result = saturate() - - assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(1, x.lowerBound) - assertEquals(3, x.upperBound) - } - - @Test - def void singleDimensionConstraintIntegerTest() { - val x = new Dimension("x", null, null) - val constraint = new LinearConstraint(#{x -> 2}, 0, 3) - createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) - - val result = saturate() - - assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(0, x.lowerBound) - assertEquals(1, x.upperBound) - } - - @Test - def void singleDimensionUnboundedFromAboveTest() { - val x = new Dimension("x", 0, null) - createSaturationOperator(new Polyhedron(#[x], #[], #[x])) - - val result = saturate() - - assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(0, x.lowerBound) - assertEquals(null, x.upperBound) - } - - @Test - def void singleDimensionUnboundedFromBelowTest() { - val x = new Dimension("x", null, 0) - createSaturationOperator(new Polyhedron(#[x], #[], #[x])) - - val result = saturate() - - assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(null, x.lowerBound) - assertEquals(0, x.upperBound) - } - - @Test - def void singleDimensionUnsatisfiableTest() { - val x = new Dimension("x", 0, 1) - val constraint = new LinearConstraint(#{x -> 2}, -2, -1) - createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) - - val result = saturate() - - assertEquals(PolyhedronSaturationResult.EMPTY, result) - } - - @Test - def void equalityConstraintTest() { - val x = new Dimension("x", null, null) - val y = new Dimension("y", 1, 2) - val constraint = new LinearConstraint(#{x -> 2, y -> 2}, 6, 6) - createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[x])) - - val result = saturate() - - assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(1, x.lowerBound) - assertEquals(2, x.upperBound) - } - - @Test - def void saturateConstraintTest() { - val x = new Dimension("x", 0, 2) - val y = new Dimension("y", 1, 2) - val constraint = new LinearConstraint(#{x -> 2, y -> 1}, 0, 8) - createSaturationOperator(new Polyhedron(#[x, y], #[constraint], #[constraint])) - - val result = saturate() - - assertEquals(PolyhedronSaturationResult.SATURATED, result) - assertEquals(1, constraint.lowerBound) - assertEquals(6, constraint.upperBound) - } - - @Test(expected=IllegalArgumentException) - def void unknownVariableTest() { - val x = new Dimension("x", 0, 1) - val y = new Dimension("y", 0, 1) - val constraint = new LinearConstraint(#{y -> 2}, 0, 2) - createSaturationOperator(new Polyhedron(#[x], #[constraint], #[x])) - - saturate() - } - - @Test - def void unsatisfiableMultipleInheritanceTest() { - val x = new Dimension("x", 0, 1) - val y = new Dimension("y", 0, 1) - val z = new Dimension("z", 0, 1) - createSaturationOperator(new Polyhedron( - #[x, y, z], - #[ - new LinearConstraint(#{x -> 1, y -> 1}, 1, 1), - new LinearConstraint(#{x -> 1, z -> 1}, 1, 1), - new LinearConstraint(#{y -> 1, z -> 1}, 1, 1) - ], - #[x, y, z] - )) - - val result = saturate() - - assertEquals(PolyhedronSaturationResult.EMPTY, result) - } - - private def createSaturationOperator(Polyhedron polyhedron) { - destroyOperatorIfExists() - operator = solver.createSaturationOperator(polyhedron) - } - - private def destroyOperatorIfExists() { - if (operator !== null) { - operator.close - } - } - - private def saturate() { - operator.saturate +class Z3PolyhedronSolverTest extends PolyhedronSolverTest { + + override protected createSolver() { + new Z3PolyhedronSolver(false) } } -- cgit v1.2.3-54-g00ecf