Migrating Additional projects

author: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
committer: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
commit: 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree: 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend
parent: Initial commit, migrating from SVN (diff)
download: VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
1 files changed, 183 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend
new file mode 100644
index 00000000..48952288
--- /dev/null
+++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend
@@ -0,0 +1,183 @@
+package hu.bme.mit.inf.dslreasoner.smt.reasoner
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
+import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
+import java.util.ArrayList
+import java.util.List
+import java.util.Map
+import org.eclipse.emf.ecore.EObject
+import org.eclipse.emf.ecore.util.EcoreUtil
+import org.eclipse.xtend.lib.annotations.Data
+import java.util.HashMap
+import java.util.LinkedList
+abstract class TransformedSubterm {
+        val static extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
+        def LogicSubterm expectLogic() 
+        def NumericSubterm expectNumber()
+        
+        def List<SubtermOption> getPossibleValues()
+        
+        public static def List<List<SubtermOption>> allCombinations(List<SubtermOption>... possibleValues) {
+                return allCombinations(possibleValues.toList)
+        }
+        public static def List<List<SubtermOption>> allCombinations(Iterable<List<SubtermOption>> possibleValues) {
+                if(possibleValues.size == 1) {
+                        return possibleValues.head.map[x|#[x.copy]]
+                } else {
+                        val head = possibleValues.head
+                        val tails = possibleValues.tail.allCombinations
+                        val res = new ArrayList(tails.size * head.size)
+                        for(headElement : head) {
+                                for(tail : tails) {
+                                        val combination = new ArrayList(tail.size+1)
+                                        combination.add(headElement)
+                                        combination.addAll(tail.map[copy])
+                                        res.add(combination)
+                                }
+                        }
+                        return res
+                }
+        }
+        
+        public static def resolveToLogic(List<SubtermOption> subterms, SMTTerm value) {
+                val allDefinitions = subterms.map[it.variables].flatten
+                val allPreconditions = subterms.map[it.preconditions].flatten
+                val preconditionedExpression = if(allPreconditions.empty) {
+                        value
+                } else {
+                        createSMTAnd => [it.operands += allPreconditions it.operands += value]
+                }
+                val quantifiedExpression = if(allDefinitions.empty) {
+                        preconditionedExpression
+                } else {
+                        createSMTForall => [
+                                it.quantifiedVariables += allDefinitions
+                                it.expression = preconditionedExpression]
+                }
+                return quantifiedExpression
+        }
+}
+@Data class SubtermOption {
+        List<SMTSortedVariable> variables
+        List<SMTTerm> preconditions
+        SMTTerm expression
+        TypeDescriptor type
+        
+        public new(
+                List<SMTSortedVariable> variables,
+                List<SMTTerm> preconditions,
+                SMTTerm expression,
+                TypeDescriptor type)
+        {
+                this.variables = variables
+                this.preconditions = preconditions
+                this.expression = expression
+                this.type = type
+        }
+        
+        public new(
+                List<SubtermOption> previousSubterms,
+                List<SMTSortedVariable> newVariables,
+                List<SMTTerm> newPreconditions,
+                SMTTerm newExpression,
+                TypeDescriptor newType)
+        {
+                val old2New = new HashMap
+                variables = new LinkedList
+                for(variable : previousSubterms.map[getVariables].flatten) {
+                        val newVariable = EcoreUtil.copy(variable)
+                        old2New.put(variable,newVariable)
+                        variables+=newVariable
+                }
+                
+                preconditions = new LinkedList
+                preconditions += previousSubterms.map[getPreconditions].flatten.map[x|EcoreUtil.copy(x)]
+                preconditions += newPreconditions.map[x|EcoreUtil.copy(x)]
+                preconditions.forEach[relinkAllVariableReference(old2New)]
+                
+                expression = EcoreUtil.copy(newExpression)
+                relinkAllVariableReference(expression,old2New)
+                
+                type = newType
+        }
+        
+        public def copy() {
+                val old2New = variables.toInvertedMap[EcoreUtil.copy(it)]
+                val newPreconditions = preconditions.map[EcoreUtil.copy(it)]
+                newPreconditions.forEach[it.relinkAllVariableReference(old2New)]
+                val newExpression = EcoreUtil.copy(expression)
+                return new SubtermOption(variables.map[old2New.get(it)],newPreconditions,newExpression,type)
+        }
+        
+        def private relinkAllVariableReference(EObject root,Map<SMTSortedVariable, SMTSortedVariable> map) {
+                if(root instanceof SMTSymbolicValue) root.relinkVariableReference(map)
+                root.eAllContents().filter(SMTSymbolicValue).forEach[relinkVariableReference(map)]
+        }
+        def private relinkVariableReference(SMTSymbolicValue target,Map<SMTSortedVariable, SMTSortedVariable> map) {
+                if(map.containsKey(target.symbolicReference)) {
+                        target.symbolicReference = map.get(target.symbolicReference)
+                }
+        }
+}
+@Data
+class LogicSubterm extends TransformedSubterm{
+        
+        SMTTerm value
+        override expectLogic() {return this}
+        override expectNumber() { throw new AssertionError("A term is not a number") }
+        
+        public new(SMTTerm expression)
+        {
+                this.value = expression
+        }
+        override getPossibleValues() {
+                #[new SubtermOption(#[],#[],value,TypeDescriptor::logicTypeDescriptor_Instance)]
+        }
+}
+@Data
+class NumericSubterm extends TransformedSubterm {
+        List<SubtermOption> values
+        
+        public new(
+                List<SMTSortedVariable> variables,
+                List<SMTTerm> preconditions,
+                SMTTerm expression) {
+                this.values = #[new SubtermOption(variables,preconditions,expression,TypeDescriptor.numericTypeDescriptor_Instance)]
+        }
+        public new(List<SubtermOption> values) {
+                this.values = values
+        }
+        
+        override expectLogic() { throw new AssertionError("A term is not a logic value") }
+        override expectNumber() { return this }
+        
+        override getPossibleValues() {
+                values
+        }
+}
+@Data
+class ComplexSubterm extends TransformedSubterm {
+        List<SubtermOption> options
+        override expectLogic() { throw new AssertionError("A term is not a logic value") }
+        override expectNumber() { throw new AssertionError("A term is not a number") }
+        public new(List<SMTSortedVariable> variables,
+                List<SMTTerm> preconditions,
+                SMTTerm expression,
+                TypeDescriptor type)
+        {
+                this.options = #[new SubtermOption(variables,preconditions,expression,type)]
+        }
+        public new(List<SubtermOption> subterms) {
+                this.options = subterms
+        }
+        override getPossibleValues() {
+                this.options
+        }
+}
author	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
committer	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
commit	60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree	5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend
parent	Initial commit, migrating from SVN (diff)
download	VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip

diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend new file mode 100644 index 00000000..48952288 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend
@@ -0,0 +1,183 @@
	1	package hu.bme.mit.inf.dslreasoner.smt.reasoner
	2
	3	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable
	4	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue
	5	import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
	6	import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory
	7	import java.util.ArrayList
	8	import java.util.List
	9	import java.util.Map
	10	import org.eclipse.emf.ecore.EObject
	11	import org.eclipse.emf.ecore.util.EcoreUtil
	12	import org.eclipse.xtend.lib.annotations.Data
	13	import java.util.HashMap
	14	import java.util.LinkedList
	15
	16	abstract class TransformedSubterm {
	17	val static extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE
	18	def LogicSubterm expectLogic()
	19	def NumericSubterm expectNumber()
	20
	21	def List<SubtermOption> getPossibleValues()
	22
	23	public static def List<List<SubtermOption>> allCombinations(List<SubtermOption>... possibleValues) {
	24	return allCombinations(possibleValues.toList)
	25	}
	26	public static def List<List<SubtermOption>> allCombinations(Iterable<List<SubtermOption>> possibleValues) {
	27	if(possibleValues.size == 1) {
	28	return possibleValues.head.map[x\|#[x.copy]]
	29	} else {
	30	val head = possibleValues.head
	31	val tails = possibleValues.tail.allCombinations
	32	val res = new ArrayList(tails.size * head.size)
	33	for(headElement : head) {
	34	for(tail : tails) {
	35	val combination = new ArrayList(tail.size+1)
	36	combination.add(headElement)
	37	combination.addAll(tail.map[copy])
	38	res.add(combination)
	39	}
	40	}
	41	return res
	42	}
	43	}
	44
	45	public static def resolveToLogic(List<SubtermOption> subterms, SMTTerm value) {
	46	val allDefinitions = subterms.map[it.variables].flatten
	47	val allPreconditions = subterms.map[it.preconditions].flatten
	48	val preconditionedExpression = if(allPreconditions.empty) {
	49	value
	50	} else {
	51	createSMTAnd => [it.operands += allPreconditions it.operands += value]
	52	}
	53	val quantifiedExpression = if(allDefinitions.empty) {
	54	preconditionedExpression
	55	} else {
	56	createSMTForall => [
	57	it.quantifiedVariables += allDefinitions
	58	it.expression = preconditionedExpression]
	59	}
	60	return quantifiedExpression
	61	}
	62	}
	63
	64	@Data class SubtermOption {
	65	List<SMTSortedVariable> variables
	66	List<SMTTerm> preconditions
	67	SMTTerm expression
	68	TypeDescriptor type
	69
	70	public new(
	71	List<SMTSortedVariable> variables,
	72	List<SMTTerm> preconditions,
	73	SMTTerm expression,
	74	TypeDescriptor type)
	75	{
	76	this.variables = variables
	77	this.preconditions = preconditions
	78	this.expression = expression
	79	this.type = type
	80	}
	81
	82	public new(
	83	List<SubtermOption> previousSubterms,
	84	List<SMTSortedVariable> newVariables,
	85	List<SMTTerm> newPreconditions,
	86	SMTTerm newExpression,
	87	TypeDescriptor newType)
	88	{
	89	val old2New = new HashMap
	90	variables = new LinkedList
	91	for(variable : previousSubterms.map[getVariables].flatten) {
	92	val newVariable = EcoreUtil.copy(variable)
	93	old2New.put(variable,newVariable)
	94	variables+=newVariable
	95	}
	96
	97	preconditions = new LinkedList
	98	preconditions += previousSubterms.map[getPreconditions].flatten.map[x\|EcoreUtil.copy(x)]
	99	preconditions += newPreconditions.map[x\|EcoreUtil.copy(x)]
	100	preconditions.forEach[relinkAllVariableReference(old2New)]
	101
	102	expression = EcoreUtil.copy(newExpression)
	103	relinkAllVariableReference(expression,old2New)
	104
	105	type = newType
	106	}
	107
	108	public def copy() {
	109	val old2New = variables.toInvertedMap[EcoreUtil.copy(it)]
	110	val newPreconditions = preconditions.map[EcoreUtil.copy(it)]
	111	newPreconditions.forEach[it.relinkAllVariableReference(old2New)]
	112	val newExpression = EcoreUtil.copy(expression)
	113	return new SubtermOption(variables.map[old2New.get(it)],newPreconditions,newExpression,type)
	114	}
	115
	116	def private relinkAllVariableReference(EObject root,Map<SMTSortedVariable, SMTSortedVariable> map) {
	117	if(root instanceof SMTSymbolicValue) root.relinkVariableReference(map)
	118	root.eAllContents().filter(SMTSymbolicValue).forEach[relinkVariableReference(map)]
	119	}
	120	def private relinkVariableReference(SMTSymbolicValue target,Map<SMTSortedVariable, SMTSortedVariable> map) {
	121	if(map.containsKey(target.symbolicReference)) {
	122	target.symbolicReference = map.get(target.symbolicReference)
	123	}
	124	}
	125	}
	126
	127	@Data
	128	class LogicSubterm extends TransformedSubterm{
	129
	130	SMTTerm value
	131	override expectLogic() {return this}
	132	override expectNumber() { throw new AssertionError("A term is not a number") }
	133
	134	public new(SMTTerm expression)
	135	{
	136	this.value = expression
	137	}
	138	override getPossibleValues() {
	139	#[new SubtermOption(#[],#[],value,TypeDescriptor::logicTypeDescriptor_Instance)]
	140	}
	141	}
	142
	143	@Data
	144	class NumericSubterm extends TransformedSubterm {
	145	List<SubtermOption> values
	146
	147	public new(
	148	List<SMTSortedVariable> variables,
	149	List<SMTTerm> preconditions,
	150	SMTTerm expression) {
	151	this.values = #[new SubtermOption(variables,preconditions,expression,TypeDescriptor.numericTypeDescriptor_Instance)]
	152	}
	153	public new(List<SubtermOption> values) {
	154	this.values = values
	155	}
	156
	157	override expectLogic() { throw new AssertionError("A term is not a logic value") }
	158	override expectNumber() { return this }
	159
	160	override getPossibleValues() {
	161	values
	162	}
	163	}
	164
	165	@Data
	166	class ComplexSubterm extends TransformedSubterm {
	167	List<SubtermOption> options
	168	override expectLogic() { throw new AssertionError("A term is not a logic value") }
	169	override expectNumber() { throw new AssertionError("A term is not a number") }
	170	public new(List<SMTSortedVariable> variables,
	171	List<SMTTerm> preconditions,
	172	SMTTerm expression,
	173	TypeDescriptor type)
	174	{
	175	this.options = #[new SubtermOption(variables,preconditions,expression,type)]
	176	}
	177	public new(List<SubtermOption> subterms) {
	178	this.options = subterms
	179	}
	180	override getPossibleValues() {
	181	this.options
	182	}
	183	}