public class JoinProcessor extends Object implements 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 String |
HIDE_RIGHT_TACLET |
private LinkedList<JoinProcessor.Listener> |
listeners |
private static String |
OR_RIGHT_TACLET |
private ProspectivePartner |
partner |
private Proof |
proof |
private Services |
services |
static 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(String[] tacletNames,
Goal goal,
PosInOccurrence pio)
Applies one of the given taclets if this possible otherwise an exception
is thrown.
|
private Term |
buildIfElseTerm() |
private Collection<Term> |
computeCommonFormulas(Semisequent s1,
Semisequent s2,
Term exclude) |
private Collection<Term> |
computeDifference(Semisequent s,
Collection<Term> excludeSet,
Term exclude) |
private Collection<Term> |
createConstrainedTerms(Collection<Term> terms,
Term predicate,
boolean gamma) |
private Term |
createCutFormula() |
private Term |
createDisjunction(Term seed,
Collection<Term> formulas,
boolean needNot) |
private Term |
createPhi() |
private TreeSet<Term> |
createTree() |
private 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 LinkedList<JoinProcessor.Listener> listeners
private static final String HIDE_RIGHT_TACLET
private static final String OR_RIGHT_TACLET
public static final 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(String[] tacletNames, Goal goal, PosInOccurrence pio)
private Term createCutFormula()
private Term buildIfElseTerm()
private Term createPhi()
private Term createDisjunction(Term seed, Collection<Term> formulas, boolean needNot)
private Collection<Term> createConstrainedTerms(Collection<Term> terms, Term predicate, boolean gamma)
private Collection<Term> computeCommonFormulas(Semisequent s1, Semisequent s2, Term exclude)
private Collection<Term> computeDifference(Semisequent s, Collection<Term> excludeSet, Term exclude)
private TreeSet<Term> createTree(Semisequent semisequent, Term exclude)