blob: 1b4d16dec7469169e2bdc8d40a5c2ae199e75087 (
plain)
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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
import java.util.ArrayList;
import java.util.Collection;
import kodkod.ast.Relation;
import kodkod.instance.Bounds;
import kodkod.instance.TupleFactory;
import kodkod.instance.TupleSet;
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 final boolean is_function;
private boolean is_used;
public VHDLPredicate
(
final String name,
final VHDLType[] signature,
final boolean is_function
)
{
this.name = name;
this.is_function = is_function;
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 boolean is_function ()
{
return is_function;
}
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;
if (Main.get_parameters().be_verbose())
{
System.out.println("Enabling predicate: " + name);
}
}
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);
}
}
|
