From 3997c2408f192e22f809cd96faa5bc552530289d Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Sun, 14 Jun 2020 19:38:40 -0400 Subject: This branch is ready to be merged into master --- .../reasoner/VampireAnalyzerConfiguration.xtend | 2 +- .../vampire/reasoner/VampireSolver.xtend | 61 ++- .../Logic2VampireLanguageMapper_Support.xtend | 16 +- .../.VampireAnalyzerConfiguration.xtendbin | Bin 3449 -> 0 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 10104 -> 0 bytes .../ecse/dslreasoner/vampire/reasoner/.gitignore | 10 - .../vampire/reasoner/TypeMappingTechnique.java | 6 - .../vampire/reasoner/VampireSolver.java | 275 ----------- .../reasoner/VampireSolverConfiguration.java | 19 - .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 19565 -> 0 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 5080 -> 0 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 0 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 11807 -> 0 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 7880 -> 0 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 10684 -> 0 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 17151 -> 0 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11037 -> 0 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 3998 -> 0 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 7743 -> 0 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 0 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 0 bytes .../vampire/reasoner/builder/.gitignore | 42 -- .../builder/Logic2VampireLanguageMapper.java | 510 -------------------- .../builder/Logic2VampireLanguageMapperTrace.java | 65 --- ...Logic2VampireLanguageMapper_ConstantMapper.java | 34 -- ...ic2VampireLanguageMapper_ContainmentMapper.java | 386 --------------- ...Logic2VampireLanguageMapper_RelationMapper.java | 205 -------- .../Logic2VampireLanguageMapper_ScopeMapper.java | 302 ------------ .../Logic2VampireLanguageMapper_Support.java | 515 --------------------- .../Logic2VampireLanguageMapper_TypeMapper.java | 339 -------------- ...ogic2VampireLanguageMapper_TypeMapperTrace.java | 5 - .../reasoner/builder/Vampire2LogicMapper.java | 42 -- .../vampire/reasoner/builder/VampireHandler.java | 82 ---- ...pireModelInterpretation_TypeInterpretation.java | 5 - ...pretation_TypeInterpretation_FilteredTypes.java | 7 - .../reasoner/builder/VampireSolverException.java | 19 - 36 files changed, 65 insertions(+), 2882 deletions(-) delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java delete mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner') 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 1fda24d9..c3b344eb 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 @@ -8,7 +8,7 @@ class VampireSolverConfiguration public var int contCycleLevel = 0 public var boolean uniquenessDuplicates = false public var int iteration = -1 - public var BackendSolver solver = BackendSolver::VAMPIRE + public var BackendSolver solver = BackendSolver::LOCVAMP public var genModel = true public var server = false //choose needed backend solver diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend index 59084843..4b8b10a9 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend @@ -83,26 +83,27 @@ class VampireSolver extends LogicReasoner { var done = false print(" ") while (!done) { - print("(x)") +// print("(x)") done = false response = support.sendPost(form) var responseFound = false ind = 0 - while (!responseFound) { + while (!responseFound && ind= 5 && line.substring(0, 5) == "ERROR") { done = false responseFound = true } else { - if (line == "") { + if (line == "" && response.get(ind-1) != "
") {
 								done = true
 								responseFound = true
 							}
 						}
 						ind++
 					}
+					if (!done) println("(Server call failed. Trying again...)")
 				}
 				val satRaw = response.get(ind - 3)
 				val modRaw = response.get(ind - 2)
