diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-08 03:00:08 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:10 -0400 |
commit | d0e4ffcc9dfc85367ccc73bf070404416081a477 (patch) | |
tree | 0db0134207f473f6a12d7c362512b008bd6449eb /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill | |
parent | VAMPIRE: Implement Vampire measurement code (diff) | |
download | VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.tar.gz VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.tar.zst VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.zip |
VAMPIRE: fix bug in transformation, further implement measurement code
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill')
6 files changed, 75 insertions, 46 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 98967181..fc8d3e99 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 | |||
@@ -6,6 +6,7 @@ class VampireSolverConfiguration extends LogicSolverConfiguration { | |||
6 | 6 | ||
7 | public var int contCycleLevel = 0 | 7 | public var int contCycleLevel = 0 |
8 | public var boolean uniquenessDuplicates = false | 8 | public var boolean uniquenessDuplicates = false |
9 | public var int iteration = -1 | ||
9 | //choose needed backend solver | 10 | //choose needed backend solver |
10 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J | 11 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J |
11 | } | 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 3b5cec0a..3281a196 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 | |||
@@ -46,6 +46,8 @@ class VampireSolver extends LogicReasoner { | |||
46 | val transformationStart = System.currentTimeMillis | 46 | val transformationStart = System.currentTimeMillis |
47 | // TODO | 47 | // TODO |
48 | val result = forwardMapper.transformProblem(problem, vampireConfig) | 48 | val result = forwardMapper.transformProblem(problem, vampireConfig) |
49 | val transformationTime = System.currentTimeMillis - transformationStart | ||
50 | |||
49 | val vampireProblem = result.output | 51 | val vampireProblem = result.output |
50 | val forwardTrace = result.trace | 52 | val forwardTrace = result.trace |
51 | 53 | ||
@@ -71,19 +73,17 @@ class VampireSolver extends LogicReasoner { | |||
71 | 73 | ||
72 | 74 | ||
73 | // Result as String | 75 | // Result as String |
74 | val transformationTime = System.currentTimeMillis - transformationStart | 76 | |
75 | // Finish: Logic -> Vampire mapping | 77 | // Finish: Logic -> Vampire mapping |
76 | 78 | ||
77 | // Start: Solving .tptp problem | 79 | // Start: Solving .tptp problem |
78 | val solverStart = System.currentTimeMillis | ||
79 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) | 80 | val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig) |
80 | val solvingTime = System.currentTimeMillis - solverStart | ||
81 | // Finish: Solving .tptp problem | 81 | // Finish: Solving .tptp problem |
82 | 82 | ||
83 | // Start: Vampire -> Logic mapping | 83 | // Start: Vampire -> Logic mapping |
84 | val backTransformationStart = System.currentTimeMillis | 84 | val backTransformationStart = System.currentTimeMillis |
85 | // Backwards Mapper | 85 | // Backwards Mapper |
86 | val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,solvingTime) | 86 | val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime) |
87 | 87 | ||
88 | val backTransformationTime = System.currentTimeMillis - backTransformationStart | 88 | val backTransformationTime = System.currentTimeMillis - backTransformationStart |
89 | // Finish: Vampire -> Logic Mapping | 89 | // Finish: Vampire -> Logic Mapping |
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 b617912d..60309f2d 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 | |||
@@ -79,14 +79,15 @@ class Logic2VampireLanguageMapper { | |||
79 | if (!problem.types.isEmpty) { | 79 | if (!problem.types.isEmpty) { |
80 | typeMapper.transformTypes(problem.types, problem.elements, this, trace) | 80 | typeMapper.transformTypes(problem.types, problem.elements, this, trace) |
81 | } | 81 | } |
82 | 82 | ||
83 | // RELATION MAPPER | 83 | // RELATION MAPPER |
84 | trace.relationDefinitions = problem.collectRelationDefinitions | 84 | trace.relationDefinitions = problem.collectRelationDefinitions |
85 | // println(problem.relations.filter[class == RelationDefinitionImpl]) | 85 | // println(problem.relations.filter[class == RelationDefinitionImpl]) |
86 | toTrace(problem.relations.filter[class == RelationDefinitionImpl], trace) | ||
86 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace, new Logic2VampireLanguageMapper)] | 87 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace, new Logic2VampireLanguageMapper)] |
87 | 88 | ||
88 | // CONTAINMENT MAPPER | 89 | // CONTAINMENT MAPPER |
89 | containmentMapper.transformContainment(config,problem.containmentHierarchies, trace) | 90 | containmentMapper.transformContainment(config, problem.containmentHierarchies, trace) |
90 | 91 | ||
91 | // SCOPE MAPPER | 92 | // SCOPE MAPPER |
92 | scopeMapper.transformScope(problem.types, config, trace) | 93 | scopeMapper.transformScope(problem.types, config, trace) |
@@ -107,6 +108,39 @@ class Logic2VampireLanguageMapper { | |||
107 | return new TracedOutput(specification, trace) | 108 | return new TracedOutput(specification, trace) |
108 | } | 109 | } |
109 | 110 | ||
111 | def toTrace(Iterable<Relation> relations, Logic2VampireLanguageMapperTrace trace) { | ||
112 | val List<VLSVariable> vars = newArrayList | ||
113 | for (rel : relations) { | ||
114 | //decide name | ||
115 | val nameArray = rel.name.split(" ") | ||
116 | var relNameVar = "" | ||
117 | if (nameArray.length == 3) { | ||
118 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) | ||
119 | } else { | ||
120 | relNameVar = rel.name | ||
121 | } | ||
122 | val relName = relNameVar | ||
123 | |||
124 | val relDef = rel as RelationDefinition | ||
125 | for (i : 0 ..< rel.parameters.length) { | ||
126 | |||
127 | val v = createVLSVariable => [ | ||
128 | it.name = support.toIDMultiple("V", i.toString) | ||
129 | ] | ||
130 | vars.add(v) | ||
131 | } | ||
132 | |||
133 | val relFunc = createVLSFunction => [ | ||
134 | it.constant = support.toIDMultiple("r", relName) | ||
135 | for (v : vars) { | ||
136 | it.terms += support.duplicate(v) | ||
137 | } | ||
138 | ] | ||
139 | trace.relDef2Predicate.put(relDef, relFunc) | ||
140 | trace.predicate2RelDef.put(relFunc, relDef) | ||
141 | } | ||
142 | } | ||
143 | |||
110 | // End of transformProblem | 144 | // End of transformProblem |
111 | // //////////// | 145 | // //////////// |
112 | // Type References | 146 | // Type References |
@@ -169,7 +203,6 @@ class Logic2VampireLanguageMapper { | |||
169 | // Map<Variable, VLSVariable> variables) { | 203 | // Map<Variable, VLSVariable> variables) { |
170 | // createVLSReal => [it.value = literal.value.toString()] | 204 | // createVLSReal => [it.value = literal.value.toString()] |
171 | // } | 205 | // } |
172 | |||
173 | def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace, | 206 | def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace, |
174 | Map<Variable, VLSVariable> variables) { | 207 | Map<Variable, VLSVariable> variables) { |
175 | createVLSUnaryNegation => [operand = not.operand.transformTerm(trace, variables)] | 208 | createVLSUnaryNegation => [operand = not.operand.transformTerm(trace, variables)] |
@@ -265,10 +298,10 @@ class Logic2VampireLanguageMapper { | |||
265 | def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, | 298 | def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, |
266 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | 299 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, |
267 | Map<Variable, VLSVariable> variables) { | 300 | Map<Variable, VLSVariable> variables) { |
268 | val name = referred.lookup(trace.definedElement2String) | 301 | val name = referred.lookup(trace.definedElement2String) |
269 | return createVLSConstant => [ | 302 | return createVLSConstant => [ |
270 | it.name = name | 303 | it.name = name |
271 | ] | 304 | ] |
272 | // typeMapper.transformReference(referred, trace) | 305 | // typeMapper.transformReference(referred, trace) |
273 | } | 306 | } |
274 | 307 | ||
@@ -390,12 +423,11 @@ class Logic2VampireLanguageMapper { | |||
390 | // } | 423 | // } |
391 | return createVLSFunction => [ | 424 | return createVLSFunction => [ |
392 | if (relation.class == RelationDeclarationImpl) { | 425 | if (relation.class == RelationDeclarationImpl) { |
393 | it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant | 426 | it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant |
394 | } | 427 | } else { |
395 | else { | ||
396 | it.constant = (relation as RelationDefinition).lookup(trace.relDef2Predicate).constant | 428 | it.constant = (relation as RelationDefinition).lookup(trace.relDef2Predicate).constant |
397 | } | 429 | } |
398 | 430 | ||
399 | it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] | 431 | it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] |
400 | ] | 432 | ] |
401 | } | 433 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend index 181c59ca..efedf6dc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend | |||
@@ -23,7 +23,8 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
23 | this.base = base | 23 | this.base = base |
24 | } | 24 | } |
25 | 25 | ||
26 | def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) { | 26 | def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace, |
27 | Logic2VampireLanguageMapper mapper) { | ||
27 | 28 | ||
28 | // 1. store all variables in support wrt their name | 29 | // 1. store all variables in support wrt their name |
29 | // 1.1 if variable has type, creating list of type declarations | 30 | // 1.1 if variable has type, creating list of type declarations |
@@ -42,19 +43,18 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
42 | 43 | ||
43 | } | 44 | } |
44 | 45 | ||
45 | //deciding name of relation | 46 | // deciding name of relation |
46 | val nameArray = r.name.split(" ") | 47 | val nameArray = r.name.split(" ") |
47 | var relNameVar = "" | 48 | var relNameVar = "" |
48 | if (nameArray.length == 3) { | 49 | if (nameArray.length == 3) { |
49 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) | 50 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) |
50 | } | 51 | } else { |
51 | else { | ||
52 | relNameVar = r.name | 52 | relNameVar = r.name |
53 | } | 53 | } |
54 | val relName = relNameVar | 54 | val relName = relNameVar |
55 | 55 | ||
56 | val comply = createVLSFofFormula=> [ | 56 | val comply = createVLSFofFormula => [ |
57 | 57 | ||
58 | it.name = support.toIDMultiple("compliance", relName) | 58 | it.name = support.toIDMultiple("compliance", relName) |
59 | it.fofRole = "axiom" | 59 | it.fofRole = "axiom" |
60 | it.fofFormula = createVLSUniversalQuantifier => [ | 60 | it.fofFormula = createVLSUniversalQuantifier => [ |
@@ -79,10 +79,10 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
79 | trace.specification.formulas += comply | 79 | trace.specification.formulas += comply |
80 | } | 80 | } |
81 | 81 | ||
82 | def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) { | 82 | def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace, |
83 | 83 | Logic2VampireLanguageMapper mapper) { | |
84 | // println("XXXXXXXXXXXXXXXXX") | ||
85 | 84 | ||
85 | // println("XXXXXXXXXXXXXXXXX") | ||
86 | // 1. store all variables in support wrt their name | 86 | // 1. store all variables in support wrt their name |
87 | // 1.1 if variable has type, creating list of type declarations | 87 | // 1.1 if variable has type, creating list of type declarations |
88 | val Map<Variable, VLSVariable> relVar2VLS = new HashMap | 88 | val Map<Variable, VLSVariable> relVar2VLS = new HashMap |
@@ -102,34 +102,30 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
102 | 102 | ||
103 | } | 103 | } |
104 | 104 | ||
105 | //deciding name of relation | 105 | // deciding name of relation |
106 | val nameArray = r.name.split(" ") | 106 | val nameArray = r.name.split(" ") |
107 | var relNameVar = "" | 107 | var relNameVar = "" |
108 | if (nameArray.length == 3) { | 108 | if (nameArray.length == 3) { |
109 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) | 109 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) |
110 | } | 110 | } else { |
111 | else { | ||
112 | relNameVar = r.name | 111 | relNameVar = r.name |
113 | } | 112 | } |
114 | val relName = relNameVar | 113 | val relName = relNameVar |
115 | 114 | ||
116 | //define logic for pattern | 115 | // define logic for pattern |
117 | // val map = new HashMap | 116 | // val map = new HashMap |
118 | // map.put(r.variables.get(0), createVLSVariable) | 117 | // map.put(r.variables.get(0), createVLSVariable) |
119 | val definition = mapper.transformTerm(r.value, trace, relVar2VLS) | 118 | val definition = mapper.transformTerm(r.value, trace, relVar2VLS) |
120 | 119 | ||
121 | 120 | // get entire contents of and | |
122 | |||
123 | |||
124 | //get entire contents of and | ||
125 | val compliance = support.unfoldAnd(relVar2TypeDecComply) | 121 | val compliance = support.unfoldAnd(relVar2TypeDecComply) |
126 | val compDefn = createVLSAnd=> [ | 122 | val compDefn = createVLSAnd => [ |
127 | it.left = compliance | 123 | it.left = compliance |
128 | it.right = definition | 124 | it.right = definition |
129 | ] | 125 | ] |
130 | 126 | ||
131 | val relDef = createVLSFofFormula=> [ | 127 | val relDef = createVLSFofFormula => [ |
132 | 128 | ||
133 | it.name = support.toID(relName) | 129 | it.name = support.toID(relName) |
134 | it.fofRole = "axiom" | 130 | it.fofRole = "axiom" |
135 | it.fofFormula = createVLSUniversalQuantifier => [ | 131 | it.fofFormula = createVLSUniversalQuantifier => [ |
@@ -143,14 +139,13 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
143 | it.terms += support.duplicate(v) | 139 | it.terms += support.duplicate(v) |
144 | } | 140 | } |
145 | ] | 141 | ] |
146 | trace.relDef2Predicate.put(r, rel) | 142 | // trace.relDef2Predicate.put(r, rel) |
147 | trace.predicate2RelDef.put(rel, r) | 143 | // trace.predicate2RelDef.put(rel, r) |
148 | it.left = support.duplicate(rel) | 144 | it.left = support.duplicate(rel) |
149 | it.right = compDefn | 145 | it.right = compDefn |
150 | ] | 146 | ] |
151 | ] | 147 | ] |
152 | ] | 148 | ] |
153 | |||
154 | trace.specification.formulas += relDef | 149 | trace.specification.formulas += relDef |
155 | 150 | ||
156 | } | 151 | } |
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 489bf423..e136d1c6 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 | |||
@@ -8,7 +8,7 @@ class Vampire2LogicMapper { | |||
8 | 8 | ||
9 | // | 9 | // |
10 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, | 10 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, |
11 | MonitoredVampireSolution monitoredVampireSolution, Logic2VampireLanguageMapperTrace trace, | 11 | MonitoredVampireSolution monitoredVampireSolution, Logic2VampireLanguageMapperTrace trace, |
12 | long transformationTime) { | 12 | long transformationTime) { |
13 | 13 | ||
14 | // ModelRsult implements LogicResult | 14 | // ModelRsult implements LogicResult |
@@ -22,7 +22,8 @@ class Vampire2LogicMapper { | |||
22 | 22 | ||
23 | def transformStatistics(MonitoredVampireSolution solution, long transformationTime) { | 23 | def transformStatistics(MonitoredVampireSolution solution, long transformationTime) { |
24 | return createStatistics => [ | 24 | return createStatistics => [ |
25 | it.transformationTime = solution.solverTime as int | 25 | it.solverTime = solution.solverTime as int |
26 | it.transformationTime = transformationTime as int | ||
26 | ] | 27 | ] |
27 | // createStatistics => [ | 28 | // createStatistics => [ |
28 | // it.transformationTime = transformationTime as int | 29 | // it.transformationTime = transformationTime as int |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend index 74532ee5..c5cfb1c7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend | |||
@@ -44,7 +44,7 @@ class VampireHandler { | |||
44 | val VAMPNAME = "vampire.exe" | 44 | val VAMPNAME = "vampire.exe" |
45 | val TEMPNAME = "TEMP.tptp" | 45 | val TEMPNAME = "TEMP.tptp" |
46 | val OPTION = " --mode casc_sat -t 300 " | 46 | val OPTION = " --mode casc_sat -t 300 " |
47 | val SOLNNAME = "_solution" + configuration.typeScopes.maxNewElements + ".tptp" | 47 | val SOLNNAME = "solution" + configuration.typeScopes.maxNewElements +"_" + configuration.iteration + ".tptp" |
48 | val PATH = "C:/cygwin64/bin" | 48 | val PATH = "C:/cygwin64/bin" |
49 | 49 | ||
50 | val wsURI = workspace.workspaceURI | 50 | val wsURI = workspace.workspaceURI |