Adds 'eq' and 'iff' to the language.

2 files changed, 38 insertions, 0 deletions

diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4
index f5b553e..46a6d3d 100644
--- a/instr-to-kodkod/parser/PropertyLexer.g4
+++ b/instr-to-kodkod/parser/PropertyLexer.g4
@@ -9,11 +9,13 @@ R_BRAKT: ']';
 
 TAG_EXISTING_KW: '(tag_existing' SEP;
 
+IFF_OPERATOR_KW: '(iff' SEP;
 AND_OPERATOR_KW: '(and' SEP;
 OR_OPERATOR_KW: '(or' SEP;
 NOT_OPERATOR_KW: '(not' SEP ;
 IMPLIES_OPERATOR_KW: '(implies' SEP;
 
+EQ_SPECIAL_PREDICATE_KW: '(eq' SEP;
 REGEX_SPECIAL_PREDICATE_KW: '(string_matches' SEP;
 
 EXISTS_OPERATOR_KW: '(exists' SEP;
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 021f02c..778f49c 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -318,6 +318,19 @@ function [Variable current_node]
    }
 ;
 
+eq_special_predicate [Variable current_node]
+   returns [Formula result]:
+
+   (WS)* EQ_SPECIAL_PREDICATE_KW
+      a=id_or_string_or_fun[current_node]
+      (WS)+ b=id_or_string_or_fun[current_node]
+   (WS)* R_PAREN
+
+   {
+      $result = ($a.value).eq(($b.value));
+   }
+;
+
 regex_special_predicate [Variable current_node]
    returns [Formula result]:
 
@@ -448,6 +461,19 @@ implies_operator [Variable current_node]
    }
 ;
 
+iff_operator [Variable current_node]
+   returns [Formula result]:
+
+   (WS)* IFF_OPERATOR_KW
+      a=formula[current_node]
+      b=formula[current_node]
+   (WS)* R_PAREN
+
+   {
+      $result = ($a.result).iff(($b.result));
+   }
+;
+
 /** Quantified Expressions ****************************************************/
 variable_declaration
    returns [Variable var_as_var, Relation type_as_rel]:
@@ -1303,6 +1329,11 @@ formula [Variable current_node]
       $result = ($predicate.result);
    }
 
+   | eq_special_predicate[current_node]
+   {
+      $result = ($eq_special_predicate.result);
+   }
+
    | regex_special_predicate[current_node]
    {
       $result = ($regex_special_predicate.result);
@@ -1323,6 +1354,11 @@ formula [Variable current_node]
       $result = ($not_operator.result);
    }
 
+   | iff_operator[current_node]
+   {
+      $result = ($iff_operator.result);
+   }
+
    | implies_operator[current_node]
    {
       $result = ($implies_operator.result);