Unused predicates & types -> not in kodkod.

4 files changed, 78 insertions, 13 deletions

diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index ec55450..ba9ebaa 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -9,6 +9,7 @@ import kodkod.instance.*;
 public class Main
 {
    private static Parameters PARAMETERS;
+   private static VHDLModel MODEL;
 
    private static Formula get_formula (final VHDLModel model)
    {
@@ -25,14 +26,21 @@ public class Main
 
    public static void main (final String... args)
    {
-      final VHDLModel model;
-
+      /*
+       * Order of operations:
+       * 1/ Load Levels (Types + predicates)
+       * 2/ Load Properties (will change 'is_used()' on predicates)
+       * 3/ Generate complementary model according to used predicates.
+       * 4/ Load Model, but only for used predicates and types.
+       * 5/ Add all used types and predicates to the Universe.
+       */
       final Universe univ;
       final TupleFactory tf;
       final Bounds bounds;
 
       final Solver solver;
       final Solution sol;
+      final Formula property;
 
       PARAMETERS = new Parameters(args);
 
@@ -41,13 +49,14 @@ public class Main
          return;
       }
 
-      model = new VHDLModel();
+      MODEL = new VHDLModel();
 
+      /* 1/ Load Levels (Types + predicates) */
       try
       {
          VHDLLevel.add_to_model
          (
-            model,
+            MODEL,
             (
                PARAMETERS.get_levels_directory()
                + "/structural_level.data"
@@ -62,9 +71,17 @@ public class Main
          return;
       }
 
+       /* 2/ Load Properties (will change 'is_used()' on predicates) */
+       property = get_formula(MODEL);
+       /* TODO */
+
+       /* 3/ Generate complementary model according to used predicates. */
+       /* TODO */
+
+      /* 4/ Load Model, but only for used predicates and types. */
       try
       {
-         model.parse_file(PARAMETERS.get_model_file());
+         MODEL.parse_file(PARAMETERS.get_model_file());
       }
       catch (final Exception e)
       {
@@ -74,17 +91,18 @@ public class Main
          return;
       }
 
-      univ = new Universe(model.get_atoms());
+      /* 5/ Add all types and used predicates to the Universe. */
+      univ = new Universe(MODEL.get_atoms());
       tf = univ.factory();
       bounds = new Bounds(univ);
 
-      model.add_to_bounds(bounds, tf);
+      MODEL.add_to_bounds(bounds, tf);
 
       solver = new Solver();
       solver.options().setSolver(SATFactory.DefaultSAT4J);
       solver.options().setReporter(new ConsoleReporter());
 
-      sol = solver.solve(get_formula(model), bounds);
+      sol = solver.solve(property, bounds);
 
       System.out.println(sol);
    }
diff --git a/instr-to-kodkod/src/VHDLModel.java b/instr-to-kodkod/src/VHDLModel.java
index bdb5e4b..ed448c4 100644
--- a/instr-to-kodkod/src/VHDLModel.java
+++ b/instr-to-kodkod/src/VHDLModel.java
@@ -178,7 +178,10 @@ public class VHDLModel
          return false;
       }
 
-      t.add_member(cmd[2]);
+      if (t.is_used())
+      {
+         t.add_member(cmd[2]);
+      }
 
       return true;
    }
@@ -230,6 +233,11 @@ public class VHDLModel
          return false;
       }
 
+      if (!p.is_used())
+      {
+         return true;
+      }
+
       if (params.length != p.get_arity())
       {
          System.err.println
@@ -293,12 +301,18 @@ public class VHDLModel
    {
       for (final VHDLType t: types.values())
       {
-         t.add_to_bounds(b, f);
+         if (t.is_used())
+         {
+            t.add_to_bounds(b, f);
+         }
       }
 
       for (final VHDLPredicate p: predicates.values())
       {
-         p.add_to_bounds(b, f);
+         if (p.is_used())
+         {
+            p.add_to_bounds(b, f);
+         }
       }
    }
 
diff --git a/instr-to-kodkod/src/VHDLPredicate.java b/instr-to-kodkod/src/VHDLPredicate.java
index a94e5ec..210dd7e 100644
--- a/instr-to-kodkod/src/VHDLPredicate.java
+++ b/instr-to-kodkod/src/VHDLPredicate.java
@@ -14,6 +14,7 @@ public class VHDLPredicate
    private final String name;
    private final int arity;
    private final Relation as_relation;
+   private boolean is_used;
 
    public VHDLPredicate (final String name, final VHDLType[] signature)
    {
@@ -22,6 +23,7 @@ public class VHDLPredicate
 
       signatures = new ArrayList<VHDLType[]>();
       members = new ArrayList<String[]>();
+      is_used = false;
 
       as_relation = Relation.nary(name, arity);
 
@@ -33,6 +35,11 @@ public class VHDLPredicate
       members.add(tuple);
    }
 
+   public boolean is_used ()
+   {
+      return is_used;
+   }
+
    public int get_arity ()
    {
       return arity;
@@ -40,13 +47,26 @@ public class VHDLPredicate
 
    public Relation get_as_relation ()
    {
+      if (!is_used)
+      {
+         for (final VHDLType[] sig: signatures)
+         {
+            for (final VHDLType t: sig)
+            {
+               t.flag_as_used();
+            }
+         }
+
+         is_used = true;
+      }
+
       return as_relation;
    }
 
    /* pre: i < get_arity() */
    public boolean accepts_as_nth_param (final int i, final String id)
    {
-      for (VHDLType[] sig: signatures)
+      for (final VHDLType[] sig: signatures)
       {
          if (sig[i].get_member_as_relation(id) != null)
          {
diff --git a/instr-to-kodkod/src/VHDLType.java b/instr-to-kodkod/src/VHDLType.java
index c4c1b0f..73cd9cf 100644
--- a/instr-to-kodkod/src/VHDLType.java
+++ b/instr-to-kodkod/src/VHDLType.java
@@ -12,10 +12,12 @@ public class VHDLType
    private final Map<String, Relation> members;
    private final String name;
    private final Relation as_relation;
+   private boolean is_used;
 
    public VHDLType (final String name)
    {
       members = new HashMap<String, Relation>();
+      is_used = false;
 
       this.name = name;
       as_relation = Relation.unary(name);
@@ -31,12 +33,23 @@ public class VHDLType
       return name;
    }
 
+   public void flag_as_used ()
+   {
+      is_used = true;
+   }
+
+   public boolean is_used ()
+   {
+      return is_used;
+   }
+
    public Relation get_as_relation ()
    {
+      is_used = true;
+
       return as_relation;
    }
 
-
    public Relation get_member_as_relation (final String id)
    {
       return members.get(id);