From 15602c7cfbfc80b8c826855b94c9f9582650dd21 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 29 Aug 2019 06:26:02 -0400 Subject: VAMPIRE: adapt grammar to Vampire solution + get model from text --- .../mcgill/ecse/dslreasoner/VampireLanguage.xtext | 113 ++++++++++++++------- .../formatting2/VampireLanguageFormatter.xtend | 26 +++-- 2 files changed, 90 insertions(+), 49 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext index 7d20da72..1b115d45 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/VampireLanguage.xtext @@ -11,7 +11,7 @@ generate vampireLanguage "http://www.mcgill.ca/ecse/dslreasoner/VampireLanguage" VampireModel: ( - includes += VLSInclude | +// includes += VLSInclude | comments += VLSComment | confirmations += VLSConfirmations| formulas += VLSFofFormula | @@ -42,17 +42,17 @@ terminal DOUBLE_DOLLAR_ID: ('$$') (LOWER_WORD_ID); terminal LITERAL: '0' | ('1'..'9') (INT)?; terminal SIGNED_LITERAL: (SIGN)* (LITERAL); -terminal UNSIGNED_REAL_FRAC_ID: (LITERAL) ('.') (INT); -terminal UNSIGNED_REAL_EXP_ID: (LITERAL | UNSIGNED_REAL_FRAC_ID) ('Ee') (SIGN)* (INT) ; -terminal SIGNED_REAL_ID: (SIGN)* (UNSIGNED_REAL_FRAC_ID | UNSIGNED_REAL_EXP_ID); - -terminal UNSIGNED_RAT_ID: (LITERAL) ('/') ('1'..'9') (INT)? ; -terminal SIGNED_RAT_ID: (SIGN)* (UNSIGNED_RAT_ID); +//terminal UNSIGNED_REAL_FRAC_ID: (LITERAL) ('.') (INT); +//terminal UNSIGNED_REAL_EXP_ID: (LITERAL | UNSIGNED_REAL_FRAC_ID) ('Ee') (SIGN)* (INT) ; +//terminal SIGNED_REAL_ID: (SIGN)* (UNSIGNED_REAL_FRAC_ID | UNSIGNED_REAL_EXP_ID); +// +//terminal UNSIGNED_RAT_ID: (LITERAL) ('/') ('1'..'9') (INT)? ; +//terminal SIGNED_RAT_ID: (SIGN)* (UNSIGNED_RAT_ID); //Overwriting is necessary -terminal ID: (!('\n'|'\r'))* ; -terminal ANY_OTHER: ID; -terminal SINGLE_COMMENT: ANY_OTHER; +//terminal ID: (!('\n'|'\r'))* ('\r'? '\n')?; +//terminal ANY_OTHER: ; +terminal SINGLE_COMMENT: '%' (!('\n'|'\r'))* ('\r'? '\n')?; //terminal ID: ( !('('|')'|'\r'|'\n') )+ ; @@ -61,38 +61,29 @@ terminal SINGLE_COMMENT: ANY_OTHER; ////////////////////////////////// // -VLSInclude: - 'include(' fileName = SINGLE_QUOTE ( ',[' names += VLSName (',' names += VLSName)* ']' )? -; +//VLSInclude: +// 'include(' fileName = SINGLE_QUOTE ( ',[' names += VLSName (',' names += VLSName)* ']' )? +//; -VLSName: - name = (LOWER_WORD_ID | SINGLE_QUOTE | LITERAL | SIGNED_LITERAL) -; +//VLSName: +// name = (LOWER_WORD_ID | SINGLE_QUOTE | LITERAL | SIGNED_LITERAL) +//; // VLSComment: - '%' comment = SINGLE_COMMENT + comment = SINGLE_COMMENT //need to add a new line at the end of the file for the case where the last line is a comment ; //VLSConstantDeclaration: name = (LOWER_WORD_ID | SINGLE_QUOTE | DOLLAR_ID | DOUBLE_DOLLAR_ID ); VLSConfirmations: - VLSSatisfiable //| VLSFiniteModel// | VLSTrying + {VLSSatisfiable} 'Satisfiable!' | + {VLSWarning} "WARNING!" "Could" "not" "set" "resource" "limit:" "Virtual" "memory." | + {VLSTrying} 'TRYING' '[' name = LITERAL ']' | + {VLSFiniteModel} 'Finite' 'Model' 'Found!' ; -VLSSatisfiable: - {VLSSatisfiable} 'Satisfiable!' -; - -//VLSTrying: -// 'TRYING' '[' name = LITERAL ']' -//; -// -//VLSFiniteModel: -// {VLSFiniteModel} 'Finite' 'Model' 'Found!' -//; - // VLSFofFormula: 'fof' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.' @@ -100,7 +91,23 @@ VLSFofFormula: VLSTffFormula: - 'tff' '(' name = (LOWER_WORD_ID | SIGNED_LITERAL | SINGLE_QUOTE) ',' fofRole = VLSRole ',' fofFormula = VLSTerm (',' annotations = VLSAnnotation)? ')' '.' + 'tff' '(' name = VLSTffName ',' tffRole = VLSRole ',' fofFormula = VLSTffTerm (',' annotations = VLSAnnotation)? ')' '.' +; + +VLSTffName: + VLSTffDeclPred | VLSTffFinite | VLSTffDistinct +; + +VLSTffDistinct: + 'distinct_domain' +; + +VLSTffFinite: + 'finite_domain' +; + +VLSTffDeclPred: + 'declare_' DOLLAR_ID | LOWER_WORD_ID ; @@ -118,6 +125,7 @@ VLSRole: "fi_domain" | "fi_functors" | "fi_predicates" | "unknown" ; +/* //VLSRole: // VLSAxiom | VLSConjecture | VLSHypothesis | VLSDefinition | // VLSAssumption | VLSLemma | VLSTheorem | VLSCorollary | VLSNegated_Conjecture | @@ -183,6 +191,7 @@ VLSRole: //VLSUnknown: // "unknown" //; +*/ // // Not at all based on the website. based on what we think the output will be like @@ -197,6 +206,36 @@ VLSAnnotationTerms returns VLSAnnotation: ////////////////////////////////// // VLS Terms ////////////////////////////////// +VLSTffTerm: + VLSTerm | + VLSDeclaration +; + +///////////////// +//TFF Specific +VLSDeclaration: + VLSVariableDeclaration | + VLSOtherDeclaration + +; + +VLSOtherDeclaration: + VLSAtomicConstant ':' type = VLSTypeDef +; + +VLSVariableDeclaration: + VLSVariable ':' type = VLSTypeDef +; + +VLSTypeDef: + typeSig = VLSUnitaryTerm ('>' mapsTo = VLSAtomicConstant)? //might need to make VLSAtomic to include VLSVariable +; + +VLSUnitaryTerm returns VLSTypeDef: + initType = VLSAtomic ('*' nextType = VLSAtomicConstant)* //might need to make VLSAtomic to include VLSVariable +; +//TFF Specific +///////////////// VLSTerm: //( VLSLogic | VLSSequent) @@ -228,11 +267,15 @@ VLSUnitaryFormula returns VLSTerm: ; VLSUniversalQuantifier returns VLSTerm: - {VLSUniversalQuantifier} (("!") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula + {VLSUniversalQuantifier} (("!") '[' variables += (VLSVariable | VLSVariableDeclaration) + (',' variables += (VLSVariable | VLSVariableDeclaration))* ']' ':' + ) operand = VLSUnitaryFormula ; VLSExistentialQuantifier returns VLSTerm: - {VLSExistentialQuantifier} (("?") '[' variables += VLSVariable (',' variables += VLSVariable)* ']' ':') operand = VLSUnitaryFormula + {VLSExistentialQuantifier} (("?") '[' variables += (VLSVariable | VLSVariableDeclaration) + (',' variables += (VLSVariable | VLSVariableDeclaration))* ']' ':' + ) operand = VLSUnitaryFormula ; VLSUnaryNegation returns VLSTerm: @@ -300,8 +343,8 @@ VLSFunctionAsTerm: VLSDefinedTerm: {VLSInt} value = SIGNED_LITERAL | - {VLSReal} value = SIGNED_REAL_ID | - {VLSRational} value = SIGNED_RAT_ID | +// {VLSReal} value = SIGNED_REAL_ID | +// {VLSRational} value = SIGNED_RAT_ID | {VLSDoubleQuote} value = DOUBLE_QUOTE ; diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend index f943daad..4fc67b22 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/src/ca/mcgill/ecse/dslreasoner/formatting2/VampireLanguageFormatter.xtend @@ -6,8 +6,6 @@ package ca.mcgill.ecse.dslreasoner.formatting2 import ca.mcgill.ecse.dslreasoner.services.VampireLanguageGrammarAccess import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInclude -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSName import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel import com.google.inject.Inject import org.eclipse.xtext.formatting2.AbstractFormatter2 @@ -19,23 +17,23 @@ class VampireLanguageFormatter extends AbstractFormatter2 { def dispatch void format(VampireModel vampireModel, extension IFormattableDocument document) { // TODO: format HiddenRegions around keywords, attributes, cross references, etc. - for (VLSInclude vLSInclude : vampireModel.getIncludes()) { - vLSInclude.format; - } +// for (VLSInclude vLSInclude : vampireModel.getIncludes()) { +// vLSInclude.format; +// } for (VLSComment vLSComment : vampireModel.getComments()) { vLSComment.format; } - for (VLSFofFormula vLSFofFormula : vampireModel.getFormulas()) { - vLSFofFormula.format; - } +// for (VLSFofFormula vLSFofFormula : vampireModel.getFormulas()) { +// vLSFofFormula.format; +// } } - def dispatch void format(VLSInclude vLSInclude, extension IFormattableDocument document) { - // TODO: format HiddenRegions around keywords, attributes, cross references, etc. - for (VLSName vLSName : vLSInclude.getNames()) { - vLSName.format; - } - } +// def dispatch void format(VLSInclude vLSInclude, extension IFormattableDocument document) { +// // TODO: format HiddenRegions around keywords, attributes, cross references, etc. +// for (VLSName vLSName : vLSInclude.getNames()) { +// vLSName.format; +// } +// } def dispatch void format(VLSFofFormula formula, extension IFormattableDocument document){ formula.append[newLine] -- cgit v1.2.3-54-g00ecf