Solver gives partial solutions even if it fails due to timeout or unsat

2 files changed, 5 insertions, 1 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
index 51c10b23..2a271acf 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF
@@ -15,7 +15,7 @@ Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
  org.eclipse.xtend.lib.macro,
  org.eclipse.viatra.query.runtime.matchers;bundle-version="1.5.0",
  org.eclipse.viatra.query.runtime;bundle-version="1.5.0",
- org.eclipse.viatra.dse;bundle-version="0.15.0",
+ org.eclipse.viatra.dse;bundle-version="0.20.0",
  org.eclipse.emf.ecore.edit;bundle-version="2.9.0",
  org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.7.0"
 Bundle-RequiredExecutionEnvironment: JavaSE-1.8
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 dfd8ca1a..6639e5f3 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
@@ -31,6 +31,8 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer
 import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel

 import org.eclipse.viatra.dse.solutionstore.SolutionStore

 import org.eclipse.viatra.dse.statecode.IStateCoderFactory

+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SolutionStoreWithDiversityDescriptor

+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityGranularity

 

 class ViatraReasoner extends LogicReasoner{

         val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser()

@@ -169,12 +171,14 @@ class ViatraReasoner extends LogicReasoner{
                         return createInsuficientResourcesResult=>[

                                 it.problem = problem

                                 it.resourceName="time"

+                                it.representation += strategy.solutionStoreWithCopy.solutions

                                 it.statistics = statistics

                         ]

                 } else {

                         if(solutionStore.solutions.empty) {

                                 return createInconsistencyResult => [

                                         it.problem = problem

+                                        it.representation += strategy.solutionStoreWithCopy.solutions

                                         it.statistics = statistics

                                 ]

                         } else {