diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-07 00:35:42 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:42:47 -0400 |
commit | b503c81bee920c18806af25393d0a90b8f77dba6 (patch) | |
tree | 9b70f606bfa7fa450457c04714e045e5ac5f6199 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java | |
parent | VAMPIRE: fix model generation (diff) | |
download | VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.tar.gz VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.tar.zst VIATRA-Generator-b503c81bee920c18806af25393d0a90b8f77dba6.zip |
VAMPIRE: Implement Vampire measurement code
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src-gen/ca/mcgill/ecse/dslreasoner/serializer/VampireLanguageSemanticSequencer.java | 31 |
1 files changed, 27 insertions, 4 deletions
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 67be7b9a..884180e1 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 | |||
@@ -28,6 +28,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; | |||
28 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOtherDeclaration; | 28 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOtherDeclaration; |
29 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRevImplies; | 29 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSRevImplies; |
30 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable; | 30 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSSatisfiable; |
31 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
31 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula; | 32 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffFormula; |
32 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrue; | 33 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrue; |
33 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying; | 34 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTrying; |
@@ -145,6 +146,9 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
145 | case VampireLanguagePackage.VLS_SATISFIABLE: | 146 | case VampireLanguagePackage.VLS_SATISFIABLE: |
146 | sequence_VLSConfirmations(context, (VLSSatisfiable) semanticObject); | 147 | sequence_VLSConfirmations(context, (VLSSatisfiable) semanticObject); |
147 | return; | 148 | return; |
149 | case VampireLanguagePackage.VLS_TERM: | ||
150 | sequence_VLSCommentTerm(context, (VLSTerm) semanticObject); | ||
151 | return; | ||
148 | case VampireLanguagePackage.VLS_TFF_FORMULA: | 152 | case VampireLanguagePackage.VLS_TFF_FORMULA: |
149 | sequence_VLSTffFormula(context, (VLSTffFormula) semanticObject); | 153 | sequence_VLSTffFormula(context, (VLSTffFormula) semanticObject); |
150 | return; | 154 | return; |
@@ -621,6 +625,25 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
621 | 625 | ||
622 | /** | 626 | /** |
623 | * Contexts: | 627 | * Contexts: |
628 | * VLSTffTerm returns VLSTerm | ||
629 | * VLSCommentTerm returns VLSTerm | ||
630 | * | ||
631 | * Constraint: | ||
632 | * comment=SINGLE_COMMENT | ||
633 | */ | ||
634 | protected void sequence_VLSCommentTerm(ISerializationContext context, VLSTerm semanticObject) { | ||
635 | if (errorAcceptor != null) { | ||
636 | if (transientValues.isValueTransient(semanticObject, VampireLanguagePackage.Literals.VLS_TERM__COMMENT) == ValueTransient.YES) | ||
637 | errorAcceptor.accept(diagnosticProvider.createFeatureValueMissing(semanticObject, VampireLanguagePackage.Literals.VLS_TERM__COMMENT)); | ||
638 | } | ||
639 | SequenceFeeder feeder = createSequencerFeeder(context, semanticObject); | ||
640 | feeder.accept(grammarAccess.getVLSCommentTermAccess().getCommentSINGLE_COMMENTTerminalRuleCall_0(), semanticObject.getComment()); | ||
641 | feeder.finish(); | ||
642 | } | ||
643 | |||
644 | |||
645 | /** | ||
646 | * Contexts: | ||
624 | * VLSComment returns VLSComment | 647 | * VLSComment returns VLSComment |
625 | * | 648 | * |
626 | * Constraint: | 649 | * Constraint: |
@@ -782,8 +805,8 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
782 | * Constraint: | 805 | * Constraint: |
783 | * ( | 806 | * ( |
784 | * (variables+=VLSVariable | variables+=VLSVariableDeclaration) | 807 | * (variables+=VLSVariable | variables+=VLSVariableDeclaration) |
785 | * variables+=VLSVariableDeclaration? | 808 | * variables+=VLSVariable? |
786 | * (variables+=VLSVariable? variables+=VLSVariableDeclaration?)* | 809 | * (variables+=VLSVariableDeclaration? variables+=VLSVariable?)* |
787 | * operand=VLSUnitaryFormula | 810 | * operand=VLSUnitaryFormula |
788 | * ) | 811 | * ) |
789 | */ | 812 | */ |
@@ -1024,8 +1047,8 @@ public class VampireLanguageSemanticSequencer extends AbstractDelegatingSemantic | |||
1024 | * Constraint: | 1047 | * Constraint: |
1025 | * ( | 1048 | * ( |
1026 | * (variables+=VLSVariable | variables+=VLSVariableDeclaration) | 1049 | * (variables+=VLSVariable | variables+=VLSVariableDeclaration) |
1027 | * variables+=VLSVariable? | 1050 | * variables+=VLSVariableDeclaration? |
1028 | * (variables+=VLSVariableDeclaration? variables+=VLSVariable?)* | 1051 | * (variables+=VLSVariable? variables+=VLSVariableDeclaration?)* |
1029 | * operand=VLSUnitaryFormula | 1052 | * operand=VLSUnitaryFormula |
1030 | * ) | 1053 | * ) |
1031 | */ | 1054 | */ |