1 | package tuffy.mln; |
2 | |
3 | import java.util.ArrayList; |
4 | |
5 | /** |
6 | * A tuple of constants/variables, represented as |
7 | * a transparent list of integers. |
8 | * |
9 | */ |
10 | public class Tuple { |
11 | |
12 | /** |
13 | * positive element = constant; |
14 | * negative element = variable. |
15 | * variables are encoded as -1, -2, ... |
16 | */ |
17 | public int[] list = null; |
18 | |
19 | // ASSUMPTION OF DATA STRUCTURE: the naming of variables |
20 | // are conducted sequentially by 1 step for each new variable |
21 | // does not see before. |
22 | |
23 | /** |
24 | * The degree of freedom, i.e. the number of distinct variables. |
25 | * Actually, it corresponds to the smallest integer name of variables. |
26 | */ |
27 | public int dimension; |
28 | |
29 | /** |
30 | * Constructor of Tuple. |
31 | * Assuming args is already canonicalized |
32 | * |
33 | * @param args |
34 | */ |
35 | public Tuple(ArrayList<Integer> args) { |
36 | list = new int[args.size()]; |
37 | dimension = 0; |
38 | for(int i=0; i<args.size(); i++) { |
39 | list[i] = args.get(i); |
40 | if(list[i] < dimension) { |
41 | dimension = list[i]; |
42 | } |
43 | } |
44 | dimension = -dimension; |
45 | } |
46 | |
47 | /** |
48 | * Return the i-th element. This value is the variable/constant |
49 | * name of the i-th element. |
50 | */ |
51 | public int get(int i) { |
52 | return list[i]; |
53 | } |
54 | |
55 | ///** |
56 | // * Test if this tuple subsumes the argument. |
57 | // * |
58 | // * @return 1 if subsumes, 0 if equiv, -1 if neither |
59 | // */ |
60 | |
61 | /** |
62 | * Test if the tuple subsumes the argument tuple. |
63 | * Tuple $a$ subsumes tuple $b$, if there exists a mapping $\pi$ |
64 | * from variable to variable/constant, s.t., $\forall i$, |
65 | * $\pi$(a.variable[i]) = b.variable[i]. |
66 | * |
67 | * @return true if subsumes, false otherwise; |
68 | */ |
69 | public boolean subsumes(Tuple other) { |
70 | int[] l2 = other.list; |
71 | assert(list.length == l2.length); |
72 | int[] sub = new int[dimension+1]; |
73 | for(int i=0; i<list.length; i++) { |
74 | if(list[i] > 0) { // a constant |
75 | if(l2[i] != list[i]) return false; |
76 | }else { // a variable |
77 | int target = sub[-list[i]]; |
78 | if(target == 0) { |
79 | sub[-list[i]] = l2[i]; |
80 | }else if(target != l2[i]) { |
81 | return false; |
82 | } |
83 | } |
84 | } |
85 | return true; |
86 | } |
87 | } |