001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.proof;
012:
013: import java.util.Iterator;
014: import java.util.Vector;
015:
016: import javax.swing.table.AbstractTableModel;
017:
018: import de.uka.ilkd.key.logic.Constraint;
019: import de.uka.ilkd.key.logic.Term;
020: import de.uka.ilkd.key.proof.incclosure.BranchRestricter;
021: import de.uka.ilkd.key.proof.incclosure.Sink;
022:
023: /** Table model storing a raw constraint as a vector of equalities
024: * (term pairs) */
025:
026: public class ConstraintTableModel extends AbstractTableModel {
027:
028: /** Vector of term pairs representing equalities */
029: protected Vector entries = new Vector();
030:
031: /** This constraint normalized */
032: protected Constraint currentConstraint = Constraint.BOTTOM;
033:
034: public ConstraintTableModel() {
035: }
036:
037: public Constraint getConstraint() {
038: return currentConstraint;
039: }
040:
041: /**
042: * @return true iff p_node should be displayed as a closed
043: * goal/node (i.e. it is really closed or it is part of a subtree
044: * that should be displayed as closed regarding the current user
045: * constraint)
046: */
047: public boolean displayClosed(Node p_node) {
048: if (p_node.isClosed())
049: return true;
050:
051: Sink sink = p_node.getBranchSink();
052: return (sink instanceof BranchRestricter)
053: && getConstraint().isSatisfiable()
054: && (((BranchRestricter) sink).getPathConstraint()
055: .isAsWeakAs(getConstraint()));
056: }
057:
058: /** Methods from AbstractTableModel */
059:
060: public int getRowCount() {
061: return entries.size();
062: }
063:
064: public int getColumnCount() {
065: return 2;
066: }
067:
068: public Object getValueAt(int p_row, int p_column) {
069: if (p_column == 0)
070: return ((PairOfTerm) entries.get(p_row)).left;
071: else
072: return ((PairOfTerm) entries.get(p_row)).right;
073: }
074:
075: public Class getColumnClass(int arg0) {
076: return Term.class;
077: }
078:
079: public String getColumnName(int p_column) {
080: if (p_column == 0)
081: return "Left";
082: else
083: return "Right";
084: }
085:
086: /** Add a new equality to this constraint, consisting of a pair of
087: * terms (not of Sort.FORMULA)
088: * @param p_left left side of the equality
089: * @param p_right right side of the equality
090: */
091: public void addEquality(Term p_left, Term p_right) {
092: addEquality(p_left, p_right, entries.size());
093: }
094:
095: /**
096: * Add a new equality to this constraint, consisting of a pair of
097: * terms (not of Sort.FORMULA). The new pair is inserted at position
098: * <code>p_index</code>
099: * @param p_left left side of the equality
100: * @param p_right right side of the equality
101: * @param p_index row number at which the new pair will turn up
102: * @throws ArrayIndexOutOfBoundsException iff the value of
103: * <code>p_index</code> is invalid, i.e. not within [0..getRowCount()]
104: */
105: public void addEquality(Term p_left, Term p_right, int p_index) {
106: // this throws an exception for invalid <code>p_index</code>
107: entries.add(p_index, new PairOfTerm(p_left, p_right));
108: currentConstraint = currentConstraint.unify(p_left, p_right,
109: null);
110: fireTableRowsInserted(p_index, p_index);
111: fireConstraintChanged(new ConstraintTableEvent(this ));
112: }
113:
114: /**
115: * Delete one equality
116: *
117: * @param p_row
118: * number of the equality, has to be within [0..getRowCount())
119: */
120: public void deleteRow(int p_row) {
121: entries.remove(p_row);
122:
123: currentConstraint = Constraint.BOTTOM;
124: Iterator it = entries.iterator();
125: PairOfTerm p;
126:
127: while (it.hasNext()) {
128: p = (PairOfTerm) it.next();
129: currentConstraint = currentConstraint.unify(p.left,
130: p.right, null);
131: }
132:
133: fireTableRowsDeleted(p_row, p_row);
134: fireConstraintChanged(new ConstraintTableEvent(this ));
135: }
136:
137: /**
138: * Remove the contents of the table, creating the BOTTOM
139: * constraint
140: */
141: public void reset() {
142: entries.clear();
143: currentConstraint = Constraint.BOTTOM;
144: fireTableDataChanged();
145: fireConstraintChanged(new ConstraintTableEvent(this ));
146: }
147:
148: /** handle listeners */
149: public synchronized void addConstraintTableListener(
150: ConstraintTableListener p_l) {
151: listenerList.add(ConstraintTableListener.class, p_l);
152: }
153:
154: public synchronized void removeConstraintTableListener(
155: ConstraintTableListener p_l) {
156: listenerList.remove(ConstraintTableListener.class, p_l);
157: }
158:
159: protected synchronized void fireConstraintChanged(
160: ConstraintTableEvent e) {
161: Object[] listeners = listenerList.getListenerList();
162: for (int i = listeners.length - 2; i >= 0; i -= 2) {
163: if (listeners[i] == ConstraintTableListener.class) {
164: ((ConstraintTableListener) listeners[i + 1])
165: .constraintChanged(e);
166: }
167: }
168: }
169:
170: /** The attribute (vector) "entries" contains objects of this class */
171: private static class PairOfTerm {
172: public PairOfTerm() {
173: }
174:
175: public PairOfTerm(Term p_left, Term p_right) {
176: left = p_left;
177: right = p_right;
178: }
179:
180: public Term left;
181: public Term right;
182: }
183:
184: }
|