VAMPIRE: Implement Vampire measurement code

3 files changed, 180 insertions, 32 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTermImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTermImpl.java
index c56d7ecd..9f1fa64f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTermImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VLSTermImpl.java
@@ -6,18 +6,48 @@ package ca.mcgill.ecse.dslreasoner.vampireLanguage.impl;
 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;

 

+import org.eclipse.emf.common.notify.Notification;

+

 import org.eclipse.emf.ecore.EClass;

 

+import org.eclipse.emf.ecore.impl.ENotificationImpl;

+

 /**

  * <!-- begin-user-doc -->

  * An implementation of the model object '<em><b>VLS Term</b></em>'.

  * <!-- end-user-doc -->

+ * <p>

+ * The following features are implemented:

+ * </p>

+ * <ul>

+ *   <li>{@link ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VLSTermImpl#getComment <em>Comment</em>}</li>

+ * </ul>

  *

  * @generated

  */

 public class VLSTermImpl extends VLSTffTermImpl implements VLSTerm

 {

   /**

+   * The default value of the '{@link #getComment() <em>Comment</em>}' attribute.

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @see #getComment()

+   * @generated

+   * @ordered

+   */

+  protected static final String COMMENT_EDEFAULT = null;

+

+  /**

+   * The cached value of the '{@link #getComment() <em>Comment</em>}' attribute.

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @see #getComment()

+   * @generated

+   * @ordered

+   */

+  protected String comment = COMMENT_EDEFAULT;

+

+  /**

    * <!-- begin-user-doc -->

    * <!-- end-user-doc -->

    * @generated

@@ -38,4 +68,110 @@ public class VLSTermImpl extends VLSTffTermImpl implements VLSTerm
     return VampireLanguagePackage.Literals.VLS_TERM;

   }

 

+  /**

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @generated

+   */

+  public String getComment()

+  {

+    return comment;

+  }

+

+  /**

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @generated

+   */

+  public void setComment(String newComment)

+  {

+    String oldComment = comment;

+    comment = newComment;

+    if (eNotificationRequired())

+      eNotify(new ENotificationImpl(this, Notification.SET, VampireLanguagePackage.VLS_TERM__COMMENT, oldComment, comment));

+  }

+

+  /**

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @generated

+   */

+  @Override

+  public Object eGet(int featureID, boolean resolve, boolean coreType)

+  {

+    switch (featureID)

+    {

+      case VampireLanguagePackage.VLS_TERM__COMMENT:

+        return getComment();

+    }

+    return super.eGet(featureID, resolve, coreType);

+  }

+

+  /**

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @generated

+   */

+  @Override

+  public void eSet(int featureID, Object newValue)

+  {

+    switch (featureID)

+    {

+      case VampireLanguagePackage.VLS_TERM__COMMENT:

+        setComment((String)newValue);

+        return;

+    }

+    super.eSet(featureID, newValue);

+  }

+

+  /**

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @generated

+   */

+  @Override

+  public void eUnset(int featureID)

+  {

+    switch (featureID)

+    {

+      case VampireLanguagePackage.VLS_TERM__COMMENT:

+        setComment(COMMENT_EDEFAULT);

+        return;

+    }

+    super.eUnset(featureID);

+  }

+

+  /**

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @generated

+   */

+  @Override

+  public boolean eIsSet(int featureID)

+  {

+    switch (featureID)

+    {

+      case VampireLanguagePackage.VLS_TERM__COMMENT:

+        return COMMENT_EDEFAULT == null ? comment != null : !COMMENT_EDEFAULT.equals(comment);

+    }

+    return super.eIsSet(featureID);

+  }

+

+  /**

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @generated

+   */

+  @Override

+  public String toString()

+  {

+    if (eIsProxy()) return super.toString();

+

+    StringBuilder result = new StringBuilder(super.toString());

+    result.append(" (comment: ");

+    result.append(comment);

+    result.append(')');

+    return result.toString();

+  }

+

 } //VLSTermImpl

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguageFactoryImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguageFactoryImpl.java
index 0e25a4cc..c87155c9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguageFactoryImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguageFactoryImpl.java
@@ -72,11 +72,11 @@ public class VampireLanguageFactoryImpl extends EFactoryImpl implements VampireL
       case VampireLanguagePackage.VLS_TFF_FORMULA: return createVLSTffFormula();

       case VampireLanguagePackage.VLS_ANNOTATION: return createVLSAnnotation();

       case VampireLanguagePackage.VLS_TFF_TERM: return createVLSTffTerm();

