001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.logic.model;
017
018 import java.util.ArrayList;
019 import java.util.List;
020
021 import org.qedeq.base.utility.Enumerator;
022
023
024 /**
025 * Interpret function variables.
026 *
027 * @author Michael Meyling
028 */
029 public final class FunctionVariableInterpreter {
030
031 /** Model contains entities, functions, predicates. */
032 private Model model;
033
034 /** List of function variables. */
035 private List functionVariables;
036
037 /** List of counters for function variables. */
038 private List functionVariableCounters;
039
040 /** Counter for next calls for one cycle. */
041 private double counter;
042
043 /**
044 * Constructor.
045 *
046 * @param model Model we work on.
047 */
048 public FunctionVariableInterpreter(final Model model) {
049 this.model = model;
050 functionVariables = new ArrayList();
051 functionVariableCounters = new ArrayList();
052 }
053
054 /**
055 * Get selection for function of model for given function variable.
056 *
057 * @param var Function variable we want an interpretation for.
058 * @return Function selection number of model.
059 */
060 private int getFunctionVariableSelection(final FunctionVariable var) {
061 int selection;
062 if (functionVariables.contains(var)) {
063 final int index = functionVariables.indexOf(var);
064 selection = ((Enumerator) functionVariableCounters.get(index)).getNumber();
065 } else {
066 // System.out.println("added function variable " + var);
067 selection = 0;
068 functionVariables.add(var);
069 functionVariableCounters.add(new Enumerator());
070 }
071 return selection;
072 }
073
074 /**
075 * Get interpretation for function of model for given function variable.
076 *
077 * @param var Function variable we want an interpretation for.
078 * @return Function.
079 */
080 public Function getFunction(final FunctionVariable var) {
081 return model.getFunction(var.getArgumentNumber(),
082 getFunctionVariableSelection(var));
083 }
084
085 /**
086 * Change to next valuation.
087 *
088 * @return Is there a next new valuation?
089 */
090 public boolean next() {
091 counter++;
092 boolean next = true;
093 for (int i = functionVariables.size() - 1; i >= -1; i--) {
094 if (i < 0) {
095 next = false;
096 counter = 0;
097 break;
098 }
099 final FunctionVariable var = (FunctionVariable) functionVariables.get(i);
100 final Enumerator number = (Enumerator) functionVariableCounters.get(i);
101 if (number.getNumber() + 1 < model.getFunctionSize(var.getArgumentNumber())) {
102 number.increaseNumber();
103 break;
104 } else {
105 number.reset();
106 }
107
108 }
109 return next;
110 }
111
112 public String toString() {
113 final StringBuffer buffer = new StringBuffer();
114 buffer.append("function variables {");
115 for (int i = 0; i < functionVariables.size(); i++) {
116 if (i > 0) {
117 buffer.append(", ");
118 }
119 FunctionVariable var = (FunctionVariable) functionVariables.get(i);
120 buffer.append(functionVariables.get(i));
121 buffer.append("=");
122 buffer.append(getFunction(var));
123 }
124 buffer.append("}");
125 return buffer.toString();
126 }
127
128 /**
129 * Clear variable interpretation.
130 */
131 public void clear() {
132 functionVariables.clear();
133 functionVariableCounters.clear();
134 }
135
136 }
|