Polyhedron solver SAT fix and initial scope filtering

3 files changed, 25 insertions, 6 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend
index 75c396b4..708f93dc 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/CbcPolyhedronSolver.xtend
@@ -193,7 +193,11 @@ class CbcSaturationOperator extends AbstractPolyhedronSaturationOperator {
                                 setBound(expressionToSaturate, constraints, Double.POSITIVE_INFINITY, columnUpperBounds, rowUpperBounds)
                         }
                         case CbcResult.UNSAT:
-                                throw new RuntimeException("Minimization was SAT, but maximization is UNSAT")
+                                if (lpRelaxation) {
+                                        return PolyhedronSaturationResult.EMPTY
+                                } else {
+                                        throw new RuntimeException("Minimization was SAT, but maximization is UNSAT")
+                                }
                         case CbcResult.ABANDONED,
                         case CbcResult.TIMEOUT:
                                 return PolyhedronSaturationResult.UNKNOWN
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend
index c92260ea..3e4fea8a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend
@@ -44,6 +44,8 @@ class RelationMultiplicityConstraint {
         }
 
         def constrainsUnrepairable() {
+                // TODO Optimize the unrepairable matches computation,
+                // or come up with a heuristic when does computing unrepairables worth the overhead.
                 constrainsUnfinished && canHaveMultipleSourcesPerTarget && false
         }
 
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend
index 8aaaacb5..cb5b587f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend
@@ -1,5 +1,6 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic

 

+import com.google.common.collect.ImmutableList

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput

@@ -12,18 +13,18 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.Par
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.Problem2PartialInterpretationTrace

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory

+import java.math.BigDecimal

 import java.util.HashMap

+import java.util.HashSet

 import java.util.List

 import java.util.Map

+import java.util.Set

 import org.eclipse.emf.common.util.Enumerator

+import org.eclipse.emf.ecore.EAttribute

 import org.eclipse.emf.ecore.EObject

 import org.eclipse.emf.ecore.resource.Resource

 

 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

-import java.util.HashSet

-import java.util.Set

-import java.math.BigDecimal

-import org.eclipse.emf.ecore.EAttribute

 

 class InstanceModel2PartialInterpretation {

         val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE

@@ -36,7 +37,19 @@ class InstanceModel2PartialInterpretation {
                 Resource resource,

                 boolean withID) 

         {

-                val objects = resource.allContents.toList

+                val objectsBuilder = ImmutableList.builder

+                val treeIterator = resource.allContents

+                val referencesUsed = ecore2Logic.allReferencesInScope(metamodelTranslationResult.trace).toSet

+                while (treeIterator.hasNext) {

+                        val object = treeIterator.next

+                        val containingReference = object.eContainmentFeature

+                        if (containingReference === null || referencesUsed.contains(containingReference)) {

+                                objectsBuilder.add(object)

+                        } else {

+                                treeIterator.prune

+                        }

+                }

+                val objects = objectsBuilder.build

                 return transform(metamodelTranslationResult,objects,withID)

         }