@@ -118,10 +119,35 @@ class VampireSolver extends LogicReasoner {
 				println()
 				println(sat)
 				println(mod)
+				
+				return createUndecidableResult => [
+					it.statistics = createStatistics => [
+						it.transformationTime = transformationTime as int
+						it.entries += createStringStatisticEntry => [
+							it.name = "satOut"
+							it.value = satOut
+						]
+						it.entries += createStringStatisticEntry => [
+							it.name = "satTime"
+							it.value = satTime
+						]
+						it.entries += createStringStatisticEntry => [
+							it.name = "modOut"
+							it.value = modOut
+						]
+						it.entries += createStringStatisticEntry => [
+							it.name = "modTime"
+							it.value = modTime
+						]
 
+					]
+				]
+					
+				/*
+				 * TODO
 				return createModelResult => [
 					it.problem = null
-					it.representation += createVampireModel => []
+					it.representation += createVampireModel => []//TODO Add something here
 					it.trace = trace
 					it.statistics = createStatistics => [
 						it.transformationTime = transformationTime as int
@@ -144,6 +170,7 @@ class VampireSolver extends LogicReasoner {
 
 					]
 				]
+				*/
 
 //				return newArrayList(line1, line2)
 			} else {
@@ -172,8 +199,31 @@ class VampireSolver extends LogicReasoner {
 				}
 				
 				val realModOut=modOut
- 
 				
+				return createUndecidableResult => [
+					it.statistics = createStatistics => [
+						it.transformationTime = transformationTime as int
+						it.entries += createStringStatisticEntry => [
+							it.name = "satOut"
+							it.value = "-"
+						]
+						it.entries += createStringStatisticEntry => [
+							it.name = "satTime"
+							it.value = "-"
+						]
+						it.entries += createStringStatisticEntry => [
+							it.name = "modOut"
+							it.value = realModOut
+						]
+						it.entries += createStringStatisticEntry => [
+							it.name = "modTime"
+							it.value = (vampSol.solverTime/1000.0).toString
+						]
+
+					]
+				]
+				
+				/*
 				return createModelResult => [
 					it.problem = null
 					it.representation += createVampireModel => []
@@ -199,6 +249,7 @@ class VampireSolver extends LogicReasoner {
 
 					]
 				]
+				*/
 			}
 		}
 //		return backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution,
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
index 44efd84e..fa334322 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend
@@ -299,23 +299,23 @@ class Logic2VampireLanguageMapper_Support {
 	def getSolverSpecs(BackendSolver solver) {
 		switch (solver) {
 			case BackendSolver::CVC4:
-				return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT")
+				return newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT")//TODO Update
 			case BackendSolver::DARWINFM:
-				return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s")
+				return newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s")//TODO Update
 			case BackendSolver::EDARWIN:
 				return newArrayList("E-Darwin---1.5",
-					"e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s")
+					"e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s")//TODO Update
 			case BackendSolver::GEOIII:
 				return newArrayList("Geo-III---2018C",
-					"geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s")
+					"geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s")//TODO Update
 			case BackendSolver::IPROVER:
-				return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s")
+				return newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s")//TODO Update
 			case BackendSolver::PARADOX:
-				return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s")
+				return newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s")//TODO Update
 			case BackendSolver::VAMPIRE:
-				return newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s")
+				return newArrayList("Vampire---SAT-4.5", "vampire --mode casc_sat -t %d %s")
 			case BackendSolver::Z3:
-				return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s")
+				return newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s")//TODO Update
 		}
 	}
 
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
deleted file mode 100644
index e999bce6..00000000
Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin and /dev/null differ
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
deleted file mode 100644
index 28154d14..00000000
Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and /dev/null differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore
deleted file mode 100644
index 70f60102..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore
+++ /dev/null
@@ -1,10 +0,0 @@
-/.VampireSolver.java._trace
-/.TypeMappingTechnique.java._trace
-/.VampireBackendSolver.java._trace
-/.VampireSolverConfiguration.java._trace
-/.VampireAnalyzerConfiguration.xtendbin
-/.VampireSolver.xtendbin
-/TypeMappingTechnique.java
-/VampireBackendSolver.java
-/VampireSolver.java
-/VampireSolverConfiguration.java
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java
deleted file mode 100644
index 8ffba2f1..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java
+++ /dev/null
@@ -1,6 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner;
-
-@SuppressWarnings("all")
-public enum TypeMappingTechnique {
-  FilteredTypes;
-}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
deleted file mode 100644
index eb6007ec..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
+++ /dev/null
@@ -1,275 +0,0 @@
-package ca.mcgill.ecse.dslreasoner.vampire.reasoner;
-
-import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup;
-import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler;
-import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
-import com.google.common.base.Objects;
-import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
-import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation;
-import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
-import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException;
-import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
-import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
-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.logic.model.logicresult.StatisticEntry;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics;
-import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry;
-import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
-import java.util.ArrayList;
-import java.util.List;
-import org.eclipse.emf.common.util.EList;
-import org.eclipse.xtend2.lib.StringConcatenation;
-import org.eclipse.xtext.xbase.lib.CollectionLiterals;
-import org.eclipse.xtext.xbase.lib.Exceptions;
-import org.eclipse.xtext.xbase.lib.Extension;
-import org.eclipse.xtext.xbase.lib.Functions.Function1;
-import org.eclipse.xtext.xbase.lib.InputOutput;
-import org.eclipse.xtext.xbase.lib.ListExtensions;
-import org.eclipse.xtext.xbase.lib.ObjectExtensions;
-import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
-
-@SuppressWarnings("all")
-public class VampireSolver extends LogicReasoner {
-  public VampireSolver() {
-    VampireLanguagePackage.eINSTANCE.eClass();
-    final VampireLanguageStandaloneSetupGenerated x = new VampireLanguageStandaloneSetupGenerated();
-    VampireLanguageStandaloneSetup.doSetup();
-  }
-  
-  private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper();
-  
-  private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper();
-  
-  private final VampireHandler handler = new VampireHandler();
-  
-  private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
-  
-  @Extension
-  private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE;
-  
-  @Extension
-  private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
-  
-  @Override
-  public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException {
-    try {
-      final VampireSolverConfiguration vampireConfig = this.asConfig(config);
-      String fileName = (((("problem_" + Integer.valueOf(vampireConfig.typeScopes.minNewElements)) + "-") + 
-        Integer.valueOf(vampireConfig.typeScopes.maxNewElements)) + ".tptp");
-      final long transformationStart = System.currentTimeMillis();
-      final TracedOutput result = this.forwardMapper.transformProblem(problem, vampireConfig);
-      long _currentTimeMillis = System.currentTimeMillis();
-      final long transformationTime = (_currentTimeMillis - transformationStart);
-      final VampireModel vampireProblem = result.getOutput();
-      final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();
-      String fileURI = null;
-      String vampireCode = null;
-      vampireCode = workspace.writeModelToString(vampireProblem, fileName);
-      final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || 
-        (vampireConfig.documentationLevel == DocumentationLevel.FULL));
-      if (writeFile) {
-        fileURI = workspace.writeModel(vampireProblem, fileName).toFileString();
-      }
-      if (vampireConfig.genModel) {
-        if (vampireConfig.server) {
-          final String form = this.support.makeForm(vampireCode, vampireConfig.solver, vampireConfig.runtimeLimit);
-          ArrayList response = CollectionLiterals.newArrayList();
-          int ind = 0;
-          boolean done = false;
-          InputOutput.print(" ");
-          while ((!done)) {
-            {
-              InputOutput.print("(x)");
-              done = false;
-              response = this.support.sendPost(form);
-              boolean responseFound = false;
-              ind = 0;
-              while ((!responseFound)) {
-                {
-                  String line = response.get(ind);
-                  if (((line.length() >= 5) && Objects.equal(line.substring(0, 5), "ERROR"))) {
-                    done = false;
-                    responseFound = true;
-                  } else {
-                    boolean _equals = Objects.equal(line, "
"); - if (_equals) { - done = true; - responseFound = true; - } - } - ind++; - } - } - } - } - final String satRaw = response.get((ind - 3)); - final String modRaw = response.get((ind - 2)); - final ArrayList sat = CollectionLiterals.newArrayList(satRaw.split(" ")); - final ArrayList mod = CollectionLiterals.newArrayList(modRaw.split(" ")); - final String satOut = sat.get(1); - final String modOut = mod.get(1); - final String satTime = sat.get(2); - final String modTime = mod.get(2); - InputOutput.println(); - InputOutput.>println(sat); - InputOutput.>println(mod); - ModelResult _createModelResult = this.resultFactory.createModelResult(); - final Procedure1 _function = (ModelResult it) -> { - it.setProblem(null); - EList _representation = it.getRepresentation(); - VampireModel _createVampireModel = this.factory.createVampireModel(); - final Procedure1 _function_1 = (VampireModel it_1) -> { - }; - VampireModel _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVampireModel, _function_1); - _representation.add(_doubleArrow); - it.setTrace(it.getTrace()); - Statistics _createStatistics = this.resultFactory.createStatistics(); - final Procedure1 _function_2 = (Statistics it_1) -> { - it_1.setTransformationTime(((int) transformationTime)); - EList _entries = it_1.getEntries(); - StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_3 = (StringStatisticEntry it_2) -> { - it_2.setName("satOut"); - it_2.setValue(satOut); - }; - StringStatisticEntry _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry, _function_3); - _entries.add(_doubleArrow_1); - EList _entries_1 = it_1.getEntries(); - StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_4 = (StringStatisticEntry it_2) -> { - it_2.setName("satTime"); - it_2.setValue(satTime); - }; - StringStatisticEntry _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_1, _function_4); - _entries_1.add(_doubleArrow_2); - EList _entries_2 = it_1.getEntries(); - StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_5 = (StringStatisticEntry it_2) -> { - it_2.setName("modOut"); - it_2.setValue(modOut); - }; - StringStatisticEntry _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_2, _function_5); - _entries_2.add(_doubleArrow_3); - EList _entries_3 = it_1.getEntries(); - StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_6 = (StringStatisticEntry it_2) -> { - it_2.setName("modTime"); - it_2.setValue(modTime); - }; - StringStatisticEntry _doubleArrow_4 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_3, _function_6); - _entries_3.add(_doubleArrow_4); - }; - Statistics _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStatistics, _function_2); - it.setStatistics(_doubleArrow_1); - }; - return ObjectExtensions.operator_doubleArrow(_createModelResult, _function); - } else { - InputOutput.println(); - final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig); - String modOut_1 = "no"; - boolean _isFiniteModelGenerated = vampSol.isFiniteModelGenerated(); - if (_isFiniteModelGenerated) { - modOut_1 = "FiniteModel"; - } - final String realModOut = modOut_1; - ModelResult _createModelResult_1 = this.resultFactory.createModelResult(); - final Procedure1 _function_1 = (ModelResult it) -> { - it.setProblem(null); - EList _representation = it.getRepresentation(); - VampireModel _createVampireModel = this.factory.createVampireModel(); - final Procedure1 _function_2 = (VampireModel it_1) -> { - }; - VampireModel _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVampireModel, _function_2); - _representation.add(_doubleArrow); - it.setTrace(it.getTrace()); - Statistics _createStatistics = this.resultFactory.createStatistics(); - final Procedure1 _function_3 = (Statistics it_1) -> { - it_1.setTransformationTime(((int) transformationTime)); - EList _entries = it_1.getEntries(); - StringStatisticEntry _createStringStatisticEntry = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_4 = (StringStatisticEntry it_2) -> { - it_2.setName("satOut"); - it_2.setValue("-"); - }; - StringStatisticEntry _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry, _function_4); - _entries.add(_doubleArrow_1); - EList _entries_1 = it_1.getEntries(); - StringStatisticEntry _createStringStatisticEntry_1 = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_5 = (StringStatisticEntry it_2) -> { - it_2.setName("satTime"); - it_2.setValue("-"); - }; - StringStatisticEntry _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_1, _function_5); - _entries_1.add(_doubleArrow_2); - EList _entries_2 = it_1.getEntries(); - StringStatisticEntry _createStringStatisticEntry_2 = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_6 = (StringStatisticEntry it_2) -> { - it_2.setName("modOut"); - it_2.setValue(realModOut); - }; - StringStatisticEntry _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_2, _function_6); - _entries_2.add(_doubleArrow_3); - EList _entries_3 = it_1.getEntries(); - StringStatisticEntry _createStringStatisticEntry_3 = this.resultFactory.createStringStatisticEntry(); - final Procedure1 _function_7 = (StringStatisticEntry it_2) -> { - it_2.setName("modTime"); - long _solverTime = vampSol.getSolverTime(); - it_2.setValue(Double.valueOf((_solverTime / 1000.0)).toString()); - }; - StringStatisticEntry _doubleArrow_4 = ObjectExtensions.operator_doubleArrow(_createStringStatisticEntry_3, _function_7); - _entries_3.add(_doubleArrow_4); - }; - Statistics _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createStatistics, _function_3); - it.setStatistics(_doubleArrow_1); - }; - return ObjectExtensions.operator_doubleArrow(_createModelResult_1, _function_1); - } - } - return null; - } catch (Throwable _e) { - throw Exceptions.sneakyThrow(_e); - } - } - - public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { - if ((configuration instanceof VampireSolverConfiguration)) { - return ((VampireSolverConfiguration)configuration); - } else { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("The configuration have to be an "); - String _simpleName = VampireSolverConfiguration.class.getSimpleName(); - _builder.append(_simpleName); - _builder.append("!"); - throw new IllegalArgumentException(_builder.toString()); - } - } - - @Override - public List getInterpretations(final ModelResult modelResult) { - List _xblockexpression = null; - { - final EList sols = modelResult.getRepresentation(); - final Function1 _function = (Object it) -> { - Object _trace = modelResult.getTrace(); - return new VampireModelInterpretation( - ((VampireModel) it), - ((Logic2VampireLanguageMapperTrace) _trace)); - }; - _xblockexpression = ListExtensions.map(sols, _function); - } - return _xblockexpression; - } -} 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 deleted file mode 100644 index c094872e..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java +++ /dev/null @@ -1,19 +0,0 @@ -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") -public class VampireSolverConfiguration extends LogicSolverConfiguration { - public int contCycleLevel = 0; - - public boolean uniquenessDuplicates = false; - - public int iteration = (-1); - - public BackendSolver solver = BackendSolver.VAMPIRE; - - public boolean genModel = true; - - public boolean server = false; -} 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 deleted file mode 100644 index 18da19a9..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and /dev/null differ 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 deleted file mode 100644 index 37c845cd..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin and /dev/null differ 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 deleted file mode 100644 index d8c61adc..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and /dev/null differ 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 deleted file mode 100644 index 1a86a55f..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin and /dev/null differ 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 deleted file mode 100644 index 216b3a4b..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin and /dev/null differ 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 deleted file mode 100644 index 8733e530..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and /dev/null differ 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 deleted file mode 100644 index 634dab6a..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and /dev/null differ 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 deleted file mode 100644 index 28c93f34..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and /dev/null differ 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 deleted file mode 100644 index faef07c1..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin and /dev/null differ 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 deleted file mode 100644 index 3d96efbf..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin and /dev/null differ 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 deleted file mode 100644 index b3756706..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin and /dev/null differ 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 deleted file mode 100644 index f75b4eaf..00000000 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin and /dev/null differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore deleted file mode 100644 index 8a9aa4bb..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore +++ /dev/null @@ -1,42 +0,0 @@ -/.Logic2VampireLanguageMapper_ConstantMapper.java._trace -/.Logic2VampireLanguageMapper.java._trace -/.Logic2VampireLanguageMapperTrace.java._trace -/.Logic2VampireLanguageMapper_TypeMapperTrace.java._trace -/.VampireModelInterpretation_TypeInterpretation.java._trace -/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.java._trace -/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java._trace -/.Logic2VampireLanguageMapper_TypeMapper.java._trace -/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java._trace -/.Logic2VampireLanguageMapper_Support.java._trace -/.Logic2VampireLanguageMapper_RelationMapper.java._trace -/.Logic2VampireLanguageMapper.xtendbin -/.Logic2VampireLanguageMapperTrace.xtendbin -/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin -/.Logic2VampireLanguageMapper_RelationMapper.xtendbin -/.Logic2VampireLanguageMapper_Support.xtendbin -/.Logic2VampireLanguageMapper_TypeMapper.xtendbin -/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin -/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin -/.VampireModelInterpretation_TypeInterpretation.xtendbin -/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin -/Logic2VampireLanguageMapper.java -/Logic2VampireLanguageMapperTrace.java -/Logic2VampireLanguageMapper_ConstantMapper.java -/Logic2VampireLanguageMapper_RelationMapper.java -/Logic2VampireLanguageMapper_Support.java -/Logic2VampireLanguageMapper_TypeMapper.java -/Logic2VampireLanguageMapper_TypeMapperTrace.java -/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java -/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java -/VampireModelInterpretation_TypeInterpretation.java -/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java -/.Vampire2LogicMapper.java._trace -/.VampireHandler.java._trace -/.MonitoredVampireSolution.java._trace -/.SolverConfiguration.java._trace -/.VampireSolverException.java._trace -/.VampireSolutionModel.java._trace -/.VampireCallerWithTimeout.java._trace -/.Logic2VampireLanguageMapper_ScopeMapper.java._trace -/.Logic2VampireLanguageMapper_Containment.java._trace -/.Logic2VampireLanguageMapper_ContainmentMapper.java._trace diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java deleted file mode 100644 index dc5ec788..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ /dev/null @@ -1,510 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ContainmentMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; -import com.google.common.base.Objects; -import com.google.common.collect.Iterables; -import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; -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.RelationDefinition; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl; -import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; -import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; -import java.util.Arrays; -import java.util.Collections; -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import java.util.function.Consumer; -import org.eclipse.emf.common.util.EList; -import org.eclipse.xtend.lib.annotations.AccessorType; -import org.eclipse.xtend.lib.annotations.Accessors; -import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Conversions; -import org.eclipse.xtext.xbase.lib.ExclusiveRange; -import org.eclipse.xtext.xbase.lib.Extension; -import org.eclipse.xtext.xbase.lib.Functions.Function1; -import org.eclipse.xtext.xbase.lib.IterableExtensions; -import org.eclipse.xtext.xbase.lib.ListExtensions; -import org.eclipse.xtext.xbase.lib.ObjectExtensions; -import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; -import org.eclipse.xtext.xbase.lib.Pure; - -@SuppressWarnings("all") -public class Logic2VampireLanguageMapper { - @Extension - private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; - - private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); - - @Accessors(AccessorType.PUBLIC_GETTER) - private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); - - @Accessors(AccessorType.PUBLIC_GETTER) - private final Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(this); - - @Accessors(AccessorType.PUBLIC_GETTER) - private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); - - @Accessors(AccessorType.PUBLIC_GETTER) - private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this); - - @Accessors(AccessorType.PUBLIC_GETTER) - private final Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper(this); - - public TracedOutput transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) { - VLSComment _createVLSComment = this.factory.createVLSComment(); - final Procedure1 _function = (VLSComment it) -> { - it.setComment("%This is an initial Test Comment"); - }; - final VLSComment initialComment = ObjectExtensions.operator_doubleArrow(_createVLSComment, _function); - VampireModel _createVampireModel = this.factory.createVampireModel(); - final Procedure1 _function_1 = (VampireModel it) -> { - EList _comments = it.getComments(); - _comments.add(initialComment); - }; - final VampireModel specification = ObjectExtensions.operator_doubleArrow(_createVampireModel, _function_1); - Logic2VampireLanguageMapperTrace _logic2VampireLanguageMapperTrace = new Logic2VampireLanguageMapperTrace(); - final Procedure1 _function_2 = (Logic2VampireLanguageMapperTrace it) -> { - it.specification = specification; - }; - final Logic2VampireLanguageMapperTrace trace = ObjectExtensions.operator_doubleArrow(_logic2VampireLanguageMapperTrace, _function_2); - boolean _isEmpty = problem.getTypes().isEmpty(); - boolean _not = (!_isEmpty); - if (_not) { - this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); - } - trace.relationDefinitions = this.collectRelationDefinitions(problem); - final Function1 _function_3 = (Relation it) -> { - Class _class = it.getClass(); - return Boolean.valueOf(Objects.equal(_class, RelationDefinitionImpl.class)); - }; - this.toTrace(IterableExtensions.filter(problem.getRelations(), _function_3), trace); - final Consumer _function_4 = (Relation it) -> { - Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper(); - this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper); - }; - problem.getRelations().forEach(_function_4); - this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); - this.scopeMapper.transformScope(problem.getTypes(), config, trace); - trace.constantDefinitions = this.collectConstantDefinitions(problem); - final Consumer _function_5 = (ConstantDefinition it) -> { - this.constantMapper.transformConstantDefinitionSpecification(it, trace); - }; - Iterables.filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_5); - EList _assertions = problem.getAssertions(); - for (final Assertion assertion : _assertions) { - this.transformAssertion(assertion, trace); - } - return new TracedOutput(specification, trace); - } - - public void toTrace(final Iterable relations, final Logic2VampireLanguageMapperTrace trace) { - final List vars = CollectionLiterals.newArrayList(); - for (final Relation rel : relations) { - { - final String[] nameArray = rel.getName().split(" "); - String relNameVar = ""; - int _length = nameArray.length; - boolean _equals = (_length == 3); - if (_equals) { - relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); - } else { - relNameVar = rel.getName(); - } - final String relName = relNameVar; - final RelationDefinition relDef = ((RelationDefinition) rel); - int _length_1 = ((Object[])Conversions.unwrapArray(rel.getParameters(), Object.class)).length; - ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length_1, true); - for (final Integer i : _doubleDotLessThan) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName(this.support.toIDMultiple("V", i.toString())); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - vars.add(v); - } - } - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function = (VLSFunction it) -> { - it.setConstant(this.support.toIDMultiple("r", relName)); - for (final VLSVariable v : vars) { - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.support.duplicate(v); - _terms.add(_duplicate); - } - }; - final VLSFunction relFunc = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); - trace.relDef2Predicate.put(relDef, relFunc); - trace.predicate2RelDef.put(relFunc, relDef); - } - } - } - - protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { - return null; - } - - private HashMap collectConstantDefinitions(final LogicProblem problem) { - final HashMap res = new HashMap(); - final Function1 _function = (ConstantDefinition it) -> { - ConstantDeclaration _defines = it.getDefines(); - return Boolean.valueOf((_defines != null)); - }; - final Consumer _function_1 = (ConstantDefinition it) -> { - res.put(it.getDefines(), it); - }; - IterableExtensions.filter(Iterables.filter(problem.getConstants(), ConstantDefinition.class), _function).forEach(_function_1); - return res; - } - - private HashMap collectRelationDefinitions(final LogicProblem problem) { - final HashMap res = new HashMap(); - final Function1 _function = (RelationDefinition it) -> { - RelationDeclaration _defines = it.getDefines(); - return Boolean.valueOf((_defines != null)); - }; - final Consumer _function_1 = (RelationDefinition it) -> { - res.put(it.getDefines(), it); - }; - IterableExtensions.filter(Iterables.filter(problem.getRelations(), RelationDefinition.class), _function).forEach(_function_1); - return res; - } - - protected boolean transformAssertion(final Assertion assertion, final Logic2VampireLanguageMapperTrace trace) { - boolean _xblockexpression = false; - { - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { - String _name = assertion.getName(); - String _plus = ("assertion_" + _name); - it.setName(this.support.toID(_plus)); - it.setFofRole("axiom"); - it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP)); - }; - final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); - EList _formulas = trace.specification.getFormulas(); - _xblockexpression = _formulas.add(res); - } - return _xblockexpression; - } - - protected VLSTerm _transformTerm(final BoolLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSTerm _xifexpression = null; - boolean _isValue = literal.isValue(); - boolean _equals = (_isValue == true); - if (_equals) { - _xifexpression = this.factory.createVLSTrue(); - } else { - _xifexpression = this.factory.createVLSFalse(); - } - return _xifexpression; - } - - protected VLSTerm _transformTerm(final IntLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSInt _createVLSInt = this.factory.createVLSInt(); - final Procedure1 _function = (VLSInt it) -> { - it.setValue(Integer.valueOf(literal.getValue()).toString()); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSInt, _function); - } - - protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function = (VLSUnaryNegation it) -> { - it.setOperand(this.transformTerm(not.getOperand(), trace, variables)); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function); - } - - protected VLSTerm _transformTerm(final And and, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - final Function1 _function = (Term it) -> { - return this.transformTerm(it, trace, variables); - }; - return this.support.unfoldAnd(ListExtensions.map(and.getOperands(), _function)); - } - - protected VLSTerm _transformTerm(final Or or, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - final Function1 _function = (Term it) -> { - return this.transformTerm(it, trace, variables); - }; - return this.support.unfoldOr(ListExtensions.map(or.getOperands(), _function)); - } - - protected VLSTerm _transformTerm(final Impl impl, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function = (VLSImplies it) -> { - it.setLeft(this.transformTerm(impl.getLeftOperand(), trace, variables)); - it.setRight(this.transformTerm(impl.getRightOperand(), trace, variables)); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function); - } - - protected VLSTerm _transformTerm(final Iff iff, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function = (VLSEquivalent it) -> { - it.setLeft(this.transformTerm(iff.getLeftOperand(), trace, variables)); - it.setRight(this.transformTerm(iff.getRightOperand(), trace, variables)); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function); - } - - protected VLSTerm _transformTerm(final Equals equals, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function = (VLSEquality it) -> { - it.setLeft(this.transformTerm(equals.getLeftOperand(), trace, variables)); - it.setRight(this.transformTerm(equals.getRightOperand(), trace, variables)); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function); - } - - protected VLSTerm _transformTerm(final Distinct distinct, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - return this.support.unfoldDistinctTerms(this, distinct.getOperands(), trace, variables); - } - - protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - return this.support.createQuantifiedExpression(this, forall, trace, variables, true); - } - - protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - return this.support.createQuantifiedExpression(this, exists, trace, variables, false); - } - - protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function = (VLSFunction it) -> { - TypeReference _range = instanceOf.getRange(); - it.setConstant(CollectionsUtil.lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate).getConstant()); - EList _terms = it.getTerms(); - VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); - _terms.add(_transformTerm); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); - } - - protected VLSTerm _transformTerm(final SymbolicValue symbolicValue, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - return this.transformSymbolicReference(symbolicValue.getSymbolicReference(), symbolicValue.getParameterSubstitutions(), trace, variables); - } - - protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - final String name = CollectionsUtil.lookup(referred, trace.definedElement2String); - VLSConstant _createVLSConstant = this.factory.createVLSConstant(); - final Procedure1 _function = (VLSConstant it) -> { - it.setName(name); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); - } - - protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSConstant _createVLSConstant = this.factory.createVLSConstant(); - final Procedure1 _function = (VLSConstant it) -> { - it.setName(this.support.toID(constant.getName())); - }; - final VLSConstant res = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); - return res; - } - - protected VLSTerm _transformSymbolicReference(final ConstantDefinition constant, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - return null; - } - - protected VLSTerm _transformSymbolicReference(final Variable variable, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - return this.support.duplicate(CollectionsUtil.lookup(variable, variables)); - } - - protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - return null; - } - - protected VLSTerm _transformSymbolicReference(final FunctionDefinition function, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - return null; - } - - /** - * def dispatch protected VLSTerm transformSymbolicReference(Relation relation, - * List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, - * Map variables) { - * if (trace.relationDefinitions.containsKey(relation)) { - * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), - * parameterSubstitutions, trace, variables) - * } - * else { - * // if (relationMapper.transformToHostedField(relation, trace)) { - * // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) - * // // R(a,b) => - * // // b in a.R - * // return createVLSSubset => [ - * // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) - * // it.rightOperand = createVLSJoin => [ - * // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) - * // it.rightOperand = createVLSReference => [it.referred = VLSRelation] - * // ] - * // ] - * // } else { - * // val target = createVLSJoin => [ - * // leftOperand = createVLSReference => [referred = trace.logicLanguage] - * // rightOperand = createVLSReference => [ - * // referred = relation.lookup(trace.relationDeclaration2Global) - * // ] - * // ] - * // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) - * // - * // return createVLSSubset => [ - * // leftOperand = source - * // rightOperand = target - * // ] - * // } - * } - * } - */ - protected VLSTerm _transformSymbolicReference(final Relation relation, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function = (VLSFunction it) -> { - Class _class = relation.getClass(); - boolean _equals = Objects.equal(_class, RelationDeclarationImpl.class); - if (_equals) { - it.setConstant(CollectionsUtil.lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); - } else { - it.setConstant(CollectionsUtil.lookup(((RelationDefinition) relation), trace.relDef2Predicate).getConstant()); - } - EList _terms = it.getTerms(); - final Function1 _function_1 = (Term p) -> { - return this.transformTerm(p, trace, variables); - }; - List _map = ListExtensions.map(parameterSubstitutions, _function_1); - Iterables.addAll(_terms, _map); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); - } - - protected VLSTerm transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { - return _transformTypeReference(boolTypeReference, trace); - } - - protected VLSTerm transformTerm(final Term and, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - if (and instanceof And) { - return _transformTerm((And)and, trace, variables); - } else if (and instanceof BoolLiteral) { - return _transformTerm((BoolLiteral)and, trace, variables); - } else if (and instanceof Distinct) { - return _transformTerm((Distinct)and, trace, variables); - } else if (and instanceof Equals) { - return _transformTerm((Equals)and, trace, variables); - } else if (and instanceof Exists) { - return _transformTerm((Exists)and, trace, variables); - } else if (and instanceof Forall) { - return _transformTerm((Forall)and, trace, variables); - } else if (and instanceof Iff) { - return _transformTerm((Iff)and, trace, variables); - } else if (and instanceof Impl) { - return _transformTerm((Impl)and, trace, variables); - } else if (and instanceof IntLiteral) { - return _transformTerm((IntLiteral)and, trace, variables); - } else if (and instanceof Not) { - return _transformTerm((Not)and, trace, variables); - } else if (and instanceof Or) { - return _transformTerm((Or)and, trace, variables); - } else if (and instanceof InstanceOf) { - return _transformTerm((InstanceOf)and, trace, variables); - } else if (and instanceof SymbolicValue) { - return _transformTerm((SymbolicValue)and, trace, variables); - } else { - throw new IllegalArgumentException("Unhandled parameter types: " + - Arrays.asList(and, trace, variables).toString()); - } - } - - protected VLSTerm transformSymbolicReference(final SymbolicDeclaration constant, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - if (constant instanceof ConstantDeclaration) { - return _transformSymbolicReference((ConstantDeclaration)constant, parameterSubstitutions, trace, variables); - } else if (constant instanceof ConstantDefinition) { - return _transformSymbolicReference((ConstantDefinition)constant, parameterSubstitutions, trace, variables); - } else if (constant instanceof FunctionDeclaration) { - return _transformSymbolicReference((FunctionDeclaration)constant, parameterSubstitutions, trace, variables); - } else if (constant instanceof FunctionDefinition) { - return _transformSymbolicReference((FunctionDefinition)constant, parameterSubstitutions, trace, variables); - } else if (constant instanceof DefinedElement) { - return _transformSymbolicReference((DefinedElement)constant, parameterSubstitutions, trace, variables); - } else if (constant instanceof Relation) { - return _transformSymbolicReference((Relation)constant, parameterSubstitutions, trace, variables); - } else if (constant instanceof Variable) { - return _transformSymbolicReference((Variable)constant, parameterSubstitutions, trace, variables); - } else { - throw new IllegalArgumentException("Unhandled parameter types: " + - Arrays.asList(constant, parameterSubstitutions, trace, variables).toString()); - } - } - - @Pure - public Logic2VampireLanguageMapper_ConstantMapper getConstantMapper() { - return this.constantMapper; - } - - @Pure - public Logic2VampireLanguageMapper_ContainmentMapper getContainmentMapper() { - return this.containmentMapper; - } - - @Pure - public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { - return this.relationMapper; - } - - @Pure - public Logic2VampireLanguageMapper_ScopeMapper getScopeMapper() { - return this.scopeMapper; - } - - @Pure - public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() { - return this.typeMapper; - } -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java deleted file mode 100644 index 22df456b..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ /dev/null @@ -1,65 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import org.eclipse.xtext.xbase.lib.CollectionLiterals; - -@SuppressWarnings("all") -public class Logic2VampireLanguageMapperTrace { - public VampireModel specification; - - public VLSFofFormula logicLanguageBody; - - public VLSTerm formula; - - public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; - - public Map definedElement2String = new HashMap(); - - public Object topLvlElementIsInInitialModel = null; - - public Object topLevelType = null; - - public final Map type2Predicate = new HashMap(); - - public final Map predicate2Type = new HashMap(); - - public final Map element2Predicate = new HashMap(); - - public final Map type2PossibleNot = new HashMap(); - - public final Map type2And = new HashMap(); - - public final List uniqueInstances = CollectionLiterals.newArrayList(); - - public Map constantDefinitions; - - public Map relationDefinitions; - - public Map rel2Predicate = new HashMap(); - - public Map predicate2Relation = new HashMap(); - - public Map relDef2Predicate = new HashMap(); - - public Map predicate2RelDef = new HashMap(); - - public final Map relationVar2VLS = new HashMap(); - - public final Map relationVar2TypeDec = new HashMap(); -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java deleted file mode 100644 index e5f42e73..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java +++ /dev/null @@ -1,34 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; -import org.eclipse.xtext.xbase.lib.Extension; - -@SuppressWarnings("all") -public class Logic2VampireLanguageMapper_ConstantMapper { - @Extension - private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; - - private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); - - private final Logic2VampireLanguageMapper base; - - public Logic2VampireLanguageMapper_ConstantMapper(final Logic2VampireLanguageMapper base) { - this.base = base; - } - - protected Object _transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { - return null; - } - - protected Object transformConstantDefinitionSpecification(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { - return null; - } - - protected Object transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { - return _transformConstant(constant, trace); - } -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java deleted file mode 100644 index 2100b92f..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ /dev/null @@ -1,386 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; -import com.google.common.base.Objects; -import com.google.common.collect.Iterables; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; -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.logic.model.logiclanguage.TypeDefinition; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl; -import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; -import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; -import java.util.ArrayList; -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import java.util.Set; -import org.eclipse.emf.common.util.EList; -import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Conversions; -import org.eclipse.xtext.xbase.lib.Extension; -import org.eclipse.xtext.xbase.lib.ObjectExtensions; -import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; - -@SuppressWarnings("all") -public class Logic2VampireLanguageMapper_ContainmentMapper { - @Extension - private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; - - private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); - - private final Logic2VampireLanguageMapper base; - - private final VLSVariable variable = ObjectExtensions.operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1) (VLSVariable it) -> { - it.setName("A"); - })); - - public Logic2VampireLanguageMapper_ContainmentMapper(final Logic2VampireLanguageMapper base) { - this.base = base; - } - - public void transformContainment(final VampireSolverConfiguration config, final List hierarchies, final Logic2VampireLanguageMapperTrace trace) { - final ContainmentHierarchy hierarchy = hierarchies.get(0); - final EList containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); - final EList relationsList = hierarchy.getContainmentRelations(); - final ArrayList toRemove = CollectionLiterals.newArrayList(); - for (final Relation l : relationsList) { - { - TypeReference _get = l.getParameters().get(1); - Type _referred = ((ComplexTypeReference) _get).getReferred(); - Type pointingTo = ((Type) _referred); - containmentListCopy.remove(pointingTo); - List allSubtypes = CollectionLiterals.newArrayList(); - this.support.listSubtypes(pointingTo, allSubtypes); - for (final Type c : allSubtypes) { - containmentListCopy.remove(c); - } - } - } - Type topTermVar = containmentListCopy.get(0); - for (final Relation l_1 : relationsList) { - { - TypeReference _get = l_1.getParameters().get(0); - Type _referred = ((ComplexTypeReference) _get).getReferred(); - Type pointingFrom = ((Type) _referred); - boolean _contains = containmentListCopy.contains(pointingFrom); - if (_contains) { - topTermVar = pointingFrom; - } - } - } - final String topName = CollectionsUtil.lookup(topTermVar, trace.type2Predicate).getConstant().toString(); - final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.lookup(topTermVar, trace.type2Predicate)); - trace.topLevelType = topTermVar; - boolean topLvlIsInInitModel = false; - String topLvlString = ""; - ArrayList listToCheck = CollectionLiterals.newArrayList(topTermVar); - listToCheck.addAll(topTermVar.getSubtypes()); - for (final Type c : listToCheck) { - Class _class = c.getClass(); - boolean _equals = Objects.equal(_class, TypeDefinitionImpl.class); - if (_equals) { - int _length = ((Object[])Conversions.unwrapArray(((TypeDefinition) c).getElements(), Object.class)).length; - boolean _greaterThan = (_length > 1); - if (_greaterThan) { - throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model"); - } - EList _elements = ((TypeDefinition) c).getElements(); - for (final DefinedElement d : _elements) { - boolean _containsKey = trace.definedElement2String.containsKey(d); - if (_containsKey) { - topLvlIsInInitModel = true; - topLvlString = CollectionsUtil.lookup(d, trace.definedElement2String); - } - } - } - } - trace.topLvlElementIsInInitialModel = Boolean.valueOf(topLvlIsInInitModel); - final boolean topInIM = topLvlIsInInitModel; - final String topStr = topLvlString; - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("containment_topLevel", topName)); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(this.variable); - _variables.add(_duplicate); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_2 = (VLSEquivalent it_2) -> { - it_2.setLeft(topTerm); - VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_3 = (VLSEquality it_3) -> { - it_3.setLeft(this.support.duplicate(this.variable)); - VLSConstant _createVLSConstant = this.factory.createVLSConstant(); - final Procedure1 _function_4 = (VLSConstant it_4) -> { - String _xifexpression = null; - if (topInIM) { - _xifexpression = topStr; - } else { - _xifexpression = "o1"; - } - it_4.setName(_xifexpression); - }; - VLSConstant _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function_4); - it_3.setRight(_doubleArrow); - }; - VLSEquality _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_3); - it_2.setRight(_doubleArrow); - }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_2); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula contTop = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(contTop); - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_1 = (VLSVariable it) -> { - it.setName("A"); - }; - final VLSVariable varA = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_1); - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); - final Procedure1 _function_2 = (VLSVariable it) -> { - it.setName("B"); - }; - final VLSVariable varB = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_2); - VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); - final Procedure1 _function_3 = (VLSVariable it) -> { - it.setName("C"); - }; - final VLSVariable varC = ObjectExtensions.operator_doubleArrow(_createVLSVariable_2, _function_3); - final ArrayList varList = CollectionLiterals.newArrayList(varB, varA); - final Map> type2cont = new HashMap>(); - for (final Relation l_2 : relationsList) { - { - final VLSFunction rel = CollectionsUtil.lookup(((RelationDeclaration) l_2), trace.rel2Predicate); - TypeReference _get = l_2.getParameters().get(1); - Type _referred = ((ComplexTypeReference) _get).getReferred(); - final Type toType = ((Type) _referred); - final VLSFunction toFunc = CollectionsUtil.lookup(toType, trace.type2Predicate); - this.addToMap(type2cont, this.support.duplicate(toFunc), this.support.duplicate(rel, varList)); - ArrayList subTypes = CollectionLiterals.newArrayList(); - this.support.listSubtypes(toType, subTypes); - for (final Type c_1 : subTypes) { - this.addToMap(type2cont, this.support.duplicate(CollectionsUtil.lookup(c_1, trace.type2Predicate)), this.support.duplicate(rel, varList)); - } - VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_4 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("containment_noDup", rel.getConstant().toString())); - it.setFofRole("axiom"); - VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); - final Procedure1 _function_5 = (VLSExistentialQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(varA); - _variables.add(_duplicate); - EList _variables_1 = it_1.getVariables(); - VLSVariable _duplicate_1 = this.support.duplicate(varB); - _variables_1.add(_duplicate_1); - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_6 = (VLSImplies it_2) -> { - it_2.setLeft(this.support.duplicate(rel, CollectionLiterals.newArrayList(varA, varB))); - VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_7 = (VLSUnaryNegation it_3) -> { - VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier(); - final Procedure1 _function_8 = (VLSExistentialQuantifier it_4) -> { - EList _variables_2 = it_4.getVariables(); - VLSVariable _duplicate_2 = this.support.duplicate(varC); - _variables_2.add(_duplicate_2); - EList _variables_3 = it_4.getVariables(); - VLSVariable _duplicate_3 = this.support.duplicate(varB); - _variables_3.add(_duplicate_3); - it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.newArrayList(varC, varB))); - }; - VLSExistentialQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier_1, _function_8); - it_3.setOperand(_doubleArrow); - }; - VLSUnaryNegation _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_7); - it_2.setRight(_doubleArrow); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_6); - it_1.setOperand(_doubleArrow); - }; - VLSExistentialQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_5); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula relFormula = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_4); - EList _formulas_1 = trace.specification.getFormulas(); - _formulas_1.add(relFormula); - } - } - Set>> _entrySet = type2cont.entrySet(); - for (final Map.Entry> e : _entrySet) { - { - VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_4 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(varA); - _variables.add(_duplicate); - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_6 = (VLSImplies it_2) -> { - it_2.setLeft(this.support.duplicate(e.getKey(), varA)); - VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); - final Procedure1 _function_7 = (VLSExistentialQuantifier it_3) -> { - EList _variables_1 = it_3.getVariables(); - VLSVariable _duplicate_1 = this.support.duplicate(varB); - _variables_1.add(_duplicate_1); - int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; - boolean _greaterThan_1 = (_length_1 > 1); - if (_greaterThan_1) { - it_3.setOperand(this.makeUnique(e.getValue())); - } else { - it_3.setOperand(e.getValue().get(0)); - } - }; - VLSExistentialQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); - it_2.setRight(_doubleArrow); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_6); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula relFormula = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_4); - EList _formulas_1 = trace.specification.getFormulas(); - _formulas_1.add(relFormula); - } - } - final ArrayList variables = CollectionLiterals.newArrayList(); - final ArrayList disjunctionList = CollectionLiterals.newArrayList(); - final ArrayList conjunctionList = CollectionLiterals.newArrayList(); - for (int i = 1; (i <= config.contCycleLevel); i++) { - { - final int ind = i; - VLSVariable _createVLSVariable_3 = this.factory.createVLSVariable(); - final Procedure1 _function_4 = (VLSVariable it) -> { - String _string = Integer.toString(ind); - String _plus = ("V" + _string); - it.setName(_plus); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_3, _function_4); - variables.add(_doubleArrow); - for (int j = 0; (j < i); j++) { - { - for (final Relation l_3 : relationsList) { - { - final VLSFunction rel = this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_3), trace.rel2Predicate), - CollectionLiterals.newArrayList(variables.get(j), variables.get(((j + 1) % i)))); - disjunctionList.add(rel); - } - } - conjunctionList.add(this.support.unfoldOr(disjunctionList)); - disjunctionList.clear(); - } - } - VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_5 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("containment_noCycle", Integer.toString(ind))); - it.setFofRole("axiom"); - VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_6 = (VLSUnaryNegation it_1) -> { - VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); - final Procedure1 _function_7 = (VLSExistentialQuantifier it_2) -> { - EList _variables = it_2.getVariables(); - List _duplicate = this.support.duplicate(variables); - Iterables.addAll(_variables, _duplicate); - it_2.setOperand(this.support.unfoldAnd(conjunctionList)); - }; - VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); - it_1.setOperand(_doubleArrow_1); - }; - VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_6); - it.setFofFormula(_doubleArrow_1); - }; - final VLSFofFormula contCycleForm = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_5); - EList _formulas_1 = trace.specification.getFormulas(); - _formulas_1.add(contCycleForm); - conjunctionList.clear(); - } - } - } - - protected VLSTerm makeUnique(final List list) { - final List possibleNots = CollectionLiterals.newArrayList(); - final List uniqueRels = CollectionLiterals.newArrayList(); - for (final VLSFunction t1 : list) { - { - for (final VLSFunction t2 : list) { - boolean _equals = Objects.equal(t1, t2); - if (_equals) { - final VLSFunction fct = this.support.duplicate(t2); - possibleNots.add(fct); - } else { - final VLSFunction op = this.support.duplicate(t2); - VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function = (VLSUnaryNegation it) -> { - it.setOperand(op); - }; - final VLSUnaryNegation negFct = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function); - possibleNots.add(negFct); - } - } - uniqueRels.add(this.support.unfoldAnd(possibleNots)); - possibleNots.clear(); - } - } - return this.support.unfoldOr(uniqueRels); - } - - protected Object addToMap(final Map> type2cont, final VLSFunction toFunc, final VLSFunction rel) { - Object _xblockexpression = null; - { - boolean keyInMap = false; - VLSFunction existingKey = this.factory.createVLSFunction(); - Set _keySet = type2cont.keySet(); - for (final VLSFunction k : _keySet) { - boolean _equals = k.getConstant().equals(toFunc.getConstant()); - if (_equals) { - keyInMap = true; - existingKey = k; - } - } - Object _xifexpression = null; - if ((!keyInMap)) { - _xifexpression = type2cont.put(toFunc, CollectionLiterals.newArrayList(rel)); - } else { - boolean _xifexpression_1 = false; - boolean _contains = type2cont.get(existingKey).contains(rel); - boolean _not = (!_contains); - if (_not) { - _xifexpression_1 = type2cont.get(existingKey).add(rel); - } - _xifexpression = Boolean.valueOf(_xifexpression_1); - } - _xblockexpression = _xifexpression; - } - return _xblockexpression; - } -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java deleted file mode 100644 index 4c14e93e..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ /dev/null @@ -1,205 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; -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.RelationDefinition; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; -import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import org.eclipse.emf.common.util.EList; -import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Conversions; -import org.eclipse.xtext.xbase.lib.ExclusiveRange; -import org.eclipse.xtext.xbase.lib.Extension; -import org.eclipse.xtext.xbase.lib.ObjectExtensions; -import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; - -@SuppressWarnings("all") -public class Logic2VampireLanguageMapper_RelationMapper { - @Extension - private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; - - private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); - - private final Logic2VampireLanguageMapper base; - - public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) { - this.base = base; - } - - public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { - final List relVar2VLS = new ArrayList(); - final List relVar2TypeDecComply = new ArrayList(); - int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; - ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); - for (final Integer i : _doubleDotLessThan) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName(this.support.toIDMultiple("V", i.toString())); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - relVar2VLS.add(v); - TypeReference _get = r.getParameters().get((i).intValue()); - final Type relType = ((ComplexTypeReference) _get).getReferred(); - final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.lookup(relType, trace.type2Predicate), v); - relVar2TypeDecComply.add(varTypeComply); - } - } - final String[] nameArray = r.getName().split(" "); - String relNameVar = ""; - int _length_1 = nameArray.length; - boolean _equals = (_length_1 == 3); - if (_equals) { - relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); - } else { - relNameVar = r.getName(); - } - final String relName = relNameVar; - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("compliance", relName)); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { - for (final VLSVariable v : relVar2VLS) { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(v); - _variables.add(_duplicate); - } - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_2 = (VLSImplies it_2) -> { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_3 = (VLSFunction it_3) -> { - it_3.setConstant(this.support.toIDMultiple("r", relName)); - for (final VLSVariable v_1 : relVar2VLS) { - EList _terms = it_3.getTerms(); - VLSVariable _duplicate_1 = this.support.duplicate(v_1); - _terms.add(_duplicate_1); - } - }; - final VLSFunction rel = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_3); - trace.rel2Predicate.put(r, rel); - trace.predicate2Relation.put(rel, r); - it_2.setLeft(this.support.duplicate(rel)); - it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula comply = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(comply); - } - - public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { - final Map relVar2VLS = new HashMap(); - final List vars = CollectionLiterals.newArrayList(); - final List relVar2TypeDecComply = new ArrayList(); - int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; - ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); - for (final Integer i : _doubleDotLessThan) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName(this.support.toIDMultiple("V", i.toString())); - }; - final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - relVar2VLS.put(r.getVariables().get((i).intValue()), v); - vars.add(v); - TypeReference _get = r.getParameters().get((i).intValue()); - final Type relType = ((ComplexTypeReference) _get).getReferred(); - final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.lookup(relType, trace.type2Predicate), v); - relVar2TypeDecComply.add(varTypeComply); - } - } - final String[] nameArray = r.getName().split(" "); - String relNameVar = ""; - int _length_1 = nameArray.length; - boolean _equals = (_length_1 == 3); - if (_equals) { - relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); - } else { - relNameVar = r.getName(); - } - final String relName = relNameVar; - final VLSTerm definition = mapper.transformTerm(r.getValue(), trace, relVar2VLS); - final VLSTerm compliance = this.support.unfoldAnd(relVar2TypeDecComply); - VLSAnd _createVLSAnd = this.factory.createVLSAnd(); - final Procedure1 _function = (VLSAnd it) -> { - it.setLeft(compliance); - it.setRight(definition); - }; - final VLSAnd compDefn = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function); - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_1 = (VLSFofFormula it) -> { - it.setName(this.support.toID(relName)); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - for (final VLSVariable v : vars) { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(v); - _variables.add(_duplicate); - } - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_3 = (VLSImplies it_2) -> { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_4 = (VLSFunction it_3) -> { - it_3.setConstant(this.support.toIDMultiple("r", relName)); - for (final VLSVariable v_1 : vars) { - EList _terms = it_3.getTerms(); - VLSVariable _duplicate_1 = this.support.duplicate(v_1); - _terms.add(_duplicate_1); - } - }; - final VLSFunction rel = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_4); - it_2.setLeft(this.support.duplicate(rel)); - it_2.setRight(compDefn); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula relDef = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(relDef); - } - - public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace, final Logic2VampireLanguageMapper mapper) { - if (r instanceof RelationDeclaration) { - _transformRelation((RelationDeclaration)r, trace, mapper); - return; - } else if (r instanceof RelationDefinition) { - _transformRelation((RelationDefinition)r, trace, mapper); - return; - } else { - throw new IllegalArgumentException("Unhandled parameter types: " + - Arrays.asList(r, trace, mapper).toString()); - } - } -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java deleted file mode 100644 index d6c90484..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ /dev/null @@ -1,302 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; -import com.google.common.base.Objects; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; -import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; -import java.util.ArrayList; -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import java.util.Set; -import org.eclipse.emf.common.util.EList; -import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Conversions; -import org.eclipse.xtext.xbase.lib.Extension; -import org.eclipse.xtext.xbase.lib.Functions.Function1; -import org.eclipse.xtext.xbase.lib.IterableExtensions; -import org.eclipse.xtext.xbase.lib.ListExtensions; -import org.eclipse.xtext.xbase.lib.ObjectExtensions; -import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; - -@SuppressWarnings("all") -public class Logic2VampireLanguageMapper_ScopeMapper { - @Extension - private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; - - private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); - - private final Logic2VampireLanguageMapper base; - - private final VLSVariable variable = ObjectExtensions.operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1) (VLSVariable it) -> { - it.setName("A"); - })); - - public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) { - this.base = base; - } - - public void _transformScope(final List types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { - int elemsInIM = trace.definedElement2String.size(); - final int ABSOLUTE_MIN = 0; - final int ABSOLUTE_MAX = (Integer.MAX_VALUE - elemsInIM); - final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); - final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); - final ArrayList localInstances = CollectionLiterals.newArrayList(); - final boolean consistant = (GLOBAL_MAX >= GLOBAL_MIN); - if ((GLOBAL_MIN != ABSOLUTE_MIN)) { - this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant)); - if (consistant) { - for (final VLSConstant i : trace.uniqueInstances) { - localInstances.add(this.support.duplicate(i)); - } - this.makeFofFormula(localInstances, trace, true, null); - } else { - this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, true, null); - } - } - if ((GLOBAL_MAX != ABSOLUTE_MAX)) { - this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant); - if (consistant) { - this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); - } else { - this.makeFofFormula(localInstances, trace, false, null); - } - } - int i_1 = 1; - if ((((Boolean) trace.topLvlElementIsInInitialModel)).booleanValue()) { - i_1 = 0; - } - int minNum = (-1); - Map startPoints = new HashMap(); - final Function1 _function = (Type it) -> { - boolean _equals = it.equals(trace.topLevelType); - return Boolean.valueOf((!_equals)); - }; - Iterable _filter = IterableExtensions.filter(config.typeScopes.minNewElementsByType.keySet(), _function); - for (final Type t : _filter) { - { - int numIniIntModel = 0; - Set _keySet = trace.definedElement2String.keySet(); - for (final DefinedElement elem : _keySet) { - EList _definedInType = elem.getDefinedInType(); - for (final TypeDefinition tDefined : _definedInType) { - boolean _dfsSubtypeCheck = this.support.dfsSubtypeCheck(t, tDefined); - if (_dfsSubtypeCheck) { - int _numIniIntModel = numIniIntModel; - numIniIntModel = (_numIniIntModel + 1); - } - } - } - Integer _lookup = CollectionsUtil.lookup(t, config.typeScopes.minNewElementsByType); - int _minus = ((_lookup).intValue() - numIniIntModel); - minNum = _minus; - if ((minNum != 0)) { - this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); - startPoints.put(t, Integer.valueOf(i_1)); - int _i = i_1; - i_1 = (_i + minNum); - this.makeFofFormula(localInstances, trace, true, t); - } - } - } - final Function1 _function_1 = (Type it) -> { - boolean _equals = it.equals(trace.topLevelType); - return Boolean.valueOf((!_equals)); - }; - Iterable _filter_1 = IterableExtensions.filter(config.typeScopes.maxNewElementsByType.keySet(), _function_1); - for (final Type t_1 : _filter_1) { - { - int numIniIntModel = 0; - Set _keySet = trace.definedElement2String.keySet(); - for (final DefinedElement elem : _keySet) { - EList _definedInType = elem.getDefinedInType(); - boolean _equals = Objects.equal(_definedInType, t_1); - if (_equals) { - int _numIniIntModel = numIniIntModel; - numIniIntModel = (_numIniIntModel + 1); - } - } - Integer _lookup = CollectionsUtil.lookup(t_1, config.typeScopes.maxNewElementsByType); - int maxNum = ((_lookup).intValue() - numIniIntModel); - boolean _contains = config.typeScopes.minNewElementsByType.keySet().contains(t_1); - if (_contains) { - Integer _lookup_1 = CollectionsUtil.lookup(t_1, config.typeScopes.minNewElementsByType); - int _minus = ((_lookup_1).intValue() - numIniIntModel); - minNum = _minus; - } else { - minNum = 0; - } - if ((minNum != 0)) { - Integer startpoint = CollectionsUtil.lookup(t_1, startPoints); - this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); - } else { - localInstances.clear(); - } - int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + maxNum) - minNum)); - this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); - this.makeFofFormula(localInstances, trace, false, t_1); - } - } - final boolean DUPLICATES = config.uniquenessDuplicates; - final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; - int ind = 1; - if ((numInst != 0)) { - if (DUPLICATES) { - for (final VLSConstant e : trace.uniqueInstances) { - { - final int x = ind; - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_2 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); - it.setFofRole("axiom"); - it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); - }; - final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_2); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(uniqueness); - ind++; - } - } - } else { - List _subList = trace.uniqueInstances.subList(0, (numInst - 1)); - for (final VLSConstant e_1 : _subList) { - { - final int x = ind; - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_2 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName())); - it.setFofRole("axiom"); - it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1)); - }; - final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_2); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(uniqueness); - ind++; - } - } - } - } - } - - protected void getInstanceConstants(final int endInd, final int startInd, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean clear, final boolean addToTrace) { - if (clear) { - list.clear(); - } - for (int i = startInd; (i < endInd); i++) { - { - final int num = (i + 1); - VLSConstant _createVLSConstant = this.factory.createVLSConstant(); - final Procedure1 _function = (VLSConstant it) -> { - it.setName(("o" + Integer.valueOf(num))); - }; - final VLSConstant cst = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); - if (addToTrace) { - trace.uniqueInstances.add(cst); - } - list.add(cst); - } - } - } - - protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { - String nm = ""; - VLSTerm tm = null; - if ((type == null)) { - nm = "object"; - tm = this.support.topLevelTypeFunc(); - } else { - nm = CollectionsUtil.lookup(type, trace.type2Predicate).getConstant().toString(); - VLSAnd _createVLSAnd = this.factory.createVLSAnd(); - final Procedure1 _function = (VLSAnd it) -> { - it.setLeft(this.support.duplicate(CollectionsUtil.lookup(type, trace.type2Predicate))); - it.setRight(this.support.topLevelTypeFunc()); - }; - VLSAnd _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function); - tm = _doubleArrow; - } - final String name = nm; - final VLSTerm term = tm; - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_1 = (VLSFofFormula it) -> { - String _xifexpression = null; - if (minimum) { - _xifexpression = "min"; - } else { - _xifexpression = "max"; - } - it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(this.variable); - _variables.add(_duplicate); - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_3 = (VLSImplies it_2) -> { - if (minimum) { - final Function1 _function_4 = (VLSTerm i) -> { - VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_5 = (VLSEquality it_3) -> { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_6 = (VLSVariable it_4) -> { - it_4.setName(this.variable.getName()); - }; - VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); - it_3.setLeft(_doubleArrow_1); - it_3.setRight(i); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); - }; - it_2.setLeft(this.support.unfoldOr(ListExtensions.map(list, _function_4))); - it_2.setRight(term); - } else { - it_2.setLeft(term); - final Function1 _function_5 = (VLSTerm i) -> { - VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_6 = (VLSEquality it_3) -> { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_7 = (VLSVariable it_4) -> { - it_4.setName(this.variable.getName()); - }; - VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_7); - it_3.setLeft(_doubleArrow_1); - it_3.setRight(i); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_6); - }; - it_2.setRight(this.support.unfoldOr(ListExtensions.map(list, _function_5))); - } - }; - VLSImplies _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); - it_1.setOperand(_doubleArrow_1); - }; - VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); - it.setFofFormula(_doubleArrow_1); - }; - final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(cstDec); - } - - public void transformScope(final List types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { - _transformScope(types, config, trace); - return; - } -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java deleted file mode 100644 index d757212a..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ /dev/null @@ -1,515 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; -import com.google.common.base.Objects; -import com.google.common.collect.Iterables; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; -import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; -import java.util.ArrayList; -import java.util.Collection; -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import java.util.concurrent.TimeUnit; -import okhttp3.MediaType; -import okhttp3.OkHttpClient; -import okhttp3.Request; -import okhttp3.RequestBody; -import okhttp3.Response; -import org.eclipse.emf.common.util.EList; -import org.eclipse.xtend2.lib.StringConcatenation; -import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Conversions; -import org.eclipse.xtext.xbase.lib.ExclusiveRange; -import org.eclipse.xtext.xbase.lib.Extension; -import org.eclipse.xtext.xbase.lib.Functions.Function1; -import org.eclipse.xtext.xbase.lib.IterableExtensions; -import org.eclipse.xtext.xbase.lib.ListExtensions; -import org.eclipse.xtext.xbase.lib.ObjectExtensions; -import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; - -@SuppressWarnings("all") -public class Logic2VampireLanguageMapper_Support { - @Extension - private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; - - protected String toIDMultiple(final String... ids) { - final Function1 _function = (String it) -> { - return IterableExtensions.join(((Iterable)Conversions.doWrapArray(it.split("\\s+"))), "_"); - }; - return IterableExtensions.join(ListExtensions.map(((List)Conversions.doWrapArray(ids)), _function), "_"); - } - - protected String toID(final String ids) { - return IterableExtensions.join(((Iterable)Conversions.doWrapArray(ids.split("\\s+"))), "_"); - } - - protected VLSVariable duplicate(final VLSVariable term) { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName(term.getName()); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - } - - protected VLSFunctionAsTerm duplicate(final VLSFunctionAsTerm term) { - VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); - final Procedure1 _function = (VLSFunctionAsTerm it) -> { - it.setFunctor(term.getFunctor()); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function); - } - - protected VLSConstant duplicate(final VLSConstant term) { - VLSConstant _createVLSConstant = this.factory.createVLSConstant(); - final Procedure1 _function = (VLSConstant it) -> { - it.setName(term.getName()); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); - } - - protected VLSFunction duplicate(final VLSFunction term) { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function = (VLSFunction it) -> { - it.setConstant(term.getConstant()); - EList _terms = term.getTerms(); - for (final VLSTerm v : _terms) { - EList _terms_1 = it.getTerms(); - VLSVariable _duplicate = this.duplicate(((VLSVariable) v)); - _terms_1.add(_duplicate); - } - }; - return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); - } - - protected VLSFunction duplicate(final VLSFunction term, final VLSVariable v) { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function = (VLSFunction it) -> { - it.setConstant(term.getConstant()); - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.duplicate(v); - _terms.add(_duplicate); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); - } - - protected VLSFunction duplicate(final VLSFunction term, final List vars) { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function = (VLSFunction it) -> { - it.setConstant(term.getConstant()); - for (final VLSVariable v : vars) { - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.duplicate(v); - _terms.add(_duplicate); - } - }; - return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); - } - - protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function = (VLSFunction it) -> { - it.setConstant(term.getConstant()); - EList _terms = it.getTerms(); - VLSFunctionAsTerm _duplicate = this.duplicate(v); - _terms.add(_duplicate); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); - } - - protected List duplicate(final List vars) { - ArrayList newList = CollectionLiterals.newArrayList(); - for (final VLSVariable v : vars) { - newList.add(this.duplicate(v)); - } - return newList; - } - - protected VLSConstant toConstant(final VLSFunctionAsTerm term) { - VLSConstant _createVLSConstant = this.factory.createVLSConstant(); - final Procedure1 _function = (VLSConstant it) -> { - it.setName(term.getFunctor()); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); - } - - protected VLSFunction topLevelTypeFunc() { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function = (VLSFunction it) -> { - it.setConstant("object"); - EList _terms = it.getTerms(); - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_1 = (VLSVariable it_1) -> { - it_1.setName("A"); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_1); - _terms.add(_doubleArrow); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); - } - - protected VLSFunction topLevelTypeFunc(final VLSVariable v) { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function = (VLSFunction it) -> { - it.setConstant("object"); - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.duplicate(v); - _terms.add(_duplicate); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); - } - - protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function = (VLSFunction it) -> { - it.setConstant("object"); - EList _terms = it.getTerms(); - VLSFunctionAsTerm _duplicate = this.duplicate(v); - _terms.add(_duplicate); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); - } - - public VLSTerm establishUniqueness(final List terms, final VLSConstant t2) { - final List eqs = CollectionLiterals.newArrayList(); - for (final VLSConstant t1 : terms) { - boolean _notEquals = (!Objects.equal(t1, t2)); - if (_notEquals) { - VLSInequality _createVLSInequality = this.factory.createVLSInequality(); - final Procedure1 _function = (VLSInequality it) -> { - VLSConstant _createVLSConstant = this.factory.createVLSConstant(); - final Procedure1 _function_1 = (VLSConstant it_1) -> { - it_1.setName(t2.getName()); - }; - VLSConstant _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function_1); - it.setLeft(_doubleArrow); - VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant(); - final Procedure1 _function_2 = (VLSConstant it_1) -> { - it_1.setName(t1.getName()); - }; - VLSConstant _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSConstant_1, _function_2); - it.setRight(_doubleArrow_1); - }; - final VLSInequality eq = ObjectExtensions.operator_doubleArrow(_createVLSInequality, _function); - eqs.add(eq); - } - } - return this.unfoldAnd(eqs); - } - - protected VLSTerm unfoldAnd(final List operands) { - int _size = operands.size(); - boolean _equals = (_size == 1); - if (_equals) { - return IterableExtensions.head(operands); - } else { - int _size_1 = operands.size(); - boolean _greaterThan = (_size_1 > 1); - if (_greaterThan) { - VLSAnd _createVLSAnd = this.factory.createVLSAnd(); - final Procedure1 _function = (VLSAnd it) -> { - it.setLeft(IterableExtensions.head(operands)); - it.setRight(this.unfoldAnd(operands.subList(1, operands.size()))); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function); - } else { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("Logic operator with 0 operands!"); - throw new UnsupportedOperationException(_builder.toString()); - } - } - } - - protected VLSTerm unfoldOr(final List operands) { - int _size = operands.size(); - boolean _equals = (_size == 1); - if (_equals) { - return IterableExtensions.head(operands); - } else { - int _size_1 = operands.size(); - boolean _greaterThan = (_size_1 > 1); - if (_greaterThan) { - VLSOr _createVLSOr = this.factory.createVLSOr(); - final Procedure1 _function = (VLSOr it) -> { - it.setLeft(IterableExtensions.head(operands)); - it.setRight(this.unfoldOr(operands.subList(1, operands.size()))); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSOr, _function); - } else { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("Logic operator with 0 operands!"); - throw new UnsupportedOperationException(_builder.toString()); - } - } - } - - protected VLSTerm unfoldDistinctTerms(final Logic2VampireLanguageMapper m, final EList operands, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - int _size = operands.size(); - boolean _equals = (_size == 1); - if (_equals) { - return m.transformTerm(IterableExtensions.head(operands), trace, variables); - } else { - int _size_1 = operands.size(); - boolean _greaterThan = (_size_1 > 1); - if (_greaterThan) { - int _size_2 = operands.size(); - int _size_3 = operands.size(); - int _multiply = (_size_2 * _size_3); - int _divide = (_multiply / 2); - final ArrayList notEquals = new ArrayList(_divide); - int _size_4 = operands.size(); - ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _size_4, true); - for (final Integer i : _doubleDotLessThan) { - int _size_5 = operands.size(); - ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(((i).intValue() + 1), _size_5, true); - for (final Integer j : _doubleDotLessThan_1) { - VLSInequality _createVLSInequality = this.factory.createVLSInequality(); - final Procedure1 _function = (VLSInequality it) -> { - it.setLeft(m.transformTerm(operands.get((i).intValue()), trace, variables)); - it.setRight(m.transformTerm(operands.get((j).intValue()), trace, variables)); - }; - VLSInequality _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSInequality, _function); - notEquals.add(_doubleArrow); - } - } - return this.unfoldAnd(notEquals); - } else { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("Logic operator with 0 operands!"); - throw new UnsupportedOperationException(_builder.toString()); - } - } - } - - /** - * def protected String toID(List ids) { - * ids.map[it.split("\\s+").join("'")].join("'") - * } - */ - protected VLSTerm createQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map variables, final boolean isUniversal) { - VLSTerm _xblockexpression = null; - { - final Function1 _function = (Variable v) -> { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_1 = (VLSVariable it) -> { - it.setName(this.toIDMultiple("V", v.getName())); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_1); - }; - final Map variableMap = IterableExtensions.toInvertedMap(expression.getQuantifiedVariables(), _function); - final ArrayList typedefs = new ArrayList(); - EList _quantifiedVariables = expression.getQuantifiedVariables(); - for (final Variable variable : _quantifiedVariables) { - { - TypeReference _range = variable.getRange(); - final VLSFunction eq = this.duplicate(CollectionsUtil.lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), - CollectionsUtil.lookup(variable, variableMap)); - typedefs.add(eq); - } - } - VLSTerm _xifexpression = null; - if (isUniversal) { - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_1 = (VLSUniversalQuantifier it) -> { - EList _variables = it.getVariables(); - Collection _values = variableMap.values(); - Iterables.addAll(_variables, _values); - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_2 = (VLSImplies it_1) -> { - it_1.setLeft(this.unfoldAnd(typedefs)); - it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); - it.setOperand(_doubleArrow); - }; - _xifexpression = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); - } else { - VLSExistentialQuantifier _xblockexpression_1 = null; - { - typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); - VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); - final Procedure1 _function_2 = (VLSExistentialQuantifier it) -> { - EList _variables = it.getVariables(); - Collection _values = variableMap.values(); - Iterables.addAll(_variables, _values); - it.setOperand(this.unfoldAnd(typedefs)); - }; - _xblockexpression_1 = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_2); - } - _xifexpression = _xblockexpression_1; - } - _xblockexpression = _xifexpression; - } - return _xblockexpression; - } - - protected boolean dfsSupertypeCheck(final Type type, final Type type2) { - boolean _xifexpression = false; - boolean _isEmpty = type.getSupertypes().isEmpty(); - if (_isEmpty) { - return false; - } else { - boolean _xifexpression_1 = false; - boolean _contains = type.getSupertypes().contains(type2); - if (_contains) { - return true; - } else { - EList _supertypes = type.getSupertypes(); - for (final Type supertype : _supertypes) { - boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2); - if (_dfsSupertypeCheck) { - return true; - } - } - } - _xifexpression = _xifexpression_1; - } - return _xifexpression; - } - - protected boolean dfsSubtypeCheck(final Type type, final Type type2) { - boolean _xifexpression = false; - boolean _isEmpty = type.getSubtypes().isEmpty(); - if (_isEmpty) { - return false; - } else { - boolean _xifexpression_1 = false; - boolean _contains = type.getSubtypes().contains(type2); - if (_contains) { - return true; - } else { - EList _subtypes = type.getSubtypes(); - for (final Type subtype : _subtypes) { - boolean _dfsSubtypeCheck = this.dfsSubtypeCheck(subtype, type2); - if (_dfsSubtypeCheck) { - return true; - } - } - } - _xifexpression = _xifexpression_1; - } - return _xifexpression; - } - - protected void listSubtypes(final Type t, final List allSubtypes) { - EList _subtypes = t.getSubtypes(); - for (final Type subt : _subtypes) { - { - allSubtypes.add(subt); - this.listSubtypes(subt, allSubtypes); - } - } - } - - protected HashMap withAddition(final Map map1, final Map map2) { - HashMap _hashMap = new HashMap(map1); - final Procedure1> _function = (HashMap it) -> { - it.putAll(map2); - }; - return ObjectExtensions.>operator_doubleArrow(_hashMap, _function); - } - - public String makeForm(final String formula, final BackendSolver solver, final int time) { - String _header = this.getHeader(); - String _plus = (_header + formula); - String _addOptions = this.addOptions(); - String _plus_1 = (_plus + _addOptions); - String _addSolver = this.addSolver(solver, time); - String _plus_2 = (_plus_1 + _addSolver); - String _addEnd = this.addEnd(); - return (_plus_2 + _addEnd); - } - - public ArrayList getSolverSpecs(final BackendSolver solver) { - if (solver != null) { - switch (solver) { - case CVC4: - return CollectionLiterals.newArrayList("CVC4---SAT-1.7", "do_CVC4 %s %d SAT"); - case DARWINFM: - return CollectionLiterals.newArrayList("DarwinFM---1.4.5", "darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s"); - case EDARWIN: - return CollectionLiterals.newArrayList("E-Darwin---1.5", - "e-darwin -pev \"TPTP\" -pmd true -if tptp -pl 2 -pc false -ps false %s"); - case GEOIII: - return CollectionLiterals.newArrayList("Geo-III---2018C", - "geo -tptp_input -nonempty -include /home/tptp/TPTP -inputfile %s"); - case IPROVER: - return CollectionLiterals.newArrayList("iProver---SAT-3.0", "iproveropt_run_sat.sh %d %s"); - case PARADOX: - return CollectionLiterals.newArrayList("Paradox---4.0", "paradox --no-progress --time %d --tstp --model %s"); - case VAMPIRE: - return CollectionLiterals.newArrayList("Vampire---SAT-4.4", "vampire --mode casc_sat -t %d %s"); - case Z3: - return CollectionLiterals.newArrayList("Z3---4.4.1", "run_z3_tptp -proof -model -t:%d -file:%s"); - default: - break; - } - } - return null; - } - - public String getHeader() { - return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n"; - } - - public String addSpec(final String spec) { - return spec.replace("\n", "\\r\\n"); - } - - public String addOptions() { - return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n"; - } - - public String addSolver(final BackendSolver solver, final int time) { - final ArrayList solverSpecs = this.getSolverSpecs(solver); - final String ID = solverSpecs.get(0); - final String cmd = solverSpecs.get(1); - return (((((((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"TimeLimit___" + ID) + - "\"\r\n\r\n") + Integer.valueOf(time)) + - "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___") + ID) + - "\"\r\n\r\n") + ID) + - "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + - "\"\r\n\r\n") + cmd) + "\r\n"); - } - - public String addEnd() { - return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"; - } - - public ArrayList sendPost(final String formData) throws Exception { - final OkHttpClient client = new OkHttpClient.Builder().connectTimeout(600, TimeUnit.SECONDS).readTimeout(350, - TimeUnit.SECONDS).build(); - final MediaType mediaType = MediaType.parse("multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); - final RequestBody body = RequestBody.create(mediaType, formData); - final Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", - "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", - "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", - "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").addHeader("Accept", - "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", - "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", - "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", - "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build(); - final Response response = client.newCall(request).execute(); - return CollectionLiterals.newArrayList(response.body().string().split("\n")); - } -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java deleted file mode 100644 index 72fea6d3..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java +++ /dev/null @@ -1,339 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; -import com.google.common.base.Objects; -import com.google.common.collect.Iterables; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; -import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; -import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; -import java.util.ArrayList; -import java.util.Collection; -import java.util.List; -import org.eclipse.emf.common.util.EList; -import org.eclipse.xtext.xbase.lib.CollectionLiterals; -import org.eclipse.xtext.xbase.lib.Conversions; -import org.eclipse.xtext.xbase.lib.Extension; -import org.eclipse.xtext.xbase.lib.Functions.Function1; -import org.eclipse.xtext.xbase.lib.IterableExtensions; -import org.eclipse.xtext.xbase.lib.ObjectExtensions; -import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; - -@SuppressWarnings("all") -public class Logic2VampireLanguageMapper_TypeMapper { - @Extension - private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; - - private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); - - private final Logic2VampireLanguageMapper base; - - public Logic2VampireLanguageMapper_TypeMapper(final Logic2VampireLanguageMapper base) { - LogicproblemPackage.eINSTANCE.getClass(); - this.base = base; - } - - protected boolean transformTypes(final Collection types, final Collection elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { - boolean _xblockexpression = false; - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName("A"); - }; - final VLSVariable variable = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - int globalCounter = 0; - for (final Type type : types) { - { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_1 = (VLSFunction it) -> { - int _length = type.getName().split(" ").length; - boolean _equals = (_length == 3); - if (_equals) { - it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0], type.getName().split(" ")[2])); - } else { - it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); - } - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.support.duplicate(variable); - _terms.add(_duplicate); - }; - final VLSFunction typePred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); - trace.type2Predicate.put(type, typePred); - trace.predicate2Type.put(typePred, type); - } - } - final Function1 _function_1 = (TypeDefinition it) -> { - boolean _isIsAbstract = it.isIsAbstract(); - return Boolean.valueOf((!_isIsAbstract)); - }; - Iterable _filter = IterableExtensions.filter(Iterables.filter(types, TypeDefinition.class), _function_1); - for (final TypeDefinition type_1 : _filter) { - { - final int len = type_1.getName().length(); - boolean _equals = type_1.getName().substring((len - 4), len).equals("enum"); - final boolean isNotEnum = (!_equals); - final List orElems = CollectionLiterals.newArrayList(); - EList _elements = type_1.getElements(); - for (final DefinedElement e : _elements) { - { - final String[] nameArray = e.getName().split(" "); - String relNameVar = ""; - int _length = nameArray.length; - boolean _equals_1 = (_length == 3); - if (_equals_1) { - relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); - } else { - relNameVar = e.getName(); - } - final String relName = relNameVar; - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_2 = (VLSFunction it) -> { - it.setConstant(this.support.toIDMultiple("e", relName)); - EList _terms = it.getTerms(); - VLSVariable _duplicate = this.support.duplicate(variable); - _terms.add(_duplicate); - }; - final VLSFunction enumElemPred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_2); - trace.element2Predicate.put(e, enumElemPred); - } - } - final List possibleNots = CollectionLiterals.newArrayList(); - final List typeDefs = CollectionLiterals.newArrayList(); - EList _elements_1 = type_1.getElements(); - for (final DefinedElement t1 : _elements_1) { - { - EList _elements_2 = type_1.getElements(); - for (final DefinedElement t2 : _elements_2) { - boolean _equals_1 = Objects.equal(t1, t2); - if (_equals_1) { - final VLSFunction fct = this.support.duplicate(CollectionsUtil.lookup(t2, trace.element2Predicate), variable); - possibleNots.add(fct); - } else { - final VLSFunction op = this.support.duplicate(CollectionsUtil.lookup(t2, trace.element2Predicate), variable); - VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_2 = (VLSUnaryNegation it) -> { - it.setOperand(op); - }; - final VLSUnaryNegation negFct = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_2); - possibleNots.add(negFct); - } - } - typeDefs.add(this.support.unfoldAnd(possibleNots)); - possibleNots.clear(); - } - } - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_2 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.lookup(type_1, trace.type2Predicate).getConstant().toString())); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_3 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(variable); - _variables.add(_duplicate); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_4 = (VLSEquivalent it_2) -> { - it_2.setLeft(CollectionsUtil.lookup(type_1, trace.type2Predicate)); - VLSAnd _createVLSAnd = this.factory.createVLSAnd(); - final Procedure1 _function_5 = (VLSAnd it_3) -> { - it_3.setLeft(this.support.topLevelTypeFunc(variable)); - it_3.setRight(this.support.unfoldOr(typeDefs)); - }; - VLSAnd _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function_5); - it_2.setRight(_doubleArrow); - }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_2); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(res); - for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { - { - final int num = (i + 1); - final int index = (i - globalCounter); - VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); - final Procedure1 _function_3 = (VLSFunctionAsTerm it) -> { - it.setFunctor(("eo" + Integer.valueOf(num))); - }; - final VLSFunctionAsTerm cstTerm = ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function_3); - trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); - final VLSConstant cst = this.support.toConstant(cstTerm); - trace.uniqueInstances.add(cst); - VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_4 = (VLSFofFormula it) -> { - String _xifexpression = null; - if (isNotEnum) { - _xifexpression = "definedType"; - } else { - _xifexpression = "enumScope"; - } - it.setName(this.support.toIDMultiple(_xifexpression, CollectionsUtil.lookup(type_1, trace.type2Predicate).getConstant().toString(), - type_1.getElements().get(index).getName().split(" ")[0])); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(variable); - _variables.add(_duplicate); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_6 = (VLSEquivalent it_2) -> { - VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_7 = (VLSEquality it_3) -> { - it_3.setLeft(this.support.duplicate(variable)); - it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); - }; - VLSEquality _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_7); - it_2.setLeft(_doubleArrow); - it_2.setRight(this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); - }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_6); - it_1.setOperand(_doubleArrow); - }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); - it.setFofFormula(_doubleArrow); - }; - final VLSFofFormula enumScope = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_4); - EList _formulas_1 = trace.specification.getFormulas(); - _formulas_1.add(enumScope); - } - } - int _globalCounter = globalCounter; - int _size = type_1.getElements().size(); - globalCounter = (_globalCounter + _size); - } - } - final Function1 _function_2 = (Type it) -> { - boolean _isIsAbstract = it.isIsAbstract(); - return Boolean.valueOf((!_isIsAbstract)); - }; - Iterable _filter_1 = IterableExtensions.filter(types, _function_2); - for (final Type t1 : _filter_1) { - { - for (final Type t2 : types) { - if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { - trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); - } else { - VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_3 = (VLSUnaryNegation it) -> { - it.setOperand(this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); - }; - VLSUnaryNegation _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); - trace.type2PossibleNot.put(t2, _doubleArrow); - } - } - Collection _values = trace.type2PossibleNot.values(); - ArrayList _arrayList = new ArrayList(_values); - trace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); - trace.type2PossibleNot.clear(); - } - } - final List type2Not = CollectionLiterals.newArrayList(); - for (final Type t : types) { - VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_3 = (VLSUnaryNegation it) -> { - it.setOperand(this.support.duplicate(CollectionsUtil.lookup(t, trace.type2Predicate))); - }; - VLSUnaryNegation _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); - type2Not.add(_doubleArrow); - } - VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_4 = (VLSFofFormula it) -> { - it.setName("notObjectHandler"); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(variable); - _variables.add(_duplicate); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_6 = (VLSEquivalent it_2) -> { - VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_7 = (VLSUnaryNegation it_3) -> { - it_3.setOperand(this.support.topLevelTypeFunc()); - }; - VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation_1, _function_7); - it_2.setLeft(_doubleArrow_1); - it_2.setRight(this.support.unfoldAnd(type2Not)); - }; - VLSEquivalent _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_6); - it_1.setOperand(_doubleArrow_1); - }; - VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); - it.setFofFormula(_doubleArrow_1); - }; - final VLSFofFormula notObj = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_4); - EList _formulas = trace.specification.getFormulas(); - _formulas.add(notObj); - VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_5 = (VLSFofFormula it) -> { - it.setName("inheritanceHierarchyHandler"); - it.setFofRole("axiom"); - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_6 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); - VLSVariable _duplicate = this.support.duplicate(variable); - _variables.add(_duplicate); - VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_7 = (VLSEquivalent it_2) -> { - it_2.setLeft(this.support.topLevelTypeFunc()); - Collection _values = trace.type2And.values(); - final ArrayList reversedList = new ArrayList(_values); - it_2.setRight(this.support.unfoldOr(reversedList)); - }; - VLSEquivalent _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_7); - it_1.setOperand(_doubleArrow_1); - }; - VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_6); - it.setFofFormula(_doubleArrow_1); - }; - final VLSFofFormula hierarch = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_5); - EList _formulas_1 = trace.specification.getFormulas(); - _xblockexpression = _formulas_1.add(hierarch); - } - return _xblockexpression; - } - - protected void transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { - throw new UnsupportedOperationException("TODO: auto-generated method stub"); - } - - protected void getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) { - throw new UnsupportedOperationException("TODO: auto-generated method stub"); - } - - protected void getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) { - throw new UnsupportedOperationException("TODO: auto-generated method stub"); - } - - protected VLSConstant transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { - VLSConstant _createVLSConstant = this.factory.createVLSConstant(); - final Procedure1 _function = (VLSConstant it) -> { - it.setName(referred.getName()); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); - } - - protected void getTypeInterpreter() { - throw new UnsupportedOperationException("TODO: auto-generated method stub"); - } -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java deleted file mode 100644 index 1e08c8ad..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java +++ /dev/null @@ -1,5 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -@SuppressWarnings("all") -public interface Logic2VampireLanguageMapper_TypeMapperTrace { -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java deleted file mode 100644 index 9fb23c71..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java +++ /dev/null @@ -1,42 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; -import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; -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.logic.model.logicresult.Statistics; -import org.eclipse.emf.common.util.EList; -import org.eclipse.xtext.xbase.lib.Extension; -import org.eclipse.xtext.xbase.lib.ObjectExtensions; -import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; - -@SuppressWarnings("all") -public class Vampire2LogicMapper { - @Extension - private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE; - - public ModelResult transformOutput(final LogicProblem problem, final int requiredNumberOfSolution, final MonitoredVampireSolution monitoredVampireSolution, final Logic2VampireLanguageMapperTrace trace, final long transformationTime) { - ModelResult _createModelResult = this.resultFactory.createModelResult(); - final Procedure1 _function = (ModelResult it) -> { - it.setProblem(problem); - EList _representation = it.getRepresentation(); - VampireModel _generatedModel = monitoredVampireSolution.getGeneratedModel(); - _representation.add(_generatedModel); - it.setTrace(trace); - it.setStatistics(this.transformStatistics(monitoredVampireSolution, transformationTime)); - }; - return ObjectExtensions.operator_doubleArrow(_createModelResult, _function); - } - - public Statistics transformStatistics(final MonitoredVampireSolution solution, final long transformationTime) { - Statistics _createStatistics = this.resultFactory.createStatistics(); - final Procedure1 _function = (Statistics it) -> { - long _solverTime = solution.getSolverTime(); - it.setSolverTime(((int) _solverTime)); - it.setTransformationTime(((int) transformationTime)); - }; - return ObjectExtensions.operator_doubleArrow(_createStatistics, _function); - } -} 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 deleted file mode 100644 index 39773357..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java +++ /dev/null @@ -1,82 +0,0 @@ -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; -import com.google.common.base.Objects; -import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; -import java.io.BufferedReader; -import java.io.FileReader; -import java.util.List; -import org.eclipse.emf.common.util.URI; -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 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 SOLNNAME = ((((("solution" + "_") + Integer.valueOf(configuration.typeScopes.minNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + - ".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 + " "); - String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); - long startTime = (-((long) 1)); - long solverTime = (-((long) 1)); - Process p = null; - boolean _equals = Objects.equal(configuration.solver, BackendSolver.LOCVAMP); - 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.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.println((((((CMD + CVC4LOC) + tempLoc) + OPTION_1) + " > ") + solnLoc)); - p = Runtime.getRuntime().exec((((((CMD + CVC4LOC) + tempLoc) + OPTION_1) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.newArrayList(("Path=" + PATH)), String.class))); - p.waitFor(); - long _currentTimeMillis_1 = System.currentTimeMillis(); - long _minus_1 = (_currentTimeMillis_1 - startTime); - solverTime = _minus_1; - } - FileReader _fileReader = new FileReader(solnLoc); - final BufferedReader reader = new BufferedReader(_fileReader); - final List output = CollectionLiterals.newArrayList(); - String line = ""; - while ((!Objects.equal((line = reader.readLine()), null))) { - boolean _equals_2 = Objects.equal(line, "Finite Model Found!"); - if (_equals_2) { - return new MonitoredVampireSolution(solverTime, null, true); - } - } - return new MonitoredVampireSolution(solverTime, null, false); - } catch (Throwable _e) { - throw Exceptions.sneakyThrow(_e); - } - } -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java deleted file mode 100644 index 507831fa..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java +++ /dev/null @@ -1,5 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -@SuppressWarnings("all") -public interface VampireModelInterpretation_TypeInterpretation { -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java deleted file mode 100644 index aff0dc9d..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java +++ /dev/null @@ -1,7 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; - -@SuppressWarnings("all") -public class VampireModelInterpretation_TypeInterpretation_FilteredTypes implements VampireModelInterpretation_TypeInterpretation { -} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java deleted file mode 100644 index b96df82a..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java +++ /dev/null @@ -1,19 +0,0 @@ -package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; - -import java.util.List; -import org.eclipse.xtext.xbase.lib.IterableExtensions; - -@SuppressWarnings("all") -public class VampireSolverException extends Exception { - public VampireSolverException(final String s) { - super(s); - } - - public VampireSolverException(final String s, final Exception e) { - super(s, e); - } - - public VampireSolverException(final String s, final List errors, final Exception e) { - super(((s + "\n") + IterableExtensions.join(errors, "\n")), e); - } -} -- cgit v1.2.3-70-g09d2