Merge branch 'master' of https://git.fortiss.org/af3/kernel.git into 4310

org.fortiss.tooling.kernel/src/org/fortiss/tooling/kernel/internal/ConstraintCheckerService.java

@@ -17,14 +17,23 @@ package org.fortiss.tooling.kernel.internal;
 
 import static java.util.Collections.emptyList;
 import static java.util.Collections.unmodifiableMap;
+import static org.conqat.lib.commons.reflect.ReflectionUtils.performNearestClassLookup;
+import static org.eclipse.core.runtime.Status.OK_STATUS;
+import static org.eclipse.core.runtime.jobs.Job.RUNNING;
 import static org.fortiss.tooling.kernel.utils.EcoreUtils.getFirstParentWithType;
 
 import java.util.ArrayList;
 import java.util.Collections;
+import java.util.HashMap;
 import java.util.Iterator;
 import java.util.LinkedList;
 import java.util.List;
+import java.util.Map;
+import java.util.function.Consumer;
 
+import org.eclipse.core.runtime.IProgressMonitor;
+import org.eclipse.core.runtime.IStatus;
+import org.eclipse.core.runtime.jobs.Job;
 import org.eclipse.emf.ecore.EObject;
 import org.fortiss.tooling.kernel.extension.IConstraintChecker;
 import org.fortiss.tooling.kernel.extension.data.IConstraintViolation;
@@ -32,6 +41,7 @@ import org.fortiss.tooling.kernel.introspection.IIntrospectionDetailsItem;
 import org.fortiss.tooling.kernel.introspection.IIntrospectionItem;
 import org.fortiss.tooling.kernel.introspection.IIntrospectiveKernelService;
 import org.fortiss.tooling.kernel.introspection.items.ConstraintCheckerKISSDetailsItem;
+import org.fortiss.tooling.kernel.model.INamedElement;
 import org.fortiss.tooling.kernel.service.IConstraintCheckerService;
 import org.fortiss.tooling.kernel.service.IKernelIntrospectionSystemService;
 import org.fortiss.tooling.kernel.service.base.EObjectAwareServiceBase;
@@ -46,6 +56,18 @@ public class ConstraintCheckerService extends EObjectAwareServiceBase<IConstrain
 	/** The singleton instance. */
 	private static final ConstraintCheckerService INSTANCE = new ConstraintCheckerService();
 
+	/** Map of all classes to the respective registered asynchronous constraint checkers. */
+	Map<Class<?>, List<IConstraintChecker<EObject>>> asynchronousConstraintCheckers =
+			new HashMap<Class<?>, List<IConstraintChecker<EObject>>>();
+
+	/** Maps all constraint checkers to their identifier. */
+	Map<IConstraintChecker<? extends EObject>, String> asynchronousCheckIdentifiers =
+			new HashMap<IConstraintChecker<? extends EObject>, String>();
+
+	/** Maps all constraint checkers to the last started Job, each. */
+	Map<IConstraintChecker<? extends EObject>, Map<EObject, Job>> asynchronousCheckerJobs =
+			new HashMap<IConstraintChecker<? extends EObject>, Map<EObject, Job>>();
+
 	/** Returns singleton instance of the service. */
 	public static ConstraintCheckerService getInstance() {
 		return INSTANCE;
@@ -155,6 +177,69 @@ public class ConstraintCheckerService extends EObjectAwareServiceBase<IConstrain
 		}
 	}
 
+	/** {@inheritDoc} */
+	@Override
+	public void performAllAsynchronousConstraintChecksRecursively(EObject modelElement,
+			Consumer<List<IConstraintViolation<? extends EObject>>> addMarkers) {
+		performAllAsynchronousConstraintChecks(modelElement, addMarkers);
+
+		for(Iterator<EObject> iter = modelElement.eAllContents(); iter.hasNext();) {
+			performAllAsynchronousConstraintChecks(iter.next(), addMarkers);
+		}
+	}
+
+	/** {@inheritDoc} */
+	@Override
+	public void performAllAsynchronousConstraintChecks(EObject modelElement,
+			Consumer<List<IConstraintViolation<? extends EObject>>> addMarkers) {
+		List<IConstraintChecker<EObject>> asyncHandlers =
+				performNearestClassLookup(modelElement.getClass(), asynchronousConstraintCheckers);
+
+		if(asyncHandlers == null) {
+			return;
+		}
+
+		for(IConstraintChecker<EObject> checker : asyncHandlers) {
+			Map<EObject, Job> jobs = asynchronousCheckerJobs.get(checker);
+			if(jobs == null) {
+				jobs = new HashMap<EObject, Job>();
+				asynchronousCheckerJobs.put(checker, jobs);
+			}
+			Job checkerJob = jobs.get(modelElement);
+			if(checkerJob != null && checkerJob.getState() == RUNNING) {
+				checkerJob.cancel();
+			}
+
+			String checkerIdentifier = asynchronousCheckIdentifiers.get(checker);
+			if(checkerIdentifier == null) {
+				checkerIdentifier = "Asynchronous Model Constraint Check";
+			}
+
+			String modelIdentifier = "";
+			if(modelElement instanceof INamedElement) {
+				modelIdentifier = " on " + ((INamedElement)modelElement).getName();
+			}
+
+			checkerJob = new Job(checkerIdentifier + modelIdentifier) {
+
+				@Override
+				protected IStatus run(IProgressMonitor monitor) {
+					List<IConstraintViolation<? extends EObject>> results =
+							new ArrayList<IConstraintViolation<? extends EObject>>();
+					results.addAll(checker.apply(modelElement));
+
+					addMarkers.accept(results);
+
+					return OK_STATUS;
+				}
+			};
+			jobs.put(modelElement, checkerJob);
+
+			checkerJob.setUser(false);
+			checkerJob.schedule();
+		}
+	}
+
 	/** {@inheritDoc} */
 	@Override
 	public List<IConstraintChecker<? extends EObject>>
@@ -204,4 +289,26 @@ public class ConstraintCheckerService extends EObjectAwareServiceBase<IConstrain
 	public IIntrospectionDetailsItem getDetailsItem() {
 		return new ConstraintCheckerKISSDetailsItem(unmodifiableMap(handlerMap));
 	}
