1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16 package org.qedeq.kernel.bo.logic.model;
17
18 import java.util.ArrayList;
19 import java.util.List;
20
21 import org.qedeq.base.trace.Trace;
22 import org.qedeq.kernel.bo.logic.common.FunctionConstant;
23 import org.qedeq.kernel.bo.logic.common.FunctionKey;
24 import org.qedeq.kernel.bo.logic.common.Operators;
25 import org.qedeq.kernel.bo.logic.common.PredicateConstant;
26 import org.qedeq.kernel.bo.logic.common.PredicateKey;
27 import org.qedeq.kernel.bo.logic.common.SubjectVariable;
28 import org.qedeq.kernel.bo.module.KernelQedeqBo;
29 import org.qedeq.kernel.bo.service.unicode.Latex2UnicodeParser;
30 import org.qedeq.kernel.se.base.list.Element;
31 import org.qedeq.kernel.se.base.list.ElementList;
32 import org.qedeq.kernel.se.common.ModuleContext;
33
34
35
36
37
38
39
40 public class DynamicDirectInterpreter {
41
42
43 private static final Class CLASS = DynamicDirectInterpreter.class;
44
45
46 private KernelQedeqBo qedeq;
47
48
49 private ModuleContext moduleContext;
50
51
52 private final StringBuffer deepness = new StringBuffer();
53
54
55 private final DynamicModel model;
56
57
58 private final SubjectVariableInterpreter subjectVariableInterpreter;
59
60
61 private final PredicateVariableInterpreter predicateVariableInterpreter;
62
63
64 private final FunctionVariableInterpreter functionVariableInterpreter;
65
66
67
68
69
70
71
72 public DynamicDirectInterpreter(final KernelQedeqBo qedeq, final DynamicModel model) {
73 this(qedeq, model, new SubjectVariableInterpreter(model), new PredicateVariableInterpreter(
74 model), new FunctionVariableInterpreter(model));
75 }
76
77
78
79
80
81
82
83
84
85
86 public DynamicDirectInterpreter(final KernelQedeqBo qedeq, final DynamicModel model,
87 final SubjectVariableInterpreter subjectVariableInterpreter,
88 final PredicateVariableInterpreter predicateVariableInterpreter,
89 final FunctionVariableInterpreter functionVariableInterpreter) {
90 this.qedeq = qedeq;
91 this.model = model;
92 this.subjectVariableInterpreter = subjectVariableInterpreter;
93 this.predicateVariableInterpreter = predicateVariableInterpreter;
94 this.functionVariableInterpreter = functionVariableInterpreter;
95 }
96
97
98
99
100
101
102
103
104
105 public Entity calculateFunctionValue(final FunctionConstant constant,
106 final Entity[] entities) throws HeuristicException {
107 final List params = constant.getSubjectVariables();
108 for (int i = 0; i < entities.length; i++) {
109 final SubjectVariable var = (SubjectVariable) params.get(i);
110 subjectVariableInterpreter.forceAddSubjectVariable(var, entities[i].getValue());
111 }
112 Entity result;
113 try {
114 result = calculateTerm(constant.getDefiningTerm());
115 } finally {
116 for (int i = entities.length - 1; i >= 0; i--) {
117 final SubjectVariable var = (SubjectVariable) params.get(i);
118 subjectVariableInterpreter.forceRemoveSubjectVariable(var);
119 }
120 }
121 return result;
122 }
123
124
125
126
127
128
129
130
131
132 public boolean calculatePredicateValue(final PredicateConstant constant,
133 final Entity[] entities) throws HeuristicException {
134 final List params = constant.getSubjectVariables();
135 for (int i = 0; i < entities.length; i++) {
136 final SubjectVariable var = (SubjectVariable) params.get(i);
137 subjectVariableInterpreter.forceAddSubjectVariable(var, entities[i].getValue());
138 }
139 boolean result;
140 try {
141 result = calculateValue(constant.getDefiningFormula());
142 } finally {
143 for (int i = entities.length - 1; i >= 0; i--) {
144 final SubjectVariable var = (SubjectVariable) params.get(i);
145 subjectVariableInterpreter.forceRemoveSubjectVariable(var);
146 }
147 }
148 return result;
149 }
150
151
152
153
154
155
156
157
158
159
160 public boolean calculateValue(final ModuleContext moduleContext, final Element formula)
161 throws HeuristicException {
162
163 this.moduleContext = new ModuleContext(moduleContext);
164
165 return calculateValue(formula);
166 }
167
168
169
170
171
172
173
174
175
176 private boolean calculateValue(final Element formula) throws HeuristicException {
177 final String method = "calculateValue(Element)";
178 if (Trace.isDebugEnabled(CLASS)) {
179 Trace.param(CLASS, this, method, deepness.toString() + "formula",
180 Latex2UnicodeParser.transform(null, qedeq.getElement2Latex().getLatex(formula), 0));
181 deepness.append("-");
182 }
183 if (formula.isAtom()) {
184 throw new HeuristicException(HeuristicErrorCodes.WRONG_CALLING_CONVENTION_CODE,
185 HeuristicErrorCodes.WRONG_CALLING_CONVENTION_TEXT, moduleContext);
186 }
187 final KernelQedeqBo qedeqOld = qedeq;
188 final ModuleContext moduleContextOld = new ModuleContext(moduleContext);
189 final String context = getLocationWithinModule();
190 boolean result;
191 try {
192 final ElementList list = formula.getList();
193 setLocationWithinModule(context + ".getList()");
194 final String op = list.getOperator();
195 if (Operators.CONJUNCTION_OPERATOR.equals(op)) {
196 result = true;
197 for (int i = 0; i < list.size() && result; i++) {
198 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
199 result &= calculateValue(list.getElement(i));
200 }
201 } else if (Operators.DISJUNCTION_OPERATOR.equals(op)) {
202 result = false;
203 for (int i = 0; i < list.size() && !result; i++) {
204 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
205 result |= calculateValue(list.getElement(i));
206 }
207 } else if (Operators.EQUIVALENCE_OPERATOR.equals(op)) {
208 result = true;
209 boolean value = false;
210 for (int i = 0; i < list.size() && result; i++) {
211 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
212 if (i > 0) {
213 if (value != calculateValue(list.getElement(i))) {
214 result = false;
215 }
216 } else {
217 value = calculateValue(list.getElement(i));
218 }
219 }
220 } else if (Operators.IMPLICATION_OPERATOR.equals(op)) {
221 result = false;
222 for (int i = 0; i < list.size() && !result; i++) {
223 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
224 if (i < list.size() - 1) {
225 result |= !calculateValue(list.getElement(i));
226 } else {
227 result |= calculateValue(list.getElement(i));
228 }
229 }
230 } else if (Operators.NEGATION_OPERATOR.equals(op)) {
231 result = true;
232 for (int i = 0; i < list.size() && result; i++) {
233 setLocationWithinModule(context + ".getList().getElement(" + i + ")");
234 result &= !calculateValue(list.getElement(i));
235 }
236 } else if (Operators.PREDICATE_VARIABLE.equals(op)) {
237 setLocationWithinModule(context + ".getList()");
238 final Entity[] arguments = getEntities(list);
239 final PredicateVariable var = new PredicateVariable(
240 list.getElement(0).getAtom().getString(), list.size() - 1);
241 result = predicateVariableInterpreter.getPredicate(var)
242 .calculate(arguments);
243 } else if (Operators.UNIVERSAL_QUANTIFIER_OPERATOR.equals(op)) {
244 result = handleUniversalQuantifier(list);
245 } else if (Operators.EXISTENTIAL_QUANTIFIER_OPERATOR.equals(op)) {
246 result = handleExistentialQuantifier(list);
247 } else if (Operators.UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR.equals(op)) {
248 result = handleUniqueExistentialQuantifier(list);
249 } else if (Operators.PREDICATE_CONSTANT.equals(op)) {
250 final String label = list.getElement(0).getAtom().getString();
251 String name = label;
252
253 KernelQedeqBo newProp = qedeq;
254 while (name.indexOf(".") >= 0) {
255 name = name.substring(label.indexOf(".") + 1);
256 final String external = label.substring(0, label.indexOf("."));
257 newProp = null;
258 if (qedeq.getKernelRequiredModules() != null) {
259 newProp = qedeq.getKernelRequiredModules().getKernelQedeqBo(external);
260 }
261 if (newProp == null) {
262 setLocationWithinModule(context + ".getList().getOperator()");
263 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_CODE,
264 HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT + "\"" + external + "\""
265 + HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT_2 + "\"" + external
266 + "." + name + "\"",
267 moduleContext);
268 }
269 }
270 final PredicateKey predicateKey = new PredicateKey(name, "" + (list.size() - 1));
271 final PredicateConstant constant = (newProp.getExistenceChecker() != null
272 ? newProp.getExistenceChecker().get(predicateKey) : null);
273 if (constant != null) {
274 setLocationWithinModule(context + ".getList()");
275 final Entity[] arguments = getEntities(list);
276 setModuleContext(newProp);
277 moduleContext = new ModuleContext(constant.getContext());
278
279 moduleContext.setLocationWithinModule(moduleContext.getLocationWithinModule()
280 + ".getElement(1)");
281 try {
282 result = calculatePredicateValue(constant, arguments);
283 } catch (HeuristicException e) {
284 setModuleContext(qedeqOld);
285 moduleContext = moduleContextOld;
286 setLocationWithinModule(context + ".getList().getElement(1)");
287 throw new HeuristicException(
288 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
289 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + predicateKey,
290 moduleContext, e.getContext());
291 }
292 } else {
293 final ModelPredicateConstant var = new ModelPredicateConstant(name, list.size()
294 - 1);
295 final Predicate predicate = model.getPredicateConstant(var);
296 if (predicate == null) {
297 setLocationWithinModule(context + ".getList().getOperator()");
298 throw new HeuristicException(
299 HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_CODE,
300 HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_TEXT + var,
301 moduleContext);
302 }
303 setLocationWithinModule(context + ".getList()");
304 final Entity[] arguments = getEntities(list);
305 result = predicate.calculate(arguments);
306 }
307 } else {
308 setLocationWithinModule(context + ".getList().getOperator()");
309 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_OPERATOR_CODE,
310 HeuristicErrorCodes.UNKNOWN_OPERATOR_TEXT + op, moduleContext);
311 }
312 } finally {
313
314 setModuleContext(qedeqOld);
315 moduleContext = moduleContextOld;
316 setLocationWithinModule(context);
317 }
318 if (Trace.isDebugEnabled(CLASS)) {
319 deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
320 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(
321 null, qedeq.getElement2Latex().getLatex(formula), 0), result);
322 }
323 return result;
324 }
325
326
327
328
329
330
331
332
333 private boolean handleUniversalQuantifier(final ElementList list)
334 throws HeuristicException {
335 final String method = "handleUniversalQuantifier(ElementList)";
336 final String context = getLocationWithinModule();
337 boolean result = true;
338 final ElementList variable = list.getElement(0).getList();
339 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
340 subjectVariableInterpreter.addSubjectVariable(var);
341 for (int i = 0; i < model.getEntitiesSize(); i++) {
342 if (Trace.isDebugEnabled(CLASS)) {
343 Trace.param(CLASS, this, method, deepness.toString()
344 + Latex2UnicodeParser.transform(null, qedeq.getElement2Latex()
345 .getLatex(variable), 0), model.getEntity(i));
346 }
347 if (list.size() == 2) {
348 setLocationWithinModule(context + ".getElement(1)");
349 result &= calculateValue(list.getElement(1));
350 } else {
351 setLocationWithinModule(context + ".getElement(1)");
352 final boolean result1 = calculateValue(list.getElement(1));
353 setLocationWithinModule(context + ".getElement(2)");
354 final boolean result2 = calculateValue(list.getElement(2));
355 result &= !result1 || result2;
356 }
357 if (!result) {
358 break;
359 }
360 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
361 }
362 subjectVariableInterpreter.removeSubjectVariable(var);
363 return result;
364 }
365
366
367
368
369
370
371
372
373 private boolean handleExistentialQuantifier(final ElementList list)
374 throws HeuristicException {
375 final String method = "handleExistentialQuantifier(ElementList)";
376 final String context = getLocationWithinModule();
377 boolean result = false;
378 final ElementList variable = list.getElement(0).getList();
379 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
380 subjectVariableInterpreter.addSubjectVariable(var);
381 for (int i = 0; i < model.getEntitiesSize(); i++) {
382 if (Trace.isDebugEnabled(CLASS)) {
383 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser
384 .transform(null, qedeq.getElement2Latex().getLatex(variable), 0),
385 model.getEntity(i));
386 }
387 if (list.size() == 2) {
388 setLocationWithinModule(context + ".getElement(1)");
389 result |= calculateValue(list.getElement(1));
390 } else {
391 setLocationWithinModule(context + ".getElement(1)");
392 final boolean result1 = calculateValue(list.getElement(1));
393 setLocationWithinModule(context + ".getElement(2)");
394 final boolean result2 = calculateValue(list.getElement(2));
395 result |= result1 && result2;
396 }
397 if (result) {
398 break;
399 }
400 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
401 }
402 subjectVariableInterpreter.removeSubjectVariable(var);
403 return result;
404 }
405
406
407
408
409
410
411
412
413 private boolean handleUniqueExistentialQuantifier(final ElementList list)
414 throws HeuristicException {
415 final String method = "handleUniqueExistentialQuantifier(ElementList)";
416 final String context = getLocationWithinModule();
417 boolean result = false;
418 final ElementList variable = list.getElement(0).getList();
419 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
420 subjectVariableInterpreter.addSubjectVariable(var);
421 for (int i = 0; i < model.getEntitiesSize(); i++) {
422 if (Trace.isDebugEnabled(CLASS)) {
423 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
424 qedeq.getElement2Latex().getLatex(variable), 0), model.getEntity(i));
425 }
426 boolean val;
427 if (list.size() == 2) {
428 setLocationWithinModule(context + ".getList().getElement(1)");
429 val = calculateValue(list.getElement(1));
430 } else {
431 setLocationWithinModule(context + ".getList().getElement(1)");
432 final boolean result1 = calculateValue(list.getElement(1));
433 setLocationWithinModule(context + ".getList().getElement(2)");
434 final boolean result2 = calculateValue(list.getElement(2));
435 val = result1 && result2;
436 }
437 if (val) {
438 if (result) {
439 result = false;
440 break;
441 }
442 result = true;
443 }
444 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
445 }
446 subjectVariableInterpreter.removeSubjectVariable(var);
447 return result;
448 }
449
450
451
452
453
454
455
456
457 private Entity[] getEntities(final ElementList terms)
458 throws HeuristicException {
459
460 final String context = getLocationWithinModule();
461 final Entity[] result = new Entity[terms.size() - 1];
462 for (int i = 0; i < result.length; i++) {
463
464 setLocationWithinModule(context + ".getElement(" + (i + 1) + ")");
465 result[i] = calculateTerm(terms.getElement(i + 1));
466 }
467 setLocationWithinModule(context);
468 return result;
469 }
470
471
472
473
474
475
476
477
478
479
480 public Entity calculateTerm(final ModuleContext moduleContext, final Element term)
481 throws HeuristicException {
482 this.moduleContext = moduleContext;
483 return calculateTerm(term);
484 }
485
486
487
488
489
490
491
492
493 private Entity calculateTerm(final Element term)
494 throws HeuristicException {
495 final String method = "calculateTerm(Element) ";
496 if (Trace.isDebugEnabled(CLASS)) {
497 Trace.param(CLASS, this, method, deepness.toString() + "term ", Latex2UnicodeParser.transform(null,
498 qedeq.getElement2Latex().getLatex(term), 0));
499 deepness.append("-");
500 }
501 if (!term.isList()) {
502 throw new RuntimeException("a term should be a list: " + term);
503 }
504 final KernelQedeqBo qedeqOld = qedeq;
505 final ModuleContext moduleContextOld = new ModuleContext(moduleContext);
506 final String context = getLocationWithinModule();
507 Entity result = null;
508 try {
509 final ElementList termList = term.getList();
510 final String op = termList.getOperator();
511 if (Operators.SUBJECT_VARIABLE.equals(op)) {
512 final String text = termList.getElement(0).getAtom().getString();
513 final SubjectVariable var = new SubjectVariable(text);
514 result = subjectVariableInterpreter.getEntity(var);
515 } else if (Operators.FUNCTION_VARIABLE.equals(op)) {
516 final FunctionVariable var = new FunctionVariable(termList.getElement(0).getAtom().getString(),
517 termList.size() - 1);
518 Function function = functionVariableInterpreter.getFunction(var);
519 setLocationWithinModule(context + ".getList()");
520 result = function.map(getEntities(termList));
521 } else if (Operators.FUNCTION_CONSTANT.equals(op)) {
522 final String label = termList.getElement(0).getAtom().getString();
523 String name = label;
524 KernelQedeqBo newProp = qedeq;
525 if (label.indexOf(".") >= 0) {
526 name = label.substring(label.indexOf(".") + 1);
527 final String external = label.substring(0, label.indexOf("."));
528 newProp = null;
529 if (qedeq.getKernelRequiredModules() != null) {
530 newProp = qedeq.getKernelRequiredModules().getKernelQedeqBo(external);
531 }
532 if (newProp == null) {
533 setLocationWithinModule(context + ".getList().getOperator()");
534 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_CODE,
535 HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT + "\"" + external + "\""
536 + HeuristicErrorCodes.UNKNOWN_IMPORT_MODULE_TEXT_2 + "\"" + label + "\"",
537 moduleContext);
538 }
539 }
540 final FunctionKey functionKey = new FunctionKey(name, "" + (termList.size() - 1));
541 FunctionConstant constant
542 = newProp.getExistenceChecker().get(functionKey);
543 if (constant != null) {
544 setLocationWithinModule(context + ".getList()");
545 final Entity[] arguments = getEntities(termList);
546 setModuleContext(newProp);
547 moduleContext = new ModuleContext(constant.getContext());
548
549 moduleContext.setLocationWithinModule(moduleContext.getLocationWithinModule() + ".getElement(2)");
550 try {
551 result = calculateFunctionValue(constant, arguments);
552 } catch (HeuristicException e) {
553 setModuleContext(qedeqOld);
554 moduleContext = moduleContextOld;
555 setLocationWithinModule(context + ".getList().getElement(1)");
556 throw new HeuristicException(HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
557 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + functionKey,
558 moduleContext, e.getContext());
559 }
560 } else {
561 final ModelFunctionConstant var = new ModelFunctionConstant(name,
562 termList.size() - 1);
563 Function function = model.getFunctionConstant(var);
564 if (function == null) {
565 setLocationWithinModule(context + ".getList().getOperator()");
566 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE,
567 HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT + var, moduleContext);
568 }
569 setLocationWithinModule(context + ".getList()");
570 final Entity[] arguments = getEntities(termList);
571 result = function.map(arguments);
572 }
573 } else if (Operators.CLASS_OP.equals(op)) {
574 List fullfillers = new ArrayList();
575 ElementList variable = termList.getElement(0).getList();
576 final SubjectVariable var = new SubjectVariable(variable.getElement(0).getAtom().getString());
577 subjectVariableInterpreter.addSubjectVariable(var);
578 KernelQedeqBo newProp = qedeq;
579 if (qedeq.getExistenceChecker() != null) {
580 newProp = qedeq.getExistenceChecker().getClassOperatorModule();
581 }
582 final PredicateConstant isSet = newProp.getExistenceChecker().getPredicate("isSet", 1);
583 if (isSet == null) {
584 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
585 HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + "isSet(*)", moduleContext);
586 }
587 for (int i = 0; i < model.getEntitiesSize(); i++) {
588 setModuleContext(qedeqOld);
589 moduleContext = moduleContextOld;
590 setLocationWithinModule(context + ".getList().getElement(1)");
591 if (calculateValue(termList.getElement(1))) {
592 setModuleContext(newProp);
593 moduleContext = newProp.getLabels().getPredicateContext("isSet", 1);
594 setLocationWithinModule(moduleContext.getLocationWithinModule()
595 + ".getFormula().getElement().getList().getElement(1)");
596 try {
597 if (calculatePredicateValue(isSet, new Entity[] {model.getEntity(i)})) {
598 fullfillers.add(model.getEntity(i));
599 }
600 } catch (HeuristicException e) {
601 setModuleContext(qedeqOld);
602 moduleContext = moduleContextOld;
603 setLocationWithinModule(context + ".getList().getElement(1)");
604 throw new HeuristicException(HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_CODE,
605 HeuristicErrorCodes.PREDICATE_CALCULATION_FAILED_TEXT + isSet,
606 moduleContext, e.getContext());
607 }
608 }
609 subjectVariableInterpreter.increaseSubjectVariableSelection(var);
610 }
611 result = model.comprehension((Entity[]) fullfillers.toArray(new Entity[] {}));
612 subjectVariableInterpreter.removeSubjectVariable(var);
613 } else {
614 setLocationWithinModule(context + ".getList().getOperator()");
615 throw new HeuristicException(HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_CODE,
616 HeuristicErrorCodes.UNKNOWN_TERM_OPERATOR_TEXT + op, moduleContext);
617 }
618 } finally {
619
620 setModuleContext(qedeqOld);
621 moduleContext = moduleContextOld;
622
623 setLocationWithinModule(context);
624 }
625 if (Trace.isDebugEnabled(CLASS)) {
626 deepness.setLength(deepness.length() > 0 ? deepness.length() - 1 : 0);
627 Trace.param(CLASS, this, method, deepness.toString() + Latex2UnicodeParser.transform(null,
628 qedeq.getElement2Latex().getLatex(term), 0), result);
629 }
630 return result;
631 }
632
633 private String getLocationWithinModule() {
634 return moduleContext.getLocationWithinModule();
635 }
636
637 protected ModuleContext getModuleContext() {
638 return moduleContext;
639 }
640
641 protected void setModuleContext(final KernelQedeqBo qedeq) {
642 this.qedeq = qedeq;
643 moduleContext = new ModuleContext(qedeq.getModuleAddress());
644 }
645
646 protected void setLocationWithinModule(final String localContext) {
647 moduleContext.setLocationWithinModule(localContext);
648 }
649
650
651
652
653
654
655 public boolean next() {
656 return subjectVariableInterpreter.next() || predicateVariableInterpreter.next()
657 || functionVariableInterpreter.next();
658 }
659
660 public String toString() {
661 final StringBuffer buffer = new StringBuffer();
662 buffer.append("Current interpretation:\n");
663 buffer.append("\t" + predicateVariableInterpreter + "\n");
664 buffer.append("\t" + subjectVariableInterpreter + "\n");
665 buffer.append("\t" + functionVariableInterpreter);
666 return buffer.toString();
667 }
668
669
670
671
672
673
674
675 public String stripReference(final String operator) {
676 final int index = operator.lastIndexOf(".");
677 if (index >= 0 && index + 1 < operator.length()) {
678 return operator.substring(index + 1);
679 }
680 return operator;
681 }
682
683
684
685
686
687
688
689
690 public boolean hasPredicateConstant(final ModelPredicateConstant constant) {
691 return null != model.getPredicateConstant(constant);
692 }
693
694
695
696
697
698
699
700 public boolean hasFunctionConstant(final ModelFunctionConstant constant) {
701 return null != model.getFunctionConstant(constant);
702 }
703
704
705
706
707 public void clearVariables() {
708 subjectVariableInterpreter.clear();
709 predicateVariableInterpreter.clear();
710 functionVariableInterpreter.clear();
711 }
712
713
714
715
716
717
718 public DynamicModel getModel() {
719 return model;
720 }
721
722
723 }