public class JoinProcessor
extends java.lang.Object
implements java.lang.Runnable
The JoinProcessor is responsible for executing the joining. Let N1 and N2 be the nodes which should be joined and let N be the node where the branches of N1 and N2 join. Further let F be the given decision formula. Then the following steps are applied:
The delayed-cut mechanism prunes the proof at a common predecessor, introduces a cut for a defined decision predicate, and replays the existing proof afterward. Note that by the means of this approach, there are no non-local rule applications in the resulting proof. This avoids certain complications arising from a "defocusing" join rule that establishes a link between a join node and its partner. However, replaying does not work in every case, for instance if a subtree of the common parent introduces new symbols.
DelayedCutProcessor
Modifier and Type | Class and Description |
---|---|
static interface |
JoinProcessor.Listener |
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
HIDE_RIGHT_TACLET |
private java.util.LinkedList<JoinProcessor.Listener> |
listeners |
private static java.lang.String |
OR_RIGHT_TACLET |
private ProspectivePartner |
partner |
private Proof |
proof |
private Services |
services |
static java.lang.String[] |
SIMPLIFY_UPDATE |
private boolean |
used |
Constructor and Description |
---|
JoinProcessor(ProspectivePartner partner,
Proof proof) |
Modifier and Type | Method and Description |
---|---|
void |
addListener(JoinProcessor.Listener listener) |
private ImmutableList<Goal> |
apply(java.lang.String[] tacletNames,
Goal goal,
PosInOccurrence pio)
Applies one of the given taclets if this possible otherwise an exception
is thrown.
|
private Term |
buildIfElseTerm() |
private java.util.Collection<Term> |
computeCommonFormulas(Semisequent s1,
Semisequent s2,
Term exclude) |
private java.util.Collection<Term> |
computeDifference(Semisequent s,
java.util.Collection<Term> excludeSet,
Term exclude) |
private java.util.Collection<Term> |
createConstrainedTerms(java.util.Collection<Term> terms,
Term predicate,
boolean gamma) |
private Term |
createCutFormula() |
private Term |
createDisjunction(Term seed,
java.util.Collection<Term> formulas,
boolean needNot) |
private Term |
createPhi() |
private java.util.TreeSet<Term> |
createTree() |
private java.util.TreeSet<Term> |
createTree(Semisequent semisequent,
Term exclude) |
private SequentFormula |
findFormula(Sequent sequent,
Term content,
boolean antecedent) |
private Goal |
hide(Goal goal) |
void |
join() |
private void |
orRight(Goal goal) |
private void |
processJoin() |
void |
run() |
private Goal |
simplifyUpdate(Goal goal,
DelayedCut cut) |
private boolean used
private final Proof proof
private final Services services
private final ProspectivePartner partner
private final java.util.LinkedList<JoinProcessor.Listener> listeners
private static final java.lang.String HIDE_RIGHT_TACLET
private static final java.lang.String OR_RIGHT_TACLET
public static final java.lang.String[] SIMPLIFY_UPDATE
public JoinProcessor(ProspectivePartner partner, Proof proof)
public void join()
public void addListener(JoinProcessor.Listener listener)
private void processJoin()
private void orRight(Goal goal)
private SequentFormula findFormula(Sequent sequent, Term content, boolean antecedent)
private Goal simplifyUpdate(Goal goal, DelayedCut cut)
private ImmutableList<Goal> apply(java.lang.String[] tacletNames, Goal goal, PosInOccurrence pio)
private Term createCutFormula()
private Term buildIfElseTerm()
private Term createPhi()
private Term createDisjunction(Term seed, java.util.Collection<Term> formulas, boolean needNot)
private java.util.Collection<Term> createConstrainedTerms(java.util.Collection<Term> terms, Term predicate, boolean gamma)
private java.util.Collection<Term> computeCommonFormulas(Semisequent s1, Semisequent s2, Term exclude)
private java.util.Collection<Term> computeDifference(Semisequent s, java.util.Collection<Term> excludeSet, Term exclude)
private java.util.TreeSet<Term> createTree(Semisequent semisequent, Term exclude)
private java.util.TreeSet<Term> createTree()
public void run()
run
in interface java.lang.Runnable