Alloy RunCommand int scope fix candidate

author: Oszkar Semerath <semerath@mit.bme.hu> 2019-08-27 18:45:22 +0200
committer: Oszkar Semerath <semerath@mit.bme.hu> 2019-08-27 18:45:22 +0200
commit: 79eb47516a27ebe1801fb8e9087f3ee1b4d123d1 (patch)
tree: 649ee654f741337020dc1a239a3981f0c778e3d5
parent: https://github.com/kris7t graph width calculation -> (diff)
download: VIATRA-Generator-79eb47516a27ebe1801fb8e9087f3ee1b4d123d1.tar.gz
VIATRA-Generator-79eb47516a27ebe1801fb8e9087f3ee1b4d123d1.tar.zst
VIATRA-Generator-79eb47516a27ebe1801fb8e9087f3ee1b4d123d1.zip
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
 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand
 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
 import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
@@ -13,15 +15,15 @@ import java.util.List
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 class RunCommandMapper {
-        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
-        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
-        private val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
+        val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
        
-        public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
+        new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
                this.typeMapper = typeMapper
        }
        
-        def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config)
+        def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config)
        {
                //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size
                
@@ -65,41 +67,88 @@ class RunCommandMapper {
                                it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) 
                                it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
                        ]
-                        if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) {
+                        setIntegerScope(specification,config,it)
-                                val integersUsed = specification.eAllContents.filter(ALSInt)
+                        setStringScope(specification,config,it)
-                                if(integersUsed.empty) {
+                ]
-                                        // If no integer scope is defined, but the problem has no integers
+        }
-                                        // => scope can be empty
+        
-                                        it.typeScopes+= createALSIntScope => [
+        protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) {
-                                                it.number = 0
+                if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) {
-                                        ]
+                        throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')
-                                } else {
+                } else {
-                                        // If no integer scope is defined, and the problem has integers
+                        if(config.typeScopes.maxNewStrings == 0) {
-                                        // => error
+                                it.typeScopes += createALSStringScope => [it.number = 0]
-                                        throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''')
-                                }
                        } else {
-                                it.typeScopes += createALSIntScope => [
+                                throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')
-                                        if(config.typeScopes.knownIntegers.empty) {
-                                                number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2)
-                                        } else {
-                                                var scope = Math.max(
-                                                        Math.abs(config.typeScopes.knownIntegers.max),
-                                                        Math.abs(config.typeScopes.knownIntegers.min))
-                                                if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) {
-                                                        scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2
-                                                }
-                                                number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1
-                                        }
-                                ]
                        }
-                        if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) {
+                }
-                                throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''')
+        }
+        
+        protected def setIntegerScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand command) {
+                //AlloySolverConfiguration config, ALSRunCommand it
+                
+                // If the scope is unlimited ...
+                if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) {
+                        val integersUsed = specification.eAllContents.filter(ALSInt)
+                        if(integersUsed.empty) {
+                                // ... but the problem has no integers => scope can be empty
+                                command.typeScopes+= createALSIntScope => [ it.number = 0 ]
                        } else {
-                                if(config.typeScopes.maxNewStrings != 0) {
+                                // If no integer scope is defined, and the problem has integers => error
-                                        it.typeScopes += createALSStringScope => [it.number = 0]
+                                throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''')
-                                }
                        }
-                ]
+                } else {
+                        // If the scope is limited, collect the integers in the problem and the scope,...
+                        val maxIntScope = config.typeScopes.maxNewIntegers
+                        val minIntScope = config.typeScopes.minNewIntegers
+                        val knownIntegers = config.typeScopes.knownIntegers
+                        val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value]
+                        // And select the range of integers
+                        val min = #[minIntScope,knownIntegers.min,integersInProblem.min].min
+                        val max = #[maxIntScope,knownIntegers.max,integersInProblem.max].max
+                        //val abs = Math.max(Math.abs(min),Math.abs(max))
+                        
+                        
+                        command.typeScopes += createALSIntScope => [
+                                it.number = toBits(min, max)
+                        ]
+                }
+                
+//              if(config.typeScopes.knownIntegers.empty) {
+//                      return Integer.SIZE-Integer.numberOfLeadingZeros((config.typeScopes.maxNewIntegers+1)/2)
+//              } else {
+//                      var scope = Math.max(
+//                              Math.abs(config.typeScopes.knownIntegers.max),
+//                              Math.abs(config.typeScopes.knownIntegers.min))
+//                      if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) {
+//                              scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2
+//                      }
+//                      return Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1
+//              }
+        }
+        
+        private static def toBits(int min, int max) {
+                // 4 Int = {-8, ..., 7}
+                // x Int = {- (2^(x-1)) , ... , 2^(x-1)-1}
+                var int bits = 1
+                // range = 2^(x-1)
+                var int range = 1
+                while((!(-range <= min)) || (!(max <= range-1))) {
+                        bits++
+                        range*=2
+                }
+                return bits
        }
+//      
+//      def static void main(String[] args) {
+//              println('''0,0->«toBits(0,0)»''')
+//              println('''1,1->«toBits(1,1)»''')
+//              println('''-1,-1->«toBits(-1,-1)»''')
+//              println('''5,6->«toBits(5,6)»''')
+//              println('''0,6->«toBits(0,6)»''')
+//              println('''-10,0->«toBits(-10,0)»''')
+//              println('''-8,7->«toBits(-8,7)»''')
+//              println('''-100,100->«toBits(-100,100)»''')
+//              println('''-300,300->«toBits(-300,300)»''')
+//      }
 }
 \ No newline at end of file
author	Oszkar Semerath <semerath@mit.bme.hu>	2019-08-27 18:45:22 +0200
committer	Oszkar Semerath <semerath@mit.bme.hu>	2019-08-27 18:45:22 +0200
commit	79eb47516a27ebe1801fb8e9087f3ee1b4d123d1 (patch)
tree	649ee654f741337020dc1a239a3981f0c778e3d5
parent	https://github.com/kris7t graph width calculation -> (diff)
download	VIATRA-Generator-79eb47516a27ebe1801fb8e9087f3ee1b4d123d1.tar.gz VIATRA-Generator-79eb47516a27ebe1801fb8e9087f3ee1b4d123d1.tar.zst VIATRA-Generator-79eb47516a27ebe1801fb8e9087f3ee1b4d123d1.zip

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