diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext | 222 |
1 files changed, 222 insertions, 0 deletions
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 @@ | |||
1 | grammar hu.bme.mit.inf.dslreasoner.SmtLanguage with org.eclipse.xtext.common.Terminals | ||
2 | |||
3 | generate smtLanguage "http://www.bme.hu/mit/inf/dslreasoner/SmtLanguage" | ||
4 | |||
5 | import "http://www.eclipse.org/emf/2002/Ecore" as ecore | ||
6 | |||
7 | SMTDocument: | ||
8 | input=SMTInput | ||
9 | ( | ||
10 | '--------------' | ||
11 | output=SMTOutput | ||
12 | )?; | ||
13 | |||
14 | SMTInput: | ||
15 | (options += SMTOption)* | ||
16 | ( | ||
17 | typeDeclarations+=SMTType | | ||
18 | functionDeclarations+=SMTFunctionDeclaration | | ||
19 | functionDefinition+=SMTFunctionDefinition | | ||
20 | assertions += SMTAssertion | ||
21 | )* | ||
22 | satCommand = SMTSatCommand | ||
23 | getModelCommand = SMTGetModelCommand; | ||
24 | |||
25 | SMTOutput:( | ||
26 | (satResult = SMTResult | ||
27 | getModelResult = SMTResult) | 'timeout' {SMTOutput}) | ||
28 | statistics=SMTStatisticsSection?; | ||
29 | |||
30 | ////////////////////////////////// | ||
31 | // SMT terminals | ||
32 | ////////////////////////////////// | ||
33 | |||
34 | terminal SL_COMMENT : ';' !('\n'|'\r')* ('\r'? '\n')?; | ||
35 | |||
36 | terminal ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'-'|'!'|'0'..'9')*; | ||
37 | // ('a'..'z'|'A'..'Z'|'_'/*|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/*|'^'*/|'<'|'>'/*|'@'*/) | ||
38 | // ('a'..'z'|'A'..'Z'|'_'/*|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/*|'^'|*/'<'|'>'/*|'@'*/|'0'..'9')* | ||
39 | SMTID: ID; | ||
40 | |||
41 | terminal PROPERTYNAME : ':' + ID; | ||
42 | terminal REAL returns ecore::EBigDecimal: INT '.' INT; | ||
43 | |||
44 | ////////////////////////////////// | ||
45 | // Options | ||
46 | ////////////////////////////////// | ||
47 | SMTOption: '(' 'set-option' name = PROPERTYNAME value = SMTAtomicTerm ')'; | ||
48 | |||
49 | ////////////////////////////////// | ||
50 | // Type declarations | ||
51 | ////////////////////////////////// | ||
52 | SMTType: SMTEnumeratedTypeDeclaration | SMTSetTypeDeclaration; | ||
53 | |||
54 | SMTEnumLiteral: name = SMTID; | ||
55 | SMTEnumeratedTypeDeclaration: '(' 'declare-datatypes' '(' ')' '(' '(' name = SMTID elements+=SMTEnumLiteral+ ')' ')' ')'; | ||
56 | SMTSetTypeDeclaration: '(' 'declare-sort' name = SMTID ')'; | ||
57 | |||
58 | SMTTypeReference: SMTComplexTypeReference | SMTPrimitiveTypeReference; | ||
59 | SMTComplexTypeReference: referred = [SMTType]; | ||
60 | SMTPrimitiveTypeReference: SMTIntTypeReference | SMTBoolTypeReference | SMTRealTypeReference; | ||
61 | |||
62 | SMTIntTypeReference: {SMTIntTypeReference} "Int"; | ||
63 | SMTBoolTypeReference: {SMTBoolTypeReference} "Bool"; | ||
64 | SMTRealTypeReference: {SMTRealTypeReference} "Real"; | ||
65 | |||
66 | ////////////////////////////////// | ||
67 | // Functions and constants | ||
68 | ////////////////////////////////// | ||
69 | |||
70 | SMTFunctionDeclaration: '(' 'declare-fun' name = SMTID '(' parameters+=SMTTypeReference* ')' range = SMTTypeReference ')'; | ||
71 | |||
72 | /*DeclaredFunctionDefinition: | ||
73 | '(' 'define-fun' declaration=[Function] '(' parameters+=SortedVariable* ')' range = TypeReference value = Term ')';*/ | ||
74 | |||
75 | SMTFunctionDefinition: | ||
76 | '(' 'define-fun' name=SMTID '(' parameters+=SMTSortedVariable* ')' range = SMTTypeReference value = SMTTerm ')'; | ||
77 | |||
78 | |||
79 | ////////////////////////////////// | ||
80 | // Expressions | ||
81 | ////////////////////////////////// | ||
82 | SMTTerm: | ||
83 | SMTSymbolicValue| | ||
84 | SMTAtomicTerm | | ||
85 | SMTBoolOperation | | ||
86 | SMTIntOperation | | ||
87 | SMTITE | | ||
88 | SMTLet | | ||
89 | SMTRelation | | ||
90 | SMTQuantifiedExpression; | ||
91 | |||
92 | SMTSymbolicDeclaration: SMTFunctionDeclaration | SMTFunctionDefinition | SMTSortedVariable | SMTEnumLiteral | SMTInlineConstantDefinition; | ||
93 | |||
94 | SMTSymbolicValue: | ||
95 | '(' symbolicReference = [SMTSymbolicDeclaration] ( parameterSubstitutions += SMTTerm )+ ')' | | ||
96 | symbolicReference = [SMTSymbolicDeclaration]; | ||
97 | |||
98 | SMTAtomicTerm: SMTIntLiteral | SMTBoolLiteral | SMTRealLiteral; | ||
99 | SMTIntLiteral: value=INT; | ||
100 | BOOLEANTERMINAL returns ecore::EBoolean: 'true' | 'false'; | ||
101 | SMTBoolLiteral: value=BOOLEANTERMINAL; | ||
102 | SMTRealLiteral: value=REAL; | ||
103 | |||
104 | // Quantified operations | ||
105 | SMTSortedVariable: '(' name = SMTID range = SMTTypeReference ')'; | ||
106 | //QuantifiedVariableValue: variable = [QuantifiedVariable]; | ||
107 | |||
108 | SMTQuantifiedExpression: SMTExists | SMTForall; | ||
109 | SMTExists: '(' 'exists' '(' (quantifiedVariables += SMTSortedVariable)+ ')' | ||
110 | (expression=SMTTerm | ('(' '!' expression = SMTTerm ':pattern' '(' pattern = SMTTerm ')' ')')) ')' | ||
111 | ; | ||
112 | SMTForall: '(' 'forall' '(' (quantifiedVariables += SMTSortedVariable)+ ')' | ||
113 | (expression=SMTTerm | ('(' '!' expression = SMTTerm ':pattern' '(' pattern = SMTTerm ')' ')')) ')' | ||
114 | ; | ||
115 | |||
116 | // Boolean operations | ||
117 | SMTBoolOperation: SMTAnd | SMTOr | SMTImpl | SMTNot | SMTIff; | ||
118 | SMTAnd: '(' 'and' operands+=SMTTerm+ ')'; | ||
119 | SMTOr: '(' 'or' operands+=SMTTerm+ ')'; | ||
120 | SMTImpl: '(' '=>' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
121 | SMTNot: '(' 'not' operand=SMTTerm ')'; | ||
122 | SMTIff: '(' 'iff' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
123 | |||
124 | // If-then-else | ||
125 | SMTITE: '(' 'ite' condition = SMTTerm if=SMTTerm else = SMTTerm ')'; | ||
126 | |||
127 | //Let | ||
128 | SMTLet: '(' 'let' '(' (inlineConstantDefinitions+=SMTInlineConstantDefinition)+ ')' term=SMTTerm ')'; | ||
129 | SMTInlineConstantDefinition: | ||
130 | '(' name=SMTID definition=SMTTerm ')' | ||
131 | ; | ||
132 | |||
133 | // Relations | ||
134 | SMTRelation: SMTEquals | SMTDistinct | SMTLT | SMTMT | SMTLEQ | SMTMEQ; | ||
135 | SMTEquals: '(' '=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
136 | SMTDistinct: '(' 'distinct' operands+=SMTTerm+ ')'; | ||
137 | SMTLT: '(' '<' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
138 | SMTMT: '(' '>' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
139 | SMTLEQ: '(' '<=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
140 | SMTMEQ: '(' '>=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
141 | |||
142 | // Int operations | ||
143 | SMTIntOperation: SMTPlus | SMTMinus | SMTMultiply | SMTDivison | SMTDiv | SMTMod; | ||
144 | SMTPlus: '(' '+' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
145 | SMTMinus: '(' '-' leftOperand=SMTTerm (rightOperand=SMTTerm)? ')'; | ||
146 | SMTMultiply: '(' '*' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
147 | SMTDivison: '(' '/' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
148 | SMTDiv: '(' 'div' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
149 | SMTMod: '(' 'mod' leftOperand=SMTTerm rightOperand=SMTTerm ')'; | ||
150 | |||
151 | ////////////////////////////////// | ||
152 | // Assertion | ||
153 | ////////////////////////////////// | ||
154 | SMTAssertion: '(' 'assert' value=SMTTerm ')'; | ||
155 | SMTCardinalityConstraint: | ||
156 | '(' 'forall' '(' '(' ID type=SMTTypeReference ')' ')' | ||
157 | (('(' 'or'('(' '=' ID elements+=SMTSymbolicValue ')')* ')') | // With multiple element | ||
158 | ('(' '=' ID elements+=SMTSymbolicValue ')')) //With single element | ||
159 | ')' | ||
160 | ; | ||
161 | |||
162 | ////////////////////////////////// | ||
163 | // Goals | ||
164 | ////////////////////////////////// | ||
165 | SMTSatCommand: SMTSimpleSatCommand | SMTComplexSatCommand; | ||
166 | SMTSimpleSatCommand : '(' 'check-sat' {SMTSimpleSatCommand} ')'; | ||
167 | SMTComplexSatCommand: '(' 'check-sat-using' method = SMTReasoningTactic ')'; | ||
168 | SMTGetModelCommand: '(' 'get-model' {SMTGetModelCommand} ')'; | ||
169 | |||
170 | SMTReasoningTactic: SMTBuiltinTactic | SMTReasoningCombinator; | ||
171 | SMTBuiltinTactic: name = ID; | ||
172 | SMTReasoningCombinator: | ||
173 | SMTAndThenCombinator | SMTOrElseCombinator | SMTParOrCombinator | SMTParThenCombinator | SMTTryForCombinator | | ||
174 | SMTIfCombinator | SMTWhenCombinator | SMTFailIfCombinator | SMTUsingParamCombinator | ||
175 | ; | ||
176 | // executes the given tactics sequencially. | ||
177 | SMTAndThenCombinator: '(' 'and-then' (tactics+=SMTReasoningTactic)+ ')'; | ||
178 | // tries the given tactics in sequence until one of them succeeds. | ||
179 | SMTOrElseCombinator: '(' 'or-else' (tactics+=SMTReasoningTactic)+ ')'; | ||
180 | // executes the given tactics in parallel until one of them succeeds. | ||
181 | SMTParOrCombinator: '(' 'par-or' (tactics+=SMTReasoningTactic)+ ')'; | ||
182 | // executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel. | ||
183 | SMTParThenCombinator: '(' 'par-then' preProcessingTactic=SMTReasoningTactic paralellyPostpricessingTactic = SMTReasoningTactic ')'; | ||
184 | // excutes the given tactic for at most <num> milliseconds, it fails if the execution takes more than <num> milliseconds. | ||
185 | SMTTryForCombinator: '(' 'try-for' tactic=SMTReasoningTactic time=INT ')'; | ||
186 | // if <probe> evaluates to true, then execute the first tactic. Otherwise execute the second. | ||
187 | SMTIfCombinator: '(' 'if' probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic ')'; | ||
188 | // shorthand for (if <probe> <tactic> skip). | ||
189 | SMTWhenCombinator: '(' 'when' probe=ReasoningProbe tactic=SMTReasoningTactic ')'; | ||
190 | // fail if <probe> evaluates to true. | ||
191 | SMTFailIfCombinator: '(' 'fail-if' probe=ReasoningProbe ')'; | ||
192 | //executes the given tactic using the given attributes, where <attribute> ::= <keyword> <value>. ! is a syntax sugar for using-params. | ||
193 | SMTUsingParamCombinator: '(' ('using-params' | '!') tactic=SMTReasoningTactic (parameters+=ReasoningTacticParameter)* ')'; | ||
194 | |||
195 | ReasoningProbe: name=ID; | ||
196 | ReasoningTacticParameter: name=PROPERTYNAME value=SMTAtomicTerm; | ||
197 | |||
198 | ////////////////////////////////// | ||
199 | // Result | ||
200 | ////////////////////////////////// | ||
201 | |||
202 | SMTResult: SMTUnsupportedResult | SMTSatResult | SMTModelResult | SMTErrorResult; | ||
203 | SMTErrorResult: '(' 'error' message = STRING ')'; | ||
204 | SMTUnsupportedResult: 'unsupported' ';' command=ID; | ||
205 | SMTSatResult: sat?='sat' | unsat?='unsat' | unknown?='unknown'; | ||
206 | SMTModelResult: {SMTModelResult} '(' 'model' | ||
207 | ( | ||
208 | newFunctionDeclarations+=SMTFunctionDeclaration | | ||
209 | typeDefinitions+=SMTCardinalityConstraint | | ||
210 | newFunctionDefinitions+=SMTFunctionDefinition | ||
211 | )* | ||
212 | ')'; | ||
213 | |||
214 | ////////////////////////////////// | ||
215 | // Statistics | ||
216 | ////////////////////////////////// | ||
217 | //IntOrReal returns ecore::EDouble: INT | REAL; | ||
218 | |||
219 | SMTStatisticValue: SMTStatisticIntValue | SMTStatisticDoubleValue; | ||
220 | SMTStatisticIntValue: name = PROPERTYNAME value=INT; | ||
221 | SMTStatisticDoubleValue: name = PROPERTYNAME value = REAL; | ||
222 | SMTStatisticsSection: '(' {SMTStatisticsSection} values += SMTStatisticValue* ')'; \ No newline at end of file | ||