From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- .../mit/inf/dslreasoner/GenerateSmtLanguage.mwe2 | 133 ++++++++++++ .../hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext | 222 +++++++++++++++++++++ .../inf/dslreasoner/SmtLanguageRuntimeModule.java | 11 + .../dslreasoner/SmtLanguageStandaloneSetup.java | 16 ++ .../formatting/SmtLanguageFormatter.xtend | 34 ++++ .../generator/SmtLanguageGenerator.xtend | 24 +++ .../scoping/SmtLanguageScopeProvider.xtend | 138 +++++++++++++ .../validation/SmtLanguageValidator.xtend | 24 +++ 8 files changed, 602 insertions(+) create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2 create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf') diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2 b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2 new file mode 100644 index 00000000..e27dbd64 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2 @@ -0,0 +1,133 @@ +module hu.bme.mit.inf.dslreasoner.GenerateSmtLanguage + +import org.eclipse.emf.mwe.utils.* +import org.eclipse.xtext.generator.* +import org.eclipse.xtext.ui.generator.* + +var grammarURI = "classpath:/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext" +var fileExtensions = "smt2" +var projectName = "hu.bme.mit.inf.dslreasoner.smt.language" +var runtimeProject = "../${projectName}" +var generateXtendStub = true +var encoding = "UTF-8" + +Workflow { + bean = StandaloneSetup { + scanClassPath = true + platformUri = "${runtimeProject}/.." + // The following two lines can be removed, if Xbase is not used. + registerGeneratedEPackage = "org.eclipse.xtext.xbase.XbasePackage" + registerGenModelFile = "platform:/resource/org.eclipse.xtext.xbase/model/Xbase.genmodel" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}/src-gen" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}/model/generated" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}.ui/src-gen" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}.tests/src-gen" + } + + component = Generator { + pathRtProject = runtimeProject + pathUiProject = "${runtimeProject}.ui" + //pathTestProject = "${runtimeProject}.tests" + projectNameRt = projectName + projectNameUi = "${projectName}.ui" + encoding = encoding + language = auto-inject { + uri = grammarURI + + // Java API to access grammar elements (required by several other fragments) + fragment = grammarAccess.GrammarAccessFragment auto-inject {} + + // generates Java API for the generated EPackages + fragment = ecore.EMFGeneratorFragment auto-inject {} + + // the old serialization component + // fragment = parseTreeConstructor.ParseTreeConstructorFragment auto-inject {} + + // serializer 2.0 + fragment = serializer.SerializerFragment auto-inject { + generateStub = false + } + + // a custom ResourceFactory for use with EMF + fragment = resourceFactory.ResourceFactoryFragment auto-inject {} + + // The antlr parser generator fragment. + fragment = parser.antlr.XtextAntlrGeneratorFragment auto-inject { + // options = { + // backtrack = true + // } + } + + // Xtend-based API for validation + fragment = validation.ValidatorFragment auto-inject { + // composedCheck = "org.eclipse.xtext.validation.ImportUriValidator" + // composedCheck = "org.eclipse.xtext.validation.NamesAreUniqueValidator" + } + + // old scoping and exporting API + // fragment = scoping.ImportURIScopingFragment auto-inject {} + // fragment = exporting.SimpleNamesFragment auto-inject {} + + // scoping and exporting API + fragment = scoping.ImportNamespacesScopingFragment auto-inject {} + fragment = exporting.QualifiedNamesFragment auto-inject {} + fragment = builder.BuilderIntegrationFragment auto-inject {} + + // generator API + fragment = generator.GeneratorFragment auto-inject {} + + // formatter API + fragment = formatting.FormatterFragment auto-inject {} + + // labeling API + fragment = labeling.LabelProviderFragment auto-inject {} + + // outline API + fragment = outline.OutlineTreeProviderFragment auto-inject {} + fragment = outline.QuickOutlineFragment auto-inject {} + + // quickfix API + fragment = quickfix.QuickfixProviderFragment auto-inject {} + + // content assist API + fragment = contentAssist.ContentAssistFragment auto-inject {} + + // generates a more lightweight Antlr parser and lexer tailored for content assist + fragment = parser.antlr.XtextAntlrUiGeneratorFragment auto-inject {} + + // generates junit test support classes into Generator#pathTestProject + //fragment = junit.Junit4Fragment auto-inject {} + + // rename refactoring + fragment = refactoring.RefactorElementNameFragment auto-inject {} + + // provides the necessary bindings for java types integration + fragment = types.TypesGeneratorFragment auto-inject {} + + // generates the required bindings only if the grammar inherits from Xbase + fragment = xbase.XbaseGeneratorFragment auto-inject {} + + // generates the required bindings only if the grammar inherits from Xtype + fragment = xbase.XtypeGeneratorFragment auto-inject {} + + // provides a preference page for template proposals + fragment = templates.CodetemplatesGeneratorFragment auto-inject {} + + // provides a compare view + fragment = compare.CompareFragment auto-inject {} + } + } +} + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext new file mode 100644 index 00000000..320e1cfe --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext @@ -0,0 +1,222 @@ +grammar hu.bme.mit.inf.dslreasoner.SmtLanguage with org.eclipse.xtext.common.Terminals + +generate smtLanguage "http://www.bme.hu/mit/inf/dslreasoner/SmtLanguage" + +import "http://www.eclipse.org/emf/2002/Ecore" as ecore + +SMTDocument: + input=SMTInput + ( + '--------------' + output=SMTOutput + )?; + +SMTInput: + (options += SMTOption)* + ( + typeDeclarations+=SMTType | + functionDeclarations+=SMTFunctionDeclaration | + functionDefinition+=SMTFunctionDefinition | + assertions += SMTAssertion + )* + satCommand = SMTSatCommand + getModelCommand = SMTGetModelCommand; + +SMTOutput:( + (satResult = SMTResult + getModelResult = SMTResult) | 'timeout' {SMTOutput}) + statistics=SMTStatisticsSection?; + +////////////////////////////////// +// SMT terminals +////////////////////////////////// + +terminal SL_COMMENT : ';' !('\n'|'\r')* ('\r'? '\n')?; + +terminal ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'-'|'!'|'0'..'9')*; +// ('a'..'z'|'A'..'Z'|'_'/*|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/*|'^'*/|'<'|'>'/*|'@'*/) +// ('a'..'z'|'A'..'Z'|'_'/*|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/*|'^'|*/'<'|'>'/*|'@'*/|'0'..'9')* +SMTID: ID; + +terminal PROPERTYNAME : ':' + ID; +terminal REAL returns ecore::EBigDecimal: INT '.' INT; + +////////////////////////////////// +// Options +////////////////////////////////// +SMTOption: '(' 'set-option' name = PROPERTYNAME value = SMTAtomicTerm ')'; + +////////////////////////////////// +// Type declarations +////////////////////////////////// +SMTType: SMTEnumeratedTypeDeclaration | SMTSetTypeDeclaration; + +SMTEnumLiteral: name = SMTID; +SMTEnumeratedTypeDeclaration: '(' 'declare-datatypes' '(' ')' '(' '(' name = SMTID elements+=SMTEnumLiteral+ ')' ')' ')'; +SMTSetTypeDeclaration: '(' 'declare-sort' name = SMTID ')'; + +SMTTypeReference: SMTComplexTypeReference | SMTPrimitiveTypeReference; +SMTComplexTypeReference: referred = [SMTType]; +SMTPrimitiveTypeReference: SMTIntTypeReference | SMTBoolTypeReference | SMTRealTypeReference; + +SMTIntTypeReference: {SMTIntTypeReference} "Int"; +SMTBoolTypeReference: {SMTBoolTypeReference} "Bool"; +SMTRealTypeReference: {SMTRealTypeReference} "Real"; + +////////////////////////////////// +// Functions and constants +////////////////////////////////// + +SMTFunctionDeclaration: '(' 'declare-fun' name = SMTID '(' parameters+=SMTTypeReference* ')' range = SMTTypeReference ')'; + +/*DeclaredFunctionDefinition: + '(' 'define-fun' declaration=[Function] '(' parameters+=SortedVariable* ')' range = TypeReference value = Term ')';*/ + +SMTFunctionDefinition: + '(' 'define-fun' name=SMTID '(' parameters+=SMTSortedVariable* ')' range = SMTTypeReference value = SMTTerm ')'; + + +////////////////////////////////// +// Expressions +////////////////////////////////// +SMTTerm: + SMTSymbolicValue| + SMTAtomicTerm | + SMTBoolOperation | + SMTIntOperation | + SMTITE | + SMTLet | + SMTRelation | + SMTQuantifiedExpression; + +SMTSymbolicDeclaration: SMTFunctionDeclaration | SMTFunctionDefinition | SMTSortedVariable | SMTEnumLiteral | SMTInlineConstantDefinition; + +SMTSymbolicValue: + '(' symbolicReference = [SMTSymbolicDeclaration] ( parameterSubstitutions += SMTTerm )+ ')' | + symbolicReference = [SMTSymbolicDeclaration]; + +SMTAtomicTerm: SMTIntLiteral | SMTBoolLiteral | SMTRealLiteral; +SMTIntLiteral: value=INT; +BOOLEANTERMINAL returns ecore::EBoolean: 'true' | 'false'; +SMTBoolLiteral: value=BOOLEANTERMINAL; +SMTRealLiteral: value=REAL; + +// Quantified operations +SMTSortedVariable: '(' name = SMTID range = SMTTypeReference ')'; +//QuantifiedVariableValue: variable = [QuantifiedVariable]; + +SMTQuantifiedExpression: SMTExists | SMTForall; +SMTExists: '(' 'exists' '(' (quantifiedVariables += SMTSortedVariable)+ ')' + (expression=SMTTerm | ('(' '!' expression = SMTTerm ':pattern' '(' pattern = SMTTerm ')' ')')) ')' +; +SMTForall: '(' 'forall' '(' (quantifiedVariables += SMTSortedVariable)+ ')' + (expression=SMTTerm | ('(' '!' expression = SMTTerm ':pattern' '(' pattern = SMTTerm ')' ')')) ')' +; + +// Boolean operations +SMTBoolOperation: SMTAnd | SMTOr | SMTImpl | SMTNot | SMTIff; +SMTAnd: '(' 'and' operands+=SMTTerm+ ')'; +SMTOr: '(' 'or' operands+=SMTTerm+ ')'; +SMTImpl: '(' '=>' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTNot: '(' 'not' operand=SMTTerm ')'; +SMTIff: '(' 'iff' leftOperand=SMTTerm rightOperand=SMTTerm ')'; + +// If-then-else +SMTITE: '(' 'ite' condition = SMTTerm if=SMTTerm else = SMTTerm ')'; + +//Let +SMTLet: '(' 'let' '(' (inlineConstantDefinitions+=SMTInlineConstantDefinition)+ ')' term=SMTTerm ')'; +SMTInlineConstantDefinition: + '(' name=SMTID definition=SMTTerm ')' +; + +// Relations +SMTRelation: SMTEquals | SMTDistinct | SMTLT | SMTMT | SMTLEQ | SMTMEQ; +SMTEquals: '(' '=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTDistinct: '(' 'distinct' operands+=SMTTerm+ ')'; +SMTLT: '(' '<' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTMT: '(' '>' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTLEQ: '(' '<=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTMEQ: '(' '>=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; + +// Int operations +SMTIntOperation: SMTPlus | SMTMinus | SMTMultiply | SMTDivison | SMTDiv | SMTMod; +SMTPlus: '(' '+' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTMinus: '(' '-' leftOperand=SMTTerm (rightOperand=SMTTerm)? ')'; +SMTMultiply: '(' '*' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTDivison: '(' '/' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTDiv: '(' 'div' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTMod: '(' 'mod' leftOperand=SMTTerm rightOperand=SMTTerm ')'; + +////////////////////////////////// +// Assertion +////////////////////////////////// +SMTAssertion: '(' 'assert' value=SMTTerm ')'; +SMTCardinalityConstraint: + '(' 'forall' '(' '(' ID type=SMTTypeReference ')' ')' + (('(' 'or'('(' '=' ID elements+=SMTSymbolicValue ')')* ')') | // With multiple element + ('(' '=' ID elements+=SMTSymbolicValue ')')) //With single element + ')' +; + +////////////////////////////////// +// Goals +////////////////////////////////// +SMTSatCommand: SMTSimpleSatCommand | SMTComplexSatCommand; +SMTSimpleSatCommand : '(' 'check-sat' {SMTSimpleSatCommand} ')'; +SMTComplexSatCommand: '(' 'check-sat-using' method = SMTReasoningTactic ')'; +SMTGetModelCommand: '(' 'get-model' {SMTGetModelCommand} ')'; + +SMTReasoningTactic: SMTBuiltinTactic | SMTReasoningCombinator; +SMTBuiltinTactic: name = ID; +SMTReasoningCombinator: + SMTAndThenCombinator | SMTOrElseCombinator | SMTParOrCombinator | SMTParThenCombinator | SMTTryForCombinator | + SMTIfCombinator | SMTWhenCombinator | SMTFailIfCombinator | SMTUsingParamCombinator +; +// executes the given tactics sequencially. +SMTAndThenCombinator: '(' 'and-then' (tactics+=SMTReasoningTactic)+ ')'; +// tries the given tactics in sequence until one of them succeeds. +SMTOrElseCombinator: '(' 'or-else' (tactics+=SMTReasoningTactic)+ ')'; +// executes the given tactics in parallel until one of them succeeds. +SMTParOrCombinator: '(' 'par-or' (tactics+=SMTReasoningTactic)+ ')'; +// executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel. +SMTParThenCombinator: '(' 'par-then' preProcessingTactic=SMTReasoningTactic paralellyPostpricessingTactic = SMTReasoningTactic ')'; +// excutes the given tactic for at most milliseconds, it fails if the execution takes more than milliseconds. +SMTTryForCombinator: '(' 'try-for' tactic=SMTReasoningTactic time=INT ')'; +// if evaluates to true, then execute the first tactic. Otherwise execute the second. +SMTIfCombinator: '(' 'if' probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic ')'; +// shorthand for (if skip). +SMTWhenCombinator: '(' 'when' probe=ReasoningProbe tactic=SMTReasoningTactic ')'; +// fail if evaluates to true. +SMTFailIfCombinator: '(' 'fail-if' probe=ReasoningProbe ')'; +//executes the given tactic using the given attributes, where ::= . ! is a syntax sugar for using-params. +SMTUsingParamCombinator: '(' ('using-params' | '!') tactic=SMTReasoningTactic (parameters+=ReasoningTacticParameter)* ')'; + +ReasoningProbe: name=ID; +ReasoningTacticParameter: name=PROPERTYNAME value=SMTAtomicTerm; + +////////////////////////////////// +// Result +////////////////////////////////// + +SMTResult: SMTUnsupportedResult | SMTSatResult | SMTModelResult | SMTErrorResult; +SMTErrorResult: '(' 'error' message = STRING ')'; +SMTUnsupportedResult: 'unsupported' ';' command=ID; +SMTSatResult: sat?='sat' | unsat?='unsat' | unknown?='unknown'; +SMTModelResult: {SMTModelResult} '(' 'model' + ( + newFunctionDeclarations+=SMTFunctionDeclaration | + typeDefinitions+=SMTCardinalityConstraint | + newFunctionDefinitions+=SMTFunctionDefinition + )* + ')'; + +////////////////////////////////// +// Statistics +////////////////////////////////// +//IntOrReal returns ecore::EDouble: INT | REAL; + +SMTStatisticValue: SMTStatisticIntValue | SMTStatisticDoubleValue; +SMTStatisticIntValue: name = PROPERTYNAME value=INT; +SMTStatisticDoubleValue: name = PROPERTYNAME value = REAL; +SMTStatisticsSection: '(' {SMTStatisticsSection} values += SMTStatisticValue* ')'; \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java new file mode 100644 index 00000000..dabb0c29 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java @@ -0,0 +1,11 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner; + +/** + * Use this class to register components to be used at runtime / without the Equinox extension registry. + */ +public class SmtLanguageRuntimeModule extends hu.bme.mit.inf.dslreasoner.AbstractSmtLanguageRuntimeModule { + +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java new file mode 100644 index 00000000..ed297373 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java @@ -0,0 +1,16 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner; + +/** + * Initialization support for running Xtext languages + * without equinox extension registry + */ +public class SmtLanguageStandaloneSetup extends SmtLanguageStandaloneSetupGenerated{ + + public static void doSetup() { + new SmtLanguageStandaloneSetup().createInjectorAndDoEMFRegistration(); + } +} + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend new file mode 100644 index 00000000..9e3e3943 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend @@ -0,0 +1,34 @@ +package hu.bme.mit.inf.dslreasoner.formatting + +import org.eclipse.xtext.formatting.impl.AbstractDeclarativeFormatter +import org.eclipse.xtext.formatting.impl.FormattingConfig +import hu.bme.mit.inf.dslreasoner.services.SmtLanguageGrammarAccess + + +/** + * This class contains custom formatting description. + * + * see : http://www.eclipse.org/Xtext/documentation.html#formatting + * on how and when to use it + * + * Also see {@link org.eclipse.xtext.xtext.XtextFormattingTokenSerializer} as an example + */ +class SmtLanguageFormatter extends AbstractDeclarativeFormatter { + +// @Inject extension SmtLanguageGrammarAccess + + override protected void configureFormatting(FormattingConfig c) { + val f = getGrammarAccess as SmtLanguageGrammarAccess + c.setAutoLinewrap(100000); + for(pair : f.findKeywordPairs("(",")")) { + c.setNoSpace().after(pair.getFirst()); + c.setNoSpace().before(pair.getSecond()); + } + c.setLinewrap.after(f.SMTAssertionRule) + c.setLinewrap.after(f.SMTFunctionDeclarationRule) + c.setLinewrap.after(f.SMTFunctionDefinitionRule) + c.setLinewrap.after(f.SMTEnumeratedTypeDeclarationRule) + c.setLinewrap.after(f.SMTSetTypeDeclarationRule) + c.setLinewrap.after(f.SMTOptionRule) + } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend new file mode 100644 index 00000000..e61c082e --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend @@ -0,0 +1,24 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.generator + +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.xtext.generator.IGenerator +import org.eclipse.xtext.generator.IFileSystemAccess + +/** + * Generates code from your model files on save. + * + * see http://www.eclipse.org/Xtext/documentation.html#TutorialCodeGeneration + */ +class SmtLanguageGenerator implements IGenerator { + + override void doGenerate(Resource resource, IFileSystemAccess fsa) { +// fsa.generateFile('greetings.txt', 'People to greet: ' + +// resource.allContents +// .filter(typeof(Greeting)) +// .map[name] +// .join(', ')) + } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend new file mode 100644 index 00000000..e93e0543 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend @@ -0,0 +1,138 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.scoping + +import java.util.Set +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable +import org.eclipse.emf.ecore.EObject +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression +import java.util.Collections +import java.util.HashSet +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInlineConstantDefinition +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLet +import java.util.Collection +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import org.eclipse.xtext.scoping.IScope +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration +import org.eclipse.emf.ecore.EReference +import java.util.HashMap +import java.util.Map +import org.eclipse.xtext.scoping.Scopes +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration + +/** + * This class contains custom scoping description. + * + * see : http://www.eclipse.org/Xtext/documentation.html#scoping + * on how and when to use it + * + */ +class SmtLanguageScopeProvider extends org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider { + /** + * Search for the first instance of containerType up in the containment hierarchy. + * @param containerType + * @param from + * @return + */ + @SuppressWarnings("unchecked") + def private ContainerType getTop(Class containerType, EObject from){ + var actualLevel = from.eContainer(); + while(actualLevel!=null){ + if(containerType.isInstance(actualLevel)) { return actualLevel as ContainerType} + else { actualLevel = actualLevel.eContainer() } + } + return null; + } + + def private Set getQuantifiedVariables(EObject from) { + //The most inner quantified variables are in this expression: + val quantifiedExpression = getTop(typeof(SMTQuantifiedExpression), from); + if(quantifiedExpression==null) return Collections.emptySet(); + + //The variables can be referred by a symbolic reference + val Set result = new HashSet(quantifiedExpression.getQuantifiedVariables()); + //The variables can defined in an outer quantifier + result.addAll(getQuantifiedVariables(quantifiedExpression)); + //println(result.map[name].join(",")) + return result; + } + + def private Set getInlineConstantDefinitions(EObject from) { + //The most inner quantified variables are in this expression: + val let = getTop(typeof(SMTLet), from); + if(let==null) return Collections.emptySet(); + + //The variables can be referred by a symbolic reference + val result = new HashSet(let.getInlineConstantDefinitions()); + //The variables can defined in an outer quantifier + result.addAll(getInlineConstantDefinitions(let)); + return result; + } + + def private Collection getParameters(SMTSymbolicValue from) { + val functionDefinition = getTop(typeof(SMTFunctionDefinition), from); + if(functionDefinition!=null) { + return functionDefinition.getParameters(); + } + else return Collections.emptySet(); + } + + def private Set getFiniteElements(SMTSymbolicValue value) { + val Set result = new HashSet(); + val document = getTop(typeof(SMTDocument),value) + for(type : document.input.getTypeDeclarations().filter(typeof(SMTEnumeratedTypeDeclaration))) { + result.addAll(type.getElements()); + } + return result; + } + + def private Set getFunctions(SMTSymbolicValue value) { + val document = getTop(typeof(SMTDocument),value); + val input = document.input + var SMTModelResult output = null; + if(document.output != null && document.output.getModelResult instanceof SMTModelResult) { + output = document.output.getModelResult as SMTModelResult + } + + val Map declarations = new HashMap + val Set definitions =new HashSet + + input.functionDeclarations.forEach[declarations.put(it.name,it)] + if(output != null) { + output.newFunctionDeclarations.forEach[declarations.put(it.name,it)] + } + input.functionDefinition.filter[!declarations.containsKey(it.name)].forEach[definitions += it] + if(output != null) { + output.newFunctionDefinitions.filter[!declarations.containsKey(it.name)].forEach[definitions += it] + } + + val referrables = new HashSet; + referrables.addAll(declarations.values) + referrables.addAll(definitions) + return referrables + } + + def public IScope scope_SMTSymbolicValue_symbolicReference(SMTSymbolicValue value, EReference ref) { + val Set referrables = new HashSet; + + referrables.addAll(value.getFiniteElements) + referrables.addAll(value.getParameters) + referrables.addAll(value.getFunctions) + referrables.addAll(value.getQuantifiedVariables) + referrables.addAll(value.getInlineConstantDefinitions) + + return Scopes.scopeFor(referrables); + } + + // Any type defined in the input section can be referred. + def public IScope scope_SMTComplexTypeReference_referred(SMTComplexTypeReference reference, EReference ref){ + return Scopes.scopeFor(getTop(typeof(SMTDocument),reference).input.typeDeclarations) + } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend new file mode 100644 index 00000000..2ae6130f --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend @@ -0,0 +1,24 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.validation +//import org.eclipse.xtext.validation.Check + +/** + * Custom validation rules. + * + * see http://www.eclipse.org/Xtext/documentation.html#validation + */ +class SmtLanguageValidator extends AbstractSmtLanguageValidator { + +// public static val INVALID_NAME = 'invalidName' +// +// @Check +// def checkGreetingStartsWithCapital(Greeting greeting) { +// if (!Character.isUpperCase(greeting.name.charAt(0))) { +// warning('Name should start with a capital', +// MyDslPackage.Literals.GREETING__NAME, +// INVALID_NAME) +// } +// } +} -- cgit v1.2.3-54-g00ecf