1 | package tuffy.mln; |
2 | import java.util.*; |
3 | |
4 | import tuffy.util.StringMan; |
5 | |
6 | /** |
7 | * A literal in first-order logic. |
8 | */ |
9 | public class Literal implements Cloneable { |
10 | |
11 | /** |
12 | * Predicate object associated with this literal. |
13 | */ |
14 | private Predicate pred; |
15 | |
16 | /** |
17 | * The index of this literal in its parent clause. |
18 | */ |
19 | private int idx = -1; |
20 | |
21 | /** |
22 | * List of terms (variable/constant) contained in this literal. |
23 | */ |
24 | private ArrayList<Term> terms = new ArrayList<Term>(); |
25 | |
26 | /** |
27 | * The positive/negative value of this literal. Here the positive/negative |
28 | * refers to that in Horn clause. |
29 | */ |
30 | private boolean sense; |
31 | |
32 | private boolean coversAllMaterializedTuples = false; |
33 | |
34 | /** |
35 | * The tuple format of this literal. Need call {@link Literal#toTuple()} to make |
36 | * this variable not null. This variable is not automatically maintained. |
37 | * To obtain the most update to date version, you need to call {@link Literal#toTuple()}. |
38 | */ |
39 | private Tuple tuple = null; |
40 | |
41 | /** |
42 | * The name set of all variables in this literal. |
43 | */ |
44 | private HashSet<String> vars = new HashSet<String>(); |
45 | |
46 | |
47 | @SuppressWarnings("unchecked") |
48 | public Object clone() throws CloneNotSupportedException { |
49 | |
50 | Literal clone=(Literal)super.clone(); |
51 | |
52 | // make the shallow copy of the object of type Department |
53 | clone.coversAllMaterializedTuples = coversAllMaterializedTuples; |
54 | clone.idx = -1; |
55 | clone.pred = pred; |
56 | clone.sense = sense; |
57 | clone.terms = (ArrayList<Term>) terms.clone(); |
58 | clone.tuple = tuple; |
59 | clone.vars = (HashSet<String>) vars.clone(); |
60 | return clone; |
61 | |
62 | } |
63 | |
64 | |
65 | /** |
66 | * Return whether the predicate of this literal is a built-in predicate. |
67 | */ |
68 | public boolean isBuiltIn(){ |
69 | return pred.isBuiltIn(); |
70 | } |
71 | |
72 | /** |
73 | * Constructor of Literal. |
74 | * |
75 | * @param predicate the predicate |
76 | * @param sense true for a positive literal; false for a negative one |
77 | */ |
78 | public Literal(Predicate predicate, boolean sense){ |
79 | this.sense = sense; |
80 | this.pred = predicate; |
81 | } |
82 | |
83 | /** |
84 | * Return the set of variable names in this literal. |
85 | */ |
86 | public HashSet<String> getVars(){ |
87 | return vars; |
88 | } |
89 | |
90 | /** |
91 | * Return the predicate of this literal. |
92 | */ |
93 | public Predicate getPred() { |
94 | return pred; |
95 | } |
96 | |
97 | /** |
98 | * Return the list of terms in this literal. |
99 | */ |
100 | public ArrayList<Term> getTerms() { |
101 | return terms; |
102 | } |
103 | |
104 | /** |
105 | * Return the assigned index of this literal in its parent clause. |
106 | */ |
107 | public int getIdx() { |
108 | return idx; |
109 | } |
110 | |
111 | /** |
112 | * Assign an unique (within its parent clause) index to this literal. |
113 | * |
114 | * @param i the index |
115 | * @see Clause#addLiteral(Literal) |
116 | */ |
117 | public void setIdx(int i) { |
118 | idx = i; |
119 | } |
120 | |
121 | ///** |
122 | // * Clique of variables. |
123 | // * Used for the purpose of computing MGU. |
124 | // * |
125 | // * @see Literal#mostGeneralUnification(Tuple) |
126 | // */ |
127 | |
128 | /** |
129 | * Clique of variables. Here by clique, it means a set of |
130 | * variables, plus a constant. |
131 | * |
132 | * @see Literal#mostGeneralUnification(Tuple) |
133 | */ |
134 | private class VarClique{ |
135 | |
136 | /** |
137 | * The set of variable names in this clique. |
138 | */ |
139 | HashSet<String> vars = new HashSet<String>(); |
140 | |
141 | /** |
142 | * The constant of this clique. |
143 | */ |
144 | Integer constant = null; |
145 | |
146 | /** |
147 | * Add variable to this clique. |
148 | * @param v the name of added variable. |
149 | */ |
150 | public void addVar(String v) { |
151 | vars.add(v); |
152 | } |
153 | |
154 | /** |
155 | * Set the constant of this clique. This is allowed when |
156 | * 1) current constant is null; 2) current constant is |
157 | * equals to the changed constant. |
158 | * @param con the added constant. |
159 | * @return whether the intending setting is allowed and succeeded. |
160 | */ |
161 | public boolean setConstant(int con) { |
162 | if(constant != null && constant != con) { |
163 | return false; |
164 | } |
165 | constant = con; |
166 | return true; |
167 | } |
168 | |
169 | /** |
170 | * Merge a new clique with the current one. Here by merge, |
171 | * it requires the constant of these two cliques should be |
172 | * either null or the same. This process involves 1) merging the |
173 | * variable set and 2) check the consistency of constant. |
174 | * @param c the new clique |
175 | * @return whether the intending swallow is allowed and succeeded. |
176 | */ |
177 | public boolean swallow(VarClique c) { |
178 | if(constant != null && c.constant != null |
179 | && constant != c.constant) { |
180 | return false; |
181 | } |
182 | if(constant == null) { |
183 | constant = c.constant; |
184 | } |
185 | vars.addAll(c.vars); |
186 | return true; |
187 | } |
188 | } |
189 | |
190 | /** |
191 | * Compute the most general unification (MGU) of two literals. |
192 | * |
193 | * @param atuple the literal (in the form of a tuple) to be unified |
194 | * @return the MGU in the form of a mapping from |
195 | * variables to variables/constants |
196 | */ |
197 | public HashMap<String, Term> mostGeneralUnification(Tuple atuple){ |
198 | Hashtable<String, VarClique> cliques = new Hashtable<String, VarClique>(); |
199 | int[] tuple = atuple.list; |
200 | for(int i=0; i<terms.size(); i++) { |
201 | Term t = terms.get(i); |
202 | if(t.isConstant()) { |
203 | // const-const map |
204 | if(tuple[i]>0 && t.constant() != tuple[i]) { |
205 | return null; |
206 | } |
207 | // const-var map |
208 | if(tuple[i] < 0) { |
209 | String var = Integer.toString(tuple[i]); |
210 | VarClique clique = cliques.get(var); |
211 | if(clique == null) { |
212 | clique = new VarClique(); |
213 | clique.addVar(var); |
214 | cliques.put(var, clique); |
215 | } |
216 | if(!clique.setConstant(t.constant())) { |
217 | return null; |
218 | } |
219 | } |
220 | }else { |
221 | VarClique clique1 = cliques.get(t.var()); |
222 | if(clique1 == null) { |
223 | clique1 = new VarClique(); |
224 | clique1.addVar(t.var()); |
225 | cliques.put(t.var(), clique1); |
226 | } |
227 | // var-const map |
228 | if(tuple[i] > 0) { |
229 | if(!clique1.setConstant(tuple[i])) { |
230 | return null; |
231 | } |
232 | }else { // var-var map |
233 | String var = Integer.toString(tuple[i]); |
234 | VarClique clique2 = cliques.get(var); |
235 | if(clique2 == null) { |
236 | clique2 = new VarClique(); |
237 | clique2.addVar(var); |
238 | cliques.put(var, clique2); |
239 | } |
240 | if(clique1.swallow(clique2)) { |
241 | for(String v : clique2.vars) { |
242 | cliques.put(v, clique1); |
243 | } |
244 | }else { |
245 | return null; |
246 | } |
247 | } |
248 | } |
249 | } |
250 | |
251 | HashMap<String, Term> lmap = new HashMap<String, Term>(); |
252 | for(String v : vars) { |
253 | VarClique clique = cliques.get(v); |
254 | Term t; |
255 | if(clique.constant == null) { |
256 | t = new Term(clique.toString()); |
257 | }else { |
258 | t = new Term(clique.constant); |
259 | } |
260 | lmap.put(v, t); |
261 | } |
262 | return lmap; |
263 | } |
264 | |
265 | /** |
266 | * Return the human-friendly representation of this literal. |
267 | */ |
268 | public String toString(){ |
269 | String s = (sense ? " " : "!"); |
270 | s += pred.getName(); |
271 | ArrayList<String> a = new ArrayList<String>(); |
272 | for(Term t : terms){ |
273 | if(t.isVariable()){ |
274 | a.add(t.var()); |
275 | }else{ |
276 | a.add("" + t.constant()); |
277 | } |
278 | } |
279 | s += StringMan.commaListParen(a); |
280 | return s; |
281 | } |
282 | |
283 | /** |
284 | * Append a new term to this literal. |
285 | * |
286 | * @param t the term to be appended |
287 | */ |
288 | public void appendTerm(Term t){ |
289 | terms.add(t); |
290 | if(t.isVariable()) { |
291 | vars.add(t.var()); |
292 | } |
293 | } |
294 | |
295 | /** |
296 | * Convert this literal into a tuple. This will assign an internal ID for |
297 | * variables obeying the syntax of class Tuple from Strings. |
298 | */ |
299 | public Tuple toTuple() { |
300 | if(tuple != null) return tuple; |
301 | ArrayList<Integer> tlist = new ArrayList<Integer>(); |
302 | Hashtable<String, Integer> varIDMap = new Hashtable<String, Integer>(); |
303 | for(Term t : terms) { |
304 | if(t.isConstant()) { |
305 | tlist.add(t.constant()); |
306 | }else { |
307 | String v = t.var(); |
308 | Integer id = varIDMap.get(v); |
309 | if(id == null) { |
310 | id = -(varIDMap.size()+1); |
311 | varIDMap.put(v, id); |
312 | } |
313 | tlist.add(id); |
314 | } |
315 | } |
316 | tuple = new Tuple(tlist); |
317 | return tuple; |
318 | } |
319 | |
320 | /** |
321 | * Compare a given literal with this one. By ``same'', it means |
322 | * 1) predicate is same; 2) sense is same; 3) corresponding constant |
323 | * is same; and 4) the name of corresponding variable is same. |
324 | * (Do not consider substitution). |
325 | * @param lit the literal needed to be compared. |
326 | * @return true if these two literals are the same, false otherwise. |
327 | */ |
328 | public boolean isSameAs(Literal lit){ |
329 | if(pred != lit.pred || sense != lit.sense) return false; |
330 | for(int i=0; i < terms.size(); i++){ |
331 | Term t1 = terms.get(i); |
332 | Term t2 = lit.terms.get(i); |
333 | if(t1.isConstant() != t2.isConstant()){ |
334 | return false; |
335 | } |
336 | if(t1.isConstant() && t1.constant() != t2.constant()){ |
337 | return false; |
338 | } |
339 | if(t1.isVariable() && !t1.var().equals(t2.var())){ |
340 | return false; |
341 | } |
342 | } |
343 | return true; |
344 | } |
345 | |
346 | /** |
347 | * Apply a substitution to this literal. |
348 | * |
349 | * @param vmap the substitution |
350 | * @return the new literal |
351 | */ |
352 | public Literal substitute(HashMap<String, Term> vmap) { |
353 | Literal copy = new Literal(pred, sense); |
354 | copy.coversAllMaterializedTuples = coversAllMaterializedTuples; |
355 | for(Term t : terms) { |
356 | if(t.isConstant()) { |
357 | copy.appendTerm(t); |
358 | }else { |
359 | Term t2 = vmap.get(t.var()); |
360 | if(t2 == null) { |
361 | copy.appendTerm(t); |
362 | }else { |
363 | copy.appendTerm(t2); |
364 | } |
365 | } |
366 | } |
367 | return copy; |
368 | } |
369 | |
370 | /** |
371 | * Convert this literal to an atom. |
372 | * |
373 | * @param type indicates if it's an evidence, a query, etc. |
374 | */ |
375 | public Atom toAtom(Atom.AtomType type){ |
376 | Atom a = new Atom(pred, this.toTuple()); |
377 | a.type = type; |
378 | return a; |
379 | } |
380 | |
381 | /** |
382 | * Flip the sense of this literal. |
383 | */ |
384 | public void flipSense(){ |
385 | sense = !sense; |
386 | } |
387 | |
388 | /** |
389 | * Return true if this is a positive literal. Here the positive/negative |
390 | * refers to that in Horn clause. |
391 | */ |
392 | public boolean getSense(){ |
393 | return sense; |
394 | } |
395 | |
396 | /** |
397 | * Set the sense of this literal. |
398 | * |
399 | * @param asense true if this is intended to be a positive literal |
400 | */ |
401 | public void setSense(boolean asense){ |
402 | sense = asense; |
403 | } |
404 | |
405 | /** |
406 | * Set whether we want this literal to cover all materialized tuples |
407 | * regardless of the sense of this literal. |
408 | * @param coversAllMaterializedTuples |
409 | */ |
410 | public void setCoversAllMaterializedTuples(boolean coversAllMaterializedTuples) { |
411 | this.coversAllMaterializedTuples = coversAllMaterializedTuples; |
412 | } |
413 | |
414 | /** |
415 | * Test whether we want this literal to cover all materialized tuples |
416 | * regardless of the sense of this literal. |
417 | */ |
418 | public boolean coversAllMaterializedTuples() { |
419 | return coversAllMaterializedTuples; |
420 | } |
421 | } |