1 | package tuffy.mln; |
2 | |
3 | import tuffy.util.ExceptionMan; |
4 | |
5 | /** |
6 | * A term in first-order logic; either a variable or a constant. |
7 | */ |
8 | public class Term { |
9 | |
10 | /** |
11 | * Whether this term is a variable. |
12 | */ |
13 | private boolean isVariable; |
14 | |
15 | public boolean isOriAConstant = false; |
16 | |
17 | public int oriConstantID = -1; |
18 | |
19 | /** |
20 | * The name of this term. $var$ is not null iff. |
21 | * this term is a variable. |
22 | */ |
23 | private String var = null; |
24 | |
25 | /** |
26 | * The ID of this term. $constantID$ is not null iff. |
27 | * this term is a constant. |
28 | */ |
29 | private Integer constantID = null; |
30 | |
31 | |
32 | /** |
33 | * Constructor of Term (variable version). |
34 | * |
35 | * @param var name of the variable |
36 | */ |
37 | public Term(String var){ |
38 | isVariable = true; |
39 | this.var = var; |
40 | } |
41 | |
42 | public void reSet(String var){ |
43 | if(isVariable == false){ |
44 | ExceptionMan.die("Cannot reset a constant term with a variable!"); |
45 | } |
46 | this.var = var; |
47 | } |
48 | |
49 | public void reSet(Integer cid){ |
50 | if(isVariable == true){ |
51 | ExceptionMan.die("Cannot reset a variable term with a constant!"); |
52 | } |
53 | this.constantID = cid; |
54 | } |
55 | |
56 | /** |
57 | * Constructor a Term (constant version). |
58 | * |
59 | * @param cid the constant in the form of its integer ID |
60 | */ |
61 | public Term(Integer cid){ |
62 | isVariable = false; |
63 | constantID = cid; |
64 | } |
65 | |
66 | /** |
67 | * Return whether this term is a variable. |
68 | */ |
69 | public boolean isVariable(){ |
70 | return isVariable; |
71 | } |
72 | |
73 | /** |
74 | * |
75 | * @return Whether this term is a constant. |
76 | */ |
77 | public boolean isConstant(){ |
78 | return !isVariable; |
79 | } |
80 | |
81 | /** |
82 | * @return The name of this term, which is null when it is |
83 | * a constant. |
84 | */ |
85 | public String var(){ |
86 | return var; |
87 | } |
88 | |
89 | /** |
90 | * |
91 | * @return The name of this term, which is null when it is |
92 | * a variable. |
93 | */ |
94 | public int constant(){ |
95 | return constantID; |
96 | } |
97 | |
98 | /** |
99 | * @return This term's human-friendly representation. |
100 | */ |
101 | public String toString() { |
102 | if(isVariable) { |
103 | return var; |
104 | }else { |
105 | return Integer.toString(constantID); |
106 | } |
107 | } |
108 | |
109 | } |