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 * This class calculates a new truth value for a given formula for a given interpretation.
026 *
027 * @author Michael Meyling
028 */
029 public final class PredicateVariableInterpreter {
030
031 /** List of predicate variables. */
032 private List predicateVariables;
033
034 /** List of counters for predicate variables. */
035 private List predicateVariableCounters;
036
037 /** Model contains entities. */
038 private Model model;
039
040 /**
041 * Constructor.
042 *
043 * @param model Model we work on.
044 */
045 public PredicateVariableInterpreter(final Model model) {
046 this.model = model;
047 predicateVariables = new ArrayList();
048 predicateVariableCounters = new ArrayList();
049 }
050
051 private int getPredicateVariableSelection(final PredicateVariable var) {
052 int selection;
053 if (predicateVariables.contains(var)) {
054 final int index = predicateVariables.indexOf(var);
055 selection = ((Enumerator) predicateVariableCounters.get(index)).getNumber();
056 } else {
057 // System.out.println("added predicate variable " + var);
058 selection = 0;
059 predicateVariables.add(var);
060 predicateVariableCounters.add(new Enumerator());
061 }
062 return selection;
063 }
064
065 /**
066 * Get model predicate for predicate variable.
067 *
068 * @param var For this predicate variable.
069 * @return Predicate for model.
070 */
071 public Predicate getPredicate(final PredicateVariable var) {
072 return model.getPredicate(var.getArgumentNumber(),
073 getPredicateVariableSelection(var));
074 }
075
076 /**
077 * Change to next valuation.
078 *
079 * @return Is there a next new valuation?
080 */
081 public boolean next() {
082 boolean next = true;
083 for (int i = predicateVariables.size() - 1; i >= -1; i--) {
084 if (i < 0) {
085 next = false;
086 break;
087 }
088 final PredicateVariable var = (PredicateVariable) predicateVariables.get(i);
089 final Enumerator number = (Enumerator) predicateVariableCounters.get(i);
090 if (number.getNumber() + 1 < model.getPredicateSize(var.getArgumentNumber())) {
091 number.increaseNumber();
092 break;
093 }
094 number.reset();
095 }
096 return next;
097 }
098
099 public String toString() {
100 final StringBuffer buffer = new StringBuffer();
101 buffer.append("predicate variables {");
102 for (int i = 0; i < predicateVariables.size(); i++) {
103 if (i > 0) {
104 buffer.append(", ");
105 }
106 PredicateVariable var = (PredicateVariable) predicateVariables.get(i);
107 buffer.append(predicateVariables.get(i));
108 buffer.append("=");
109 buffer.append(getPredicate(var));
110 }
111 buffer.append("}");
112 return buffer.toString();
113 }
114
115 /**
116 * Clear variable interpretation.
117 */
118 public void clear() {
119 predicateVariables.clear();
120 predicateVariableCounters.clear();
121 }
122
123
124 }
|