Tagged variables are now the only skolemized vars.skol_only_the_solution

1 files changed, 69 insertions, 3 deletions

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);
+      }
+   }
 }