Alloy mapping of integer scopes

2 files changed, 20 insertions, 6 deletions

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
index d00291e0..53674ca3 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
@@ -286,10 +286,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{
         override getInterpretation(ConstantDeclaration constant) {

                 constant.lookup(this.constant2Value)

         }

-        

-        override getMinimalInteger() { this.minInt }

-        override getMaximalInteger() { this.maxInt }

-        

+

         // Alloy term -> logic term

         def private atomLabel2Term(String label) {

                 if(label.number) return Integer.parseInt(label)

@@ -306,6 +303,19 @@ class AlloyModelInterpretation implements LogicModelInterpretation{
                         return false

                 }

         }

+        

+        override getAllIntegersInStructure() {

+                throw new UnsupportedOperationException("TODO: auto-generated method stub")

+        }

+        

+        override getAllRealsInStructure() {

+                throw new UnsupportedOperationException("TODO: auto-generated method stub")

+        }

+        

+        override getAllStringsInStructure() {

+                throw new UnsupportedOperationException("TODO: auto-generated method stub")

+        }

+        

 }

 

 /**

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
index 65fdcfdf..e5c443f6 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
@@ -279,10 +279,14 @@ class Logic2AlloyLanguageMapper {
                                 it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) 

                                 it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)

                         ]

-                        if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException(

+                        if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException(

                                 '''An integer scope have to be specified for Alloy!''')

                         it.typeScopes += createALSIntScope => [

-                                number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxIntScope)

+                                val knownIntegerMax = config.typeScopes.knownIntegers.max

+                                val knownIntegerMin = config.typeScopes.knownIntegers.min

+                                val needNewPlaces =  Math.max(knownIntegerMax - knownIntegerMin - config.typeScopes.maxNewIntegers,0)

+                                val maxAbsoluteValue = Math.max(Math.abs(knownIntegerMax)+needNewPlaces+1/2, Math.abs(knownIntegerMin)+needNewPlaces/2)

+                                number = Integer.SIZE-Integer.numberOfLeadingZeros(maxAbsoluteValue)

                         ]

 //                      for(definedScope : config.typeScopes.allDefinedScope) {

 //                              it.typeScopes += createALSSigScope => [