public class InfFlowProof extends Proof
keyVersionLog, userLog
Constructor and Description |
---|
InfFlowProof(java.lang.String name,
InitConfig initConfig) |
InfFlowProof(java.lang.String name,
Sequent sequent,
java.lang.String header,
TacletIndex rules,
BuiltInRuleIndex builtInRules,
InitConfig initConfig) |
InfFlowProof(java.lang.String name,
Term problem,
java.lang.String header,
InitConfig initConfig) |
Modifier and Type | Method and Description |
---|---|
void |
addGoalTemplates(Taclet t) |
void |
addIFSymbol(java.lang.Object s) |
void |
addLabeledIFSymbol(java.lang.Object s) |
void |
addLabeledTotalTerm(Term p) |
void |
addSideProof(InfFlowProof proof) |
void |
addTotalTerm(Term p) |
InfFlowProofSymbols |
getIFSymbols() |
SideProofStatistics |
getSideProofStatistics()
returns statistics of possible side proofs that contributed to this proof
|
boolean |
hasSideProofs() |
java.lang.String |
printIFSymbols() |
InfFlowProofSymbols |
removeInfFlowProofSymbols() |
void |
unionIFSymbols(InfFlowProofSymbols symbols) |
void |
unionLabeledIFSymbols(InfFlowProofSymbols symbols) |
abbreviations, add, add, addAutoModeTime, addProofDisposedListener, addProofTreeListener, addRuleAppListener, allGoals, breadthFirstSearch, clearAndDetachRuleAppIndexes, closed, closedGoals, closeGoal, containsProofTreeListener, countBranches, countNodes, deregister, dispose, find, findAny, fireNotesChanged, fireProofClosed, fireProofDisposed, fireProofDisposing, fireProofExpanded, fireProofGoalRemoved, fireProofGoalsAdded, fireProofGoalsAdded, fireProofGoalsChanged, fireProofIsBeingPruned, fireProofPruned, fireProofStructureChanged, fireRuleApplied, getActiveStrategy, getActiveStrategyFactory, getAutoModeTime, getClosedGoal, getClosedSubtreeGoals, getEnv, getGoal, getInitConfig, getJavaInfo, getNamespaces, getProofDisposedListeners, getProofFile, getProofIndependentSettings, getServices, getSettings, getStatistics, getSubtreeEnabledGoals, getSubtreeGoals, getUserData, header, isClosedGoal, isDisposed, isGoal, lookup, mgt, name, openEnabledGoals, openGoals, pruneProof, pruneProof, pruneProof, register, removeProofDisposedListener, removeProofTreeListener, removeRuleAppListener, reOpenGoal, replace, root, saveToFile, setActiveStrategy, setEnv, setNamespaces, setProofFile, setRoot, setRuleAppIndexToAutoMode, setRuleAppIndexToInteractiveMode, toString, traverseFromChildToParent
public InfFlowProof(java.lang.String name, Sequent sequent, java.lang.String header, TacletIndex rules, BuiltInRuleIndex builtInRules, InitConfig initConfig)
public InfFlowProof(java.lang.String name, Term problem, java.lang.String header, InitConfig initConfig)
public InfFlowProof(java.lang.String name, InitConfig initConfig)
public InfFlowProofSymbols removeInfFlowProofSymbols()
public InfFlowProofSymbols getIFSymbols()
public void addIFSymbol(java.lang.Object s)
public void addLabeledIFSymbol(java.lang.Object s)
public void addTotalTerm(Term p)
public void addLabeledTotalTerm(Term p)
public void addGoalTemplates(Taclet t)
public void unionIFSymbols(InfFlowProofSymbols symbols)
public void unionLabeledIFSymbols(InfFlowProofSymbols symbols)
public java.lang.String printIFSymbols()
public boolean hasSideProofs()
public void addSideProof(InfFlowProof proof)
public SideProofStatistics getSideProofStatistics()
Copyright © 2003-2019 The KeY-Project.