public abstract class AbstractSideProofRule extends java.lang.Object implements BuiltInRule
BuiltInRule
which
computes something in a side proof.Constructor and Description |
---|
AbstractSideProofRule() |
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
computeResultsAndConditions(Services services,
Goal goal,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Function newPredicate)
Starts the side proof and extracts the result
Term and conditions. |
protected Function |
createResultConstant(Services services,
Sort sort)
Creates a constant which is used in the original
Proof to
store the computed result in form of QueryResult = ... |
protected Function |
createResultFunction(Services services,
Sort sort)
Creates the result
Function used in a predicate to compute the result in the side proof. |
boolean |
isApplicableOnSubTerms() |
protected static SequentFormula |
replace(PosInOccurrence pio,
Term newTerm,
Services services)
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
createApp, isApplicable
apply, displayName, name
protected Function createResultFunction(Services services, Sort sort)
Function
used in a predicate to compute the result in the side proof.protected java.util.List<Triple<Term,java.util.Set<Term>,Node>> computeResultsAndConditions(Services services, Goal goal, ProofEnvironment sideProofEnvironment, Sequent sequentToProve, Function newPredicate) throws ProofInputException
Starts the side proof and extracts the result Term
and conditions.
New used names are automatically added to the Namespace
of the Services
.
services
- The Services
to use.goal
- The Goal
on which this BuiltInRule
should be applied on.sideProofEnvironment
- The given ProofEnvironment
of the side proof.sequentToProve
- The Sequent
to prove in a side proof.newPredicate
- The Function
which is used to compute the result.Term
and the conditions.ProofInputException
- Occurred Exception.protected static SequentFormula replace(PosInOccurrence pio, Term newTerm, Services services)
pio
- The PosInOccurrence
which defines the Term
to replace.newTerm
- The new Term
.SequentFormula
in which the Term
is replaced.public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule