From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- .../smt/reasoner/TransformedSubterm.xtend | 183 +++++++++++++++++++++ 1 file changed, 183 insertions(+) create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend') 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 getPossibleValues() + + public static def List> allCombinations(List... possibleValues) { + return allCombinations(possibleValues.toList) + } + public static def List> allCombinations(Iterable> 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 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 variables + List preconditions + SMTTerm expression + TypeDescriptor type + + public new( + List variables, + List preconditions, + SMTTerm expression, + TypeDescriptor type) + { + this.variables = variables + this.preconditions = preconditions + this.expression = expression + this.type = type + } + + public new( + List previousSubterms, + List newVariables, + List 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 map) { + if(root instanceof SMTSymbolicValue) root.relinkVariableReference(map) + root.eAllContents().filter(SMTSymbolicValue).forEach[relinkVariableReference(map)] + } + def private relinkVariableReference(SMTSymbolicValue target,Map 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 values + + public new( + List variables, + List preconditions, + SMTTerm expression) { + this.values = #[new SubtermOption(variables,preconditions,expression,TypeDescriptor.numericTypeDescriptor_Instance)] + } + public new(List 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 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 variables, + List preconditions, + SMTTerm expression, + TypeDescriptor type) + { + this.options = #[new SubtermOption(variables,preconditions,expression,type)] + } + public new(List subterms) { + this.options = subterms + } + override getPossibleValues() { + this.options + } +} -- cgit v1.2.3-54-g00ecf