First shot at the handling of regular expressions.

5 files changed, 111 insertions, 5 deletions

diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4
index 64fccb0..ec01c88 100644
--- a/instr-to-kodkod/parser/PropertyLexer.g4
+++ b/instr-to-kodkod/parser/PropertyLexer.g4
@@ -12,7 +12,9 @@ TAG_EXISTING_KW: '(tag_existing' SEP;
 AND_OPERATOR_KW: '(and' SEP;
 OR_OPERATOR_KW: '(or' SEP;
 NOT_OPERATOR_KW: '(not' SEP ;
-IMPLIES_OPERATOR_KW: '(implies' SEP ;
+IMPLIES_OPERATOR_KW: '(implies' SEP;
+
+REGEX_SPECIAL_PREDICATE_KW: '(string_matches' SEP;
 
 EXISTS_OPERATOR_KW: '(exists' SEP;
 FORALL_OPERATOR_KW: '(forall' SEP;
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 986ad3b..3e5634f 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -318,6 +318,50 @@ function [Variable current_node]
    }
 ;
 
+regex_special_predicate [Variable current_node]
+   returns [Formula result]:
+
+   (WS)* REGEX_SPECIAL_PREDICATE_KW
+      id_or_string_or_fun[current_node]
+      STRING
+   (WS)* R_PAREN
+
+   {
+      try
+      {
+         $result =
+            ($id_or_string_or_fun.value).product
+            (
+               Main.get_string_manager().get_regex_as_relation
+               (
+                  ($STRING.text)
+               )
+            ).in
+            (
+               Main.get_model().get_predicate_as_relation
+               (
+                  "is_start_node"
+               ).transpose()
+            );
+      }
+      catch (final Exception e)
+      {
+         System.err.println
+         (
+            "[F] A problem occured while handling a regex related predicate in"
+            + " the property (l."
+            + ($REGEX_SPECIAL_PREDICATE_KW.getLine())
+            + " c."
+            + ($REGEX_SPECIAL_PREDICATE_KW.getCharPositionInLine())
+            + "):"
+            + e.getMessage()
+         );
+
+         System.exit(-1);
+      }
+   }
+;
+
 non_empty_formula_list [Variable current_node]
    returns [List<Formula> list]
 
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index 6a2445b..11a357a 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -10,6 +10,7 @@ import kodkod.ast.Formula;
 
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
+import kodkod.engine.config.ConsoleReporter;
 import kodkod.engine.satlab.SATFactory;
 
 import kodkod.instance.Bounds;
@@ -337,7 +338,14 @@ public class Main
          return;
       }
 
-      /* 6/ Add all types and used predicates to the Universe. */
+      /* 6/ Handle regexps */
+      STRING_MANAGER.populate_regex_predicate
+      (
+         MODEL.get_predicate("string_matches")
+      );
+
+
+      /* 7/ Add all types and used predicates to the Universe. */
       univ = new Universe(MODEL.get_atoms());
       tf = univ.factory();
       bounds = new Bounds(univ);
@@ -348,7 +356,11 @@ public class Main
       solver = new Solver();
       solver.options().setSkolemDepth(-1);
       solver.options().setSolver(SATFactory.DefaultSAT4J);
-//      solver.options().setReporter(new ConsoleReporter());
+
+      if (PARAMETERS.be_verbose())
+      {
+         solver.options().setReporter(new ConsoleReporter());
+      }
 
       solutions =
          solver.solveAll
diff --git a/instr-to-kodkod/src/StringManager.java b/instr-to-kodkod/src/StringManager.java
index 247d8e3..9d73dd6 100644
--- a/instr-to-kodkod/src/StringManager.java
+++ b/instr-to-kodkod/src/StringManager.java
@@ -1,11 +1,17 @@
-import kodkod.ast.Relation;
-
+import java.util.ArrayList;
+import java.util.Collection;
 import java.util.Map;
 import java.util.HashMap;
+import java.util.Set;
+
+import java.util.regex.Pattern;
+
+import kodkod.ast.Relation;
 
 public class StringManager
 {
    private final Map<String, String> TO_ID;
+   private final Collection<Pattern> regexes;
    private final VHDLType string_type;
    private final String anon_string_prefix;
    private int anon_string_count;
@@ -18,6 +24,8 @@ public class StringManager
    public StringManager ()
    {
       TO_ID = new HashMap<String, String>();
+      regexes = new ArrayList<Pattern>();
+
       string_type = Main.get_model().get_string_type();
       anon_string_prefix = "_string_"; /* TODO: use a program param. */
       anon_string_count = 0;
@@ -45,6 +53,41 @@ public class StringManager
       return string_type.get_member_as_relation(id);
    }
 
+   public Relation get_regex_as_relation
+   (
+      final String str
+   )
+   {
+      regexes.add(Pattern.compile(str));
+
+      return get_string_as_relation(str);
+   }
+
+   public void populate_regex_predicate (final VHDLPredicate rp)
+   {
+      final Set<Map.Entry<String, String>> candidates;
+
+      candidates = TO_ID.entrySet();
+
+      for (final Pattern p: regexes)
+      {
+         for (final Map.Entry<String, String> c: candidates)
+         {
+            if (p.matcher(c.getKey()).matches())
+            {
+               rp.add_member
+               (
+                  new String[]
+                  {
+                     c.getValue(),
+                     TO_ID.get(p.pattern())
+                  }
+               );
+            }
+         }
+      }
+   }
+
    private void add_mapping (String str, final String id)
    {
       str = cleanup_string(str);
diff --git a/instr-to-kodkod/src/VHDLModel.java b/instr-to-kodkod/src/VHDLModel.java
index 5a628e7..5bb11c2 100644
--- a/instr-to-kodkod/src/VHDLModel.java
+++ b/instr-to-kodkod/src/VHDLModel.java
@@ -319,6 +319,11 @@ public class VHDLModel
       }
    }
 
+   public VHDLPredicate get_predicate (final String name)
+   {
+      return predicates.get(name);
+   }
+
    public Relation get_predicate_as_relation (final String name)
    {
       final VHDLPredicate p;