From eccbce5001c00413805037bc416bb14e97390c3c Mon Sep 17 00:00:00 2001
From: OszkarSemerath <oszkar.semerath@gmail.com>
Date: Wed, 7 Nov 2018 12:19:47 +0100
Subject: Fixes in string scope and string interpretation for Alloy

---
 .../builder/AlloyModelInterpretation.xtend         | 47 +++++++++++++++-------
 1 file changed, 32 insertions(+), 15 deletions(-)

(limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend')

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 95216835..107aa001 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
@@ -19,6 +19,8 @@ import java.util.LinkedList
 import java.util.List
 import java.util.Map
 import java.util.Set
+import java.util.SortedSet
+import java.util.TreeSet
 
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 
@@ -34,6 +36,8 @@ class AlloyModelInterpretation implements LogicModelInterpretation{
 	
 	private var String logicBooleanTrue;
 	private var String logicBooleanFalse;
+	private SortedSet<Integer> integerAtoms = new TreeSet
+	private SortedSet<String> stringAtoms = new TreeSet
 		
 	private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap
 	private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap
@@ -42,8 +46,8 @@ class AlloyModelInterpretation implements LogicModelInterpretation{
 	private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value
 	private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value
 	
-	private val int minInt
-	private val int maxInt
+	//private val int minInt
+	//private val int maxInt
 	
 	public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) {
 		this.typeInterpretator = typeInterpretator
@@ -60,8 +64,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{
 				name2AlloyField.put(field.label,field)
 			}
 		}
-		
-		val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution.allAtoms)
+		val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution)
 		this.typeInterpretator.resolveUnknownAtoms(
 			unknownAtoms,
 			solution,
@@ -101,31 +104,46 @@ class AlloyModelInterpretation implements LogicModelInterpretation{
 		this.relation2Value = Union(hostedRelation2Value,globalRelation2Value)
 		
 		//Int limits
-		this.minInt = solution.min
-		this.maxInt = solution.max
+		//this.minInt = solution.min
+		//this.maxInt = solution.max
 		
 		//print(trace)
 	}
 	
-	def List<ExprVar> collectUnknownAndResolveKnownAtoms(Iterable<ExprVar> allAtoms) {
+	def List<ExprVar> collectUnknownAndResolveKnownAtoms(A4Solution solution) {
+		val Iterable<ExprVar> allAtoms = solution.allAtoms
 		val List<ExprVar> unknownAtoms = new LinkedList
 		
 		for(atom: allAtoms) {
 			val typeName = getName(atom.type)
 			val atomName = atom.name
-			//println(atom.toString + "  < -  " + typeName)
+			println(atom.toString + "  < -  " + typeName)
 			if(typeName == forwardTrace.logicLanguage.name) {
 				this.logicLanguage = atom
 			} else if(typeName == "Int" || typeName == "seq/Int") {
-				// do nothing, integers will be parsed from the string
+				val value = Integer.parseInt(atomName.join)
+				this.integerAtoms.add(value)
 			} else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) {
 				if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label }
 				else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label}
 				else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''')
+			} else if(typeName == "String") {
+				val value = parseString(atomName.join)
+				this.stringAtoms.add(value)
+			} else {
+				unknownAtoms += atom
 			}
-			else unknownAtoms += atom
 		}
-		
+		val integerSignature = solution.allReachableSigs.filter[it.label=="Int"].head
+		for(i : solution.eval(integerSignature)) {
+			val value = Integer.parseInt(i.atom(0))
+			this.integerAtoms.add(value)
+		}
+		val stringSignature = solution.allReachableSigs.filter[it.label=="String"].head
+		for(i : solution.eval(stringSignature)) {
+			val value = parseString(i.atom(0))
+			this.stringAtoms.add(value)
+		}
 		return unknownAtoms
 	}
 	
@@ -196,17 +214,16 @@ class AlloyModelInterpretation implements LogicModelInterpretation{
 	}
 	
 	override getAllIntegersInStructure() {
-		throw new UnsupportedOperationException("TODO: auto-generated method stub")
+		this.integerAtoms
 	}
 	
 	override getAllRealsInStructure() {
-		throw new UnsupportedOperationException("TODO: auto-generated method stub")
+		new TreeSet
 	}
 	
 	override getAllStringsInStructure() {
-		throw new UnsupportedOperationException("TODO: auto-generated method stub")
+		this.stringAtoms
 	}
-	
 }
 
 /**
-- 
cgit v1.2.3-70-g09d2