+
+	/** {@inheritDoc} */
+	@SuppressWarnings("unchecked")
+	@Override
+	public <T extends EObject> void registerAsynchronousConstraintChecker(
+			IConstraintChecker<T> checker, Class<T> modelElementClass, String checkerName) {
+		if(checker == null) {
+			return;
+		}
+
+		List<IConstraintChecker<EObject>> checkers =
+				asynchronousConstraintCheckers.get(modelElementClass);
+
+		if(checkers == null) {
+			checkers = new ArrayList<IConstraintChecker<EObject>>();
+			asynchronousConstraintCheckers.put(modelElementClass, checkers);
+		}
+
+		checkers.add((IConstraintChecker<EObject>)checker);
+
+		asynchronousCheckIdentifiers.put(checker, checkerName);
+	}
 }

org.fortiss.tooling.kernel/src/org/fortiss/tooling/kernel/service/.ratings

 ICommandLineInterfaceService.java c3e3ba08b2a1b8125b43abd1c29b7dc0a0be2b80 GREEN
 ICommandStackService.java 678dcd1a6ab435ed0870fa2a9ec48ce47f25a187 GREEN
 IConnectionCompositorService.java 0cdf4568b2cd3e95ea195df90a84699eff36442b GREEN
-IConstraintCheckerService.java dc04965ac0265f77cb846f472d76620fb05a491a GREEN
+IConstraintCheckerService.java 7fdce90a3b6df1ebba709f8382a1c37d0cffb2e3 GREEN
 IEclipseResourceStorageService.java b1155ca15cd9474d4d533d6cb2725e8a22040ec9 GREEN
 IElementCompositorService.java acd462ec15f3bcc247b544b46ceebee971fe1408 GREEN
 IKernelIntrospectionSystemService.java 7005c3acb4c6f978729d93279c595765e94e38eb GREEN

org.fortiss.tooling.kernel/src/org/fortiss/tooling/kernel/service/IConstraintCheckerService.java

@@ -16,6 +16,7 @@
 package org.fortiss.tooling.kernel.service;
 
 import java.util.List;
+import java.util.function.Consumer;
 
 import org.eclipse.emf.ecore.EObject;
 import org.fortiss.tooling.kernel.extension.IConstraintChecker;
@@ -47,6 +48,32 @@ public interface IConstraintCheckerService {
 	List<IConstraintViolation<? extends EObject>>
 			performAllConstraintChecksRecursively(EObject modelElement);
 
+	/**
+	 * Performs all registered asynchronous constraint checks for the given {@link EObject} and all
+	 * its
+	 * contained child elements.
+	 * 
+	 * @param modelElement
+	 *            The {@link EObject} for which all checks shall be performed recursively.
+	 * @param addMarkers
+	 *            A {@link Consumer} to receive all constraint violations from the asynchronous
+	 *            checks.
+	 */
+	void performAllAsynchronousConstraintChecksRecursively(EObject modelElement,
+			Consumer<List<IConstraintViolation<? extends EObject>>> addMarkers);
+
+	/**
+	 * Performs all registered asynchronous constraint checks for the given {@link EObject}.
+	 * 
+	 * @param modelElement
+	 *            The {@link EObject} for which all checks shall be performed.
+	 * @param addMarkers
+	 *            A {@link Consumer} to receive all constraint violations from the asynchronous
+	 *            checks.
+	 */
+	void performAllAsynchronousConstraintChecks(EObject modelElement,
+			Consumer<List<IConstraintViolation<? extends EObject>>> addMarkers);
+
 	/**
 	 * Performs all constraint checks only on the given model element and
 	 * returns the check results.
@@ -70,4 +97,8 @@ public interface IConstraintCheckerService {
 	 * checks will be skipped.
 	 */
 	void registerTypeAsExcludedParentForConstraintChecks(Class<? extends EObject> clazz);
+
+	/** Registers the given checker to be run asynchronously in the service. */
+	<T extends EObject> void registerAsynchronousConstraintChecker(IConstraintChecker<T> checker,
+			Class<T> modelElementClass, String checkerName);
 }

.settings @ 310d1c04

+Subproject commit 310d1c04f28f6252d5a02dd8fde1b76ae4a4da51

org.fortiss.variability/.settings/org.eclipse.core.resources.prefs

-eclipse.preferences.version=1
-encoding//src/org/fortiss/variability/util/FeatureModelTransformationUtils.java=UTF-8
-encoding/<project>=US-ASCII

org.fortiss.variability/.settings/org.eclipse.jdt.ui.prefs

