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 * 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 /** 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 PredicateVariableInterpreter(final Model model) {
049 this.model = model;
050 predicateVariables = new ArrayList();
051 predicateVariableCounters = new ArrayList();
052 }
053
054 private int getPredicateVariableSelection(final PredicateVariable var) {
055 int selection;
056 if (predicateVariables.contains(var)) {
057 final int index = predicateVariables.indexOf(var);
058 selection = ((Enumerator) predicateVariableCounters.get(index)).getNumber();
059 } else {
060 // System.out.println("added predicate variable " + var);
061 selection = 0;
062 predicateVariables.add(var);
063 predicateVariableCounters.add(new Enumerator());
064 }
065 return selection;
066 }
067
068 /**
069 * Get model predicate for predicate variable.
070 *
071 * @param var For this predicate variable.
072 * @return Predicate for model.
073 */
074 public Predicate getPredicate(final PredicateVariable var) {
075 return model.getPredicate(var.getArgumentNumber(),
076 getPredicateVariableSelection(var));
077 }
078
079 /**
080 * Change to next valuation.
081 *
082 * @return Is there a next new valuation?
083 */
084 public boolean next() {
085 counter++;
086 boolean next = true;
087 for (int i = predicateVariables.size() - 1; i >= -1; i--) {
088 if (i < 0) {
089 next = false;
090 counter = 0;
091 break;
092 }
093 final PredicateVariable var = (PredicateVariable) predicateVariables.get(i);
094 final Enumerator number = (Enumerator) predicateVariableCounters.get(i);
095 if (number.getNumber() + 1 < model.getPredicateSize(var.getArgumentNumber())) {
096 number.increaseNumber();
097 break;
098 } else {
099 number.reset();
100 }
101
102 }
103 return next;
104 }
105
106 public String toString() {
107 final StringBuffer buffer = new StringBuffer();
108 buffer.append("predicate variables {");
109 for (int i = 0; i < predicateVariables.size(); i++) {
110 if (i > 0) {
111 buffer.append(", ");
112 }
113 PredicateVariable var = (PredicateVariable) predicateVariables.get(i);
114 buffer.append(predicateVariables.get(i));
115 buffer.append("=");
116 buffer.append(getPredicate(var));
117 }
118 buffer.append("}");
119 return buffer.toString();
120 }
121
122 /**
123 * Clear variable interpretation.
124 */
125 public void clear() {
126 predicateVariables.clear();
127 predicateVariableCounters.clear();
128 }
129
130
131 }
|