instr-to-kodkod/src/VHDLPredicate.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
111
112
113
114

/* FIXME: Finer imports */
import java.util.*;

import kodkod.ast.*;
import kodkod.ast.operator.*;

import kodkod.instance.*;


public class VHDLPredicate
{
   private final Collection<VHDLType[]> signatures;
   private final Collection<String[]> members;
   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)
   {
      this.name = name;
      arity = signature.length;

      signatures = new ArrayList<VHDLType[]>();
      members = new ArrayList<String[]>();
      is_used = false;

      as_relation = Relation.nary(name, arity);

      signatures.add(signature);
   }

   public void add_member (final String[] tuple)
   {
      members.add(tuple);
   }

   public boolean is_used ()
   {
      return is_used;
   }

   public int get_arity ()
   {
      return arity;
   }

   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 (final VHDLType[] sig: signatures)
      {
         if (sig[i].get_member_as_relation(id) != null)
         {
            return true;
         }
      }

      return false;
   }

   public boolean add_signature (final VHDLType[] signature)
   {
      if (signature.length != get_arity())
      {
         return false;
      }

      signatures.add(signature);

      return true;
   }

   public String get_name ()
   {
      return name;
   }

   public void add_to_bounds (final Bounds b, final TupleFactory f)
   {
      final TupleSet as_tuples;

      /* Empty tuple set, will contain tuples of the right arity. */
      as_tuples = f.noneOf(get_arity());

      /* For every member of this predicate ... */
      for (final Object[] ref: members)
      {
         /* add a new tuple to the tuple set representing the predicate. */
         as_tuples.add(f.tuple(ref));
      }

      /* We now have the exact definition of the predicate as a relation */
      b.boundExactly(as_relation, as_tuples);
   }
}