-eclipse.preferences.version=1
-editor_save_participant_org.eclipse.jdt.ui.postsavelistener.cleanup=true
-formatter_profile=_fortiss
-formatter_settings_version=12
-org.eclipse.jdt.ui.javadoc=true
-org.eclipse.jdt.ui.text.custom_code_templates=<?xml version\="1.0" encoding\="UTF-8" standalone\="no"?><templates><template autoinsert\="false" context\="gettercomment_context" deleted\="false" description\="Comment for getter method" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.gettercomment" name\="gettercomment">/** Returns ${bare_field_name}. */</template><template autoinsert\="false" context\="settercomment_context" deleted\="false" description\="Comment for setter method" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.settercomment" name\="settercomment">/**  Sets ${bare_field_name}. */</template><template autoinsert\="true" context\="constructorcomment_context" deleted\="false" description\="Comment for created constructors" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.constructorcomment" name\="constructorcomment">/**\n * ${tags}\n */</template><template autoinsert\="false" context\="filecomment_context" deleted\="false" description\="Comment for created Java files" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.filecomment" name\="filecomment">/*-------------------------------------------------------------------------+\n| Copyright ${year} fortiss GmbH                                              |\n|                                                                          |\n| Licensed under the Apache License, Version 2.0 (the "License");          |\n| you may not use this file except in compliance with the License.         |\n| You may obtain a copy of the License at                                  |\n|                                                                          |\n|    http\://www.apache.org/licenses/LICENSE-2.0                            |\n|                                                                          |\n| Unless required by applicable law or agreed to in writing, software      |\n| distributed under the License is distributed on an "AS IS" BASIS,        |\n| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |\n| See the License for the specific language governing permissions and      |\n| limitations under the License.                                           |\n+--------------------------------------------------------------------------*/</template><template autoinsert\="false" context\="typecomment_context" deleted\="false" description\="Comment for created types" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.typecomment" name\="typecomment">/**\n * \n * @author ${user}\n*/</template><template autoinsert\="false" context\="fieldcomment_context" deleted\="false" description\="Comment for fields" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.fieldcomment" name\="fieldcomment">\n/**  */</template><template autoinsert\="true" context\="methodcomment_context" deleted\="false" description\="Comment for non-overriding methods" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.methodcomment" name\="methodcomment">/**\n * ${tags}\n */</template><template autoinsert\="false" context\="overridecomment_context" deleted\="false" description\="Comment for overriding methods" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.overridecomment" name\="overridecomment">/** {@inheritDoc} */</template><template autoinsert\="true" context\="delegatecomment_context" deleted\="false" description\="Comment for delegate methods" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.delegatecomment" name\="delegatecomment">/**\n * ${tags}\n * ${see_to_target}\n */</template><template autoinsert\="true" context\="newtype_context" deleted\="false" description\="Newly created files" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.newtype" name\="newtype">${filecomment}\n${package_declaration}\n\n${typecomment}\n${type_declaration}</template><template autoinsert\="true" context\="classbody_context" deleted\="false" description\="Code in new class type bodies" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.classbody" name\="classbody">\n</template><template autoinsert\="true" context\="interfacebody_context" deleted\="false" description\="Code in new interface type bodies" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.interfacebody" name\="interfacebody">\n</template><template autoinsert\="true" context\="enumbody_context" deleted\="false" description\="Code in new enum type bodies" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.enumbody" name\="enumbody">\n</template><template autoinsert\="true" context\="annotationbody_context" deleted\="false" description\="Code in new annotation type bodies" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.annotationbody" name\="annotationbody">\n</template><template autoinsert\="true" context\="catchblock_context" deleted\="false" description\="Code in new catch blocks" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.catchblock" name\="catchblock">// ${todo} Auto-generated catch block\n${exception_var}.printStackTrace();</template><template autoinsert\="true" context\="methodbody_context" deleted\="false" description\="Code in created method stubs" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.methodbody" name\="methodbody">// ${todo} Auto-generated method stub\n${body_statement}</template><template autoinsert\="true" context\="constructorbody_context" deleted\="false" description\="Code in created constructor stubs" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.constructorbody" name\="constructorbody">${body_statement}\n// ${todo} Auto-generated constructor stub</template><template autoinsert\="true" context\="getterbody_context" deleted\="false" description\="Code in created getters" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.getterbody" name\="getterbody">return ${field};</template><template autoinsert\="true" context\="setterbody_context" deleted\="false" description\="Code in created setters" enabled\="true" id\="org.eclipse.jdt.ui.text.codetemplates.setterbody" name\="setterbody">${field} \= ${param};</template><template autoinsert\="true" context\="gettercomment_context" deleted\="false" description\="Comment for getter function" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.gettercomment" name\="gettercomment">/**\n * @return the ${bare_field_name}\n */</template><template autoinsert\="true" context\="settercomment_context" deleted\="false" description\="Comment for setter function" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.settercomment" name\="settercomment">/**\n * @param ${param} the ${bare_field_name} to set\n */</template><template autoinsert\="true" context\="constructorcomment_context" deleted\="false" description\="Comment for created constructors" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.constructorcomment" name\="constructorcomment">/**\n * ${tags}\n */</template><template autoinsert\="true" context\="filecomment_context" deleted\="false" description\="Comment for created JavaScript files" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.filecomment" name\="filecomment">/**\n * \n */</template><template autoinsert\="true" context\="typecomment_context" deleted\="false" description\="Comment for created types" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.typecomment" name\="typecomment">/**\n * @author ${user}\n *\n * ${tags}\n */</template><template autoinsert\="true" context\="fieldcomment_context" deleted\="false" description\="Comment for vars" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.fieldcomment" name\="fieldcomment">/**\n * \n */</template><template autoinsert\="true" context\="methodcomment_context" deleted\="false" description\="Comment for non-overriding function" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.methodcomment" name\="methodcomment">/**\n * ${tags}\n */</template><template autoinsert\="true" context\="overridecomment_context" deleted\="false" description\="Comment for overriding functions" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.overridecomment" name\="overridecomment">/* (non-JSDoc)\n * ${see_to_overridden}\n */</template><template autoinsert\="true" context\="delegatecomment_context" deleted\="false" description\="Comment for delegate functions" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.delegatecomment" name\="delegatecomment">/**\n * ${tags}\n * ${see_to_target}\n */</template><template autoinsert\="true" context\="newtype_context" deleted\="false" description\="Newly created files" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.newtype" name\="newtype">${filecomment}\n${package_declaration}\n\n${typecomment}\n${type_declaration}</template><template autoinsert\="true" context\="classbody_context" deleted\="false" description\="Code in new class type bodies" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.classbody" name\="classbody">\n</template><template autoinsert\="true" context\="catchblock_context" deleted\="false" description\="Code in new catch blocks" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.catchblock" name\="catchblock">// ${todo} Auto-generated catch block\n${exception_var}.printStackTrace();</template><template autoinsert\="true" context\="methodbody_context" deleted\="false" description\="Code in created function stubs" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.methodbody" name\="methodbody">// ${todo} Auto-generated function stub\n${body_statement}</template><template autoinsert\="true" context\="constructorbody_context" deleted\="false" description\="Code in created constructor stubs" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.constructorbody" name\="constructorbody">${body_statement}\n// ${todo} Auto-generated constructor stub</template><template autoinsert\="true" context\="getterbody_context" deleted\="false" description\="Code in created getters" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.getterbody" name\="getterbody">return ${field};</template><template autoinsert\="true" context\="setterbody_context" deleted\="false" description\="Code in created setters" enabled\="true" id\="org.eclipse.wst.jsdt.ui.text.codetemplates.setterbody" name\="setterbody">${field} \= ${param};</template></templates>
-sp_cleanup.add_default_serial_version_id=true
-sp_cleanup.add_generated_serial_version_id=false
-sp_cleanup.add_missing_annotations=true
-sp_cleanup.add_missing_deprecated_annotations=true
-sp_cleanup.add_missing_methods=false
-sp_cleanup.add_missing_nls_tags=false
-sp_cleanup.add_missing_override_annotations=true
-sp_cleanup.add_missing_override_annotations_interface_methods=true
-sp_cleanup.add_serial_version_id=false
-sp_cleanup.always_use_blocks=true
-sp_cleanup.always_use_parentheses_in_expressions=false
-sp_cleanup.always_use_this_for_non_static_field_access=false
-sp_cleanup.always_use_this_for_non_static_method_access=false
-sp_cleanup.convert_to_enhanced_for_loop=false
-sp_cleanup.correct_indentation=false
-sp_cleanup.format_source_code=true
-sp_cleanup.format_source_code_changes_only=false
-sp_cleanup.make_local_variable_final=false
-sp_cleanup.make_parameters_final=false
-sp_cleanup.make_private_fields_final=true
-sp_cleanup.make_type_abstract_if_missing_method=false
-sp_cleanup.make_variable_declarations_final=true
-sp_cleanup.never_use_blocks=false
-sp_cleanup.never_use_parentheses_in_expressions=true
-sp_cleanup.on_save_use_additional_actions=false
-sp_cleanup.organize_imports=true
-sp_cleanup.qualify_static_field_accesses_with_declaring_class=false
-sp_cleanup.qualify_static_member_accesses_through_instances_with_declaring_class=true
-sp_cleanup.qualify_static_member_accesses_through_subtypes_with_declaring_class=true
-sp_cleanup.qualify_static_member_accesses_with_declaring_class=false
-sp_cleanup.qualify_static_method_accesses_with_declaring_class=false
-sp_cleanup.remove_private_constructors=true
-sp_cleanup.remove_trailing_whitespaces=false
-sp_cleanup.remove_trailing_whitespaces_all=true
-sp_cleanup.remove_trailing_whitespaces_ignore_empty=false
-sp_cleanup.remove_unnecessary_casts=true
-sp_cleanup.remove_unnecessary_nls_tags=false
-sp_cleanup.remove_unused_imports=false
-sp_cleanup.remove_unused_local_variables=false
-sp_cleanup.remove_unused_private_fields=true
-sp_cleanup.remove_unused_private_members=false
-sp_cleanup.remove_unused_private_methods=true
-sp_cleanup.remove_unused_private_types=true
-sp_cleanup.sort_members=false
-sp_cleanup.sort_members_all=false
-sp_cleanup.use_blocks=false
-sp_cleanup.use_blocks_only_for_return_and_throw=false
-sp_cleanup.use_parentheses_in_expressions=false
-sp_cleanup.use_this_for_non_static_field_access=false
-sp_cleanup.use_this_for_non_static_field_access_only_if_necessary=true
-sp_cleanup.use_this_for_non_static_method_access=false
-sp_cleanup.use_this_for_non_static_method_access_only_if_necessary=true

