| summaryrefslogtreecommitdiff | 
diff options
Diffstat (limited to 'instr-to-kodkod/src')
| -rw-r--r-- | instr-to-kodkod/src/Main.java | 16 | ||||
| -rw-r--r-- | instr-to-kodkod/src/StringManager.java | 47 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VHDLModel.java | 5 | 
3 files changed, 64 insertions, 4 deletions
| 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; | 


