diff options
author | 2019-08-27 18:45:22 +0200 | |
---|---|---|
committer | 2019-08-27 18:45:22 +0200 | |
commit | 79eb47516a27ebe1801fb8e9087f3ee1b4d123d1 (patch) | |
tree | 649ee654f741337020dc1a239a3981f0c778e3d5 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner | |
parent | https://github.com/kris7t graph width calculation -> (diff) | |
download | VIATRA-Generator-79eb47516a27ebe1801fb8e9087f3ee1b4d123d1.tar.gz VIATRA-Generator-79eb47516a27ebe1801fb8e9087f3ee1b4d123d1.tar.zst VIATRA-Generator-79eb47516a27ebe1801fb8e9087f3ee1b4d123d1.zip |
Alloy RunCommand int scope fix candidate
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend | 123 |
1 files changed, 86 insertions, 37 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend index 3e96f7f4..cbd56abb 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend | |||
@@ -3,6 +3,8 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | 3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration |
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | 4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument |
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt | 5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt |
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | 8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm |
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | 9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
@@ -13,15 +15,15 @@ import java.util.List | |||
13 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 15 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
14 | 16 | ||
15 | class RunCommandMapper { | 17 | class RunCommandMapper { |
16 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 18 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
17 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | 19 | val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; |
18 | private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; | 20 | val Logic2AlloyLanguageMapper_TypeMapper typeMapper; |
19 | 21 | ||
20 | public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { | 22 | new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { |
21 | this.typeMapper = typeMapper | 23 | this.typeMapper = typeMapper |
22 | } | 24 | } |
23 | 25 | ||
24 | def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) | 26 | def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) |
25 | { | 27 | { |
26 | //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size | 28 | //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size |
27 | 29 | ||
@@ -65,41 +67,88 @@ class RunCommandMapper { | |||
65 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) | 67 | it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) |
66 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) | 68 | it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) |
67 | ] | 69 | ] |
68 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { | 70 | setIntegerScope(specification,config,it) |
69 | val integersUsed = specification.eAllContents.filter(ALSInt) | 71 | setStringScope(specification,config,it) |
70 | if(integersUsed.empty) { | 72 | ] |
71 | // If no integer scope is defined, but the problem has no integers | 73 | } |
72 | // => scope can be empty | 74 | |
73 | it.typeScopes+= createALSIntScope => [ | 75 | protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) { |
74 | it.number = 0 | 76 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { |
75 | ] | 77 | throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') |
76 | } else { | 78 | } else { |
77 | // If no integer scope is defined, and the problem has integers | 79 | if(config.typeScopes.maxNewStrings == 0) { |
78 | // => error | 80 | it.typeScopes += createALSStringScope => [it.number = 0] |
79 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') | ||
80 | } | ||
81 | } else { | 81 | } else { |
82 | it.typeScopes += createALSIntScope => [ | 82 | throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''') |
83 | if(config.typeScopes.knownIntegers.empty) { | ||
84 | number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) | ||
85 | } else { | ||
86 | var scope = Math.max( | ||
87 | Math.abs(config.typeScopes.knownIntegers.max), | ||
88 | Math.abs(config.typeScopes.knownIntegers.min)) | ||
89 | if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
90 | scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
91 | } | ||
92 | number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 | ||
93 | } | ||
94 | ] | ||
95 | } | 83 | } |
96 | if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { | 84 | } |
97 | throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') | 85 | } |
86 | |||
87 | protected def setIntegerScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand command) { | ||
88 | //AlloySolverConfiguration config, ALSRunCommand it | ||
89 | |||
90 | // If the scope is unlimited ... | ||
91 | if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { | ||
92 | val integersUsed = specification.eAllContents.filter(ALSInt) | ||
93 | if(integersUsed.empty) { | ||
94 | // ... but the problem has no integers => scope can be empty | ||
95 | command.typeScopes+= createALSIntScope => [ it.number = 0 ] | ||
98 | } else { | 96 | } else { |
99 | if(config.typeScopes.maxNewStrings != 0) { | 97 | // If no integer scope is defined, and the problem has integers => error |
100 | it.typeScopes += createALSStringScope => [it.number = 0] | 98 | throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') |
101 | } | ||
102 | } | 99 | } |
103 | ] | 100 | } else { |
101 | // If the scope is limited, collect the integers in the problem and the scope,... | ||
102 | val maxIntScope = config.typeScopes.maxNewIntegers | ||
103 | val minIntScope = config.typeScopes.minNewIntegers | ||
104 | val knownIntegers = config.typeScopes.knownIntegers | ||
105 | val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value] | ||
106 | // And select the range of integers | ||
107 | val min = #[minIntScope,knownIntegers.min,integersInProblem.min].min | ||
108 | val max = #[maxIntScope,knownIntegers.max,integersInProblem.max].max | ||
109 | //val abs = Math.max(Math.abs(min),Math.abs(max)) | ||
110 | |||
111 | |||
112 | command.typeScopes += createALSIntScope => [ | ||
113 | it.number = toBits(min, max) | ||
114 | ] | ||
115 | } | ||
116 | |||
117 | // if(config.typeScopes.knownIntegers.empty) { | ||
118 | // return Integer.SIZE-Integer.numberOfLeadingZeros((config.typeScopes.maxNewIntegers+1)/2) | ||
119 | // } else { | ||
120 | // var scope = Math.max( | ||
121 | // Math.abs(config.typeScopes.knownIntegers.max), | ||
122 | // Math.abs(config.typeScopes.knownIntegers.min)) | ||
123 | // if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { | ||
124 | // scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 | ||
125 | // } | ||
126 | // return Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 | ||
127 | // } | ||
128 | } | ||
129 | |||
130 | private static def toBits(int min, int max) { | ||
131 | // 4 Int = {-8, ..., 7} | ||
132 | // x Int = {- (2^(x-1)) , ... , 2^(x-1)-1} | ||
133 | var int bits = 1 | ||
134 | // range = 2^(x-1) | ||
135 | var int range = 1 | ||
136 | while((!(-range <= min)) || (!(max <= range-1))) { | ||
137 | bits++ | ||
138 | range*=2 | ||
139 | } | ||
140 | return bits | ||
104 | } | 141 | } |
142 | // | ||
143 | // def static void main(String[] args) { | ||
144 | // println('''0,0->«toBits(0,0)»''') | ||
145 | // println('''1,1->«toBits(1,1)»''') | ||
146 | // println('''-1,-1->«toBits(-1,-1)»''') | ||
147 | // println('''5,6->«toBits(5,6)»''') | ||
148 | // println('''0,6->«toBits(0,6)»''') | ||
149 | // println('''-10,0->«toBits(-10,0)»''') | ||
150 | // println('''-8,7->«toBits(-8,7)»''') | ||
151 | // println('''-100,100->«toBits(-100,100)»''') | ||
152 | // println('''-300,300->«toBits(-300,300)»''') | ||
153 | // } | ||
105 | } \ No newline at end of file | 154 | } \ No newline at end of file |