org.fortiss.variability/.settings/org.eclipse.m2e.core.prefs

-activeProfiles=
-eclipse.preferences.version=1
-resolveWorkspaceProjects=true
-version=1

org.fortiss.variability/META-INF/MANIFEST.MF

@@ -16,6 +16,7 @@ Export-Package: org.antlr.v4.runtime,
  org.antlr.v4.runtime.tree,
  org.antlr.v4.runtime.tree.pattern,
  org.antlr.v4.runtime.tree.xpath,
+ org.fortiss.variability.analysis,
  org.fortiss.variability.bind,
  org.fortiss.variability.model,
  org.fortiss.variability.model.base,

org.fortiss.variability/model/.ratings

-variability.ecore 3e85a6aa197bd9a4900f1d3236a2c5e576e7a645 GREEN
+variability.ecore 46e8f19e62bf23c1897ad71d15ed830f01cd1ce9 GREEN

org.fortiss.variability/model/variability.ecore

@@ -344,6 +344,12 @@
       <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
         <details key="documentation" value="Literal to be used in a PresenceConditionTerm. These are the propositions in a propositional logic formula."/>
       </eAnnotations>
+      <eOperations name="resolveToFeatureLiterals" eType="#//presence/PresenceConditionTerm">
+        <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
+          <details key="documentation" value="{@inheritDoc}"/>
+          <details key="body" value="return org.fortiss.variability.model.VariabilityStaticImpl.resolveToFeatureLiterals(this);"/>
+        </eAnnotations>
+      </eOperations>
       <eStructuralFeatures xsi:type="ecore:EReference" name="literalReference" eType="#//presence/ILiteralReferencable">
         <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
           <details key="documentation" value="Reference to an referable element. This can be Features but also other model elements."/>
@@ -355,6 +361,11 @@
       <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
         <details key="documentation" value="Base interface for all elements that can be used as literals in a presence condition."/>
       </eAnnotations>
+      <eOperations name="resolveToFeatureLiterals" eType="#//presence/PresenceConditionTerm">
+        <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
+          <details key="documentation" value="Translates all literals in this presence condition which are not features already, to their respective feature combination."/>
+        </eAnnotations>
+      </eOperations>
     </eClassifiers>
     <eClassifiers xsi:type="ecore:EClass" name="DefaultPC" eSuperTypes="#//presence/PresenceCondition">
       <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
@@ -389,11 +400,23 @@
       <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
         <details key="documentation" value="PresenceCondition with two operands and a disjunctive operator."/>
       </eAnnotations>
+      <eOperations name="resolveToFeatureLiterals" eType="#//presence/PresenceConditionTerm">
+        <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
+          <details key="documentation" value="{@inheritDoc}"/>
+          <details key="body" value="return org.fortiss.variability.model.VariabilityStaticImpl.resolveToFeatureLiterals(this);"/>
+        </eAnnotations>
+      </eOperations>
     </eClassifiers>
     <eClassifiers xsi:type="ecore:EClass" name="AndPC" eSuperTypes="#//presence/BinaryOperatorPC">
       <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
         <details key="documentation" value="PresenceCondition with two operands and a conjunctive operator."/>
       </eAnnotations>
+      <eOperations name="resolveToFeatureLiterals" eType="#//presence/PresenceConditionTerm">
+        <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
+          <details key="documentation" value="{@inheritDoc}"/>
+          <details key="body" value="return org.fortiss.variability.model.VariabilityStaticImpl.resolveToFeatureLiterals(this);"/>
+        </eAnnotations>
+      </eOperations>
     </eClassifiers>
     <eClassifiers xsi:type="ecore:EClass" name="UnaryOperatorPC" abstract="true" eSuperTypes="#//presence/PresenceConditionTerm">
       <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
@@ -410,6 +433,12 @@
       <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
         <details key="documentation" value="Negated PresenceCondition."/>
       </eAnnotations>
+      <eOperations name="resolveToFeatureLiterals" eType="#//presence/PresenceConditionTerm">
+        <eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
+          <details key="documentation" value="{@inheritDoc}"/>
+          <details key="body" value="return org.fortiss.variability.model.VariabilityStaticImpl.resolveToFeatureLiterals(this);"/>
+        </eAnnotations>
+      </eOperations>
     </eClassifiers>
     <eClassifiers xsi:type="ecore:EClass" name="IEvaluationContext" abstract="true"
         interface="true">

