Starting to work on a parser for the properties.

3 files changed, 44 insertions, 1 deletions

diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 6db785e..59bdeb4 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -11,7 +11,7 @@ CLASSPATH = "kodkod.jar:./src/:org.sat4j.core.jar"
 
 ## Dependencies ################################################################
 JAR_SOURCE = https://noot-noot.org/onera_2017/jar/
-REQUIRED_JARS = kodkod.jar org.sat4j.core.jar
+REQUIRED_JARS = kodkod.jar org.sat4j.core.jar antlr-4.7-complete.jar
 
 ## Makefile Magic ##############################################################
 SOURCES = $(wildcard src/*.java)
diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4
new file mode 100644
index 0000000..27f1bca
--- /dev/null
+++ b/instr-to-kodkod/parser/PropertyLexer.g4
@@ -0,0 +1,13 @@
+lexer grammar PropertyLexer;
+
+TAG_EXISTING_KW: '(tag_existing';
+AND_OPERATOR_KW: '(and';
+OR_OPERATOR_KW: '(or';
+NOT_OPERATOR_KW: '(not';
+EXISTS_OPERATOR_KW: '(exists';
+FORALL_OPERATOR_KW: '(forall';
+ID: [a-zA-Z0-9_]+;
+L_PAREN : '(';
+R_PAREN : ')';
+
+WS: [ \t\r\n]+ -> skip;
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
new file mode 100644
index 0000000..740b308
--- /dev/null
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -0,0 +1,30 @@
+parser grammar PropertyParser;
+options { tokenVocab = PropertyLexer; }
+
+prog: tag_existing;
+
+tag_existing
+   : TAG_EXISTING_KW L_PAREN (tag_item)+ R_PAREN formula R_PAREN
+;
+
+tag_item
+   : L_PAREN ID ID R_PAREN
+;
+
+formula
+   : and_operator
+   | or_operator
+   | not_operator
+   | exists_operator
+   | forall_operator
+   | predicate
+;
+
+and_operator: AND_OPERATOR_KW formula (formula)+ R_PAREN;
+or_operator: OR_OPERATOR_KW formula (formula)+ R_PAREN;
+not_operator: NOT_OPERATOR_KW formula R_PAREN;
+exists_operator: EXISTS_OPERATOR_KW ID ID formula R_PAREN;
+forall_operator: FORALL_OPERATOR_KW ID ID formula R_PAREN;
+
+
+predicate: L_PAREN ID (ID)* R_PAREN;