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 +++--- 3 files changed, 65 insertions(+), 14 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse') 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
 		}
 	}
 
-- 
cgit v1.2.3-54-g00ecf