1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
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
import java.io.File
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/VampireTest''',"")
workspace.initAndClear
//Storing the logicProblem
val filename = "problem.logicproblem"
var LogicProblem problem = builder.createProblem
/*
deMorgan(problem)
/*/
rockPaperScisors(problem)
//*/
workspace.writeModel(problem, filename)
//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 = true
]
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
}
def name() {
return this.class.simpleName
}
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)
And(beats2.call(x,y),
x != y,
Not(beats2.call(y, x))
)
]
]))
//*/
}
}
|
