Commit 9f7e1bfe authored by Johannes Eder's avatar Johannes Eder

moved SMTConstraint and SMTObjective from efficientdeployment to z3 plugin

parent 0354ed82
......@@ -15,7 +15,20 @@ Bundle-NativeCode: lib/x64/libz3.so ; lib/x64/libz3java.so ; osname = linux ; pr
lib/x64/libz3.dylib ; lib/x64/libz3java.dylib ; osname = macosx ; processor = x86_64,
lib/x32/libz3.so ; lib/x32/libz3java.so ; osname = linux ; processor = x86,
lib/x32/libz3.dll ; lib/x32/libz3java.dll ; lib/x32/msvcp110dll ; lib/x32/msvcr110.dll ; lib/x32/vcomp110.dll ; lib/x32/Microsoft.Z3.dll ; osname = win32 ; osname = Windows 7 ; osname = Windows7 ; osname = Win7 ; processor = x86
Require-Bundle: org.eclipse.core.runtime;bundle-version="3.9.100"
Require-Bundle: org.eclipse.core.runtime;bundle-version="3.9.100",
org.eclipse.emf.ecore;visibility:=reexport,
org.fortiss.tooling.base;visibility:=reexport,
org.fortiss.af3.component;visibility:=reexport,
org.fortiss.af3.exploration;visibility:=reexport,
org.fortiss.af3.expression;visibility:=reexport,
org.fortiss.af3.platform;visibility:=reexport,
org.fortiss.af3.project;visibility:=reexport,
org.fortiss.af3.safety;visibility:=reexport,
org.fortiss.tooling.kernel;visibility:=reexport
Export-Package: com.microsoft.z3,
com.microsoft.z3.enumerations
com.microsoft.z3.enumerations,
com.microsoft.z3.model,
com.microsoft.z3.model.impl,
com.microsoft.z3.model.util,
com.microsoft.z3.util
Eclipse-BundleShape: dir
/**
*/
package com.microsoft.z3.model;
import org.fortiss.af3.exploration.model.ConstraintExpression;
/**
* <!-- begin-user-doc -->
* A representation of the model object '<em><b>SMT Constraint</b></em>'.
* <!-- end-user-doc -->
*
*
* @see com.microsoft.z3.model.Z3ProjectPackage#getSMTConstraint()
* @model superTypes="org.fortiss.af3.exploration.model.ConstraintExpression<org.eclipse.emf.ecore.EBooleanObject>"
* @generated
*/
public interface SMTConstraint extends ConstraintExpression<Boolean> {
} // SMTConstraint
/**
*/
package com.microsoft.z3.model;
import org.fortiss.af3.exploration.model.ObjectiveExpression;
/**
* <!-- begin-user-doc -->
* A representation of the model object '<em><b>SMT Objective</b></em>'.
* <!-- end-user-doc -->
*
*
* @see com.microsoft.z3.model.Z3ProjectPackage#getSMTObjective()
* @model superTypes="org.fortiss.af3.exploration.model.ObjectiveExpression<org.eclipse.emf.ecore.EBooleanObject>"
* @generated
*/
public interface SMTObjective extends ObjectiveExpression<Boolean> {
} // SMTObjective
/**
*/
package com.microsoft.z3.model;
import org.eclipse.emf.ecore.EFactory;
/**
* <!-- begin-user-doc -->
* The <b>Factory</b> for the model.
* It provides a create method for each non-abstract class of the model.
* <!-- end-user-doc -->
* @see com.microsoft.z3.model.Z3ProjectPackage
* @generated
*/
public interface Z3ProjectFactory extends EFactory {
/**
* The singleton instance of the factory.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
Z3ProjectFactory eINSTANCE = com.microsoft.z3.model.impl.Z3ProjectFactoryImpl.init();
/**
* Returns a new object of class '<em>SMT Constraint</em>'.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @return a new object of class '<em>SMT Constraint</em>'.
* @generated
*/
SMTConstraint createSMTConstraint();
/**
* Returns a new object of class '<em>SMT Objective</em>'.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @return a new object of class '<em>SMT Objective</em>'.
* @generated
*/
SMTObjective createSMTObjective();
/**
* Returns the package supported by this factory.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @return the package supported by this factory.
* @generated
*/
Z3ProjectPackage getZ3ProjectPackage();
} //Z3ProjectFactory
/**
*/
package com.microsoft.z3.model;
import org.eclipse.emf.ecore.EClass;
import org.eclipse.emf.ecore.EPackage;
import org.fortiss.af3.exploration.model.ExplorationPackage;
/**
* <!-- begin-user-doc -->
* The <b>Package</b> for the model.
* It contains accessors for the meta objects to represent
* <ul>
* <li>each class,</li>
* <li>each feature of each class,</li>
* <li>each enum,</li>
* <li>and each data type</li>
* </ul>
* <!-- end-user-doc -->
* @see com.microsoft.z3.model.Z3ProjectFactory
* @model kind="package"
* @generated
*/
public interface Z3ProjectPackage extends EPackage {
/**
* The package name.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
String eNAME = "model";
/**
* The package namespace URI.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
String eNS_URI = "http://www.microsoft.com/z3";
/**
* The package namespace name.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
String eNS_PREFIX = "com-microsoft-z3";
/**
* The singleton instance of the package.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
Z3ProjectPackage eINSTANCE = com.microsoft.z3.model.impl.Z3ProjectPackageImpl.init();
/**
* The meta object id for the '{@link com.microsoft.z3.model.impl.SMTConstraintImpl <em>SMT Constraint</em>}' class.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @see com.microsoft.z3.model.impl.SMTConstraintImpl
* @see com.microsoft.z3.model.impl.Z3ProjectPackageImpl#getSMTConstraint()
* @generated
*/
int SMT_CONSTRAINT = 0;
/**
* The feature id for the '<em><b>Id</b></em>' attribute.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_CONSTRAINT__ID = ExplorationPackage.CONSTRAINT_EXPRESSION__ID;
/**
* The feature id for the '<em><b>Name</b></em>' attribute.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_CONSTRAINT__NAME = ExplorationPackage.CONSTRAINT_EXPRESSION__NAME;
/**
* The feature id for the '<em><b>Comment</b></em>' attribute.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_CONSTRAINT__COMMENT = ExplorationPackage.CONSTRAINT_EXPRESSION__COMMENT;
/**
* The feature id for the '<em><b>Is Soft</b></em>' attribute.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_CONSTRAINT__IS_SOFT = ExplorationPackage.CONSTRAINT_EXPRESSION__IS_SOFT;
/**
* The feature id for the '<em><b>Implicit</b></em>' attribute.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_CONSTRAINT__IMPLICIT = ExplorationPackage.CONSTRAINT_EXPRESSION__IMPLICIT;
/**
* The feature id for the '<em><b>Expression</b></em>' containment reference.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_CONSTRAINT__EXPRESSION = ExplorationPackage.CONSTRAINT_EXPRESSION__EXPRESSION;
/**
* The number of structural features of the '<em>SMT Constraint</em>' class.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_CONSTRAINT_FEATURE_COUNT = ExplorationPackage.CONSTRAINT_EXPRESSION_FEATURE_COUNT + 0;
/**
* The meta object id for the '{@link com.microsoft.z3.model.impl.SMTObjectiveImpl <em>SMT Objective</em>}' class.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @see com.microsoft.z3.model.impl.SMTObjectiveImpl
* @see com.microsoft.z3.model.impl.Z3ProjectPackageImpl#getSMTObjective()
* @generated
*/
int SMT_OBJECTIVE = 1;
/**
* The feature id for the '<em><b>Id</b></em>' attribute.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_OBJECTIVE__ID = ExplorationPackage.OBJECTIVE_EXPRESSION__ID;
/**
* The feature id for the '<em><b>Name</b></em>' attribute.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_OBJECTIVE__NAME = ExplorationPackage.OBJECTIVE_EXPRESSION__NAME;
/**
* The feature id for the '<em><b>Comment</b></em>' attribute.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_OBJECTIVE__COMMENT = ExplorationPackage.OBJECTIVE_EXPRESSION__COMMENT;
/**
* The feature id for the '<em><b>Expression</b></em>' containment reference.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_OBJECTIVE__EXPRESSION = ExplorationPackage.OBJECTIVE_EXPRESSION__EXPRESSION;
/**
* The number of structural features of the '<em>SMT Objective</em>' class.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
* @ordered
*/
int SMT_OBJECTIVE_FEATURE_COUNT = ExplorationPackage.OBJECTIVE_EXPRESSION_FEATURE_COUNT + 0;
/**
* Returns the meta object for class '{@link com.microsoft.z3.model.SMTConstraint <em>SMT Constraint</em>}'.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @return the meta object for class '<em>SMT Constraint</em>'.
* @see com.microsoft.z3.model.SMTConstraint
* @generated
*/
EClass getSMTConstraint();
/**
* Returns the meta object for class '{@link com.microsoft.z3.model.SMTObjective <em>SMT Objective</em>}'.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @return the meta object for class '<em>SMT Objective</em>'.
* @see com.microsoft.z3.model.SMTObjective
* @generated
*/
EClass getSMTObjective();
/**
* Returns the factory that creates the instances of the model.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @return the factory that creates the instances of the model.
* @generated
*/
Z3ProjectFactory getZ3ProjectFactory();
/**
* <!-- begin-user-doc -->
* Defines literals for the meta objects that represent
* <ul>
* <li>each class,</li>
* <li>each feature of each class,</li>
* <li>each enum,</li>
* <li>and each data type</li>
* </ul>
* <!-- end-user-doc -->
* @generated
*/
interface Literals {
/**
* The meta object literal for the '{@link com.microsoft.z3.model.impl.SMTConstraintImpl <em>SMT Constraint</em>}' class.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @see com.microsoft.z3.model.impl.SMTConstraintImpl
* @see com.microsoft.z3.model.impl.Z3ProjectPackageImpl#getSMTConstraint()
* @generated
*/
EClass SMT_CONSTRAINT = eINSTANCE.getSMTConstraint();
/**
* The meta object literal for the '{@link com.microsoft.z3.model.impl.SMTObjectiveImpl <em>SMT Objective</em>}' class.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @see com.microsoft.z3.model.impl.SMTObjectiveImpl
* @see com.microsoft.z3.model.impl.Z3ProjectPackageImpl#getSMTObjective()
* @generated
*/
EClass SMT_OBJECTIVE = eINSTANCE.getSMTObjective();
}
} //Z3ProjectPackage
/**
*/
package com.microsoft.z3.model.impl;
import com.microsoft.z3.model.*;
import org.eclipse.emf.ecore.EClass;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.EPackage;
import org.eclipse.emf.ecore.impl.EFactoryImpl;
import org.eclipse.emf.ecore.plugin.EcorePlugin;
/**
* <!-- begin-user-doc -->
* An implementation of the model <b>Factory</b>.
* <!-- end-user-doc -->
* @generated
*/
public class Z3ProjectFactoryImpl extends EFactoryImpl implements Z3ProjectFactory {
/**
* Creates the default factory implementation.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
public static Z3ProjectFactory init() {
try {
Z3ProjectFactory theZ3ProjectFactory = (Z3ProjectFactory)EPackage.Registry.INSTANCE.getEFactory(Z3ProjectPackage.eNS_URI);
if (theZ3ProjectFactory != null) {
return theZ3ProjectFactory;
}
}
catch (Exception exception) {
EcorePlugin.INSTANCE.log(exception);
}
return new Z3ProjectFactoryImpl();
}
/**
* Creates an instance of the factory.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
public Z3ProjectFactoryImpl() {
super();
}
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
@Override
public EObject create(EClass eClass) {
switch (eClass.getClassifierID()) {
case Z3ProjectPackage.SMT_CONSTRAINT: return createSMTConstraint();
case Z3ProjectPackage.SMT_OBJECTIVE: return createSMTObjective();
default:
throw new IllegalArgumentException("The class '" + eClass.getName() + "' is not a valid classifier");
}
}
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
public SMTConstraint createSMTConstraint() {
SMTConstraintImpl smtConstraint = new SMTConstraintImpl();
return smtConstraint;
}
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
public SMTObjective createSMTObjective() {
SMTObjectiveImpl smtObjective = new SMTObjectiveImpl();
return smtObjective;
}
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
public Z3ProjectPackage getZ3ProjectPackage() {
return (Z3ProjectPackage)getEPackage();
}
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @deprecated
* @generated
*/
@Deprecated
public static Z3ProjectPackage getPackage() {
return Z3ProjectPackage.eINSTANCE;
}
} //Z3ProjectFactoryImpl
/**
*/
package com.microsoft.z3.model.impl;
import com.microsoft.z3.model.SMTConstraint;
import com.microsoft.z3.model.SMTObjective;
import com.microsoft.z3.model.Z3ProjectFactory;
import com.microsoft.z3.model.Z3ProjectPackage;
import org.eclipse.emf.ecore.EClass;
import org.eclipse.emf.ecore.EGenericType;
import org.eclipse.emf.ecore.EPackage;
import org.eclipse.emf.ecore.impl.EPackageImpl;
import org.fortiss.af3.exploration.model.ExplorationPackage;
/**
* <!-- begin-user-doc -->
* An implementation of the model <b>Package</b>.
* <!-- end-user-doc -->
* @generated
*/
public class Z3ProjectPackageImpl extends EPackageImpl implements Z3ProjectPackage {
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
private EClass smtConstraintEClass = null;
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
private EClass smtObjectiveEClass = null;
/**
* Creates an instance of the model <b>Package</b>, registered with
* {@link org.eclipse.emf.ecore.EPackage.Registry EPackage.Registry} by the package
* package URI value.
* <p>Note: the correct way to create the package is via the static
* factory method {@link #init init()}, which also performs
* initialization of the package, or returns the registered package,
* if one already exists.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @see org.eclipse.emf.ecore.EPackage.Registry
* @see com.microsoft.z3.model.Z3ProjectPackage#eNS_URI
* @see #init()
* @generated
*/
private Z3ProjectPackageImpl() {
super(eNS_URI, Z3ProjectFactory.eINSTANCE);
}
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
private static boolean isInited = false;
/**
* Creates, registers, and initializes the <b>Package</b> for this model, and for any others upon which it depends.
*
* <p>This method is used to initialize {@link Z3ProjectPackage#eINSTANCE} when that field is accessed.
* Clients should not invoke it directly. Instead, they should simply access that field to obtain the package.
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @see #eNS_URI
* @see #createPackageContents()
* @see #initializePackageContents()
* @generated
*/
public static Z3ProjectPackage init() {
if (isInited) return (Z3ProjectPackage)EPackage.Registry.INSTANCE.getEPackage(Z3ProjectPackage.eNS_URI);
// Obtain or create and register package
Z3ProjectPackageImpl theZ3ProjectPackage = (Z3ProjectPackageImpl)(EPackage.Registry.INSTANCE.get(eNS_URI) instanceof Z3ProjectPackageImpl ? EPackage.Registry.INSTANCE.get(eNS_URI) : new Z3ProjectPackageImpl());
isInited = true;
// Initialize simple dependencies
ExplorationPackage.eINSTANCE.eClass();
// Create package meta-data objects
theZ3ProjectPackage.createPackageContents();
// Initialize created meta-data
theZ3ProjectPackage.initializePackageContents();
// Mark meta-data to indicate it can't be changed
theZ3ProjectPackage.freeze();
// Update the registry and return the package
EPackage.Registry.INSTANCE.put(Z3ProjectPackage.eNS_URI, theZ3ProjectPackage);
return theZ3ProjectPackage;
}
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
public EClass getSMTConstraint() {
return smtConstraintEClass;
}
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
public EClass getSMTObjective() {
return smtObjectiveEClass;
}
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
public Z3ProjectFactory getZ3ProjectFactory() {
return (Z3ProjectFactory)getEFactoryInstance();
}
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @generated
*/
private boolean isCreated = false;
/**
* Creates the meta-model objects for the package. This method is
* guarded to have no affect on any invocation but its first.
* <!-- begin-user-doc -->