From 067f596822b80b2786ce2bb895a593d479516cad Mon Sep 17 00:00:00 2001
From: Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org>
Date: Mon, 31 Jul 2017 15:05:30 +0200
Subject: First shot at the handling of regular expressions.

---
 instr-to-kodkod/src/Main.java          | 16 ++++++++++--
 instr-to-kodkod/src/StringManager.java | 47 ++++++++++++++++++++++++++++++++--
 instr-to-kodkod/src/VHDLModel.java     |  5 ++++
 3 files changed, 64 insertions(+), 4 deletions(-)

(limited to 'instr-to-kodkod/src')

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;
-- 
cgit v1.2.3-70-g09d2