Change operator for predicate definition

author: Kristóf Marussy <marussy@mit.bme.hu> 2021-07-02 01:05:54 +0200
committer: Kristóf Marussy <marussy@mit.bme.hu> 2021-07-02 01:05:54 +0200
commit: e5a042909a448a82e164aa1c89cc6faf0cbff357 (patch)
tree: b4d9bcd777f5e94f53051e045d5c73c2a2de7a99 /language
parent: Fonts and ligatures (diff)
download: refinery-e5a042909a448a82e164aa1c89cc6faf0cbff357.tar.gz
refinery-e5a042909a448a82e164aa1c89cc6faf0cbff357.tar.zst
refinery-e5a042909a448a82e164aa1c89cc6faf0cbff357.zip
3 files changed, 15 insertions, 15 deletions
diff --git a/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext b/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext
index 4aeb0acd..9e032a13 100644
--- a/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext
+++ b/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext
@@ -35,7 +35,7 @@ PredicateDefinition:
        (error?="error" "pred"? | "pred")
        name=Identifier
        "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")"
-        (":-" bodies+=Conjunction (";" bodies+=Conjunction)*)?
+        ("<=>" bodies+=Conjunction (";" bodies+=Conjunction)*)?
        ".";
 Parameter:
diff --git a/language/src/test/java/org/eclipse/viatra/solver/language/tests/ProblemParsingTest.xtend b/language/src/test/java/org/eclipse/viatra/solver/language/tests/ProblemParsingTest.xtend
index 7a6eec6a..fcf05d1d 100644
--- a/language/src/test/java/org/eclipse/viatra/solver/language/tests/ProblemParsingTest.xtend
+++ b/language/src/test/java/org/eclipse/viatra/solver/language/tests/ProblemParsingTest.xtend
@@ -42,7 +42,7 @@ class ProblemParsingTest {
                        }
                        
                        % A child cannot have any dependents.
-                        error invalidTaxStatus(Person p) :-
+                        error invalidTaxStatus(Person p) <=>
                                taxStatus(p, child), children(p, _q).
                        
                        Family('family').
