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.decproc;
012:
013: import java.util.HashSet;
014: import java.util.Iterator;
015: import java.util.Vector;
016:
017: import de.uka.ilkd.key.logic.ConstrainedFormula;
018: import de.uka.ilkd.key.logic.Constraint;
019: import de.uka.ilkd.key.logic.Semisequent;
020: import de.uka.ilkd.key.logic.Sequent;
021: import de.uka.ilkd.key.proof.Goal;
022:
023: /**
024: * A class representing a set of Constraints from which
025: * partial sets can be chosen
026: */
027: public class ConstraintSet {
028: protected Vector constrainedFormulas;
029: protected Constraint userConstraint;
030: protected HashSet usedConstrainedFormulas;
031: protected Constraint chosenConstraint;
032:
033: /**
034: * Creates a new ConstraintSet whith the goal's constraints
035: * @param g The goal the constraints should be taken from
036: * @param userConstraint the Constraint the user entered
037: */
038: public ConstraintSet(Goal g, Constraint userConstraint) {
039: constrainedFormulas = collectConstraints(g);
040: usedConstrainedFormulas = new HashSet();
041: chosenConstraint = Constraint.BOTTOM;
042: this .userConstraint = userConstraint;
043: }
044:
045: public ConstraintSet(Sequent s, Constraint userConstraint) {
046: constrainedFormulas = collectConstraints(s);
047: usedConstrainedFormulas = new HashSet();
048: chosenConstraint = Constraint.BOTTOM;
049: this .userConstraint = userConstraint;
050: }
051:
052: /**
053: * Return a collection of the goal's sequents' Constraints.
054: * @return a collection of the goal's sequents' Constraints
055: * @param g The goal which's sequent's Constraints should
056: * get collected
057: */
058: protected Vector collectConstraints(Goal g) {
059: return collectConstraints(g.sequent());
060: }
061:
062: /**
063: * Return a collection of the Sequents' Constraints.
064: * @return a collection of the Sequents' Constraints
065: * @param s The sequent from which the Constraints should
066: * get collected
067: */
068: protected Vector collectConstraints(Sequent s) {
069: Vector vec = new Vector();
070: vec = collectConstraints(s.antecedent());
071: vec.addAll(collectConstraints(s.succedent()));
072: return vec;
073: }
074:
075: /**
076: * Return a collection of the Semisequents' Constraints.
077: * @return a collection of the Semisequents' Constraints
078: * @param g The SemiSequent from which the Constraints should
079: * get collected
080: */
081: protected Vector collectConstraints(Semisequent g) {
082: Vector vec = new Vector();
083: for (int i = 0; i < g.size(); i++) {
084: vec.add(g.get(i));
085: }
086: return vec;
087: }
088:
089: /**
090: * Returns wether the parameter cf's Constraint was used
091: * to build the Constraint returned with the last call
092: * of chooseConstraint().
093: * @param cf The constrained formula to check.
094: * @returns true if cf was put into the to set, no otherwise.
095: **/
096: public boolean used(ConstrainedFormula cf) {
097: return usedConstrainedFormulas.contains(cf);
098: }
099:
100: /**
101: * Returns the Constraint generated with the last call
102: * of chooseConstraint().
103: * @returns the Constraint generated with the last call
104: * of chooseConstraint().
105: */
106: public Constraint chosenConstraint() {
107: return this .chosenConstraint;
108: }
109:
110: /**
111: * Adds a user Constraint to the current chosenConstraint.
112: * The philosophy behind this approach is that the decision
113: * procedure is always called without the user Constraints
114: * first, and the call is not handled by this class.
115: * If the new generated Constraint is not satisfiable, the
116: * user Constraint is added nevertheless. The caller should
117: * avoid calling the decision procedure afterwards.
118: *
119: * @returns Wether the new Constraint is satisfiable or not
120: * @param p_userConstraint As the name implies, this is the
121: * user Constraint.
122: */
123: public boolean addUserConstraint(Constraint p_userConstraint) {
124: chosenConstraint = chosenConstraint
125: .join(p_userConstraint, null);
126: return chosenConstraint.isSatisfiable();
127: }
128:
129: /**
130: * Chooses a new set of Constraints
131: * This method has (should/will have) a state,
132: * uses the attributes of 'this' to remember its state.
133: * This is not implemented yet. And it is likely that it will
134: * stay this way for a while.
135: * @returns A set of constraints joined to form one.
136: * It tries (using a simple heuristic) to find a maximum consistent
137: * consistent subset of all collected constraints.
138: * It remembers whose ConstrainedFormula's constraints were used.
139: */
140: public Constraint chooseConstraintSet() {
141: Constraint tempConstraint;
142: Constraint usedConstraint = Constraint.BOTTOM;
143: //System.out.println("Amount of Constraints to choose: "+
144: //constraints.size());
145: Iterator i;
146: for (i = constrainedFormulas.iterator(); i.hasNext();) {
147: ConstrainedFormula next = (ConstrainedFormula) i.next();
148: //System.out.println("Next Constrait: " + next.constraint());
149: if (next.constraint().isSatisfiable()) {
150: tempConstraint = usedConstraint.join(next.constraint(),
151: null);
152: //System.out.println("Combined: " + tempConstraint);
153: if (tempConstraint.isSatisfiable()) {
154: usedConstraint = tempConstraint;
155: this.usedConstrainedFormulas.add(next);
156: }
157: }
158: }
159: this.chosenConstraint = usedConstraint;
160: return usedConstraint;
161: }
162:
163: }
|