Tagged variables are now the only skolemized vars.skol_only_the_solution

5 files changed, 99 insertions, 20 deletions

diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index fa91a23..7232a6e 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -10,9 +10,9 @@ LEVEL_DIR = $(wildcard ../data/level/*.lvl)
 #PROPERTY_FILE = ../data/property/unread_waveforms.pro
 #PROPERTY_FILE = ../data/property/impossible_processes.pro
 #PROPERTY_FILE = ../data/property/incrementer.pro
-#PROPERTY_FILE = ../data/property/combinational_processes.pro
+PROPERTY_FILE = ../data/property/combinational_processes.pro
 #PROPERTY_FILE = ../data/property/likely_a_clock.pro
-PROPERTY_FILE = ../data/property/cnes/CNE*.pro
+#PROPERTY_FILE = ../data/property/cnes/CNE*.pro
 VAR_PREFIX = "_anon_"
 
 ## Executables #################################################################
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index d8393bd..554fa17 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -222,10 +222,13 @@ public class Main
       /*
        * 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.
+       * 2/ Load Mappings (string handling, some already have IDs).
+       * 3/ Load Property (will change 'is_used()' on predicates).
+       * 4/ Generate model according to the used predicates.
+       * 5/ Load Model, but only for used predicates and types.
+       * 6/ Add all used types and predicates to the Universe.
+       * 7/ Solve regular expressions.
+       * 8/ Add constraints linked to tagged variables.
        */
       final Universe univ;
       final TupleFactory tf;
@@ -259,8 +262,7 @@ public class Main
          return;
       }
 
-      /* 2/ Load Properties (will change 'is_used()' on predicates) */
-      /* FIXME? Currently only one property, due to the 'is_used' */
+      /* 3/ Load Properties (will change 'is_used()' on predicates) */
       property = load_property();
 
       if (property == null)
@@ -276,27 +278,37 @@ public class Main
          );
       }
 
-      /* 3/ Generate complementary model according to used predicates. */
-      /* TODO */
+      /* 4/ Generate model according to used predicates. */
+      /* Done implicitly by step 5.
 
-      /* 4/ Load Model, but only for used predicates and types. */
+      /* 5/ Load Model, but only for used predicates and types. */
       if (!load_models())
       {
          return;
       }
 
-      /* 5/ Add all types and used predicates to the Universe. */
+      /* 6/ 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);
+      VARIABLE_MANAGER.add_tagged_variables_to_bounds(bounds, tf);
 
       solver = new Solver();
+      solver.options().setSkolemDepth(-1);
       solver.options().setSolver(SATFactory.DefaultSAT4J);
       solver.options().setReporter(new ConsoleReporter());
 
-      solutions = solver.solveAll(property, bounds);
+      solutions =
+         solver.solveAll
+         (
+            property.and
+            (
+               VARIABLE_MANAGER.generate_tagged_variable_constraints()
+            ),
+            bounds
+         );
 
       while (solutions.hasNext())
       {
diff --git a/instr-to-kodkod/src/VHDLModel.java b/instr-to-kodkod/src/VHDLModel.java
index 170ce12..b1086f1 100644
--- a/instr-to-kodkod/src/VHDLModel.java
+++ b/instr-to-kodkod/src/VHDLModel.java
@@ -329,6 +329,11 @@ public class VHDLModel
       }
    }
 
+   public VHDLType get_type (final String name)
+   {
+      return types.get(name);
+   }
+
    public Relation get_type_as_relation (final String name)
    {
       final VHDLType t;
diff --git a/instr-to-kodkod/src/VHDLProperty.java b/instr-to-kodkod/src/VHDLProperty.java
index ac88e6e..f74aae4 100644
--- a/instr-to-kodkod/src/VHDLProperty.java
+++ b/instr-to-kodkod/src/VHDLProperty.java
@@ -9,14 +9,10 @@ import org.antlr.v4.runtime.*;
 public class VHDLProperty
 {
    private final String filename;
-   private final List<Variable> tagged_variables;
-   private final List<VHDLType> tagged_variables_types;
 
    public VHDLProperty (final String filename)
    {
       this.filename = filename;
-      tagged_variables = new ArrayList<Variable>();
-      tagged_variables_types = new ArrayList<VHDLType>();
    }
 
    public Formula generate_base_formula ()
diff --git a/instr-to-kodkod/src/VariableManager.java b/instr-to-kodkod/src/VariableManager.java
index eaa20d2..4753341 100644
--- a/instr-to-kodkod/src/VariableManager.java
+++ b/instr-to-kodkod/src/VariableManager.java
@@ -3,16 +3,18 @@ import java.util.*;
 
 import kodkod.ast.*;
 
+import kodkod.instance.*;
+
 public class VariableManager
 {
    private final Map<String, Expression> from_string;
-   private final Map<String, String> tags;
+   private final Map<String, TaggedVariable> tagged_variables;
    private int next_id;
 
    public VariableManager (final String var_prefix)
    {
       from_string = new HashMap<String, Expression>();
-      tags = new HashMap<String, String>();
+      tagged_variables = new HashMap<String, TaggedVariable>();
    }
 
    private String generate_new_anonymous_variable_name ()
@@ -34,6 +36,8 @@ public class VariableManager
    )
    throws Exception
    {
+      final TaggedVariable tg;
+
       System.out.println("[D] Skolemizing: " + var_name);
 
       if (from_string.containsKey(var_name))
@@ -48,7 +52,10 @@ public class VariableManager
             );
       }
 
-      from_string.put(var_name, Variable.unary(var_name));
+      tg = new TaggedVariable(var_name, var_type, tag_name);
+
+      from_string.put(var_name, tg.as_relation);
+      tagged_variables.put(var_name, tg);
    }
 
    public Variable add_variable (final String var_name)
@@ -99,4 +106,63 @@ public class VariableManager
    {
       return Variable.unary(generate_new_anonymous_variable_name());
    }
+
+   public void add_tagged_variables_to_bounds
+   (
+      final Bounds b,
+      final TupleFactory f
+   )
+   {
+      for (final TaggedVariable tg: tagged_variables.values())
+      {
+         b.bound
+         (
+            tg.as_relation,
+            f.setOf(new Object[0]),
+            f.setOf
+            (
+               Main.get_model().get_type
+               (
+                  tg.type
+               ).get_all_members_as_atoms().toArray()
+            )
+         );
+      }
+   }
+
+   public Formula generate_tagged_variable_constraints ()
+   {
+      Formula result;
+
+      result = Formula.TRUE;
+
+      for (final TaggedVariable tg: tagged_variables.values())
+      {
+         result = result.and(tg.as_relation.one());
+      }
+
+      return result;
+   }
+
+   private static class TaggedVariable
+   {
+      private final String name;
+      private final String type;
+      private final String tag;
+      private final Relation as_relation;
+
+      private TaggedVariable
+      (
+         final String name,
+         final String type,
+         final String tag
+      )
+      {
+         this.name = name;
+         this.type = type;
+         this.tag = tag;
+
+         as_relation = Relation.unary(name);
+      }
+   }
 }