org.fortiss.variability/model/variability.genmodel

@@ -127,8 +127,12 @@
       <genClasses ecoreClass="variability.ecore#//presence/LiteralPC">
         <genFeatures notify="false" createChild="false" propertySortChoices="true"
             ecoreFeature="ecore:EReference variability.ecore#//presence/LiteralPC/literalReference"/>
+        <genOperations ecoreOperation="variability.ecore#//presence/LiteralPC/resolveToFeatureLiterals"
+            body="return org.fortiss.variability.model.VariabilityStaticImpl.resolveToFeatureLiterals(this);"/>
+      </genClasses>
+      <genClasses image="false" ecoreClass="variability.ecore#//presence/ILiteralReferencable">
+        <genOperations ecoreOperation="variability.ecore#//presence/ILiteralReferencable/resolveToFeatureLiterals"/>
       </genClasses>
-      <genClasses image="false" ecoreClass="variability.ecore#//presence/ILiteralReferencable"/>
       <genClasses ecoreClass="variability.ecore#//presence/DefaultPC">
         <genOperations ecoreOperation="variability.ecore#//presence/DefaultPC/getStringRepresentation"
             body="return &quot;DEFAULT&quot;;"/>
@@ -141,11 +145,15 @@
         <genAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
           <details key="body" value="return org.fortiss.variability.model.VariabilityStaticImpl.evaluateOrPC(this, context);"/>
         </genAnnotations>
+        <genOperations ecoreOperation="variability.ecore#//presence/OrPC/resolveToFeatureLiterals"
+            body="return org.fortiss.variability.model.VariabilityStaticImpl.resolveToFeatureLiterals(this);"/>
       </genClasses>
       <genClasses ecoreClass="variability.ecore#//presence/AndPC">
         <genAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
           <details key="body" value="return org.fortiss.variability.model.VariabilityStaticImpl.evaluateAndPC(this, context);"/>
         </genAnnotations>
+        <genOperations ecoreOperation="variability.ecore#//presence/AndPC/resolveToFeatureLiterals"
+            body="return org.fortiss.variability.model.VariabilityStaticImpl.resolveToFeatureLiterals(this);"/>
       </genClasses>
       <genClasses image="false" ecoreClass="variability.ecore#//presence/UnaryOperatorPC">
         <genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference variability.ecore#//presence/UnaryOperatorPC/operand"/>
@@ -154,6 +162,8 @@
         <genAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
           <details key="body" value="return org.fortiss.variability.model.VariabilityStaticImpl.evaluateNotPC(this, context);"/>
         </genAnnotations>
+        <genOperations ecoreOperation="variability.ecore#//presence/NotPC/resolveToFeatureLiterals"
+            body="return org.fortiss.variability.model.VariabilityStaticImpl.resolveToFeatureLiterals(this);"/>
       </genClasses>
       <genClasses image="false" ecoreClass="variability.ecore#//presence/IEvaluationContext"/>
       <genClasses image="false" ecoreClass="variability.ecore#//presence/ICompleteEvaluationContext">

org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings

+BucketSetMap.java 665a28c80a9693b9b9e31b7ebe59f2de4195d56c GREEN
+DualKeyMap.java 75fbe85a54e5a655aaf67108ae004f98ed2879d8 GREEN
+EMFProductLineTranslation.java b590fbf053c21d9e6b0ee6d0818779e4adb1fe0b GREEN
+GenericProductLineAnalysis.java 1026cd6d7d0286c0f2402c5918d83cf7dc84407b GREEN
+IProductLineConstraint.java 1b0e1231cc578a6e7e544441ac33533b4feafeb1 GREEN
+IProductLineTranslation.java 733dae03e2baae237b6f0b33f0dd618a4f47cf73 GREEN
+ProductLineConstraintBase.java 04097c7c31367fdd11a054ba2b259a0535a313f4 GREEN
+ProductLineConstraintViolation.java 2a2bd9341e0b8f407ad9b4c663b507bd10d083ea GREEN

org.fortiss.variability/src/org/fortiss/variability/analysis/BucketSetMap.java

+/*-------------------------------------------------------------------------+
+| Copyright 2022 fortiss GmbH                                              |
+|                                                                          |
+| Licensed under the Apache License, Version 2.0 (the "License");          |
+| you may not use this file except in compliance with the License.         |
+| You may obtain a copy of the License at                                  |
+|                                                                          |
+|    http://www.apache.org/licenses/LICENSE-2.0                            |
+|                                                                          |
+| Unless required by applicable law or agreed to in writing, software      |
+| distributed under the License is distributed on an "AS IS" BASIS,        |
+| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
+| See the License for the specific language governing permissions and      |
+| limitations under the License.                                           |
++--------------------------------------------------------------------------*/
+package org.fortiss.variability.analysis;
+
+import static java.util.Collections.emptySet;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+
+/**
+ * {@link Map} implementation which maps a key to a {@link Set} of values.
+ * 
+ * @author bayha
+ */
+public class BucketSetMap<K, V> extends HashMap<K, Set<V>> {
+	/** ISerializable */
+	private static final long serialVersionUID = 312480465506162554L;
+
+	/**
+	 * Adds a given value to the set for the given key.
+	 * 
+	 * @param key
+	 *            The key for which an additional value shall be added.
+	 * @param value
+	 *            The additional value that shall be added.
+	 * 
+	 * @return The new set of values for the given key.
+	 */
+	public Set<V> add(K key, V value) {
+		Set<V> set = super.get(key);
+
+		if(set == null) {
+			set = new HashSet<V>();
+			this.put(key, set);
+		}
+
+		set.add(value);
+
+		return set;
+	}
+
+	/** {@inheritDoc} */
+	@Override
+	public Set<V> get(Object key) {
+		Set<V> ret = super.get(key);
+
+		if(ret == null) {
+			return emptySet();
+		}
+
+		return ret;
+	}
+}

org.fortiss.variability/src/org/fortiss/variability/analysis/DualKeyMap.java

