1 files changed, 153 insertions, 0 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend
new file mode 100644
index 00000000..64914fd0
--- /dev/null
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend
@@ -0,0 +1,153 @@
+package ca.mcgill.ecse.dslreasoner.vampire.test
+import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
+import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
+import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
+import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
+import java.util.Collections
+import org.eclipse.emf.common.util.URI
+import org.eclipse.emf.ecore.resource.Resource
+import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl
+import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
+class VampireTest {
+        
+        val static extension LogicProblemBuilder builder = new LogicProblemBuilder
+        
+        def static void main(String[] args) {
+//              val inputs = new FileSystemWorkspace('''initialModels/''',"")
+                
+                
+                //create logic problem
+                //var LogicProblem problem = builder.createProblem
+                
+                
+                LogicproblemPackage.eINSTANCE.eClass()
+                Ecore2logicannotationsPackage.eINSTANCE.eClass()
+                Viatra2LogicAnnotationsPackage.eINSTANCE.eClass()
+                val reg = Resource.Factory.Registry.INSTANCE
+                val map = reg.extensionToFactoryMap
+                map.put("logicproblem", new XMIResourceFactoryImpl)
+                VampireLanguageStandaloneSetup.doSetup
+                
+                val workspace = new FileSystemWorkspace('''output/models/''',"")
+                workspace.initAndClear
+                
+                // Load and create top level elements
+                // Load source model
+                val rs = new ResourceSetImpl
+                val logicURI = URI.createFileURI("output/files/logProb.logicproblem")
+                val logRes = rs.createResource(logicURI)
+                
+                var LogicProblem problem = builder.createProblem
+                
+                //*
+                deMorgan(problem)
+                /*/
+                rockPaperScisors(problem)
+                //*/
+                
+                logRes.contents.add(problem)
+                logRes.save(Collections.EMPTY_MAP)
+                //problem.add(Assertion( Y && X <=> X) )
+                
+                println("Problem Created");
+                
+                var LogicResult solution
+                var LogicReasoner reasoner
+                
+                reasoner = new VampireSolver
+                val vampireConfig = new VampireSolverConfiguration => [
+                        //add configuration things, in config file first
+                        it.writeToFile = false
+                ]
+                
+                solution = reasoner.solve(problem, vampireConfig,       workspace)
+                
+//              if(solution instanceof ModelResult) {
+//                      reasoner.getInterpretations(solution)
+//              }
+                //^can extract everything (ex, vars) from solver
+                
+                //call the solver
+                
+                println("Problem Solved")
+                
+                //output solution
+                
+        }
+        
+        static def deMorgan(LogicProblem problem) {
+                
+                
+                var X = ConstantDeclaration(LogicBool)
+                var Y = ConstantDeclaration(LogicBool)
+                problem.add(X)
+                problem.add(Y)
+                
+                //assertion is negated manually because logic problem can only handle axioms (assertions)
+                //so ya
+                problem.add(Assertion( !(X && Y) <=> ( !X || !Y)) )
+        }
+        
+        static def rockPaperScisors(LogicProblem problem) {
+                val rock = Element("Rock")
+                val paper= Element("Paper")
+                val scissor = Element("Scissor")
+                
+                problem.elements += rock
+                problem.elements += paper
+                problem.elements += scissor 
+                
+//              val red = Element("Red")
+//              val green = Element("Green")
+//              
+//              problem.elements += red
+//              problem.elements += green
+                
+                
+                //val allRPS = problem.add(TypeDeclaration("allRPS", true))
+                //val newRPS = problem.add(TypeDeclaration("newRPS", false))
+                val oldRPS = problem.add(TypeDefinition("oldRPS", false, rock, paper, scissor)) //n+1 axioms, where n is the number of type definitions. 1. rocjk, paper, scissor are all rps. 2. every object is rps
+                
+//              val color = problem.add(TypeDefinition("color", false, red, green ))
+                //Supertype(oldRPS,allRPS)
+                //Supertype(newRPS,oldRPS)
+                
+                
+                
+                
+                /* Remains
+                val beats = problem.add(RelationDefinition("beats",[
+                        val x = addVar("x",oldRPS)
+                        val y = addVar("y",oldRPS)
+                        (x==rock && y==scissor)||(x==scissor && y==paper)||(x==paper && y==rock)
+                ]))
+                
+                /*/
+                //below needs to be added as an axiom
+                val beats2 = problem.add(RelationDeclaration("beats2",oldRPS,oldRPS))
+                problem.add(Assertion(Forall[
+                        val x = addVar("x",oldRPS) 
+                        //x.range
+                        Exists[
+                                val y = addVar("y",oldRPS)
+                                beats2.call(x,y)
+                        ]
+                ]))
+                //*/
+                
+        }
+}
+\ No newline at end of file

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend new file mode 100644 index 00000000..64914fd0 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.xtend
@@ -0,0 +1,153 @@
	1	package ca.mcgill.ecse.dslreasoner.vampire.test
	2
	3
	4	import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup
	5	import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
	6	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
	7	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
	8	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
	9	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
	10	import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
	11	import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
	12	import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
	13	import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
	14	import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
	15	import java.util.Collections
	16	import org.eclipse.emf.common.util.URI
	17	import org.eclipse.emf.ecore.resource.Resource
	18	import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl
	19	import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
	20
	21	class VampireTest {
	22
	23	val static extension LogicProblemBuilder builder = new LogicProblemBuilder
	24
	25	def static void main(String[] args) {
	26	// val inputs = new FileSystemWorkspace('''initialModels/''',"")
	27
	28
	29	//create logic problem
	30	//var LogicProblem problem = builder.createProblem
	31
	32
	33
	34	LogicproblemPackage.eINSTANCE.eClass()
	35	Ecore2logicannotationsPackage.eINSTANCE.eClass()
	36	Viatra2LogicAnnotationsPackage.eINSTANCE.eClass()
	37	val reg = Resource.Factory.Registry.INSTANCE
	38	val map = reg.extensionToFactoryMap
	39	map.put("logicproblem", new XMIResourceFactoryImpl)
	40	VampireLanguageStandaloneSetup.doSetup
	41
	42	val workspace = new FileSystemWorkspace('''output/models/''',"")
	43	workspace.initAndClear
	44
	45	// Load and create top level elements
	46	// Load source model
	47	val rs = new ResourceSetImpl
	48	val logicURI = URI.createFileURI("output/files/logProb.logicproblem")
	49	val logRes = rs.createResource(logicURI)
	50
	51	var LogicProblem problem = builder.createProblem
	52
	53	//*
	54	deMorgan(problem)
	55	/*/
	56	rockPaperScisors(problem)
	57	//*/
	58
	59	logRes.contents.add(problem)
	60	logRes.save(Collections.EMPTY_MAP)
	61
	62	//problem.add(Assertion( Y && X <=> X) )
	63
	64	println("Problem Created");
	65
	66	var LogicResult solution
	67	var LogicReasoner reasoner
	68
	69	reasoner = new VampireSolver
	70	val vampireConfig = new VampireSolverConfiguration => [
	71	//add configuration things, in config file first
	72	it.writeToFile = false
	73	]
	74
	75	solution = reasoner.solve(problem, vampireConfig, workspace)
	76
	77	// if(solution instanceof ModelResult) {
	78	// reasoner.getInterpretations(solution)
	79	// }
	80	//^can extract everything (ex, vars) from solver
	81
	82
	83	//call the solver
	84
	85	println("Problem Solved")
	86
	87	//output solution
	88
	89	}
	90
	91	static def deMorgan(LogicProblem problem) {
	92
	93
	94	var X = ConstantDeclaration(LogicBool)
	95	var Y = ConstantDeclaration(LogicBool)
	96	problem.add(X)
	97	problem.add(Y)
	98
	99	//assertion is negated manually because logic problem can only handle axioms (assertions)
	100	//so ya
	101	problem.add(Assertion( !(X && Y) <=> ( !X \|\| !Y)) )
	102	}
	103
	104	static def rockPaperScisors(LogicProblem problem) {
	105
	106	val rock = Element("Rock")
	107	val paper= Element("Paper")
	108	val scissor = Element("Scissor")
	109
	110	problem.elements += rock
	111	problem.elements += paper
	112	problem.elements += scissor
	113
	114	// val red = Element("Red")
	115	// val green = Element("Green")
	116	//
	117	// problem.elements += red
	118	// problem.elements += green
	119
	120
	121	//val allRPS = problem.add(TypeDeclaration("allRPS", true))
	122	//val newRPS = problem.add(TypeDeclaration("newRPS", false))
	123	val oldRPS = problem.add(TypeDefinition("oldRPS", false, rock, paper, scissor)) //n+1 axioms, where n is the number of type definitions. 1. rocjk, paper, scissor are all rps. 2. every object is rps
	124
	125	// val color = problem.add(TypeDefinition("color", false, red, green ))
	126	//Supertype(oldRPS,allRPS)
	127	//Supertype(newRPS,oldRPS)
	128
	129
	130
	131
	132	/* Remains
	133	val beats = problem.add(RelationDefinition("beats",[
	134	val x = addVar("x",oldRPS)
	135	val y = addVar("y",oldRPS)
	136	(x==rock && y==scissor)\|\|(x==scissor && y==paper)\|\|(x==paper && y==rock)
	137	]))
	138
	139	/*/
	140	//below needs to be added as an axiom
	141	val beats2 = problem.add(RelationDeclaration("beats2",oldRPS,oldRPS))
	142	problem.add(Assertion(Forall[
	143	val x = addVar("x",oldRPS)
	144	//x.range
	145	Exists[
	146	val y = addVar("y",oldRPS)
	147	beats2.call(x,y)
	148	]
	149	]))
	150	//*/
	151
	152	}
	153	} \ No newline at end of file