001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, 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 /**
041 * Constructor.
042 *
043 * @param model Model we work on.
044 */
045 public FunctionVariableInterpreter(final Model model) {
046 this.model = model;
047 functionVariables = new ArrayList();
048 functionVariableCounters = new ArrayList();
049 }
050
051 /**
052 * Get selection for function of model for given function variable.
053 *
054 * @param var Function variable we want an interpretation for.
055 * @return Function selection number of model.
056 */
057 private int getFunctionVariableSelection(final FunctionVariable var) {
058 int selection;
059 if (functionVariables.contains(var)) {
060 final int index = functionVariables.indexOf(var);
061 selection = ((Enumerator) functionVariableCounters.get(index)).getNumber();
062 } else {
063 // System.out.println("added function variable " + var);
064 selection = 0;
065 functionVariables.add(var);
066 functionVariableCounters.add(new Enumerator());
067 }
068 return selection;
069 }
070
071 /**
072 * Get interpretation for function of model for given function variable.
073 *
074 * @param var Function variable we want an interpretation for.
075 * @return Function.
076 */
077 public Function getFunction(final FunctionVariable var) {
078 return model.getFunction(var.getArgumentNumber(),
079 getFunctionVariableSelection(var));
080 }
081
082 /**
083 * Change to next valuation.
084 *
085 * @return Is there a next new valuation?
086 */
087 public boolean next() {
088 boolean next = true;
089 for (int i = functionVariables.size() - 1; i >= -1; i--) {
090 if (i < 0) {
091 next = false;
092 break;
093 }
094 final FunctionVariable var = (FunctionVariable) functionVariables.get(i);
095 final Enumerator number = (Enumerator) functionVariableCounters.get(i);
096 if (number.getNumber() + 1 < model.getFunctionSize(var.getArgumentNumber())) {
097 number.increaseNumber();
098 break;
099 }
100 number.reset();
101 }
102 return next;
103 }
104
105 public String toString() {
106 final StringBuffer buffer = new StringBuffer();
107 buffer.append("function variables {");
108 for (int i = 0; i < functionVariables.size(); i++) {
109 if (i > 0) {
110 buffer.append(", ");
111 }
112 FunctionVariable var = (FunctionVariable) functionVariables.get(i);
113 buffer.append(functionVariables.get(i));
114 buffer.append("=");
115 buffer.append(getFunction(var));
116 }
117 buffer.append("}");
118 return buffer.toString();
119 }
120
121 /**
122 * Clear variable interpretation.
123 */
124 public void clear() {
125 functionVariables.clear();
126 functionVariableCounters.clear();
127 }
128
129 }
|