+/*-------------------------------------------------------------------------+
+| Copyright 2022 fortiss GmbH                                              |
+|                                                                          |
+| Licensed under the Apache License, Version 2.0 (the "License");          |
+| you may not use this file except in compliance with the License.         |
+| You may obtain a copy of the License at                                  |
+|                                                                          |
+|    http://www.apache.org/licenses/LICENSE-2.0                            |
+|                                                                          |
+| Unless required by applicable law or agreed to in writing, software      |
+| distributed under the License is distributed on an "AS IS" BASIS,        |
+| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
+| See the License for the specific language governing permissions and      |
+| limitations under the License.                                           |
++--------------------------------------------------------------------------*/
+package org.fortiss.variability.analysis;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * A map which uses a combination of two keys to identify all values.
+ * 
+ * @author bayha
+ */
+public class DualKeyMap<K1, K2, V> {
+	/** Internally used map of maps. */
+	private Map<K1, Map<K2, V>> internalMap = new HashMap<K1, Map<K2, V>>();
+
+	/**
+	 * Retrieves the value for the given combination of keys.
+	 * 
+	 * @param key1
+	 *            The first part of the key.
+	 * @param key2
+	 *            The second part of the key.
+	 * 
+	 * @return The value which is identified by the given combination of the two keys.
+	 */
+	public V get(K1 key1, K2 key2) {
+		Map<K2, V> map = internalMap.get(key1);
+		if(map != null) {
+			return map.get(key2);
+		}
+		return null;
+	}
+
+	/**
+	 * Adds the given value for the given combination of keys.
+	 * 
+	 * @param key1
+	 *            The first part of the key.
+	 * @param key2
+	 *            The second part of the key.
+	 * @param value
+	 *            The value to be associated with the given combination of keys.
+	 * 
+	 * @return The previous value associated with the given combination of keys, or null if there
+	 *         was no mapping.
+	 */
+	public V put(K1 key1, K2 key2, V value) {
+		Map<K2, V> map = internalMap.get(key1);
+		if(map == null) {
+			map = new HashMap<K2, V>();
+			internalMap.put(key1, map);
+		}
+
+		return map.put(key2, value);
+	}
+}

org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineAnalysis.java

+package org.fortiss.variability.analysis;
+
+import static com.microsoft.z3.Status.SATISFIABLE;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import org.eclipse.emf.ecore.EAttribute;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.EReference;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.Model;
+import com.microsoft.z3.Solver;
+import com.microsoft.z3.Status;
+
+/**
+ * Base class that implements the translation of model product-lines to SMT in order to perform
+ * product-line analysis via constraint lifting.
+ * 
+ * @author bayha
+ */
+public abstract class GenericProductLineAnalysis {
+
+	/** The product-line translation to be used. */
+	protected final IProductLineTranslation translation;
+
+	/** {@link EObject} of the model to be translated. */
+	protected final EObject model;
+
+	/** The constraints to be checked by this analysis. */
+	protected Collection<IProductLineConstraint> plConstraints;
+
+	/**
+	 * Constructor.
+	 */
+	protected GenericProductLineAnalysis(EObject model, IProductLineTranslation translation) {
+		this.model = model;
+		this.translation = translation;
+	}
+
+	/**  Creates the {@link IProductLineConstraint}s to be checked by this analysis. */
+	protected abstract Collection<IProductLineConstraint> createConstraints();
+
+	/**
+	 * Performs a product-line analysis for the given model.
+	 * 
+	 * @return 'true' if all constraints are fulfilled for all variants of the product-line
+	 *         analysis. 'false' otherwise.
+	 */
+	public List<ProductLineConstraintViolation> doCheck() {
+		plConstraints = createConstraints();
+
+		setTranslatedMetamodelElements();
+
+		translation.translateModel(model);
+		Map<BoolExpr, IProductLineConstraint> constraintTracker2Constraint =
+				translation.translateConstraints(plConstraints);
+		Solver solver = translation.createSolver();
+
+		Status result = solver.check();
+
+		List<ProductLineConstraintViolation> ret = new ArrayList<ProductLineConstraintViolation>();
+
+		if(result.equals(SATISFIABLE)) {
+			// A violating configuration (i.e., model for negated constraints) was found -> extract
+			// violating model elements.
+			Model z3Model = solver.getModel();
+
+			for(BoolExpr constTrack : constraintTracker2Constraint.keySet()) {
+				Expr<?> constInterp = z3Model.getConstInterp(constTrack);
+
+				if(constInterp instanceof BoolExpr) {
+					if(constInterp.equals(translation.getContext().mkTrue())) {
+						IProductLineConstraint failedConstraint =
+								constraintTracker2Constraint.get(constTrack);
+
+						List<EObject> violatingObjects = new ArrayList<EObject>();
+						for(Expr<?> varTrack : failedConstraint.getVariableTracker()) {
+							Expr<?> interpr = z3Model.getConstInterp(varTrack);
+							EObject eObject = translation.getEObjectForExpression(interpr);
+
+							violatingObjects.add(eObject);
+						}
+
+						ret.add(new ProductLineConstraintViolation(failedConstraint,
+								violatingObjects, null));
+					}
+				}
+
+			}
+		}
+
+		translation.getContext().close();
+
+		return ret;
+	}
+
+	/** Retrieves the classes, references and attributes required by the constraints. */
+	private void setTranslatedMetamodelElements() {
+		Set<EClass> classes = new HashSet<EClass>();
+		Set<EReference> references = new HashSet<EReference>();
+		Set<EAttribute> attributes = new HashSet<EAttribute>();
+
+		for(IProductLineConstraint constraint : plConstraints) {
+			classes.addAll(constraint.getTranslatedClasses());
+			references.addAll(constraint.getTranslatedReferences());
+			attributes.addAll(constraint.getTranslatedAttributes());
+		}
+
+		translation.setTranslatedEClasses(classes);
+		translation.setTranslatedEReferences(references);
+		translation.setTranslatedEAttributes(attributes);
+	}
+}

org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineConstraint.java

