Scope unsat benchmarks

4 files changed, 24 insertions, 20 deletions

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath
index de68b5f7..25b7f16f 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath
@@ -1,11 +1,15 @@
-<?xml version="1.0" encoding="UTF-8"?>

-<classpath>

-        <classpathentry kind="src" path="xtend-gen"/>

-        <classpathentry kind="src" path="queries"/>

-        <classpathentry kind="src" path="vql-gen"/>

-        <classpathentry exported="true" kind="lib" path="lib/alloy4.2_2015-02-22.jar"/>

-        <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>

-        <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>

-        <classpathentry kind="src" path="src"/>

-        <classpathentry kind="output" path="bin"/>

-</classpath>

+<?xml version="1.0" encoding="UTF-8"?>
+<classpath>
+        <classpathentry kind="src" path="xtend-gen"/>
+        <classpathentry kind="src" path="queries"/>
+        <classpathentry kind="src" path="vql-gen"/>
+        <classpathentry exported="true" kind="lib" path="lib/alloy4.2_2015-02-22.jar"/>
+        <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
+        <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
+        <classpathentry kind="src" path="src">
+                <attributes>
+                        <attribute name="org.eclipse.jdt.launching.CLASSPATH_ATTR_LIBRARY_PATH_ENTRY" value="hu.bme.mit.inf.dlsreasoner.alloy.reasoner/lib"/>
+                </attributes>
+        </classpathentry>
+        <classpathentry kind="output" path="bin"/>
+</classpath>
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
index b944302b..75581def 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
@@ -20,7 +20,8 @@ Require-Bundle: com.google.guava,
  org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.3.0",
  hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
  org.eclipse.viatra.query.runtime;bundle-version="2.0.0"
-Import-Package: org.apache.log4j;version="1.2.15"
-Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner
-Bundle-ActivationPolicy: lazy
 Bundle-RequiredExecutionEnvironment: JavaSE-1.8
+Bundle-ActivationPolicy: lazy
+Bundle-NativeCode: libminisat.so;osname=Linux;processor=x86_64
+Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner
+Import-Package: org.apache.log4j;version="1.2.15"
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend
index 5e442ca7..f19ac30f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/statecoder/NeighbourhoodBasedStateCoderFactory.xtend
@@ -59,15 +59,14 @@ class NeighbourhoodBasedPartialInterpretationStateCoder<ModelRep, NodeRep> exten
         override doCreateActivationCode(IPatternMatch match) {
                 val size = match.specification.parameters.size
                 val res = new ArrayList(size)
-                var int index = 0
                 var int equivalenceHash = 0
                 val prime = 31
 
-                while (index < size) {
-                        res.add(getCode(match.get(index)))
-                        index++
+                for (var int index = 0; index < size; index++) {
+                        val matchArgument = match.get(index)
+                        res.add(getCode(matchArgument))
                         for (var i = 0; i < index; i++) {
-                                val number = if (match.get(index) === match.get(i)) {
+                                val number = if (matchArgument === match.get(i)) {
                                                 1
                                         } else {
                                                 0
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 6f38d261..c0a71c85 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
@@ -55,7 +55,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
          */

         public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint

 

-        public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(

+        public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.Polyhedral(

                 PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)

         

         public var List<LinearTypeConstraintHint> hints = newArrayList