1 files changed, 167 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend
new file mode 100644
index 00000000..fb0739ab
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend
@@ -0,0 +1,167 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.smt.reasoner.builder.SmtModelQueryEngine
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration
+import org.eclipse.xtend.lib.annotations.Accessors
+import org.eclipse.xtend.lib.annotations.Data
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
+@Data
+class ValueType {
+        TypeDescriptor descriptor
+        Object value
+}
+class SmtModelInterpretation implements LogicModelInterpretation {
+        //val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        @Accessors(PUBLIC_GETTER) val SmtModelQueryEngine queryEngine;
+        
+        // Trace info
+        val Logic2SmtMapperTrace newTrace;
+        val Logic2SMT_TypeMapperInterpretation typeInterpretation
+        
+        /**
+         * Creates a model builder which queries a logic structure.
+         * @param document The whole SMT2 document.
+         * @param trace The trace of the [Logic problem -> SMT problem] mapping 
+         */
+        new(LogicProblem problem, SMTDocument document, Logic2SmtMapper forwardMapper, Logic2SmtMapperTrace forwardTrace) {
+                //document.input.typeDeclarations.forEach[typeNames.put(it.name,it)]
+                
+                this.queryEngine = new SmtModelQueryEngine(document)
+                this.newTrace = initialiseNewTrace(document,forwardTrace)
+                this.typeInterpretation = forwardMapper.typeMapper.getTypeInterpretation(problem,document,this,newTrace)
+        }
+        
+        /**
+         * Creates a new trace from the logic model to the new smt file by using the old trace.
+         */
+        def protected Logic2SmtMapperTrace initialiseNewTrace(SMTDocument document, Logic2SmtMapperTrace oldTrace) {
+                val i = document.input
+                
+                val res = new Logic2SmtMapperTrace => [ typeMapperTrace = oldTrace.typeMapperTrace.copy(i) ]
+                
+                for(entry : oldTrace.relationUnfolding.entrySet) {
+                        val rel = entry.key
+                        val descriptors = entry.value.map[old | 
+                                new Descriptor<Relation>(
+                                        old.parameterTypes.map[copyTypeDescriptor(i)],
+                                        old.relation)
+                        ]
+                        res.relationUnfolding.put(rel,descriptors)
+                }
+                
+                for(entry : oldTrace.relationMap.entrySet) {
+                        val desc = new Descriptor<Relation>(
+                                        entry.key.parameterTypes.map[copyTypeDescriptor(i)],
+                                        entry.key.relation)
+                        val fun = i.functionDeclarations.filter[it.name == entry.value.name].head
+                        res.relationMap.put(desc,fun)
+                }
+                
+                return res
+        }
+        
+        def private copyTypeDescriptor(TypeDescriptor original, SMTInput i) {
+                if(original.complexType == null) return original
+                else {
+                        val newType = i.typeDeclarations.filter[it.name == original.complexType.name].head
+                        new TypeDescriptor(newType)
+                }
+        }
+        
+        /*def protected initialiseTypes(SMTDocument document) {
+                val model = document.output.getModelResult as SMTModelResult
+                val smtUndefinedType2LogicType = this.newTrace.typeDeclarationMap.bijectiveInverse
+                
+                for(cardinalityConstraint : model.typeDefinitions) {
+                        val targetType = (cardinalityConstraint.type as SMTComplexTypeReference).referred as SMTSetTypeDeclaration
+                        val List<DefinedElement> elementCollection = new LinkedList
+                        for(element : cardinalityConstraint.elements.map[symbolicReference]) {
+                                if(element instanceof SMTFunctionDeclaration) {
+                                        val definedElementRepresentation = createDefinedElement => [name += element.name.split("!")]
+                                        newElement2Constants.put(definedElementRepresentation,element)
+                                        newConstants2Elements.put(element,definedElementRepresentation)
+                                } else{
+                                        throw new UnsupportedOperationException(
+                                                "Unresolvable reference in cardinality constraint: " + element.class.name + ": " + element.name)        
+                                }
+                        }
+                        undefinedTypeDefinitions.put(targetType.lookup(smtUndefinedType2LogicType),elementCollection);
+                }
+        }*/
+        
+        def private dispatch ValueType logicLiteral2SmtLiteral(Integer literal) {
+                new ValueType(TypeDescriptor::numericTypeDescriptor_Instance, literal)
+        }
+        def private dispatch ValueType logicLiteral2SmtLiteral(Boolean literal) {
+                new ValueType(TypeDescriptor::logicTypeDescriptor_Instance, literal)
+        }
+        def private dispatch ValueType logicLiteral2SmtLiteral(DefinedElement literal) {
+                this.typeInterpretation.logicElement2Smt(literal)
+        }
+//      def private dispatch Object smt2Literal2LogicLiteral(Integer literal) { literal }
+//      def private dispatch Object smt2Literal2LogicLiteral(Boolean literal) { literal }
+//      def private dispatch Object smt2Literal2LogicLiteral(SMTSymbolicDeclaration literal) { 
+//              this.typeInterpretation.smtElement2Logic(literal)
+//      }
+        override getElements(Type type) {
+                return this.typeInterpretation.getElements(type)
+        }
+        
+        override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
+                /*queryEngine.resolveFunctionDeclaration(
+                        function.lookup(newTrace.functionDeclarationMap),
+                        parameterSubstitution.map[logicLiteral2SmtLiteral]
+                ).smt2Literal2LogicLiteral*/
+                throw new UnsupportedOperationException
+        }
+        
+        override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
+                val transformedParameters = parameterSubstitution.map[logicLiteral2SmtLiteral]
+                
+                val smtFunction = new Descriptor<Relation>(
+                        transformedParameters.map[descriptor],
+                        relation)
+                        .lookup(newTrace.relationMap)
+                        
+                val result = queryEngine.resolveFunctionDeclaration(
+                        smtFunction as SMTFunctionDeclaration,
+                        transformedParameters.map[value]
+                ) as Boolean
+                
+                return result
+        }
+        
+        override getInterpretation(ConstantDeclaration constant) {
+                /*queryEngine.resolveFunctionDeclaration(
+                        constant.lookup(newTrace.constantDeclarationMap),
+                        Collections.EMPTY_LIST
+                ).smt2Literal2LogicLiteral*/
+                throw new UnsupportedOperationException
+        }
+        
+        override getMaximalInteger() {
+                100
+                //throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+        
+        override getMinimalInteger() {
+                -100
+                //throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+}
+\ No newline at end of file

diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend new file mode 100644 index 00000000..fb0739ab --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend
@@ -0,0 +1,167 @@
	1	package hu.bme.mit.inf.dslreasoner.smt.reasoner
	2
	3	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
	4	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
	5	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
	6	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
	7	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
	8	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
	9	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
	10	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
	11	import hu.bme.mit.inf.dslreasoner.smt.reasoner.builder.SmtModelQueryEngine
	12	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
	13	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
	14	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration
	15	import org.eclipse.xtend.lib.annotations.Accessors
	16	import org.eclipse.xtend.lib.annotations.Data
	17
	18	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
	19	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration
	20
	21	@Data
	22	class ValueType {
	23	TypeDescriptor descriptor
	24	Object value
	25	}
	26
	27	class SmtModelInterpretation implements LogicModelInterpretation {
	28	//val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
	29	@Accessors(PUBLIC_GETTER) val SmtModelQueryEngine queryEngine;
	30
	31	// Trace info
	32	val Logic2SmtMapperTrace newTrace;
	33	val Logic2SMT_TypeMapperInterpretation typeInterpretation
	34
	35	/**
	36	* Creates a model builder which queries a logic structure.
	37	* @param document The whole SMT2 document.
	38	* @param trace The trace of the [Logic problem -> SMT problem] mapping
	39	*/
	40	new(LogicProblem problem, SMTDocument document, Logic2SmtMapper forwardMapper, Logic2SmtMapperTrace forwardTrace) {
	41	//document.input.typeDeclarations.forEach[typeNames.put(it.name,it)]
	42
	43	this.queryEngine = new SmtModelQueryEngine(document)
	44	this.newTrace = initialiseNewTrace(document,forwardTrace)
	45	this.typeInterpretation = forwardMapper.typeMapper.getTypeInterpretation(problem,document,this,newTrace)
	46	}
	47
	48	/**
	49	* Creates a new trace from the logic model to the new smt file by using the old trace.
	50	*/
	51	def protected Logic2SmtMapperTrace initialiseNewTrace(SMTDocument document, Logic2SmtMapperTrace oldTrace) {
	52	val i = document.input
	53
	54	val res = new Logic2SmtMapperTrace => [ typeMapperTrace = oldTrace.typeMapperTrace.copy(i) ]
	55
	56	for(entry : oldTrace.relationUnfolding.entrySet) {
	57	val rel = entry.key
	58	val descriptors = entry.value.map[old \|
	59	new Descriptor<Relation>(
	60	old.parameterTypes.map[copyTypeDescriptor(i)],
	61	old.relation)
	62	]
	63	res.relationUnfolding.put(rel,descriptors)
	64	}
	65
	66	for(entry : oldTrace.relationMap.entrySet) {
	67	val desc = new Descriptor<Relation>(
	68	entry.key.parameterTypes.map[copyTypeDescriptor(i)],
	69	entry.key.relation)
	70	val fun = i.functionDeclarations.filter[it.name == entry.value.name].head
	71	res.relationMap.put(desc,fun)
	72	}
	73
	74	return res
	75	}
	76
	77	def private copyTypeDescriptor(TypeDescriptor original, SMTInput i) {
	78	if(original.complexType == null) return original
	79	else {
	80	val newType = i.typeDeclarations.filter[it.name == original.complexType.name].head
	81	new TypeDescriptor(newType)
	82	}
	83	}
	84
	85	/*def protected initialiseTypes(SMTDocument document) {
	86	val model = document.output.getModelResult as SMTModelResult
	87	val smtUndefinedType2LogicType = this.newTrace.typeDeclarationMap.bijectiveInverse
	88
	89	for(cardinalityConstraint : model.typeDefinitions) {
	90	val targetType = (cardinalityConstraint.type as SMTComplexTypeReference).referred as SMTSetTypeDeclaration
	91	val List<DefinedElement> elementCollection = new LinkedList
	92	for(element : cardinalityConstraint.elements.map[symbolicReference]) {
	93	if(element instanceof SMTFunctionDeclaration) {
	94	val definedElementRepresentation = createDefinedElement => [name += element.name.split("!")]
	95	newElement2Constants.put(definedElementRepresentation,element)
	96	newConstants2Elements.put(element,definedElementRepresentation)
	97	} else{
	98	throw new UnsupportedOperationException(
	99	"Unresolvable reference in cardinality constraint: " + element.class.name + ": " + element.name)
	100	}
	101	}
	102	undefinedTypeDefinitions.put(targetType.lookup(smtUndefinedType2LogicType),elementCollection);
	103	}
	104	}*/
	105
	106	def private dispatch ValueType logicLiteral2SmtLiteral(Integer literal) {
	107	new ValueType(TypeDescriptor::numericTypeDescriptor_Instance, literal)
	108	}
	109	def private dispatch ValueType logicLiteral2SmtLiteral(Boolean literal) {
	110	new ValueType(TypeDescriptor::logicTypeDescriptor_Instance, literal)
	111	}
	112	def private dispatch ValueType logicLiteral2SmtLiteral(DefinedElement literal) {
	113	this.typeInterpretation.logicElement2Smt(literal)
	114	}
	115
	116	// def private dispatch Object smt2Literal2LogicLiteral(Integer literal) { literal }
	117	// def private dispatch Object smt2Literal2LogicLiteral(Boolean literal) { literal }
	118	// def private dispatch Object smt2Literal2LogicLiteral(SMTSymbolicDeclaration literal) {
	119	// this.typeInterpretation.smtElement2Logic(literal)
	120	// }
	121
	122	override getElements(Type type) {
	123	return this.typeInterpretation.getElements(type)
	124	}
	125
	126	override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
	127	/*queryEngine.resolveFunctionDeclaration(
	128	function.lookup(newTrace.functionDeclarationMap),
	129	parameterSubstitution.map[logicLiteral2SmtLiteral]
	130	).smt2Literal2LogicLiteral*/
	131	throw new UnsupportedOperationException
	132	}
	133
	134	override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
	135	val transformedParameters = parameterSubstitution.map[logicLiteral2SmtLiteral]
	136
	137	val smtFunction = new Descriptor<Relation>(
	138	transformedParameters.map[descriptor],
	139	relation)
	140	.lookup(newTrace.relationMap)
	141
	142	val result = queryEngine.resolveFunctionDeclaration(
	143	smtFunction as SMTFunctionDeclaration,
	144	transformedParameters.map[value]
	145	) as Boolean
	146
	147	return result
	148	}
	149
	150	override getInterpretation(ConstantDeclaration constant) {
	151	/*queryEngine.resolveFunctionDeclaration(
	152	constant.lookup(newTrace.constantDeclarationMap),
	153	Collections.EMPTY_LIST
	154	).smt2Literal2LogicLiteral*/
	155	throw new UnsupportedOperationException
	156	}
	157
	158	override getMaximalInteger() {
	159	100
	160	//throw new UnsupportedOperationException("TODO: auto-generated method stub")
	161	}
	162
	163	override getMinimalInteger() {
	164	-100
	165	//throw new UnsupportedOperationException("TODO: auto-generated method stub")
	166	}
	167	} \ No newline at end of file