public class DefaultGoalChooser extends java.lang.Object implements GoalChooser
Modifier and Type | Class and Description |
---|---|
(package private) class |
DefaultGoalChooser.ProofTreeObserver
Important when a proof is pruned
|
Modifier and Type | Field and Description |
---|---|
protected boolean |
allGoalsSatisfiable
true iff all goals have satisfiable constraints
|
protected Node |
currentSubtreeRoot |
protected ImmutableList<Goal> |
goalList
list of goals on which the strategy should be applied
|
protected int |
nextGoalCounter |
protected ImmutableList<Goal> |
nextGoals
part of goalList that should be worked on next
|
protected Proof |
proof
the proof that is worked with
|
private DefaultGoalChooser.ProofTreeObserver |
proofTreeListener |
protected ImmutableList<Goal> |
selectedList
Subset of the goals to which currently taclets are applied.
|
Constructor and Description |
---|
DefaultGoalChooser() |
Modifier and Type | Method and Description |
---|---|
protected void |
findMinimalSubtree(Node p_startNode)
Search for a minimal subtree of the proof tree which is not
closable (constraints of its goals are inconsistent) starting
at p_startNode
PRECONDITION: all goals have satisfiable constraints
|
protected boolean |
findMinimalSubtreeBelow(Node p_startNode)
Search for a minimal subtree of the proof tree which is not
closable (constraints of its goals are inconsistent) below
p_startNode
PRECONDITION: * !
|
Goal |
getNextGoal() |
void |
init(Proof p_proof,
ImmutableList<Goal> p_goals)
Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
|
protected ImmutableList<Goal> |
insertNewGoals(ImmutableList<Goal> newGoals,
ImmutableList<Goal> prevGoalList) |
protected boolean |
isSatisfiableSubtree(Node p_root) |
protected void |
removeClosedGoals() |
void |
removeGoal(Goal p_goal)
Remove p_goal from selectedList (e.g. no taclet can be applied to
p_goal)
|
protected static ImmutableList<Goal> |
rotateList(ImmutableList<Goal> p_list) |
protected void |
setupGoals(ImmutableList<Goal> p_goals) |
void |
updateGoalList(Node node,
ImmutableList<Goal> newGoals)
The given node has become an internal node of the proof tree, and the
children of the node are the given goals
|
protected void |
updateGoalListHelp(Node node,
ImmutableList<Goal> newGoals) |
protected Proof proof
protected ImmutableList<Goal> goalList
protected ImmutableList<Goal> nextGoals
protected boolean allGoalsSatisfiable
protected ImmutableList<Goal> selectedList
protected Node currentSubtreeRoot
private DefaultGoalChooser.ProofTreeObserver proofTreeListener
protected int nextGoalCounter
public void init(Proof p_proof, ImmutableList<Goal> p_goals)
GoalChooser
init
in interface GoalChooser
p_proof
- *param p_goals the initial list of goalsprotected void setupGoals(ImmutableList<Goal> p_goals)
public Goal getNextGoal()
getNextGoal
in interface GoalChooser
public void removeGoal(Goal p_goal)
GoalChooser
removeGoal
in interface GoalChooser
public void updateGoalList(Node node, ImmutableList<Goal> newGoals)
GoalChooser
updateGoalList
in interface GoalChooser
protected void updateGoalListHelp(Node node, ImmutableList<Goal> newGoals)
protected ImmutableList<Goal> insertNewGoals(ImmutableList<Goal> newGoals, ImmutableList<Goal> prevGoalList)
protected static ImmutableList<Goal> rotateList(ImmutableList<Goal> p_list)
protected void removeClosedGoals()
protected boolean findMinimalSubtreeBelow(Node p_startNode)
protected void findMinimalSubtree(Node p_startNode)
protected boolean isSatisfiableSubtree(Node p_root)