From 57e614aabedc176ba9965d0ca5e6daa23c5f4758 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 1 Feb 2019 16:03:30 -0500 Subject: Fix FAM Test. Begin Grammar Fix. --- .../VampireLanguageSemanticSequencer.java | 73 +++++++++++++++++++++- 1 file changed, 72 insertions(+), 1 deletion(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java index c300c218..d763a193 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java @@ -14,6 +14,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFalse; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFiniteModel; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionFof; @@ -29,7 +30,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRational; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRevImplies; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrue; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; @@ -99,6 +103,9 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic case VampireLanguagePackage.VLS_FALSE: sequence_VLSAtomicConstant(context, (VLSFalse) semanticObject); return; + case VampireLanguagePackage.VLS_FINITE_MODEL: + sequence_VLSFiniteModel(context, (VLSFiniteModel) semanticObject); + return; case VampireLanguagePackage.VLS_FOF_FORMULA: sequence_VLSFofFormula(context, (VLSFofFormula) semanticObject); return; @@ -144,9 +151,18 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic case VampireLanguagePackage.VLS_REV_IMPLIES: sequence_VLSBinary(context, (VLSRevImplies) semanticObject); return; + case VampireLanguagePackage.VLS_SATISFIABLE: + sequence_VLSSatisfiable(context, (VLSSatisfiable) semanticObject); + return; + case VampireLanguagePackage.VLS_TFF_FORMULA: + sequence_VLSTffFormula(context, (VLSTffFormula) semanticObject); + return; case VampireLanguagePackage.VLS_TRUE: sequence_VLSAtomicConstant(context, (VLSTrue) semanticObject); return; + case VampireLanguagePackage.VLS_TRYING: + sequence_VLSTrying(context, (VLSTrying) semanticObject); + return; case VampireLanguagePackage.VLS_UNARY_NEGATION: sequence_VLSUnaryNegation(context, (VLSUnaryNegation) semanticObject); return; @@ -764,6 +780,18 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic } + /** + * Contexts: + * VLSFiniteModel returns VLSFiniteModel + * + * Constraint: + * {VLSFiniteModel} + */ + protected void sequence_VLSFiniteModel(ISerializationContext context, VLSFiniteModel semanticObject) { + genericSequencer.createSequence(context, semanticObject); + } + + /** * Contexts: * VLSFofFormula returns VLSFofFormula @@ -813,6 +841,49 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic } + /** + * Contexts: + * VLSConfirmations returns VLSSatisfiable + * VLSSatisfiable returns VLSSatisfiable + * + * Constraint: + * {VLSSatisfiable} + */ + protected void sequence_VLSSatisfiable(ISerializationContext context, VLSSatisfiable semanticObject) { + genericSequencer.createSequence(context, semanticObject); + } + + + /** + * Contexts: + * VLSTffFormula returns VLSTffFormula + * + * Constraint: + * ((name=LOWER_WORD_ID | name=SIGNED_LITERAL | name=SINGLE_QUOTE) fofRole=VLSRole fofFormula=VLSTerm annotations=VLSAnnotation?) + */ + protected void sequence_VLSTffFormula(ISerializationContext context, VLSTffFormula semanticObject) { + genericSequencer.createSequence(context, semanticObject); + } + + + /** + * Contexts: + * VLSTrying returns VLSTrying + * + * Constraint: + * name=LITERAL + */ + protected void sequence_VLSTrying(ISerializationContext context, VLSTrying semanticObject) { + if (errorAcceptor != null) { + if (transientValues.isValueTransient(semanticObject, VampireLanguagePackage.Literals.VLS_TRYING__NAME) == ValueTransient.YES) + errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, VampireLanguagePackage.Literals.VLS_TRYING__NAME)); + } + SequenceFeeder feeder = createSequencerFeeder(context, semanticObject); + feeder.accept(grammarAccess.getVLSTryingAccess().getNameLITERALTerminalRuleCall_2_0(), semanticObject.getName()); + feeder.finish(); + } + + /** * Contexts: * VLSTerm returns VLSAssignment @@ -1001,7 +1072,7 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic * VampireModel returns VampireModel * * Constraint: - * (includes+=VLSInclude | comments+=VLSComment | formulas+=VLSFofFormula)+ + * (includes+=VLSInclude | comments+=VLSComment | confirmations+=VLSConfirmations | formulas+=VLSFofFormula | tfformulas+=VLSTffFormula)+ */ protected void sequence_VampireModel(ISerializationContext context, VampireModel semanticObject) { genericSequencer.createSequence(context, semanticObject); -- cgit v1.2.3-70-g09d2