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