blob: eaa20d258f3d1165d01cdf3f5806e810cd1e06ab (
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
|
/* FIXME: finer imports. */
import java.util.*;
import kodkod.ast.*;
public class VariableManager
{
private final Map<String, Expression> from_string;
private final Map<String, String> tags;
private int next_id;
public VariableManager (final String var_prefix)
{
from_string = new HashMap<String, Expression>();
tags = new HashMap<String, String>();
}
private String generate_new_anonymous_variable_name ()
{
final String result;
result = "_var" + next_id;
next_id += 1;
return result;
}
public void add_tag
(
final String var_name,
final String var_type,
final String tag_name
)
throws Exception
{
System.out.println("[D] Skolemizing: " + var_name);
if (from_string.containsKey(var_name))
{
throw
new Exception
(
"[F] Invalid property: the variable name \""
+ var_name
+ "\" is bound multiple times in the \"tag_existing\""
+ " operator."
);
}
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 Expression get_variable (final String var_name)
throws Exception
{
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 Variable generate_new_anonymous_variable ()
{
return Variable.unary(generate_new_anonymous_variable_name());
}
}
|
