instr-to-kodkod/src/VHDLType.java


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.Map;
import java.util.Set;

import kodkod.ast.Relation;
import kodkod.ast.Formula;

import kodkod.instance.Bounds;
import kodkod.instance.TupleFactory;


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

   public void add_member (final String id)
   {
      if (!members.containsKey(id))
      {
         members.put(id, Relation.unary(id));
      }
   }

   public String get_name ()
   {
      return name;
   }

   public void flag_as_used ()
   {
      if (!is_used)
      {
         if (Main.get_parameters().be_verbose())
         {
            System.out.println("Enabling type: " + name);
         }

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

   public Collection<String> get_all_members_as_atoms ()
   {
      return members.keySet();
   }

   public Formula generate_declarations ()
   {
      Formula result;

      result = Formula.TRUE;

      return result;
   }

   public void add_to_bounds (final Bounds b, final TupleFactory f)
   {
      final Set<Map.Entry<String, Relation>> members_as_set;

      members_as_set = members.entrySet();

      if (name.toLowerCase().equals("string"))
      {
         /* Other types do not require direct access to a member. */
         /* TODO: only bound the strings that are actually mentionned in the
          * formula.
          */
         for (final Map.Entry<String, Relation> member: members_as_set)
         {
            b.boundExactly(member.getValue(), f.setOf(member.getKey()));
         }
      }
      /*
       * the toArray() is required to avoid the collection being considered as
       * a single atom.
       */
      b.boundExactly(as_relation, f.setOf(get_all_members_as_atoms().toArray()));
   }
}