VAMPIRE: Further develop testing fo r Vampire solver

44 files changed, 155 insertions, 89 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
index 2a46499b..ef511dca 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
index e5f3b018..c9ed86f5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
index cdc646f3..e24f55b7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
index 8d3c30f6..af221451 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
index 40d6d3a8..1f1241ce 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
index 999df988..e89f2182 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
index b3a37f45..9c0c7969 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
index dcca29b0..fe289357 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
index 07d0db76..6cb28d31 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
index 221a8681..7e8ae1ab 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
index f24c9c20..81de0171 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
index 0d110422..c5672cca 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
index aebb5604..2b96a53a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
index f4911143..5faad94e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
index fc8d3e99..b223dbe5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
@@ -7,12 +7,15 @@ class VampireSolverConfiguration extends LogicSolverConfiguration {
         public var int contCycleLevel = 0
         public var boolean uniquenessDuplicates = false
         public var int iteration = -1
+        public var BackendSolver solver = BackendSolver::VAMP
         //choose needed backend solver
 //      public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
 }
 
 
-enum VampireBackendSolver {
+enum BackendSolver {
+        VAMP,
+        CVC4
         //add needed things
 }
 
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
index c5cfb1c7..c1eb3382 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
@@ -10,6 +10,7 @@ import org.eclipse.emf.ecore.resource.Resource
 import org.eclipse.xtend.lib.annotations.Data

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver

 

 class VampireSolverException extends Exception {

         new(String s) {

@@ -39,30 +40,58 @@ class VampireHandler {
         // val fileName = "problem.als"

         public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration) {

 

-                val CMD = "cmd /c "

+                // Vampire

                 val VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"

                 val VAMPNAME = "vampire.exe"

+                val VAMPLOC = VAMPDIR + VAMPNAME

+

+                // CVC4

+                val CVC4DIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"

+                val CVC4NAME = "vampire.exe"

+                val CVC4LOC = CVC4DIR + CVC4NAME

+

+                val CMD = "cmd /c "

                 val TEMPNAME = "TEMP.tptp"

-                val OPTION = " --mode casc_sat -t 300 "

-                val SOLNNAME = "solution" + configuration.typeScopes.maxNewElements +"_" + configuration.iteration + ".tptp"

+                val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements +

+                        "_" + configuration.iteration + ".tptp"

                 val PATH = "C:/cygwin64/bin"

 

                 val wsURI = workspace.workspaceURI

                 val tempLoc = wsURI + TEMPNAME

                 val solnLoc = wsURI + SOLNNAME + " "

-                val vampLoc = VAMPDIR + VAMPNAME

 

                 // 1. create temp file for vampire problem

                 var tempURI = workspace.writeModel(problem, TEMPNAME).toFileString

 

                 // 2. run command and save to 

                 // need to have cygwin downloaded

-                var startTime = System.currentTimeMillis

-                val p = Runtime.runtime.exec(CMD + vampLoc + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH))

-                // 2.1 determine time left

-                p.waitFor

-                val solverTime = System.currentTimeMillis - startTime

+                var long startTime = -1 as long

+                var long solverTime = -1 as long

+                var Process p = null

+                if (configuration.solver == BackendSolver::VAMP) {

 

+                        var OPTION = " --mode casc_sat "

+                        if (configuration.runtimeLimit != -1) {

+                                OPTION = OPTION + "-t " + configuration.runtimeLimit + " "

+                        }

+

+                        startTime = System.currentTimeMillis

+                        p = Runtime.runtime.exec(CMD + VAMPLOC + OPTION + tempLoc + " > " + solnLoc, newArrayList("Path=" + PATH))

+                        p.waitFor

+                        solverTime = System.currentTimeMillis - startTime

+                }

+                if (configuration.solver == BackendSolver::CVC4) {

+                        var OPTION = " SAT "

+                        if (configuration.runtimeLimit != -1) {

+                                OPTION = " " + configuration.runtimeLimit + OPTION

+                        }

+                        println(CMD + CVC4LOC + tempLoc + OPTION + " > " + solnLoc)

+                        p = Runtime.runtime.exec(CMD + CVC4LOC + tempLoc + OPTION + " > " + solnLoc, newArrayList("Path=" + PATH))

+                        p.waitFor

+                        solverTime = System.currentTimeMillis - startTime

+                }

+

+                // 2.1 determine time left

                 // 2.2 store output into local variable

                 val BufferedReader reader = new BufferedReader(new InputStreamReader(p.getInputStream()));

                 val List<String> output = newArrayList

@@ -74,14 +103,13 @@ class VampireHandler {
 

 //      println(output.toString())

                 // 4. delete temp file

-                workspace.getFile(TEMPNAME).delete              

+                workspace.getFile(TEMPNAME).delete

 

                 // 5. determine and return whether or not finite model was found

                 // 6. save solution as a .tptp model

                 val root = workspace.readModel(VampireModel, SOLNNAME).eResource.contents

 

 //              println((root.get(0) as VampireModel ).comments)

-                

                 return new MonitoredVampireSolution(solverTime, root.get(0) as VampireModel)

 

         /*

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index 2c203d6e..85f3773c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index f2461efc..77dc060f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java
deleted file mode 100644
index 91e9bed0..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java
+++ /dev/null
@@ -1,5 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner;

-

-@SuppressWarnings("all")

-public enum VampireBackendSolver {

-}

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
index 5086d15a..7bb17b59 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
@@ -1,5 +1,6 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner;

 

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver;

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;

 

 @SuppressWarnings("all")

@@ -9,4 +10,6 @@ public class VampireSolverConfiguration extends LogicSolverConfiguration {
   public boolean uniquenessDuplicates = false;

   

   public int iteration = (-1);

+  

+  public BackendSolver solver = BackendSolver.VAMP;

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index f537b830..eb1685d1 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
index ebe7bb60..3ddf9cfc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index 14a639ad..66f9d9e8 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index ba5dbd89..bafcfab6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index f5e4ca8c..a4af882f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index 6c06a366..08f9fd96 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index 1ee73cd6..dc25e3be 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index edda9f05..37b0c7a5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index 8edf2fe9..6d562aa8 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index 18c788c6..5ed9ac3b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
index 8fe89f37..111053a4 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
index b327631b..f33599f9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
index a1f19410..7906c5fb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
@@ -1,5 +1,6 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;

 

+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;

@@ -15,29 +16,63 @@ import org.eclipse.emf.ecore.EObject;
 import org.eclipse.xtext.xbase.lib.CollectionLiterals;

 import org.eclipse.xtext.xbase.lib.Conversions;

 import org.eclipse.xtext.xbase.lib.Exceptions;

+import org.eclipse.xtext.xbase.lib.InputOutput;

 

 @SuppressWarnings("all")

 public class VampireHandler {

   public MonitoredVampireSolution callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) {

     try {

-      final String CMD = "cmd /c ";

       final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\";

       final String VAMPNAME = "vampire.exe";

+      final String VAMPLOC = (VAMPDIR + VAMPNAME);

+      final String CVC4DIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\";

+      final String CVC4NAME = "vampire.exe";

+      final String CVC4LOC = (CVC4DIR + CVC4NAME);

+      final String CMD = "cmd /c ";

       final String TEMPNAME = "TEMP.tptp";

-      final String OPTION = " --mode casc_sat -t 300 ";

-      final String SOLNNAME = (((("solution" + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + ".tptp");

+      String _string = configuration.solver.toString();

+      String _plus = ("solution" + _string);

+      String _plus_1 = (_plus + "_");

+      String _plus_2 = (_plus_1 + Integer.valueOf(configuration.typeScopes.maxNewElements));

+      String _plus_3 = (_plus_2 + 

+        "_");

+      String _plus_4 = (_plus_3 + Integer.valueOf(configuration.iteration));

+      final String SOLNNAME = (_plus_4 + ".tptp");

       final String PATH = "C:/cygwin64/bin";

       final URI wsURI = workspace.getWorkspaceURI();

       final String tempLoc = (wsURI + TEMPNAME);

-      String _plus = (wsURI + SOLNNAME);

-      final String solnLoc = (_plus + " ");

-      final String vampLoc = (VAMPDIR + VAMPNAME);

+      String _plus_5 = (wsURI + SOLNNAME);

+      final String solnLoc = (_plus_5 + " ");

       String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString();

-      long startTime = System.currentTimeMillis();

-      final Process p = Runtime.getRuntime().exec((((((CMD + vampLoc) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class)));

-      p.waitFor();

-      long _currentTimeMillis = System.currentTimeMillis();

-      final long solverTime = (_currentTimeMillis - startTime);

+      long startTime = (-((long) 1));

+      long solverTime = (-((long) 1));

+      Process p = null;

+      boolean _equals = Objects.equal(configuration.solver, BackendSolver.VAMP);

+      if (_equals) {

+        String OPTION = " --mode casc_sat ";

+        if ((configuration.runtimeLimit != (-1))) {

+          OPTION = (((OPTION + "-t ") + Integer.valueOf(configuration.runtimeLimit)) + " ");

+        }

+        startTime = System.currentTimeMillis();

+        p = Runtime.getRuntime().exec((((((CMD + VAMPLOC) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class)));

+        p.waitFor();

+        long _currentTimeMillis = System.currentTimeMillis();

+        long _minus = (_currentTimeMillis - startTime);

+        solverTime = _minus;

+      }

+      boolean _equals_1 = Objects.equal(configuration.solver, BackendSolver.CVC4);

+      if (_equals_1) {

+        String OPTION_1 = " SAT ";

+        if ((configuration.runtimeLimit != (-1))) {

+          OPTION_1 = ((" " + Integer.valueOf(configuration.runtimeLimit)) + OPTION_1);

+        }

+        InputOutput.<String>println((((((CMD + CVC4LOC) + tempLoc) + OPTION_1) + " > ") + solnLoc));

+        p = Runtime.getRuntime().exec((((((CMD + CVC4LOC) + tempLoc) + OPTION_1) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class)));

+        p.waitFor();

+        long _currentTimeMillis_1 = System.currentTimeMillis();

+        long _minus_1 = (_currentTimeMillis_1 - startTime);

+        solverTime = _minus_1;

+      }

       InputStream _inputStream = p.getInputStream();

       InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream);

       final BufferedReader reader = new BufferedReader(_inputStreamReader);

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
index b786abfb..0af80e6c 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
@@ -7,47 +7,47 @@ Bundle-ClassPath: .
 Bundle-Vendor: %providerName
 Bundle-Localization: plugin
 Export-Package: ca.mcgill.ecse.dslreasoner.vamipre.yakindumm,
-  ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.impl,
-  ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.util,
-  ca.mcgill.ecse.dslreasoner.vampire.queries,
-  ca.mcgill.ecse.dslreasoner.vampire.yakindumm,
-  ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl,
-  ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util,
-  yakindumm,
-  yakindumm.impl,
-  yakindumm.util,
-  yakindumm.yakindumm,
-  yakindumm.yakindumm.impl,
-  yakindumm.yakindumm.util
+ ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.impl,
+ ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.util,
+ ca.mcgill.ecse.dslreasoner.vampire.queries,
+ ca.mcgill.ecse.dslreasoner.vampire.yakindumm,
+ ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl,
+ ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util,
+ yakindumm,
+ yakindumm.impl,
+ yakindumm.util,
+ yakindumm.yakindumm,
+ yakindumm.yakindumm.impl,
+ yakindumm.yakindumm.util
 Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime,
-  org.eclipse.core.runtime,
-  org.eclipse.emf.ecore;visibility:=reexport,
-  org.eclipse.viatra.query.runtime.rete,
-  org.eclipse.viatra.query.runtime.localsearch,
-  com.google.guava,
-  org.eclipse.xtext.xbase.lib,
-  org.eclipse.xtend.lib,
-  org.eclipse.xtend.lib.macro,
-  ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0",
-  hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
-  ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0",
-  hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
-  hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0",
-  org.eclipse.emf.ecore.xmi;bundle-version="2.13.0",
-  hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0",
-  hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0",
-  hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0",
-  hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0",
-  hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0",
-  hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0",
-  ModelGenExampleFAM_plugin;bundle-version="1.0.0",
-  ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1",
-  hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0",
-  hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1",
-  org.eclipse.viatra.query.runtime;bundle-version="2.1.0",
-  org.eclipse.collections;bundle-version="9.2.0",
-  hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0",
-  ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0"
+ org.eclipse.core.runtime,
+ org.eclipse.emf.ecore;visibility:=reexport,
+ org.eclipse.viatra.query.runtime.rete,
+ org.eclipse.viatra.query.runtime.localsearch,
+ com.google.guava,
+ org.eclipse.xtext.xbase.lib,
+ org.eclipse.xtend.lib,
+ org.eclipse.xtend.lib.macro,
+ ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0",
+ hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0",
+ ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0",
+ hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
+ hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0",
+ org.eclipse.emf.ecore.xmi;bundle-version="2.13.0",
+ hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0",
+ hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0",
+ hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0",
+ hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0",
+ hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0",
+ hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0",
+ ModelGenExampleFAM_plugin;bundle-version="1.0.0",
+ ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1",
+ hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0",
+ hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1",
+ org.eclipse.viatra.query.runtime;bundle-version="2.1.0",
+ org.eclipse.collections;bundle-version="9.2.0",
+ hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0",
+ ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0"
 Import-Package: org.apache.log4j
 Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test
 Bundle-ActivationPolicy: lazy
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
index cc7f4809..28e3e685 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
@@ -54,17 +54,17 @@ class YakinduTest {
 //              val queries = null

                 println("DSL loaded")

 

-                var MAX = 150

-                var START = 10

-                var INC = 20

-                var REPS = 1

+                var MAX = 80

+                var START = 79

+                var INC = 1

+                var REPS = 3

 

-                val EXACT = 50

+                val EXACT = 130

                 if (EXACT != -1) {

                         MAX = EXACT

                         START = EXACT

-                        INC = 1

-                        REPS = 3

+                        INC = 5

+                        REPS = 1

                 }

 

                 var writer = new PrintWriter(workspace.workspaceURI + "//_yakinduStats.csv")

@@ -93,7 +93,7 @@ class YakinduTest {
                                 var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem,

                                         new Viatra2LogicConfiguration)

 

-                                var problem = validModelExtensionProblem.output

+                                var problem = modelGenerationProblem.output

                                 workspace.writeModel(problem, "Yakindu.logicproblem")

 

 //                               println("Problem created")

@@ -125,9 +125,10 @@ class YakinduTest {
                                         // add configuration things, in config file first

                                         it.documentationLevel = DocumentationLevel::FULL

                                         it.iteration = iter

-

-                                        it.typeScopes.minNewElements = size - inc

+                                        it.runtimeLimit = 60

                                         it.typeScopes.maxNewElements = size

+                                        it.typeScopes.minNewElements = size - 5

+

 //                      if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin

 //                      if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax

                                         it.contCycleLevel = 5

@@ -167,8 +168,8 @@ class YakinduTest {
 //                       println("Time was: " + totalTimeMin + ":" + totalTimeSec)

                         }

                         println()

-                        var solverMed = solverTimes.sort.get(REPS/2)

-                        var transformationMed = transformationTimes.sort.get(REPS/2)

+                        var solverMed = solverTimes.sort.get(REPS / 2)

+                        var transformationMed = transformationTimes.sort.get(REPS / 2)

                         writer.append(solverMed.toString + "," + transformationMed.toString)

                         writer.append("\n")

                 }

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
index 1d9db781..084503b5 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
index 15159cb7..2315cd50 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
index 69cbcc0a..a3386941 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
index 16a24539..dee6f742 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
index 57a6fa02..f54cd3a0 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
index 35c48de2..b18ede4f 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
@@ -72,16 +72,16 @@ public class YakinduTest {
       final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi");

       final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance());

       InputOutput.<String>println("DSL loaded");

-      int MAX = 150;

-      int START = 10;

-      int INC = 20;

-      int REPS = 1;

-      final int EXACT = 50;

+      int MAX = 80;

+      int START = 79;

+      int INC = 1;

+      int REPS = 3;

+      final int EXACT = 130;

       if ((EXACT != (-1))) {

         MAX = EXACT;

         START = EXACT;

-        INC = 1;

-        REPS = 3;

+        INC = 5;

+        REPS = 1;

       }

       URI _workspaceURI = workspace.getWorkspaceURI();

       String _plus_2 = (_workspaceURI + "//_yakinduStats.csv");

@@ -115,7 +115,7 @@ public class YakinduTest {
                 TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel);

                 Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration();

                 TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration);

-                LogicProblem problem = validModelExtensionProblem.getOutput();

+                LogicProblem problem = modelGenerationProblem.getOutput();

                 workspace.writeModel(problem, "Yakindu.logicproblem");

                 long startTime = System.currentTimeMillis();

                 VampireSolver reasoner = null;

@@ -128,8 +128,9 @@ public class YakinduTest {
                 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {

                   it.documentationLevel = DocumentationLevel.FULL;

                   it.iteration = iter;

-                  it.typeScopes.minNewElements = (size - inc);

+                  it.runtimeLimit = 60;

                   it.typeScopes.maxNewElements = size;

+                  it.typeScopes.minNewElements = (size - 5);

                   it.contCycleLevel = 5;

                   it.uniquenessDuplicates = false;

                 };

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
index 74f8e73f..e77449e7 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
index 68b3fd77..97f29b0c 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
index fc4464b3..0e320f18 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin