EMMA Coverage Report (generated Fri Feb 14 08:28:31 UTC 2014)
[all classes][org.qedeq.kernel.bo.logic.model]

COVERAGE SUMMARY FOR SOURCE FILE [DynamicDirectInterpreter.java]

nameclass, %method, %block, %line, %
DynamicDirectInterpreter.java100% (1/1)79%  (19/24)64%  (1373/2133)77%  (263.9/342)

COVERAGE BREAKDOWN BY CLASS AND METHOD

nameclass, %method, %block, %line, %
     
class DynamicDirectInterpreter100% (1/1)79%  (19/24)64%  (1373/2133)77%  (263.9/342)
calculateTerm (ModuleContext, Element): Entity 0%   (0/1)0%   (0/7)0%   (0/2)
getModel (): DynamicModel 0%   (0/1)0%   (0/3)0%   (0/1)
hasFunctionConstant (ModelFunctionConstant): boolean 0%   (0/1)0%   (0/10)0%   (0/1)
stripReference (String): String 0%   (0/1)0%   (0/20)0%   (0/4)
toString (): String 0%   (0/1)0%   (0/51)0%   (0/6)
handleExistentialQuantifier (ElementList): boolean 100% (1/1)52%  (73/140)73%  (16/22)
calculateTerm (Element): Entity 100% (1/1)52%  (332/635)66%  (65.7/100)
handleUniqueExistentialQuantifier (ElementList): boolean 100% (1/1)54%  (77/142)76%  (19/25)
calculateValue (Element): boolean 100% (1/1)72%  (505/704)84%  (87.7/104)
handleUniversalQuantifier (ElementList): boolean 100% (1/1)82%  (115/140)95%  (21/22)
<static initializer> 100% (1/1)90%  (9/10)90%  (0.9/1)
hasPredicateConstant (ModelPredicateConstant): boolean 100% (1/1)90%  (9/10)90%  (0.9/1)
calculateFunctionValue (FunctionConstant, Entity []): Entity 100% (1/1)93%  (53/57)98%  (10.8/11)
calculatePredicateValue (PredicateConstant, Entity []): boolean 100% (1/1)93%  (53/57)98%  (10.8/11)
DynamicDirectInterpreter (KernelQedeqBo, DynamicModel): void 100% (1/1)100% (17/17)100% (2/2)
DynamicDirectInterpreter (KernelQedeqBo, DynamicModel, SubjectVariableInterpr... 100% (1/1)100% (23/23)100% (8/8)
calculateValue (ModuleContext, Element): boolean 100% (1/1)100% (10/10)100% (2/2)
clearVariables (): void 100% (1/1)100% (10/10)100% (4/4)
getEntities (ElementList): Entity [] 100% (1/1)100% (48/48)100% (7/7)
getLocationWithinModule (): String 100% (1/1)100% (4/4)100% (1/1)
getModuleContext (): ModuleContext 100% (1/1)100% (3/3)100% (1/1)
next (): boolean 100% (1/1)100% (16/16)100% (1/1)
setLocationWithinModule (String): void 100% (1/1)100% (5/5)100% (2/2)
setModuleContext (KernelQedeqBo): void 100% (1/1)100% (11/11)100% (3/3)

1/* This file is part of the project "Hilbert II" - http://www.qedeq.org
2 *
3 * Copyright 2000-2014,  Michael Meyling <mime@qedeq.org>.
4 *
5 * "Hilbert II" is free software; you can redistribute
6 * it and/or modify it under the terms of the GNU General Public
7 * License as published by the Free Software Foundation; either
8 * version 2 of the License, or (at your option) any later version.
9 *
10 * This program is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 */
15 
16package org.qedeq.kernel.bo.logic.model;
17 
18import java.util.ArrayList;
19import java.util.List;
20 
21import org.qedeq.base.trace.Trace;
22import org.qedeq.kernel.bo.logic.common.FunctionConstant;
23import org.qedeq.kernel.bo.logic.common.FunctionKey;
24import org.qedeq.kernel.bo.logic.common.Operators;
25import org.qedeq.kernel.bo.logic.common.PredicateConstant;
26import org.qedeq.kernel.bo.logic.common.PredicateKey;
27import org.qedeq.kernel.bo.logic.common.SubjectVariable;
28import org.qedeq.kernel.bo.module.KernelQedeqBo;
29import org.qedeq.kernel.bo.service.unicode.Latex2UnicodeParser;
30import org.qedeq.kernel.se.base.list.Element;
31import org.qedeq.kernel.se.base.list.ElementList;
32import org.qedeq.kernel.se.common.ModuleContext;
33 
34 
35/**
36 * This class calculates a new truth value for a given formula for a given interpretation.
37 *
38 * @author  Michael Meyling
39 */
40public class DynamicDirectInterpreter {
41 
42    /** This class. */
43    private static final Class CLASS = DynamicDirectInterpreter.class;
44 
45    /** We work with this module. */
46    private KernelQedeqBo qedeq;
47 
48    /** Module context. Here were are currently. */
49    private ModuleContext moduleContext;
50 
51    /** For formatting debug trace output. */
52    private final StringBuffer deepness = new StringBuffer();
53 
54    /** Model contains entities, functions, predicates. */
55    private final DynamicModel model;
56 
57    /** Interpret subject variables. */
58    private final SubjectVariableInterpreter subjectVariableInterpreter;
59 
60    /** Interpret predicate variables. */
61    private final PredicateVariableInterpreter predicateVariableInterpreter;
62 
63    /** Interpret function variables. */
64    private final FunctionVariableInterpreter functionVariableInterpreter;
65 
66   /**
67    * Constructor.
68    *
69    * @param   qedeq       We work with this module.
70    * @param   model       We work with this model.
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     * Constructor.
79     *
80     * @param   qedeq                           We work with this module.
81     * @param   model                           We work with this model.
82     * @param   subjectVariableInterpreter      Subject variable interpreter.
83     * @param   predicateVariableInterpreter    Predicate variable interpreter.
84     * @param   functionVariableInterpreter     Function variable interpreter.
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     * Calculate function value.
99     *
100     * @param   constant            This is the function definition.
101     * @param   entities            Function arguments.
102     * @return  Result of calculation;
103     * @throws  HeuristicException  Calculation of function value failed.
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     * Calculate function value.
126     *
127     * @param   constant        This is the predicate definition.
128     * @param   entities        Function arguments.
129     * @return  Result of calculation;
130     * @throws  HeuristicException  Calculation failed.
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     * Calculate the truth value of a given formula is a tautology. This is done by checking with
153     * a model and certain variable values.
154     *
155     * @param   moduleContext   Where we are within an module.
156     * @param   formula         Formula.
157     * @return  Truth value of formula.
158     * @throws  HeuristicException      We couldn't calculate the value.
159     */
160    public boolean calculateValue(final ModuleContext moduleContext, final Element formula)
161            throws  HeuristicException {
162//        this.startElement = formula;
163        this.moduleContext = new ModuleContext(moduleContext);
164//        this.startContext = new ModuleContext(moduleContext);
165        return calculateValue(formula);
166    }
167 
168    /**
169     * Calculate the truth value of a given formula is a tautology. This is done by checking with
170     * a model and certain variable values.
171     *
172     * @param   formula         Formula.
173     * @return  Truth value of formula.
174     * @throws  HeuristicException      We couldn't calculate the value.
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//                System.out.println(label);
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                    // we must get the second argument of equivalence
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 {  // should be initial predicate, must be in the model
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//            qedeq = qedeqOld;
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     * Handle universal quantifier operator.
328     *
329     * @param   list    Work on this formula.
330     * @return  result  Calculated truth value.
331     * @throws  HeuristicException  Calculation not possible.
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 {  // must be 3
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     * Handle existential quantifier operator.
368     *
369     * @param   list    Work on this formula.
370     * @return  result  Calculated truth value.
371     * @throws  HeuristicException  Calculation not possible.
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 {  // must be 3
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     * Handle unique existential quantifier operator.
408     *
409     * @param   list            Work on this formula.
410     * @return  result          Calculated truth value.
411     * @throws  HeuristicException  Calculation not possible.
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 {  // must be 3
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     * Interpret terms.
452     *
453     * @param   terms           Interpret these terms. The first entry is stripped.
454     * @return  Values.
455     * @throws  HeuristicException evaluation failed.
456     */
457    private Entity[] getEntities(final ElementList terms)
458            throws HeuristicException {
459//        System.out.println(terms);
460        final String context = getLocationWithinModule();
461        final Entity[] result =  new Entity[terms.size() - 1];    // strip first argument
462        for (int i = 0; i < result.length; i++) {
463//            System.out.println(i + " " + terms.getElement(i + 1));
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     * Calculate the term value of a given term. This is done by checking with
473     * a model and certain variable values.
474     *
475     * @param   moduleContext   Where we are within an module.
476     * @param   term            Term.
477     * @return  Entity of model.
478     * @throws  HeuristicException      We couldn't calculate the value.
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     * Interpret term.
488     *
489     * @param   term    Interpret this term.
490     * @return  Value.
491     * @throws  HeuristicException evaluation failed.
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                    // we must get the second argument of equal relation
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//            qedeq = qedeqOld;
620            setModuleContext(qedeqOld);
621            moduleContext = moduleContextOld;
622//            System.out.println("module context old: " + moduleContextOld);
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     * Change to next valuation.
652     *
653     * @return  Is there a next new valuation?
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     * Strips the reference to external modules.
671     *
672     * @param   operator    Might have reference to an external module.
673     * @return  Operator as local reference.
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     * Is the given predicate constant already defined?
686     *
687     * @param   constant    Predicate constant to check for.
688     * @return  Is the given predicate constant already defined?
689     */
690    public boolean hasPredicateConstant(final ModelPredicateConstant constant) {
691        return null != model.getPredicateConstant(constant);
692    }
693 
694    /**
695     * Is the given function constant already defined?
696     *
697     * @param   constant    Function constant to check for.
698     * @return  Is the given function constant already defined?
699     */
700    public boolean hasFunctionConstant(final ModelFunctionConstant constant) {
701        return null != model.getFunctionConstant(constant);
702    }
703 
704    /**
705     * Clear all variable settings.
706     */
707    public void clearVariables() {
708        subjectVariableInterpreter.clear();
709        predicateVariableInterpreter.clear();
710        functionVariableInterpreter.clear();
711    }
712 
713    /**
714     * Get model.
715     *
716     * @return  Model we work with.
717     */
718    public DynamicModel getModel() {
719        return model;
720    }
721 
722 
723}

[all classes][org.qedeq.kernel.bo.logic.model]
EMMA 2.1.5320 (stable) (C) Vladimir Roubtsov