+/*-------------------------------------------------------------------------+
+| Copyright 2023 fortiss GmbH                                              |
+|                                                                          |
+| Licensed under the Apache License, Version 2.0 (the "License");          |
+| you may not use this file except in compliance with the License.         |
+| You may obtain a copy of the License at                                  |
+|                                                                          |
+|    http://www.apache.org/licenses/LICENSE-2.0                            |
+|                                                                          |
+| Unless required by applicable law or agreed to in writing, software      |
+| distributed under the License is distributed on an "AS IS" BASIS,        |
+| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
+| See the License for the specific language governing permissions and      |
+| limitations under the License.                                           |
++--------------------------------------------------------------------------*/
+package org.fortiss.variability.analysis;
+
+import java.util.Collection;
+import java.util.List;
+
+import org.eclipse.emf.ecore.EAttribute;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.EReference;
+import org.fortiss.variability.model.features.configuration.VariantConfiguration;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Expr;
+
+/**
+ * Interface for product line constraints to be checked by the {@link GenericProductLineAnalysis}.
+ * 
+ * Note that usually this interface should not be implemented immediately. Instead use the base
+ * class {@link ProductLineConstraintBase} to define new constraints.
+ * 
+ * @author bayha
+ */
+public interface IProductLineConstraint {
+
+	/**
+	 * The name of the constraint.
+	 * 
+	 * @return The name as {@link String}.
+	 */
+	public String getConstraintName();
+
+	/**
+	 * Creates a meaningful error message for violations of this constraint.
+	 * 
+	 * @param violatingObjects
+	 *            The {@link EObject}s which violate the constraint in combination.
+	 * @param violatingConfiguration
+	 *            A {@link VariantConfiguration} which will result in a model variant in which the
+	 *            'violatingObjects' will violate this constraint.
+	 * @return The error message as a {@link String}.
+	 */
+	public String createErrorMessage(List<EObject> violatingObjects,
+			VariantConfiguration violatingConfiguration);
+
+	/**
+	 * Retrieves the quantified variables for this constraint.
+	 * 
+	 * @return An array of variables as {@link Expr}s.
+	 */
+	public Expr<?>[] getQuantifierVariables();
+
+	/**
+	 * Retrieves the constrain body for this constraint.
+	 * 
+	 * @return The constraint body as a {@link BoolExpr}.
+	 */
+	public BoolExpr getBody();
+
+	/**
+	 * Specifies whether this constraint is quantified as "for all".
+	 * 
+	 * @return 'true' if this constraint is quantified as "for all". 'false' if "exists".
+	 */
+	public boolean isForAll();
+
+	/**
+	 * Retrieves the generated tracker variables to identify violating interpretations for the
+	 * quantifier variables.
+	 * 
+	 * @return An array of {@link Expr}s with the quantifier variables.
+	 */
+	public Expr<?>[] getVariableTracker();
+
+	/**
+	 * Retrieves the {@link EClass} types for the quantified variables.
+	 * 
+	 * @return An array of {@link EClass}s for all quantified variables.
+	 */
+	public EClass[] getVariablesClasses();
+
+	/**
+	 * Specifies the classes which need to be translated in order to evaluate this constraint.
+	 * 
+	 * @return A {@link Collection} with all {@link EClass} which will be required to be translated.
+	 */
+	public Collection<EClass> getTranslatedClasses();
+
+	/**
+	 * Specifies the references which are used in this constraint and need to translated.
+	 * 
+	 * @return A {@link Collection} with all {@link EReference} which will be required to be
+	 *         translated.
+	 */
+	public Collection<EReference> getTranslatedReferences();
+
+	/**
+	 * Specifies the attributes which are used in this constraint and need to translated.
+	 * 
+	 * @return A {@link Collection} with all {@link EAttribute} which will be required to be
+	 *         translated.
+	 */
+	public Collection<EAttribute> getTranslatedAttributes();
+}

org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineTranslation.java

+/*-------------------------------------------------------------------------+
+| Copyright 2023 fortiss GmbH                                              |
+|                                                                          |
+| Licensed under the Apache License, Version 2.0 (the "License");          |
+| you may not use this file except in compliance with the License.         |
+| You may obtain a copy of the License at                                  |
+|                                                                          |
+|    http://www.apache.org/licenses/LICENSE-2.0                            |
+|                                                                          |
+| Unless required by applicable law or agreed to in writing, software      |
+| distributed under the License is distributed on an "AS IS" BASIS,        |
+| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
+| See the License for the specific language governing permissions and      |
+| limitations under the License.                                           |
++--------------------------------------------------------------------------*/
+package org.fortiss.variability.analysis;
+
+import java.util.Collection;
+import java.util.Map;
+
+import org.eclipse.emf.ecore.EAttribute;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.EReference;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.EnumSort;
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.FuncDecl;
+import com.microsoft.z3.Solver;
+
+/**
+ * Interface for generic translation of model product-lines to SMT.
+ * 
+ * @author bayha
+ */
+public interface IProductLineTranslation {
+
+	/**
+	 * Retrieves the context used for this translation.
+	 * 
+	 * @return The Z3 {@link Context}.
+	 */
+	public Context getContext();
+
+	/**
+	 * Translates the given model to Z3 SMT.
+	 * 
+	 * @param model
+	 *            {@link EObject} with model to be translated.
+	 */
+	public void translateModel(EObject model);
+
+	/**
+	 * Translates the given product-line constraints to Z3 SMT.
+	 * 
+	 * @param constraints
+	 *            A {@link Collection} of {@link IProductLineConstraint} to be translated.
+	 * 
+	 * @return A {@link Map} with Z3 {@link BoolExpr} to track the constraints in Z3
+	 *         models.
+	 */
+	public Map<BoolExpr, IProductLineConstraint>
+			translateConstraints(Collection<IProductLineConstraint> constraints);
+
+	/**
+	 * Retrieves the model element which was the source for the given Z3 expression.
+	 * 
+	 * @param expr
+	 *            The Z3 {@link Expr} for which to retrieve the originating {@link EObject}.
+	 * 
+	 * @return The {@link EObject} which was the source for the given Z3 expression.
+	 */
+	public EObject getEObjectForExpression(Expr<?> expr);
+
+	/**
+	 * Creates and initializes the Z3 solver to be used for analyzes.
+	 * 
+	 * Note, that {@code translateModel()} and {@code translateConstraints} should be called prior
+	 * to this method.
+	 * 
+	 * @return The Z3 {@link Solver} containing the model translation.
+	 */
+	public Solver createSolver();
+
+	/**
+	 * Retrieves the Z3 expression representing null for the given {@link EClass}.
+	 * 
+	 * @param cls
+	 *            The {@link EClass} to retrieve the Z3 null element for.
+	 * @return The Z3 {@link Expr} encoding null.
+	 */
+	public Expr<?> getNullElement(EClass cls);
+
+	/**
+	 * Retrieves the Z3 sort which represents the given EClass and its objects.
+	 * 
+	 * @param eClass
+	 *            The {@link EClass} to get the Z3 sort for.
+	 * @return The Z3 {@link EnumSort} for the given eClass.
+	 */
+	public EnumSort<?> getDatatype(EClass eClass);
+
+	/**
+	 * Retrieve the Z3 function declaration which represents the given attribute or reference for
+	 * the given EClass.
+	 * 
+	 * @param eClass
+	 *            The {@link EClass} for which to get a attribute or reference function.
+	 * @param attRefName
+	 *            {@link String} with the name for the attribute or reference.
+	 * @return A Z3 {@link FuncDecl} representing the attribute or reference.
+	 */
+	FuncDecl<?> getAttributeReferenceFunctionDeclaration(EClass eClass, String attRefName);
+
+	/**
+	 * Specifies the classes for which model elements shall be translated.
+	 * 
+	 * Note, that all classes which are relevant for evaluating the constraints need to specified
+	 * here, before staring a translation.
+	 * 
+	 * @param clss
+	 *            A {@link Collection} of all {@link EClass} to be translated.
+	 */
+	public void setTranslatedEClasses(Collection<EClass> clss);
+
+	/**
+	 * Specifies the references which shall be translated.
+	 * 
+	 * Note, that all references which are used in the constraints need to specified
+	 * here, before staring a translation.
+	 * 
+	 * @param refs
+	 *            A {@link Collection} of all {@link EReference} to be translated.
+	 */
+	public void setTranslatedEReferences(Collection<EReference> refs);
+
+	/**
+	 * Specifies the attributes which shall be translated.
+	 * 
+	 * Note, that all attributes which are used in the constraints need to specified
+	 * here, before staring a translation.
+	 * 
+	 * @param atts
+	 *            A {@link Collection} of all {@link EAttribute} to be translated.
+	 */
+	public void setTranslatedEAttributes(Collection<EAttribute> atts);
+}

