| java.lang.Object
 de.uka.ilkd.key.proof.decproc.ConstraintSet
| ConstraintSet | | public class ConstraintSet (Code) | | A class representing a set of Constraints from which
partial sets can be chosen
|
| Method Summary | |
| public boolean | addUserConstraint(Constraint p_userConstraint)
Adds a user Constraint to the current chosenConstraint.
The philosophy behind this approach is that the decision
procedure is always called without the user Constraints
first, and the call is not handled by this class.
If the new generated Constraint is not satisfiable, the
user Constraint is added nevertheless. | | public Constraint | chooseConstraintSet()
Chooses a new set of Constraints
This method has (should/will have) a state,
uses the attributes of 'this' to remember its state.
This is not implemented yet. | | public Constraint | chosenConstraint()
Returns the Constraint generated with the last call
of chooseConstraint(). | | protected Vector | collectConstraints(Goal g)
Return a collection of the goal's sequents' Constraints. | | protected Vector | collectConstraints(Sequent s)
Return a collection of the Sequents' Constraints. | | protected Vector | collectConstraints(Semisequent g)
Return a collection of the Semisequents' Constraints. | | public boolean | used(ConstrainedFormula cf)
Returns wether the parameter cf's Constraint was used
to build the Constraint returned with the last call
of chooseConstraint(). |
| constrainedFormulas | | protected Vector constrainedFormulas(Code) | | |
| usedConstrainedFormulas | | protected HashSet usedConstrainedFormulas(Code) | | |
| ConstraintSet | | public ConstraintSet(Goal g, Constraint userConstraint)(Code) | | Creates a new ConstraintSet whith the goal's constraints
Parameters:
g - The goal the constraints should be taken from
Parameters:
userConstraint - the Constraint the user entered |
| addUserConstraint | | public boolean addUserConstraint(Constraint p_userConstraint)(Code) | | Adds a user Constraint to the current chosenConstraint.
The philosophy behind this approach is that the decision
procedure is always called without the user Constraints
first, and the call is not handled by this class.
If the new generated Constraint is not satisfiable, the
user Constraint is added nevertheless. The caller should
avoid calling the decision procedure afterwards.
Parameters:
p_userConstraint - As the name implies, this is the user Constraint. |
| chooseConstraintSet | | public Constraint chooseConstraintSet()(Code) | | Chooses a new set of Constraints
This method has (should/will have) a state,
uses the attributes of 'this' to remember its state.
This is not implemented yet. And it is likely that it will
stay this way for a while.
|
| chosenConstraint | | public Constraint chosenConstraint()(Code) | | Returns the Constraint generated with the last call
of chooseConstraint().
|
| collectConstraints | | protected Vector collectConstraints(Goal g)(Code) | | Return a collection of the goal's sequents' Constraints.
a collection of the goal's sequents' Constraints
Parameters:
g - The goal which's sequent's Constraints should get collected |
| collectConstraints | | protected Vector collectConstraints(Sequent s)(Code) | | Return a collection of the Sequents' Constraints.
a collection of the Sequents' Constraints
Parameters:
s - The sequent from which the Constraints should get collected |
| collectConstraints | | protected Vector collectConstraints(Semisequent g)(Code) | | Return a collection of the Semisequents' Constraints.
a collection of the Semisequents' Constraints
Parameters:
g - The SemiSequent from which the Constraints should get collected |
| used | | public boolean used(ConstrainedFormula cf)(Code) | | Returns wether the parameter cf's Constraint was used
to build the Constraint returned with the last call
of chooseConstraint().
Parameters:
cf - The constrained formula to check. |
|
|