From 8a5c12d1c52498ad9abc11057f6c23456e272585 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Sat, 6 Jun 2020 19:19:18 -0400 Subject: VAMPIRE: Rebase on Master --- .../META-INF/MANIFEST.MF | 24 +++++++++--------- .../vampire/reasoner/queries/VLSAnd.java | 28 ++++++++++++++------- .../vampire/reasoner/queries/VLSAnnotation.java | 28 ++++++++++++++------- .../vampire/reasoner/queries/VLSComment.java | 28 ++++++++++++++------- .../vampire/reasoner/queries/VLSEquivalent.java | 28 ++++++++++++++------- .../reasoner/queries/VLSExistentialQuantifier.java | 28 ++++++++++++++------- .../vampire/reasoner/queries/VLSFofFormula.java | 28 ++++++++++++++------- .../vampire/reasoner/queries/VLSFunction.java | 28 ++++++++++++++------- .../vampire/reasoner/queries/VLSFunctionFof.java | 28 ++++++++++++++------- .../vampire/reasoner/queries/VLSInequality.java | 28 ++++++++++++++------- .../vampire/reasoner/queries/VLSOr.java | 28 ++++++++++++++------- .../vampire/reasoner/queries/VLSUnaryNegation.java | 28 ++++++++++++++------- .../reasoner/queries/VLSUniversalQuantifier.java | 28 ++++++++++++++------- .../.VampireAnalyzerConfiguration.xtendbin | Bin 3449 -> 3449 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 10104 -> 10104 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 19565 -> 19565 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 5080 -> 5080 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 11807 -> 11807 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 7880 -> 7880 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 10684 -> 10684 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 17151 -> 17151 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11037 -> 11037 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 3998 -> 3998 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 7743 -> 7743 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes 27 files changed, 240 insertions(+), 120 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF index 6ed29084..31a52d09 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF @@ -4,19 +4,19 @@ Bundle-Name: Reasoner Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.reasoner;singleton:=true Bundle-Version: 1.0.0.qualifier Export-Package: ca.mcgill.ecse.dslreasoner.vampire.reasoner, - ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder, - ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries + ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder, + ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries Require-Bundle: org.eclipse.emf.ecore, - org.eclipse.viatra.query.runtime.rete, - org.eclipse.viatra.query.runtime.localsearch, - org.eclipse.xtext.xbase.lib, - org.eclipse.xtend.lib, - hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", - ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", - org.eclipse.viatra.query.runtime;bundle-version="2.1.0", - org.eclipse.viatra.query.runtime.base.itc;bundle-version="2.1.0", - org.apache.log4j;bundle-version="1.2.15" + org.eclipse.viatra.query.runtime.rete, + org.eclipse.viatra.query.runtime.localsearch, + org.eclipse.xtext.xbase.lib, + org.eclipse.xtend.lib, + hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", + ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", + org.eclipse.viatra.query.runtime;bundle-version="2.1.0", + org.eclipse.viatra.query.runtime.base.itc;bundle-version="2.1.0", + org.apache.log4j;bundle-version="1.2.15" Bundle-RequiredExecutionEnvironment: JavaSE-1.8 Import-Package: org.apache.log4j Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.reasoner diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSAnd.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSAnd.java index 68bebb93..553d455c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSAnd.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSAnd.java @@ -74,8 +74,18 @@ public final class VLSAnd extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSAnd} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSAnd (visibility: PUBLIC, simpleName: VLSAnd, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSAnd, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSAnd#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSAnd INSTANCE = new VLSAnd(); + private static final VLSAnd INSTANCE = new VLSAnd(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -478,7 +488,7 @@ public final class VLSAnd extends BaseGeneratedEMFQuerySpecification The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -487,7 +497,7 @@ public final class VLSAnd extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSAnnotation} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSAnnotation (visibility: PUBLIC, simpleName: VLSAnnotation, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSAnnotation, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSAnnotation#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSAnnotation INSTANCE = new VLSAnnotation(); + private static final VLSAnnotation INSTANCE = new VLSAnnotation(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -478,7 +488,7 @@ public final class VLSAnnotation extends BaseGeneratedEMFQuerySpecification The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -487,7 +497,7 @@ public final class VLSAnnotation extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSComment} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSComment (visibility: PUBLIC, simpleName: VLSComment, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSComment, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSComment#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSComment INSTANCE = new VLSComment(); + private static final VLSComment INSTANCE = new VLSComment(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -478,7 +488,7 @@ public final class VLSComment extends BaseGeneratedEMFQuerySpecification The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -487,7 +497,7 @@ public final class VLSComment extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSEquivalent} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSEquivalent (visibility: PUBLIC, simpleName: VLSEquivalent, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSEquivalent, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSEquivalent#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSEquivalent INSTANCE = new VLSEquivalent(); + private static final VLSEquivalent INSTANCE = new VLSEquivalent(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -478,7 +488,7 @@ public final class VLSEquivalent extends BaseGeneratedEMFQuerySpecification The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -487,7 +497,7 @@ public final class VLSEquivalent extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSExistentialQuantifier} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSExistentialQuantifier (visibility: PUBLIC, simpleName: VLSExistentialQuantifier, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSExistentialQuantifier, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSExistentialQuantifier#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSExistentialQuantifier INSTANCE = new VLSExistentialQuantifier(); + private static final VLSExistentialQuantifier INSTANCE = new VLSExistentialQuantifier(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -478,7 +488,7 @@ public final class VLSExistentialQuantifier extends BaseGeneratedEMFQuerySpecifi *

The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -487,7 +497,7 @@ public final class VLSExistentialQuantifier extends BaseGeneratedEMFQuerySpecifi } private static class GeneratedPQuery extends BaseGeneratedEMFPQuery { - private final static VLSExistentialQuantifier.GeneratedPQuery INSTANCE = new GeneratedPQuery(); + private static final VLSExistentialQuantifier.GeneratedPQuery INSTANCE = new GeneratedPQuery(); private final PParameter parameter_term = new PParameter("term", "ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage", "VLSExistentialQuantifier")), PParameterDirection.INOUT); diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSFofFormula.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSFofFormula.java index e35ffaa2..666795b5 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSFofFormula.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/VLSFofFormula.java @@ -74,8 +74,18 @@ public final class VLSFofFormula extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSFofFormula} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSFofFormula (visibility: PUBLIC, simpleName: VLSFofFormula, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSFofFormula, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSFofFormula#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSFofFormula INSTANCE = new VLSFofFormula(); + private static final VLSFofFormula INSTANCE = new VLSFofFormula(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -478,7 +488,7 @@ public final class VLSFofFormula extends BaseGeneratedEMFQuerySpecification The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -487,7 +497,7 @@ public final class VLSFofFormula extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSFunction} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSFunction (visibility: PUBLIC, simpleName: VLSFunction, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSFunction, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSFunction#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSFunction INSTANCE = new VLSFunction(); + private static final VLSFunction INSTANCE = new VLSFunction(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -478,7 +488,7 @@ public final class VLSFunction extends BaseGeneratedEMFQuerySpecification The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -487,7 +497,7 @@ public final class VLSFunction extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSFunctionFof} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSFunctionFof (visibility: PUBLIC, simpleName: VLSFunctionFof, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSFunctionFof, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSFunctionFof#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSFunctionFof INSTANCE = new VLSFunctionFof(); + private static final VLSFunctionFof INSTANCE = new VLSFunctionFof(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -479,7 +489,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -488,7 +498,7 @@ public final class VLSFunctionFof extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSInequality} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSInequality (visibility: PUBLIC, simpleName: VLSInequality, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSInequality, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSInequality#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSInequality INSTANCE = new VLSInequality(); + private static final VLSInequality INSTANCE = new VLSInequality(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -478,7 +488,7 @@ public final class VLSInequality extends BaseGeneratedEMFQuerySpecification The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -487,7 +497,7 @@ public final class VLSInequality extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSOr} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSOr (visibility: PUBLIC, simpleName: VLSOr, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSOr, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSOr#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSOr INSTANCE = new VLSOr(); + private static final VLSOr INSTANCE = new VLSOr(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -480,7 +490,7 @@ public final class VLSOr extends BaseGeneratedEMFQuerySpecification The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -489,7 +499,7 @@ public final class VLSOr extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSUnaryNegation} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSUnaryNegation (visibility: PUBLIC, simpleName: VLSUnaryNegation, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSUnaryNegation, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSUnaryNegation#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSUnaryNegation INSTANCE = new VLSUnaryNegation(); + private static final VLSUnaryNegation INSTANCE = new VLSUnaryNegation(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -478,7 +488,7 @@ public final class VLSUnaryNegation extends BaseGeneratedEMFQuerySpecification The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -487,7 +497,7 @@ public final class VLSUnaryNegation extends BaseGeneratedEMFQuerySpecification) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)} to be created + * Inner class allowing the singleton instance of {@link VLSUniversalQuantifier} to be created * not at the class load time of the outer class, - * but rather at the first call to {@link JvmGenericType: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSUniversalQuantifier (visibility: PUBLIC, simpleName: VLSUniversalQuantifier, identifier: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries.VLSUniversalQuantifier, deprecated: ) (abstract: false, static: false, final: true, packageName: ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries) (interface: false, strictFloatingPoint: false, anonymous: false)#instance()}. + * but rather at the first call to {@link VLSUniversalQuantifier#instance()}. * *

This workaround is required e.g. to support recursion. * */ private static class LazyHolder { - private final static VLSUniversalQuantifier INSTANCE = new VLSUniversalQuantifier(); + private static final VLSUniversalQuantifier INSTANCE = new VLSUniversalQuantifier(); /** * Statically initializes the query specification after the field {@link #INSTANCE} is assigned. @@ -478,7 +488,7 @@ public final class VLSUniversalQuantifier extends BaseGeneratedEMFQuerySpecifica *

The static initializer is defined using a helper field to work around limitations of the code generator. * */ - private final static Object STATIC_INITIALIZER = ensureInitialized(); + private static final Object STATIC_INITIALIZER = ensureInitialized(); public static Object ensureInitialized() { INSTANCE.ensureInitializedInternal(); @@ -487,7 +497,7 @@ public final class VLSUniversalQuantifier extends BaseGeneratedEMFQuerySpecifica } private static class GeneratedPQuery extends BaseGeneratedEMFPQuery { - private final static VLSUniversalQuantifier.GeneratedPQuery INSTANCE = new GeneratedPQuery(); + private static final VLSUniversalQuantifier.GeneratedPQuery INSTANCE = new GeneratedPQuery(); private final PParameter parameter_term = new PParameter("term", "ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier", new EClassTransitiveInstancesKey((EClass)getClassifierLiteralSafe("http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage", "VLSUniversalQuantifier")), PParameterDirection.INOUT); diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index d21e62df..e999bce6 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index 6fa1ad33..28154d14 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 16598303..18da19a9 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index 760c5e1f..37c845cd 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index db66ddba..d8c61adc 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index d6fe4078..1a86a55f 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index 81468f27..216b3a4b 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index d6924639..8733e530 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index 9541df30..634dab6a 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index bb87d246..28c93f34 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index 61879add..faef07c1 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 1d6d6da8..3d96efbf 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index 3a055e01..b3756706 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index e7c2bd91..f75b4eaf 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin differ -- cgit v1.2.3-54-g00ecf