org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintBase.java

+/*-------------------------------------------------------------------------+
+| Copyright 2023 fortiss GmbH                                              |
+|                                                                          |
+| Licensed under the Apache License, Version 2.0 (the "License");          |
+| you may not use this file except in compliance with the License.         |
+| You may obtain a copy of the License at                                  |
+|                                                                          |
+|    http://www.apache.org/licenses/LICENSE-2.0                            |
+|                                                                          |
+| Unless required by applicable law or agreed to in writing, software      |
+| distributed under the License is distributed on an "AS IS" BASIS,        |
+| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
+| See the License for the specific language governing permissions and      |
+| limitations under the License.                                           |
++--------------------------------------------------------------------------*/
+package org.fortiss.variability.analysis;
+
+import java.util.HashMap;
+import java.util.Map;
+
+import org.eclipse.emf.ecore.EClass;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.EnumSort;
+import com.microsoft.z3.Expr;
+
+/**
+ * Base class for product line constraints to be checked by the product-line analysis.
+ * 
+ * All constraints are quantified expressions of the form:
+ * [ForAll|Exists] <list of quantifed variables>: <body using quantified variables>
+ * 
+ * @author bayha
+ */
+public abstract class ProductLineConstraintBase implements IProductLineConstraint {
+	/** Prefix to label tracking variables. */
+	private static final String TRACK_PREFIX = "TRACK_";
+
+	/** The body of this constraint. I.e. the quantified expression. */
+	protected BoolExpr body;
+
+	/** The {@link EClass} types of the quantified variables. */
+	protected EClass[] variableTypes;
+
+	/** The names of the quantified variables. */
+	protected String[] variableNames;
+
+	/** The quantified variables */
+	protected Expr<?>[] variables;
+
+	/**
+	 * The tracking constants which are used to extract violating interpretations for the quantifier
+	 * variables.
+	 */
+	protected Expr<?>[] trackerVars;
+
+	/** A map from variable names to expressions which can be used in the body. */
+	protected Map<String, Expr<?>> name2Variables = new HashMap<String, Expr<?>>();
+
+	/** The {@link IProductLineTranslation} to be used for creation of variables. */
+	protected IProductLineTranslation translation;
+
+	/** Constructor. */
+	public ProductLineConstraintBase(IProductLineTranslation translation) {
+		this.translation = translation;
+
+		variableTypes = createVariablesClasses();
+		variableNames = createVariableNames();
+		trackerVars = new Expr[variableNames.length];
+	}
+
+	/** Creates the actual body for this constraint using the quantified variables. */
+	protected abstract BoolExpr createBody();
+
+	/** Specifies the names for the quantified variables. */
+	protected abstract String[] createVariableNames();
+
+	/** Specifies the EClass types for the quantified variables. */
+	protected abstract EClass[] createVariablesClasses();
+
+	/** {@inheritDoc} */
+	@Override
+	public final Expr<?>[] getQuantifierVariables() {
+		if(variables == null) {
+			createVariables();
+		}
+		return variables;
+	}
+
+	/** {@inheritDoc} */
+	@Override
+	public final Expr<?>[] getVariableTracker() {
+		return trackerVars;
+	}
+
+	/** {@inheritDoc} */
+	@Override
+	public final BoolExpr getBody() {
+		if(variables == null) {
+			createVariables();
+		}
+
+		if(body == null) {
+			body = createBody();
+			createTracking();
+		}
+
+		return body;
+	}
+
+	/** {@inheritDoc} */
+	@Override
+	public final EClass[] getVariablesClasses() {
+		return variableTypes;
+	}
+
+	/** Creates tracking variables and adds them to the body. */
+	private final void createTracking() {
+		int numVariables = variableNames.length;
+		BoolExpr[] trackExprs = new BoolExpr[numVariables + 1];
+
+		for(int i = 0; i < variables.length; i++) {
+			trackExprs[i] = translation.getContext().mkEq(trackerVars[i], variables[i]);
+		}
+
+		trackExprs[numVariables] = body;
+
+		body = translation.getContext().mkAnd(trackExprs);
+	}
+
+	/** Creates the Z3 variables for this constraint, using the translation. */
+	private final void createVariables() {
+		int numVariables = variableTypes.length;
+		variables = new Expr[numVariables];
+
+		for(int i = 0; i < numVariables; i++) {
+			EClass ec = variableTypes[i];
+			EnumSort<?> ecSort = translation.getDatatype(ec);
+
+			String varName = variableNames[i];
+			trackerVars[i] = translation.getContext().mkConst(TRACK_PREFIX + varName, ecSort);
+
+			Expr<?> var = translation.getContext().mkConst(varName, ecSort);
+			variables[i] = var;
+			name2Variables.put(varName, var);
+		}
+	}
+}