+      case VampireLanguagePackage.VLS_TERM: return createVLSTerm();

       case VampireLanguagePackage.VLS_DECLARATION: return createVLSDeclaration();

       case VampireLanguagePackage.VLS_OTHER_DECLARATION: return createVLSOtherDeclaration();

       case VampireLanguagePackage.VLS_VARIABLE_DECLARATION: return createVLSVariableDeclaration();

       case VampireLanguagePackage.VLS_TYPE_DEF: return createVLSTypeDef();

-      case VampireLanguagePackage.VLS_TERM: return createVLSTerm();

       case VampireLanguagePackage.VLS_VARIABLE: return createVLSVariable();

       case VampireLanguagePackage.VLS_FUNCTION_AS_TERM: return createVLSFunctionAsTerm();

       case VampireLanguagePackage.VLS_DEFINED_TERM: return createVLSDefinedTerm();

@@ -192,6 +192,17 @@ public class VampireLanguageFactoryImpl extends EFactoryImpl implements VampireL
    * <!-- end-user-doc -->

    * @generated

    */

+  public VLSTerm createVLSTerm()

+  {

+    VLSTermImpl vlsTerm = new VLSTermImpl();

+    return vlsTerm;

+  }

+

+  /**

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @generated

+   */

   public VLSDeclaration createVLSDeclaration()

   {

     VLSDeclarationImpl vlsDeclaration = new VLSDeclarationImpl();

@@ -236,17 +247,6 @@ public class VampireLanguageFactoryImpl extends EFactoryImpl implements VampireL
    * <!-- end-user-doc -->

    * @generated

    */

-  public VLSTerm createVLSTerm()

-  {

-    VLSTermImpl vlsTerm = new VLSTermImpl();

-    return vlsTerm;

-  }

-

-  /**

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   */

   public VLSVariable createVLSVariable()

   {

     VLSVariableImpl vlsVariable = new VLSVariableImpl();

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
index 676b2786..eae57e97 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/vampireLanguage/impl/VampireLanguagePackageImpl.java
@@ -115,35 +115,35 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    * <!-- end-user-doc -->

    * @generated

    */

-  private EClass vlsDeclarationEClass = null;

+  private EClass vlsTermEClass = null;

 

   /**

    * <!-- begin-user-doc -->

    * <!-- end-user-doc -->

    * @generated

    */

-  private EClass vlsOtherDeclarationEClass = null;

+  private EClass vlsDeclarationEClass = null;

 

   /**

    * <!-- begin-user-doc -->

    * <!-- end-user-doc -->

    * @generated

    */

-  private EClass vlsVariableDeclarationEClass = null;

+  private EClass vlsOtherDeclarationEClass = null;

 

   /**

    * <!-- begin-user-doc -->

    * <!-- end-user-doc -->

    * @generated

    */

-  private EClass vlsTypeDefEClass = null;

+  private EClass vlsVariableDeclarationEClass = null;

 

   /**

    * <!-- begin-user-doc -->

    * <!-- end-user-doc -->

    * @generated

    */

-  private EClass vlsTermEClass = null;

+  private EClass vlsTypeDefEClass = null;

 

   /**

    * <!-- begin-user-doc -->

@@ -639,6 +639,26 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    * <!-- end-user-doc -->

    * @generated

    */

+  public EClass getVLSTerm()

+  {

+    return vlsTermEClass;

+  }

+

+  /**

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @generated

+   */

+  public EAttribute getVLSTerm_Comment()

+  {

+    return (EAttribute)vlsTermEClass.getEStructuralFeatures().get(0);

+  }

+

+  /**

+   * <!-- begin-user-doc -->

+   * <!-- end-user-doc -->

+   * @generated

+   */

   public EClass getVLSDeclaration()

   {

     return vlsDeclarationEClass;

@@ -749,16 +769,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
    * <!-- end-user-doc -->

    * @generated

    */

-  public EClass getVLSTerm()

-  {

-    return vlsTermEClass;

-  }

-

-  /**

-   * <!-- begin-user-doc -->

-   * <!-- end-user-doc -->

-   * @generated

-   */

   public EClass getVLSVariable()

   {

     return vlsVariableEClass;

@@ -1464,6 +1474,9 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
 

     vlsTffTermEClass = createEClass(VLS_TFF_TERM);

 

+    vlsTermEClass = createEClass(VLS_TERM);

+    createEAttribute(vlsTermEClass, VLS_TERM__COMMENT);

+

     vlsDeclarationEClass = createEClass(VLS_DECLARATION);

     createEReference(vlsDeclarationEClass, VLS_DECLARATION__TYPE);

 

@@ -1479,8 +1492,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
     createEReference(vlsTypeDefEClass, VLS_TYPE_DEF__INIT_TYPE);

     createEReference(vlsTypeDefEClass, VLS_TYPE_DEF__NEXT_TYPE);

 

-    vlsTermEClass = createEClass(VLS_TERM);

-

     vlsVariableEClass = createEClass(VLS_VARIABLE);

     createEAttribute(vlsVariableEClass, VLS_VARIABLE__NAME);

 

@@ -1604,10 +1615,10 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
     // Set bounds for type parameters

 

     // Add supertypes to classes

+    vlsTermEClass.getESuperTypes().add(this.getVLSTffTerm());

     vlsDeclarationEClass.getESuperTypes().add(this.getVLSTffTerm());

     vlsOtherDeclarationEClass.getESuperTypes().add(this.getVLSDeclaration());

     vlsVariableDeclarationEClass.getESuperTypes().add(this.getVLSDeclaration());

-    vlsTermEClass.getESuperTypes().add(this.getVLSTffTerm());

     vlsVariableEClass.getESuperTypes().add(this.getVLSTerm());

     vlsFunctionAsTermEClass.getESuperTypes().add(this.getVLSTerm());

     vlsDefinedTermEClass.getESuperTypes().add(this.getVLSTerm());

@@ -1668,6 +1679,9 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
 

     initEClass(vlsTffTermEClass, VLSTffTerm.class, "VLSTffTerm", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

 

+    initEClass(vlsTermEClass, VLSTerm.class, "VLSTerm", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

+    initEAttribute(getVLSTerm_Comment(), ecorePackage.getEString(), "comment", null, 0, 1, VLSTerm.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);

+

     initEClass(vlsDeclarationEClass, VLSDeclaration.class, "VLSDeclaration", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

     initEReference(getVLSDeclaration_Type(), this.getVLSTypeDef(), null, "type", null, 0, 1, VLSDeclaration.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);

 

@@ -1683,8 +1697,6 @@ public class VampireLanguagePackageImpl extends EPackageImpl implements VampireL
     initEReference(getVLSTypeDef_InitType(), this.getVLSTerm(), null, "initType", null, 0, 1, VLSTypeDef.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);

     initEReference(getVLSTypeDef_NextType(), this.getVLSTerm(), null, "nextType", null, 0, 1, VLSTypeDef.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);

 

-    initEClass(vlsTermEClass, VLSTerm.class, "VLSTerm", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

-

     initEClass(vlsVariableEClass, VLSVariable.class, "VLSVariable", !IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS);

     initEAttribute(getVLSVariable_Name(), ecorePackage.getEString(), "name", null, 0, 1, VLSVariable.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED);