diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder')
2 files changed, 7 insertions, 4 deletions
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 index df3cfd82..39862c65 100644 --- 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 | |||
@@ -25,8 +25,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
25 | 25 | ||
26 | def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, | 26 | def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, |
27 | Logic2VampireLanguageMapperTrace trace) { | 27 | Logic2VampireLanguageMapperTrace trace) { |
28 | val ABSOLUTE_MIN = 0 | 28 | |
29 | val ABSOLUTE_MAX = Integer.MAX_VALUE | ||
30 | 29 | ||
31 | // TODO HANDLE ERRORS RELATED TO MAX > MIN | 30 | // TODO HANDLE ERRORS RELATED TO MAX > MIN |
32 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS | 31 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS |
@@ -40,6 +39,8 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
40 | // Number of defined non-abstract elements that are not enum elements | 39 | // Number of defined non-abstract elements that are not enum elements |
41 | // Equals the number of elements in te initial model | 40 | // Equals the number of elements in te initial model |
42 | var elemsInIM = trace.definedElement2String.size | 41 | var elemsInIM = trace.definedElement2String.size |
42 | val ABSOLUTE_MIN = 0 | ||
43 | val ABSOLUTE_MAX = -1-elemsInIM | ||
43 | // var elemsInIM = 0 | 44 | // var elemsInIM = 0 |
44 | // | 45 | // |
45 | // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { | 46 | // for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) { |
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 c1eb3382..47eae807 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 | |||
@@ -52,8 +52,10 @@ class VampireHandler { | |||
52 | 52 | ||
53 | val CMD = "cmd /c " | 53 | val CMD = "cmd /c " |
54 | val TEMPNAME = "TEMP.tptp" | 54 | val TEMPNAME = "TEMP.tptp" |
55 | val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + | 55 | // val SOLNNAME = "solution" + configuration.solver.toString + "_" + configuration.typeScopes.maxNewElements + |
56 | "_" + configuration.iteration + ".tptp" | 56 | // "_" + configuration.iteration + ".tptp" |
57 | val SOLNNAME = "solution" + "_" + configuration.typeScopes.maxNewElements + "_" + configuration.iteration + | ||
58 | ".tptp" | ||
57 | val PATH = "C:/cygwin64/bin" | 59 | val PATH = "C:/cygwin64/bin" |
58 | 60 | ||
59 | val wsURI = workspace.workspaceURI | 61 | val wsURI = workspace.workspaceURI |