diff --git a/language/src/test/java/org/eclipse/viatra/solver/language/tests/scoping/NodeScopingTest.xtend b/language/src/test/java/org/eclipse/viatra/solver/language/tests/scoping/NodeScopingTest.xtend
index 91a9e8a4..5c34083c 100644
--- a/language/src/test/java/org/eclipse/viatra/solver/language/tests/scoping/NodeScopingTest.xtend
+++ b/language/src/test/java/org/eclipse/viatra/solver/language/tests/scoping/NodeScopingTest.xtend
@@ -42,7 +42,7 @@ class NodeScopingTest {
        @Test
        def void implicitNodeInAssertionTest() {
                val it = parseHelper.parse('''
-                        pred predicate(node x, node y) :- node(x).
+                        pred predicate(node x, node y) <=> node(x).
                        predicate(a, a).
                        ?predicate(a, b).
                ''')
@@ -66,7 +66,7 @@ class NodeScopingTest {
        def void implicitNodeInPredicateTest() {
                val it = parseHelper.parse('''
-                        pred predicate(node a) :- node(b).
+                        pred predicate(node a) <=> node(b).
                        predicate(b).
                ''')
                assertThat(errors, empty)
@@ -78,7 +78,7 @@ class NodeScopingTest {
        @Test
        def void quotedNodeInAssertionTest() {
                val it = parseHelper.parse('''
-                        pred predicate(node x, node y) :- node(x).
+                        pred predicate(node x, node y) <=> node(x).
                        predicate('a', 'a').
                        ?predicate('a', 'b').
                ''')
@@ -103,7 +103,7 @@ class NodeScopingTest {
        @Test
        def void quotedNodeInPredicateTest() {
                val it = parseHelper.parse('''
-                        pred predicate(node a) :- node('b').
+                        pred predicate(node a) <=> node('b').
                ''')
                assertThat(errors, empty)
                assertThat(nodeNames, hasItem("'b'"))
@@ -114,7 +114,7 @@ class NodeScopingTest {
        @MethodSource("builtInNodeReferencesSource")
        def void builtInNodeTest(String qualifiedName) {
                val it = parseHelper.parse('''
-                        pred predicate(node x) :- node(x).
+                        pred predicate(node x) <=> node(x).
                        predicate(«qualifiedName»).
                ''')
                assertThat(errors, empty)
@@ -137,7 +137,7 @@ class NodeScopingTest {
        @MethodSource("builtInNodeReferencesSource")
        def void builtInNodeInPredicateTest(String qualifiedName) {
                val it = parseHelper.parse('''
-                        pred predicate(node x) :- node(«qualifiedName»).
+                        pred predicate(node x) <=> node(«qualifiedName»).
                ''')
                assertThat(errors, empty)
                assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(builtin.findClass('int').newNode))
@@ -156,7 +156,7 @@ class NodeScopingTest {
                val it = parseHelper.parse('''
                        «IF namedProblem»problem test.«ENDIF»
                        class Foo.
-                        pred predicate(node x) :- node(x).
+                        pred predicate(node x) <=> node(x).
                        predicate(«qualifiedName»).
                ''')
                assertThat(errors, empty)
@@ -183,7 +183,7 @@ class NodeScopingTest {
                val it = parseHelper.parse('''
                        «IF namedProblem»problem test.«ENDIF»
                        class Foo.
-                        pred predicate(node x) :- node(«qualifiedName»).
+                        pred predicate(node x) <=> node(«qualifiedName»).
                ''')
                assertThat(errors, empty)
                assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(findClass('Foo').newNode))
@@ -201,7 +201,7 @@ class NodeScopingTest {
        def void newNodeIsNotSpecial() {
                val it = parseHelper.parse('''
                        class Foo.
-                        pred predicate(node x) :- node(x).
+                        pred predicate(node x) <=> node(x).
                        predicate(new).
                ''')
                assertThat(errors, empty)
@@ -215,7 +215,7 @@ class NodeScopingTest {
                val it = parseHelper.parse('''
                        «IF namedProblem»problem test.«ENDIF»
                        enum Foo { alpha, beta }
-                        pred predicate(Foo a) :- node(a).
+                        pred predicate(Foo a) <=> node(a).
                        predicate(«qualifiedName»).
                ''')
                assertThat(errors, empty)
@@ -242,7 +242,7 @@ class NodeScopingTest {
                val it = parseHelper.parse('''
                        «IF namedProblem»problem test.«ENDIF»
                        enum Foo { alpha, beta }
-                        pred predicate(Foo a) :- node(«qualifiedName»).
+                        pred predicate(Foo a) <=> node(«qualifiedName»).
                ''')
                assertThat(errors, empty)
                assertThat(nodes, empty)
@@ -264,7 +264,7 @@ class NodeScopingTest {
        @MethodSource("builtInEnumLiteralReferencesSource")
        def void builtInEnumLiteralTest(String qualifiedName) {
                val it = parseHelper.parse('''
-                        pred predicate(node a) :- node(a).
+                        pred predicate(node a) <=> node(a).
                        predicate(«qualifiedName»).
                ''')
                assertThat(errors, empty)
@@ -287,7 +287,7 @@ class NodeScopingTest {
        @MethodSource("builtInEnumLiteralReferencesSource")
        def void bultInEnumLiteralInPredicateTest(String qualifiedName) {
                val it = parseHelper.parse('''
-                        pred predicate() :- node(«qualifiedName»).
+                        pred predicate() <=> node(«qualifiedName»).
                ''')
                assertThat(errors, empty)
                assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(builtin.findEnum("bool").literal("true")))
author	Kristóf Marussy <marussy@mit.bme.hu>	2021-07-02 01:05:54 +0200
committer	Kristóf Marussy <marussy@mit.bme.hu>	2021-07-02 01:05:54 +0200
commit	e5a042909a448a82e164aa1c89cc6faf0cbff357 (patch)
tree	b4d9bcd777f5e94f53051e045d5c73c2a2de7a99 /language
parent	Fonts and ligatures (diff)
download	refinery-e5a042909a448a82e164aa1c89cc6faf0cbff357.tar.gz refinery-e5a042909a448a82e164aa1c89cc6faf0cbff357.tar.zst refinery-e5a042909a448a82e164aa1c89cc6faf0cbff357.zip

diff --git a/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext b/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext index 4aeb0acd..9e032a13 100644 --- a/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext +++ b/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext
@@ -35,7 +35,7 @@ PredicateDefinition:
35	(error?="error" "pred"? \| "pred")	35	(error?="error" "pred"? \| "pred")
36	name=Identifier	36	name=Identifier
37	"(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")"	37	"(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")"
38	(":-" bodies+=Conjunction (";" bodies+=Conjunction)*)?	38	("<=>" bodies+=Conjunction (";" bodies+=Conjunction)*)?
39	".";	39	".";
40		40
41	Parameter:	41	Parameter:


diff --git a/language/src/test/java/org/eclipse/viatra/solver/language/tests/ProblemParsingTest.xtend b/language/src/test/java/org/eclipse/viatra/solver/language/tests/ProblemParsingTest.xtend index 7a6eec6a..fcf05d1d 100644 --- a/language/src/test/java/org/eclipse/viatra/solver/language/tests/ProblemParsingTest.xtend +++ b/language/src/test/java/org/eclipse/viatra/solver/language/tests/ProblemParsingTest.xtend
@@ -42,7 +42,7 @@ class ProblemParsingTest {
42	}	42	}
43		43
44	% A child cannot have any dependents.	44	% A child cannot have any dependents.
45	error invalidTaxStatus(Person p) :-	45	error invalidTaxStatus(Person p) <=>
46	taxStatus(p, child), children(p, _q).	46	taxStatus(p, child), children(p, _q).
47		47
48	Family('family').	48	Family('family').


diff --git a/language/src/test/java/org/eclipse/viatra/solver/language/tests/scoping/NodeScopingTest.xtend b/language/src/test/java/org/eclipse/viatra/solver/language/tests/scoping/NodeScopingTest.xtend index 91a9e8a4..5c34083c 100644 --- a/language/src/test/java/org/eclipse/viatra/solver/language/tests/scoping/NodeScopingTest.xtend +++ b/language/src/test/java/org/eclipse/viatra/solver/language/tests/scoping/NodeScopingTest.xtend
@@ -42,7 +42,7 @@ class NodeScopingTest {
42	@Test	42	@Test
43	def void implicitNodeInAssertionTest() {	43	def void implicitNodeInAssertionTest() {
44	val it = parseHelper.parse('''	44	val it = parseHelper.parse('''
45	pred predicate(node x, node y) :- node(x).	45	pred predicate(node x, node y) <=> node(x).
46	predicate(a, a).	46	predicate(a, a).
47	?predicate(a, b).	47	?predicate(a, b).
48	''')	48	''')
@@ -66,7 +66,7 @@ class NodeScopingTest {
66		66
67	def void implicitNodeInPredicateTest() {	67	def void implicitNodeInPredicateTest() {
68	val it = parseHelper.parse('''	68	val it = parseHelper.parse('''
69	pred predicate(node a) :- node(b).	69	pred predicate(node a) <=> node(b).
70	predicate(b).	70	predicate(b).
71	''')	71	''')
72	assertThat(errors, empty)	72	assertThat(errors, empty)
@@ -78,7 +78,7 @@ class NodeScopingTest {
78	@Test	78	@Test
79	def void quotedNodeInAssertionTest() {	79	def void quotedNodeInAssertionTest() {
80	val it = parseHelper.parse('''	80	val it = parseHelper.parse('''
81	pred predicate(node x, node y) :- node(x).	81	pred predicate(node x, node y) <=> node(x).
82	predicate('a', 'a').	82	predicate('a', 'a').
83	?predicate('a', 'b').	83	?predicate('a', 'b').
84	''')	84	''')
@@ -103,7 +103,7 @@ class NodeScopingTest {
103	@Test	103	@Test
104	def void quotedNodeInPredicateTest() {	104	def void quotedNodeInPredicateTest() {
105	val it = parseHelper.parse('''	105	val it = parseHelper.parse('''
106	pred predicate(node a) :- node('b').	106	pred predicate(node a) <=> node('b').
107	''')	107	''')
108	assertThat(errors, empty)	108	assertThat(errors, empty)
109	assertThat(nodeNames, hasItem("'b'"))	109	assertThat(nodeNames, hasItem("'b'"))
@@ -114,7 +114,7 @@ class NodeScopingTest {
114	@MethodSource("builtInNodeReferencesSource")	114	@MethodSource("builtInNodeReferencesSource")
115	def void builtInNodeTest(String qualifiedName) {	115	def void builtInNodeTest(String qualifiedName) {
116	val it = parseHelper.parse('''	116	val it = parseHelper.parse('''
117	pred predicate(node x) :- node(x).	117	pred predicate(node x) <=> node(x).
118	predicate(«qualifiedName»).	118	predicate(«qualifiedName»).
119	''')	119	''')
120	assertThat(errors, empty)	120	assertThat(errors, empty)
@@ -137,7 +137,7 @@ class NodeScopingTest {
137	@MethodSource("builtInNodeReferencesSource")	137	@MethodSource("builtInNodeReferencesSource")
138	def void builtInNodeInPredicateTest(String qualifiedName) {	138	def void builtInNodeInPredicateTest(String qualifiedName) {
139	val it = parseHelper.parse('''	139	val it = parseHelper.parse('''
140	pred predicate(node x) :- node(«qualifiedName»).	140	pred predicate(node x) <=> node(«qualifiedName»).
141	''')	141	''')
142	assertThat(errors, empty)	142	assertThat(errors, empty)
143	assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(builtin.findClass('int').newNode))	143	assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(builtin.findClass('int').newNode))
@@ -156,7 +156,7 @@ class NodeScopingTest {
156	val it = parseHelper.parse('''	156	val it = parseHelper.parse('''
157	«IF namedProblem»problem test.«ENDIF»	157	«IF namedProblem»problem test.«ENDIF»
158	class Foo.	158	class Foo.
159	pred predicate(node x) :- node(x).	159	pred predicate(node x) <=> node(x).
160	predicate(«qualifiedName»).	160	predicate(«qualifiedName»).
161	''')	161	''')
162	assertThat(errors, empty)	162	assertThat(errors, empty)
@@ -183,7 +183,7 @@ class NodeScopingTest {
183	val it = parseHelper.parse('''	183	val it = parseHelper.parse('''
184	«IF namedProblem»problem test.«ENDIF»	184	«IF namedProblem»problem test.«ENDIF»
185	class Foo.	185	class Foo.
186	pred predicate(node x) :- node(«qualifiedName»).	186	pred predicate(node x) <=> node(«qualifiedName»).
187	''')	187	''')
188	assertThat(errors, empty)	188	assertThat(errors, empty)
189	assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(findClass('Foo').newNode))	189	assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(findClass('Foo').newNode))
@@ -201,7 +201,7 @@ class NodeScopingTest {
201	def void newNodeIsNotSpecial() {	201	def void newNodeIsNotSpecial() {
202	val it = parseHelper.parse('''	202	val it = parseHelper.parse('''
203	class Foo.	203	class Foo.
204	pred predicate(node x) :- node(x).	204	pred predicate(node x) <=> node(x).
205	predicate(new).	205	predicate(new).
206	''')	206	''')
207	assertThat(errors, empty)	207	assertThat(errors, empty)
@@ -215,7 +215,7 @@ class NodeScopingTest {
215	val it = parseHelper.parse('''	215	val it = parseHelper.parse('''
216	«IF namedProblem»problem test.«ENDIF»	216	«IF namedProblem»problem test.«ENDIF»
217	enum Foo { alpha, beta }	217	enum Foo { alpha, beta }
218	pred predicate(Foo a) :- node(a).	218	pred predicate(Foo a) <=> node(a).
219	predicate(«qualifiedName»).	219	predicate(«qualifiedName»).
220	''')	220	''')
221	assertThat(errors, empty)	221	assertThat(errors, empty)
@@ -242,7 +242,7 @@ class NodeScopingTest {
242	val it = parseHelper.parse('''	242	val it = parseHelper.parse('''
243	«IF namedProblem»problem test.«ENDIF»	243	«IF namedProblem»problem test.«ENDIF»
244	enum Foo { alpha, beta }	244	enum Foo { alpha, beta }
245	pred predicate(Foo a) :- node(«qualifiedName»).	245	pred predicate(Foo a) <=> node(«qualifiedName»).
246	''')	246	''')
247	assertThat(errors, empty)	247	assertThat(errors, empty)
248	assertThat(nodes, empty)	248	assertThat(nodes, empty)
@@ -264,7 +264,7 @@ class NodeScopingTest {
264	@MethodSource("builtInEnumLiteralReferencesSource")	264	@MethodSource("builtInEnumLiteralReferencesSource")
265	def void builtInEnumLiteralTest(String qualifiedName) {	265	def void builtInEnumLiteralTest(String qualifiedName) {
266	val it = parseHelper.parse('''	266	val it = parseHelper.parse('''
267	pred predicate(node a) :- node(a).	267	pred predicate(node a) <=> node(a).
268	predicate(«qualifiedName»).	268	predicate(«qualifiedName»).
269	''')	269	''')
270	assertThat(errors, empty)	270	assertThat(errors, empty)
@@ -287,7 +287,7 @@ class NodeScopingTest {
287	@MethodSource("builtInEnumLiteralReferencesSource")	287	@MethodSource("builtInEnumLiteralReferencesSource")
288	def void bultInEnumLiteralInPredicateTest(String qualifiedName) {	288	def void bultInEnumLiteralInPredicateTest(String qualifiedName) {
289	val it = parseHelper.parse('''	289	val it = parseHelper.parse('''
290	pred predicate() :- node(«qualifiedName»).	290	pred predicate() <=> node(«qualifiedName»).
291	''')	291	''')
292	assertThat(errors, empty)	292	assertThat(errors, empty)
293	assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(builtin.findEnum("bool").literal("true")))	293	assertThat(pred("predicate").conj(0).lit(0).arg(0).node, equalTo(builtin.findEnum("bool").literal("true")))