4 files changed, 79 insertions, 20 deletions

diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index b835c28..d8393bd 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -76,7 +76,7 @@ public class Main
             + "\"..."
          );
 
-         return pro.generate_formula();
+         return pro.generate_base_formula();
       }
       catch (final IOException e)
       {
diff --git a/instr-to-kodkod/src/VHDLModel.java b/instr-to-kodkod/src/VHDLModel.java
index 4b6e053..170ce12 100644
--- a/instr-to-kodkod/src/VHDLModel.java
+++ b/instr-to-kodkod/src/VHDLModel.java
@@ -345,6 +345,16 @@ public class VHDLModel
       }
    }
 
+   public boolean type_exists (final String name)
+   {
+      return types.containsKey(name);
+   }
+
+   public boolean predicate_exists (final String name)
+   {
+      return predicates.containsKey(name);
+   }
+
    public Relation get_atom_as_relation
    (
       final String type,
diff --git a/instr-to-kodkod/src/VHDLProperty.java b/instr-to-kodkod/src/VHDLProperty.java
index a91d25a..ac88e6e 100644
--- a/instr-to-kodkod/src/VHDLProperty.java
+++ b/instr-to-kodkod/src/VHDLProperty.java
@@ -9,13 +9,17 @@ 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_formula ()
+   public Formula generate_base_formula ()
    throws IOException
    {
       final PropertyLexer lexer;
diff --git a/instr-to-kodkod/src/VariableManager.java b/instr-to-kodkod/src/VariableManager.java
index 381a774..eaa20d2 100644
--- a/instr-to-kodkod/src/VariableManager.java
+++ b/instr-to-kodkod/src/VariableManager.java
@@ -5,53 +5,98 @@ import kodkod.ast.*;
 
 public class VariableManager
 {
-   private final Map<String, Variable> from_string;
+   private final Map<String, Expression> from_string;
    private final Map<String, String> tags;
-   private final String var_prefix;
    private int next_id;
 
    public VariableManager (final String var_prefix)
    {
-      from_string = new HashMap<String, Variable>();
+      from_string = new HashMap<String, Expression>();
       tags = new HashMap<String, String>();
-
-      this.var_prefix = var_prefix;
    }
 
-   private String generate_new_id ()
+   private String generate_new_anonymous_variable_name ()
    {
       final String result;
 
-      result = var_prefix + next_id;
+      result = "_var" + next_id;
 
       next_id += 1;
 
       return result;
    }
 
-   public Variable get_variable (final String name)
+   public void add_tag
+   (
+      final String var_name,
+      final String var_type,
+      final String tag_name
+   )
+   throws Exception
    {
-      Variable result;
-
-      result = from_string.get(name);
+      System.out.println("[D] Skolemizing: " + var_name);
 
-      if (result == null)
+      if (from_string.containsKey(var_name))
       {
-         result = Variable.unary(name);
+         throw
+            new Exception
+            (
+               "[F] Invalid property: the variable name \""
+               + var_name
+               + "\" is bound multiple times in the \"tag_existing\""
+               + " operator."
+            );
+      }
 
-         from_string.put(name, result);
+      from_string.put(var_name, Variable.unary(var_name));
+   }
+
+   public Variable add_variable (final String var_name)
+   throws Exception
+   {
+      final Variable result;
+
+      if (from_string.containsKey(var_name))
+      {
+         throw
+            new Exception
+            (
+               "[F] Invalid property: the variable name \""
+               + var_name
+               + "\" is declared multiple times."
+            );
       }
 
+      result = Variable.unary(var_name);
+
+      from_string.put(var_name, result);
+
       return result;
    }
 
-   public Variable generate_new_variable ()
+   public Expression get_variable (final String var_name)
+   throws Exception
    {
-      return get_variable(generate_new_id());
+      final Expression result;
+
+      result = from_string.get(var_name);
+
+      if (result == null)
+      {
+         throw
+            new Exception
+            (
+               "[F] Variable \""
+               + var_name
+               + "\" is used, but not declared."
+            );
+      }
+
+      return result;
    }
 
-   public void tag_variable (final String name, final String tag)
+   public Variable generate_new_anonymous_variable ()
    {
-      tags.put(name, tag);
+      return Variable.unary(generate_new_anonymous_variable_name());
    }
 }