aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend3
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend101
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend203
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend74
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend45
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend9
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend74
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend119
8 files changed, 367 insertions, 261 deletions
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 27e00ccf..618980a3 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
@@ -4,10 +4,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
4 4
5class VampireSolverConfiguration extends LogicSolverConfiguration { 5class VampireSolverConfiguration extends LogicSolverConfiguration {
6 6
7 public var int symmetry = 0 // by default 7 //public var int symmetry = 0 // by default
8 //choose needed backend solver 8 //choose needed backend solver
9// public var VampireBackendSolver solver = VampireBackendSolver.SAT4J 9// public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
10 public var boolean writeToFile = false
11} 10}
12 11
13 12
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 cbe53bff..ee802a99 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
@@ -7,6 +7,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage
7import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper 7import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper
8import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler 8import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage 9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage
10import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
10import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner 11import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
11import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException 12import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration 13import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
@@ -14,80 +15,81 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult 15import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
15import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 16import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
16 17
17class VampireSolver extends LogicReasoner{ 18class VampireSolver extends LogicReasoner {
18 19
19 new() { 20 new() {
20 VampireLanguagePackage.eINSTANCE.eClass 21 VampireLanguagePackage.eINSTANCE.eClass
21 val x = new VampireLanguageStandaloneSetupGenerated 22 val x = new VampireLanguageStandaloneSetupGenerated
22 VampireLanguageStandaloneSetup::doSetup() 23 VampireLanguageStandaloneSetup::doSetup()
23 } 24 }
24 25
25 val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes) 26 val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(
26 val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper 27 new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes)
27 val VampireHandler handler = new VampireHandler 28 val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper
28 29 val VampireHandler handler = new VampireHandler
29 30
30 val fileName = "vampireProblem.tptp" 31 val fileName = "vampireProblem.tptp"
31 32
32 override solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace) throws LogicReasonerException { 33 override solve(LogicProblem problem, LogicSolverConfiguration config,
34 ReasonerWorkspace workspace) throws LogicReasonerException {
33 val vampireConfig = config.asConfig 35 val vampireConfig = config.asConfig
34 36
35 // Start: Logic -> Vampire mapping 37 // Start: Logic -> Vampire mapping
36 val transformationStart = System.currentTimeMillis 38 val transformationStart = System.currentTimeMillis
37 //TODO 39 // TODO
38 val result = forwardMapper.transformProblem(problem,vampireConfig) 40 val result = forwardMapper.transformProblem(problem, vampireConfig)
39 val vampireProblem = result.output 41 val vampireProblem = result.output
40 val forwardTrace = result.trace 42 val forwardTrace = result.trace
41 43
42 var String fileURI = null; 44 var String fileURI = null;
43 var String vampireCode = null; 45 var String vampireCode = null;
44 vampireCode = workspace.writeModelToString(vampireProblem,fileName) 46 vampireCode = workspace.writeModelToString(vampireProblem, fileName)
45 if(vampireConfig.writeToFile) { 47
46 fileURI = workspace.writeModel(vampireProblem,fileName).toFileString 48 val writeFile = (
49 vampireConfig.documentationLevel === DocumentationLevel::NORMAL ||
50 vampireConfig.documentationLevel === DocumentationLevel::FULL)
51 if (writeFile) {
52 fileURI = workspace.writeModel(vampireProblem, fileName).toFileString
47 } 53 }
48
49 //Result as String
50 54
51 55 // Result as String
52 val transformationTime = System.currentTimeMillis - transformationStart 56 val transformationTime = System.currentTimeMillis - transformationStart
53 // Finish: Logic -> Vampire mapping 57 // Finish: Logic -> Vampire mapping
54
55
56 /* 58 /*
57 // Start: Solving Alloy problem 59 * // Start: Solving Alloy problem
58 val solverStart = System.currentTimeMillis 60 * val solverStart = System.currentTimeMillis
59 //Calling Solver (Currently Manually) 61 * //Calling Solver (Currently Manually)
60 val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode) 62 * val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode)
61// val result2 = null 63 * // val result2 = null
62 //TODO 64 * //TODO
63 //Backwards Mapper 65 * //Backwards Mapper
64 val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) 66 * val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime)
65 67 *
66 val solverFinish = System.currentTimeMillis-solverStart 68 * val solverFinish = System.currentTimeMillis-solverStart
67 // Finish: Solving Alloy problem 69 * // Finish: Solving Alloy problem
68 70 *
69 if(vampireConfig.writeToFile) workspace.deactivateModel(fileName) 71 * if(vampireConfig.writeToFile) workspace.deactivateModel(fileName)
70 72 *
71 return logicResult 73 * return logicResult
72 74 *
73 /*/ 75 /*/
74 return null // for now 76 return null // for now
75 //*/ 77 // */
76 } 78 }
77 79
78 def asConfig(LogicSolverConfiguration configuration){ 80 def asConfig(LogicSolverConfiguration configuration) {
79 if(configuration instanceof VampireSolverConfiguration) { 81 if (configuration instanceof VampireSolverConfiguration) {
80 return configuration 82 return configuration
81 } else { 83 } else {
82 throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''') 84 throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''')
83 } 85 }
84 } 86 }
85 87
86// /* 88// /*
87// * not for now 89// * not for now
88// * 90// *
89 override getInterpretations(ModelResult modelResult) { 91 override getInterpretations(ModelResult modelResult) {
90 //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] 92 // val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key]
91// val sols = modelResult.representation// as List<A4Solution> 93// val sols = modelResult.representation// as List<A4Solution>
92// //val res = answers.map 94// //val res = answers.map
93// sols.map[ 95// sols.map[
@@ -98,7 +100,6 @@ class VampireSolver extends LogicReasoner{
98// modelResult.trace as Logic2AlloyLanguageMapperTrace 100// modelResult.trace as Logic2AlloyLanguageMapperTrace
99// ) 101// )
100// ] 102// ]
101 } 103 }
102// */ 104// */
103 105}
104} \ No newline at end of file
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index cd48a032..e2c15b75 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -48,6 +48,8 @@ class Logic2VampireLanguageMapper {
48 this) 48 this)
49 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( 49 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(
50 this) 50 this)
51 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(
52 this)
51 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper 53 @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper
52 54
53 public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) { 55 public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) {
@@ -72,11 +74,15 @@ class Logic2VampireLanguageMapper {
72// it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem)) 74// it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem))
73 ] 75 ]
74 76
75 // call mappers 77 // TYPE MAPPER
76 if (!problem.types.isEmpty) { 78 if (!problem.types.isEmpty) {
77 typeMapper.transformTypes(problem.types, problem.elements, this, trace) 79 typeMapper.transformTypes(problem.types, problem.elements, this, trace)
78 } 80 }
79 81
82 // SCOPE MAPPER
83 scopeMapper.transformScope(config, trace)
84
85
80 trace.constantDefinitions = problem.collectConstantDefinitions 86 trace.constantDefinitions = problem.collectConstantDefinitions
81 trace.relationDefinitions = problem.collectRelationDefinitions 87 trace.relationDefinitions = problem.collectRelationDefinitions
82 88
@@ -204,8 +210,9 @@ class Logic2VampireLanguageMapper {
204 ] 210 ]
205 } 211 }
206 212
207 def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { 213 def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace,
208 support.unfoldDistinctTerms(this,distinct.operands,trace,variables) } 214 Map<Variable, VLSVariable> variables) { support.unfoldDistinctTerms(this, distinct.operands, trace, variables) }
215
209// 216//
210// def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { 217// def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
211// createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] } 218// createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] }
@@ -228,12 +235,14 @@ class Logic2VampireLanguageMapper {
228 support.createExistentiallyQuantifiedExpression(this, exists, trace, variables) 235 support.createExistentiallyQuantifiedExpression(this, exists, trace, variables)
229 } 236 }
230 237
231 def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { 238 def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace,
239 Map<Variable, VLSVariable> variables) {
232 return createVLSFunction => [ 240 return createVLSFunction => [
233 it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name ) 241 it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name)
234 it.terms += instanceOf.value.transformTerm(trace, variables) 242 it.terms += instanceOf.value.transformTerm(trace, variables)
235 ] 243 ]
236 } 244 }
245
237// 246//
238// def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { 247// def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {
239// return this.relationMapper.transformTransitiveRelationReference( 248// return this.relationMapper.transformTransitiveRelationReference(
@@ -253,50 +262,49 @@ class Logic2VampireLanguageMapper {
253 def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, 262 def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred,
254 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, 263 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
255 Map<Variable, VLSVariable> variables) { 264 Map<Variable, VLSVariable> variables) {
256 typeMapper.transformReference(referred, trace) 265 typeMapper.transformReference(referred, trace)
257 } 266 }
258 267
259 def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant, 268 def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant,
260 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, 269 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
261 Map<Variable, VLSVariable> variables) { 270 Map<Variable, VLSVariable> variables) {
262 // might need to make sure that only declared csts get transformed. see for Alloy 271 // might need to make sure that only declared csts get transformed. see for Alloy
263 val res = createVLSConstant => [ 272 val res = createVLSConstant => [
264 // ask if necessary VLSConstantDeclaration and not just directly strng 273 // ask if necessary VLSConstantDeclaration and not just directly strng
265 it.name = support.toID(constant.name) 274 it.name = support.toID(constant.name)
266 ] 275 ]
267 // no postprocessing cuz booleans are accepted 276 // no postprocessing cuz booleans are accepted
268 return res 277 return res
269 } 278 }
270 279
271 // NOT NEEDED FOR NOW 280 // NOT NEEDED FOR NOW
272 // TODO 281 // TODO
273 def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant, 282 def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant,
274 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, 283 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
275 Map<Variable, VLSVariable> variables) { 284 Map<Variable, VLSVariable> variables) {
276// val res = createVLSFunctionCall => [ 285// val res = createVLSFunctionCall => [
277// it.referredDefinition = constant.lookup(trace.constantDefinition2Function) 286// it.referredDefinition = constant.lookup(trace.constantDefinition2Function)
278// ] 287// ]
279// return support.postprocessResultOfSymbolicReference(constant.type,res,trace) 288// return support.postprocessResultOfSymbolicReference(constant.type,res,trace)
280 } 289 }
281 290
282 def dispatch protected VLSTerm transformSymbolicReference(Variable variable, 291 def dispatch protected VLSTerm transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions,
283 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, 292 Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
284 Map<Variable, VLSVariable> variables) {
285 293
286 // cannot treat variable as function (constant) because of name ID not being the same 294 // cannot treat variable as function (constant) because of name ID not being the same
287 // below does not work 295 // below does not work
288 val res = createVLSVariable => [ 296 val res = createVLSVariable => [
289// it.name = support.toIDMultiple("Var", variable.lookup(variables).name) 297// it.name = support.toIDMultiple("Var", variable.lookup(variables).name)
290 it.name = support.toID(variable.lookup(variables).name) 298 it.name = support.toID(variable.lookup(variables).name)
291 ] 299 ]
292 // no need for potprocessing cuz booleans are supported 300 // no need for potprocessing cuz booleans are supported
293 return res 301 return res
294 } 302 }
295 303
296 // TODO 304 // TODO
297 def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function, 305 def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function,
298 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, 306 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
299 Map<Variable, VLSVariable> variables) { 307 Map<Variable, VLSVariable> variables) {
300// if(trace.functionDefinitions.containsKey(function)) { 308// if(trace.functionDefinitions.containsKey(function)) {
301// return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables) 309// return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables)
302// } else { 310// } else {
@@ -316,71 +324,68 @@ class Logic2VampireLanguageMapper {
316// return support.postprocessResultOfSymbolicReference(function.range,res,trace) 324// return support.postprocessResultOfSymbolicReference(function.range,res,trace)
317// } 325// }
318// } 326// }
319 } 327 }
320 328
321 // TODO 329 // TODO
322 def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function, 330 def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function,
323 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, 331 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
324 Map<Variable, VLSVariable> variables) { 332 Map<Variable, VLSVariable> variables) {
325// val result = createVLSFunctionCall => [ 333// val result = createVLSFunctionCall => [
326// it.referredDefinition = function.lookup(trace.functionDefinition2Function) 334// it.referredDefinition = function.lookup(trace.functionDefinition2Function)
327// it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)] 335// it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)]
328// ] 336// ]
329// return support.postprocessResultOfSymbolicReference(function.range,result,trace) 337// return support.postprocessResultOfSymbolicReference(function.range,result,trace)
330 } 338 }
331 339
332 // TODO 340 // TODO
333 /* 341 /*
334 def dispatch protected VLSTerm transformSymbolicReference(Relation relation, 342 * def dispatch protected VLSTerm transformSymbolicReference(Relation relation,
335 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, 343 * List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
336 Map<Variable, VLSVariable> variables) { 344 * Map<Variable, VLSVariable> variables) {
337 if (trace.relationDefinitions.containsKey(relation)) { 345 * if (trace.relationDefinitions.containsKey(relation)) {
338 this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), 346 * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),
339 parameterSubstitutions, trace, variables) 347 * parameterSubstitutions, trace, variables)
340 } 348 * }
341 else { 349 * else {
342// if (relationMapper.transformToHostedField(relation, trace)) { 350 * // if (relationMapper.transformToHostedField(relation, trace)) {
343// val VLSRelation = relation.lookup(trace.relationDeclaration2Field) 351 * // val VLSRelation = relation.lookup(trace.relationDeclaration2Field)
344// // R(a,b) => 352 * // // R(a,b) =>
345// // b in a.R 353 * // // b in a.R
346// return createVLSSubset => [ 354 * // return createVLSSubset => [
347// it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) 355 * // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables)
348// it.rightOperand = createVLSJoin => [ 356 * // it.rightOperand = createVLSJoin => [
349// it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) 357 * // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables)
350// it.rightOperand = createVLSReference => [it.referred = VLSRelation] 358 * // it.rightOperand = createVLSReference => [it.referred = VLSRelation]
351// ] 359 * // ]
352// ] 360 * // ]
353// } else { 361 * // } else {
354// val target = createVLSJoin => [ 362 * // val target = createVLSJoin => [
355// leftOperand = createVLSReference => [referred = trace.logicLanguage] 363 * // leftOperand = createVLSReference => [referred = trace.logicLanguage]
356// rightOperand = createVLSReference => [ 364 * // rightOperand = createVLSReference => [
357// referred = relation.lookup(trace.relationDeclaration2Global) 365 * // referred = relation.lookup(trace.relationDeclaration2Global)
358// ] 366 * // ]
359// ] 367 * // ]
360// val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) 368 * // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables)
361// 369 * //
362// return createVLSSubset => [ 370 * // return createVLSSubset => [
363// leftOperand = source 371 * // leftOperand = source
364// rightOperand = target 372 * // rightOperand = target
365// ] 373 * // ]
366// } 374 * // }
367 } 375 * }
368 } 376 * }
369 */ 377 */
370 378 // TODO
371 // TODO 379 def dispatch protected VLSTerm transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions,
372 def dispatch protected VLSTerm transformSymbolicReference(Relation relation, 380 Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
373 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
374 Map<Variable, VLSVariable> variables) {
375// createVLSFunction => [ 381// createVLSFunction => [
376// it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) 382// it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate)
377// it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] 383// it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
378// ] 384// ]
379 return createVLSFunction => [ 385 return createVLSFunction => [
380 it.constant = support.toIDMultiple("rel", relation.name) 386 it.constant = support.toIDMultiple("rel", relation.name)
381 it.terms += parameterSubstitutions.map[p | p.transformTerm(trace,variables)] 387 it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
382 ] 388 ]
383 } 389 }
384 390
385 } 391}
386 \ No newline at end of file
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
new file mode 100644
index 00000000..84aa521d
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -0,0 +1,74 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
2
3import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant
4import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
7import java.util.List
8
9class Logic2VampireLanguageMapper_ScopeMapper {
10 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
11 private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
12 val Logic2VampireLanguageMapper base
13
14 public new(Logic2VampireLanguageMapper base) {
15 this.base = base
16 }
17
18 def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
19 val VLSVariable variable = createVLSVariable => [it.name = "A"]
20
21
22 // 1. make a list of constants equaling the min number of specified objects
23 val List<VLSConstant> instances = newArrayList
24 for (var i = 0; i < config.typeScopes.minNewElements; i++) {
25 val num = i + 1
26 val cst = createVLSConstant => [
27 it.name = "o" + num
28 ]
29 instances.add(cst)
30 }
31
32
33 // TODO: specify for the max
34
35
36 // 2. Create initial fof formula to specify the number of elems
37 val cstDec = createVLSFofFormula => [
38 it.name = "typeScope"
39 it.fofRole = "axiom"
40 it.fofFormula = createVLSUniversalQuantifier => [
41 it.variables += support.duplicate(variable)
42 // check below
43 it.operand = createVLSEquivalent => [
44 it.left = support.topLevelTypeFunc
45 it.right = support.unfoldOr(instances.map [ i |
46 createVLSEquality => [
47 it.left = createVLSVariable => [it.name = variable.name]
48 it.right = i
49 ]
50 ])
51 ]
52 ]
53 ]
54 trace.specification.formulas += cstDec
55
56
57 // TODO: specify for scope per type
58
59
60
61 // 3. Specify uniqueness of elements
62 val uniqueness = createVLSFofFormula => [
63 it.name = "typeUniqueness"
64 it.fofRole = "axiom"
65 it.fofFormula = support.unfoldOr(instances.map [ i |
66 createVLSEquality => [
67 it.left = createVLSVariable => [it.name = variable.name]
68 it.right = i
69 ]
70 ])
71 ]
72 trace.specification.formulas += cstDec
73 }
74}
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 ab92b42f..e69f0d51 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
@@ -1,17 +1,18 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder 1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
2 2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression 3import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm 4import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable 5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory 6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
8import java.util.ArrayList 11import java.util.ArrayList
9import java.util.HashMap 12import java.util.HashMap
10import java.util.List 13import java.util.List
11import java.util.Map 14import java.util.Map
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
13import org.eclipse.emf.common.util.EList 15import org.eclipse.emf.common.util.EList
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
15 16
16class Logic2VampireLanguageMapper_Support { 17class Logic2VampireLanguageMapper_Support {
17 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE 18 private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -25,6 +26,19 @@ class Logic2VampireLanguageMapper_Support {
25 ids.split("\\s+").join("_") 26 ids.split("\\s+").join("_")
26 } 27 }
27 28
29 def protected VLSVariable duplicate(VLSVariable vrbl) {
30 return createVLSVariable => [it.name = vrbl.name]
31 }
32
33 def protected VLSFunction topLevelTypeFunc() {
34 return createVLSFunction => [
35 it.constant = "object"
36 it.terms += createVLSVariable => [
37 it.name = "A"
38 ]
39 ]
40 }
41
28 // Support Functions 42 // Support Functions
29 // booleans 43 // booleans
30 // AND and OR 44 // AND and OR
@@ -41,7 +55,6 @@ class Logic2VampireLanguageMapper_Support {
41 } 55 }
42 56
43 def protected VLSTerm unfoldOr(List<? extends VLSTerm> operands) { 57 def protected VLSTerm unfoldOr(List<? extends VLSTerm> operands) {
44
45// if(operands.size == 0) {basically return true} 58// if(operands.size == 0) {basically return true}
46 /*else*/ if (operands.size == 1) { 59 /*else*/ if (operands.size == 1) {
47 return operands.head 60 return operands.head
@@ -56,20 +69,21 @@ class Logic2VampireLanguageMapper_Support {
56 69
57 def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands, 70 def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands,
58 Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { 71 Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) {
59 if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) } 72 if (operands.size == 1) {
60 else if(operands.size > 1) { 73 return m.transformTerm(operands.head, trace, variables)
61 val notEquals = new ArrayList<VLSTerm>(operands.size*operands.size/2) 74 } else if (operands.size > 1) {
62 for(i:0..<operands.size) { 75 val notEquals = new ArrayList<VLSTerm>(operands.size * operands.size / 2)
63 for(j: i+1..<operands.size) { 76 for (i : 0 ..< operands.size) {
64 notEquals+=createVLSInequality=>[ 77 for (j : i + 1 ..< operands.size) {
65 it.left= m.transformTerm(operands.get(i),trace,variables) 78 notEquals += createVLSInequality => [
66 it.right = m.transformTerm(operands.get(j),trace,variables) 79 it.left = m.transformTerm(operands.get(i), trace, variables)
80 it.right = m.transformTerm(operands.get(j), trace, variables)
67 ] 81 ]
68 } 82 }
69 } 83 }
70 return notEquals.unfoldAnd 84 return notEquals.unfoldAnd
71 } 85 } else
72 else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') 86 throw new UnsupportedOperationException('''Logic operator with 0 operands!''')
73 } 87 }
74 88
75 // Symbolic 89 // Symbolic
@@ -105,7 +119,6 @@ class Logic2VampireLanguageMapper_Support {
105 ] 119 ]
106 typedefs.add(eq) 120 typedefs.add(eq)
107 } 121 }
108
109 122
110 createVLSUniversalQuantifier => [ 123 createVLSUniversalQuantifier => [
111 it.variables += variableMap.values 124 it.variables += variableMap.values
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
index a0f0edda..aba47edb 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
@@ -1,20 +1,17 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder 1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
2 2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction 3import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm 4import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
8import java.util.ArrayList 5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
9import java.util.HashMap 7import java.util.HashMap
10import java.util.List
11import java.util.Map 8import java.util.Map
12 9
13class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace{ 10class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace{
14 11
15// public var VLSFofFormula objectSuperClass 12// public var VLSFofFormula objectSuperClass
16 public val Map<Type, VLSFunction> type2Predicate = new HashMap; 13 public val Map<Type, VLSFunction> type2Predicate = new HashMap;
17 public val Map<DefinedElement, VLSEquality> definedElement2Declaration = new HashMap //Not Yet Used 14 public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap
18 public val Map<Type, VLSTerm> type2PossibleNot = new HashMap 15 public val Map<Type, VLSTerm> type2PossibleNot = new HashMap
19 public val Map<Type, VLSTerm> type2And = new HashMap 16 public val Map<Type, VLSTerm> type2And = new HashMap
20 17
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
index 41e2137c..eed10656 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -11,6 +11,8 @@ import java.util.ArrayList
11import java.util.Collection 11import java.util.Collection
12 12
13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
14import java.util.List
15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
14 16
15class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { 17class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {
16 private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support 18 private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
@@ -25,50 +27,66 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
25 val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes 27 val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
26 trace.typeMapperTrace = typeTrace 28 trace.typeMapperTrace = typeTrace
27 29
28 val VLSVariable variable = createVLSVariable => [it.name = "A"] // did not work 30 // The variable
29 // 1. store predicates for declarations in trace 31 val VLSVariable variable = createVLSVariable => [it.name = "A"]
32
33 // 1. Each type (class) is a predicate with a single variable as input
30 for (type : types) { 34 for (type : types) {
31 val typePred = createVLSFunction => [ 35 val typePred = createVLSFunction => [
32 it.constant = support.toIDMultiple("type", type.name) 36 it.constant = support.toIDMultiple("t", type.name)
33 it.terms += createVLSVariable => [it.name = variable.name] 37 it.terms += support.duplicate(variable)
34 ] 38 ]
35 typeTrace.type2Predicate.put(type, typePred) 39 typeTrace.type2Predicate.put(type, typePred)
36 } 40 }
37 41
38 // 2. Map each type definition to fof formula 42 // 2. Map each ENUM type definition to fof formula
39 for (type : types.filter(TypeDefinition)) { 43 for (type : types.filter(TypeDefinition)) {
44 val List<VLSFunction> orElems = newArrayList
45 for (e : type.elements) {
46 val enumElemPred = createVLSFunction => [
47 it.constant = support.toIDMultiple("e", e.name, type.name)
48 it.terms += support.duplicate(variable)
49 ]
50 typeTrace.element2Predicate.put(e, enumElemPred)
51 orElems.add(enumElemPred)
52 }
40 53
41 val res = createVLSFofFormula => [ 54 val res = createVLSFofFormula => [
42 it.name = support.toIDMultiple("typeDef", type.name) 55 it.name = support.toIDMultiple("typeDef", type.name)
43 // below is temporary solution 56 // below is temporary solution
44 it.fofRole = "axiom" 57 it.fofRole = "axiom"
45 it.fofFormula = createVLSUniversalQuantifier => [ 58 it.fofFormula = createVLSUniversalQuantifier => [
46 it.variables += createVLSVariable => [it.name = variable.name] 59 it.variables += support.duplicate(variable)
47 it.operand = createVLSEquivalent => [ 60 it.operand = createVLSEquivalent => [
48 it.left = createVLSFunction => [ 61// it.left = createVLSFunction => [
49 it.constant = type.lookup(typeTrace.type2Predicate).constant 62// it.constant = type.lookup(typeTrace.type2Predicate).constant
50 it.terms += createVLSVariable => [it.name = "A"] 63// it.terms += createVLSVariable => [it.name = "A"]
51 ] 64// ]
52 65 it.left = type.lookup(typeTrace.type2Predicate)
53 type.lookup(typeTrace.type2Predicate) 66
54 it.right = support.unfoldOr(type.elements.map [ e | 67 it.right = support.unfoldOr(orElems)
55 createVLSEquality => [ 68
56 it.left = createVLSVariable => [it.name = variable.name] 69 // TEMPPPPPPP
70// it.right = support.unfoldOr(type.elements.map [e |
71//
72// createVLSEquality => [
73// it.left = support.duplicate(variable)
57// it.right = createVLSDoubleQuote => [ 74// it.right = createVLSDoubleQuote => [
58// it.value = "\"" + e.name + "\"" 75// it.value = "\"a" + e.name + "\""
59// ] 76// ]
60 it.right = createVLSDoubleQuote => [ 77// ]
61 it.value = "\"a" + e.name + "\"" 78// ])
62 ] 79 // END TEMPPPPP
63 ]
64 ])
65 ] 80 ]
66 ] 81 ]
67 82
68 ] 83 ]
69 trace.specification.formulas += res 84 trace.specification.formulas += res
70 } 85 }
71 // 2.5. Currently allowing duplicate types. Not problematic cuz strings are by def unique 86
87 //HIERARCHY HANDLER
88
89
72 // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates 90 // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
73 // and store in a map 91 // and store in a map
74// val List<VLSTerm> type2PossibleNot = new ArrayList 92// val List<VLSTerm> type2PossibleNot = new ArrayList
@@ -97,19 +115,17 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp
97 } 115 }
98 116
99 // 5. create fof function that is an or with all the elements in map 117 // 5. create fof function that is an or with all the elements in map
100 // Do this only if there are more than 1 type 118
119
120
121
101 val hierarch = createVLSFofFormula => [ 122 val hierarch = createVLSFofFormula => [
102 it.name = "hierarchyHandler" 123 it.name = "hierarchyHandler"
103 it.fofRole = "axiom" 124 it.fofRole = "axiom"
104 it.fofFormula = createVLSUniversalQuantifier => [ 125 it.fofFormula = createVLSUniversalQuantifier => [
105 it.variables += createVLSVariable => [it.name = "A"] 126 it.variables += createVLSVariable => [it.name = "A"]
106 it.operand = createVLSEquivalent => [ 127 it.operand = createVLSEquivalent => [
107 it.left = createVLSFunction => [ 128 it.left = support.topLevelTypeFunc
108 it.constant = "object"
109 it.terms += createVLSVariable => [
110 it.name = "A"
111 ]
112 ]
113 it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values)) 129 it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
114 ] 130 ]
115 ] 131 ]
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
index 5cb0198e..9c9e65b4 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
@@ -4,63 +4,64 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
4import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory 4import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
5 5
6class Vampire2LogicMapper { 6class Vampire2LogicMapper {
7 val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
8
9 public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) {
10 val models = vampireSolution.aswers.map[it.key].toList
11
12 if(!monitoredAlloySolution.finishedBeforeTimeout) {
13 return createInsuficientResourcesResult => [
14 it.problem = problem
15 it.representation += models
16 it.trace = trace
17 it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
18 ]
19 } else {
20 if(models.last.satisfiable || requiredNumberOfSolution == -1) {
21 return createModelResult => [
22 it.problem = problem
23 it.representation += models
24 it.trace = trace
25 it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
26 ]
27 } else {
28 return createInconsistencyResult => [
29 it.problem = problem
30 it.representation += models
31 it.trace = trace
32 it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
33 ]
34 }
35 }
36 }
37
38 def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
39 createStatistics => [
40 it.transformationTime = transformationTime as int
41 for(solutionIndex : 0..<solution.aswers.size) {
42 val solutionTime = solution.aswers.get(solutionIndex).value
43 it.entries+= createIntStatisticEntry => [
44 it.name = '''Answer«solutionIndex»Time'''
45 it.value = solutionTime.intValue
46 ]
47 }
48 it.entries+= createIntStatisticEntry => [
49 it.name = "Alloy2KodKodTransformationTime"
50 it.value = solution.kodkodTime as int
51 ]
52 it.entries+= createIntStatisticEntry => [
53 it.name = "Alloy2KodKodTransformationTime"
54 it.value = solution.kodkodTime as int
55 ]
56 it.entries+= createStringStatisticEntry => [
57 it.name = "warnings"
58 it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
59 ]
60 ]
61 }
62
63 def sum(Iterable<Long> ints) {
64 ints.reduce[p1, p2|p1+p2]
65 }
66} 7}
8// val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
9//
10// public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) {
11// val models = vampireSolution.aswers.map[it.key].toList
12//
13// if(!monitoredAlloySolution.finishedBeforeTimeout) {
14// return createInsuficientResourcesResult => [
15// it.problem = problem
16// it.representation += models
17// it.trace = trace
18// it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
19// ]
20// } else {
21// if(models.last.satisfiable || requiredNumberOfSolution == -1) {
22// return createModelResult => [
23// it.problem = problem
24// it.representation += models
25// it.trace = trace
26// it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
27// ]
28// } else {
29// return createInconsistencyResult => [
30// it.problem = problem
31// it.representation += models
32// it.trace = trace
33// it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
34// ]
35// }
36// }
37// }
38//
39// def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
40// createStatistics => [
41// it.transformationTime = transformationTime as int
42// for(solutionIndex : 0..<solution.aswers.size) {
43// val solutionTime = solution.aswers.get(solutionIndex).value
44// it.entries+= createIntStatisticEntry => [
45// it.name = '''Answer«solutionIndex»Time'''
46// it.value = solutionTime.intValue
47// ]
48// }
49// it.entries+= createIntStatisticEntry => [
50// it.name = "Alloy2KodKodTransformationTime"
51// it.value = solution.kodkodTime as int
52// ]
53// it.entries+= createIntStatisticEntry => [
54// it.name = "Alloy2KodKodTransformationTime"
55// it.value = solution.kodkodTime as int
56// ]
57// it.entries+= createStringStatisticEntry => [
58// it.name = "warnings"
59// it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
60// ]
61// ]
62// }
63//
64// def sum(Iterable<Long> ints) {
65// ints.reduce[p1, p2|p1+p2]
66// }
67//}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-26 14:49:45 +0000