public class StepSelectorSearch
extends java.lang.Object
Constructor and Description |
---|
StepSelectorSearch(ProofAsstPreferences proofAsstPreferences,
VerifyProofs verifyProofs,
Cnst provableLogicStmtTyp,
java.util.List<Assrt> unifySearchList)
Constructor for StepSelectorSearch
|
Modifier and Type | Method and Description |
---|---|
java.util.List<Assrt> |
getSortedAssrtSearchList() |
StepSelectorResults |
loadStepSelectorResults(DerivationStep derivStep)
Finds the assertions which unify with the given step and loads them into
StepSelectorResults.
|
void |
mergeListOfAssrtAddsSortedBySeq(java.util.List<Theorem> listOfAssrtAddsSortedBySeq) |
public StepSelectorSearch(ProofAsstPreferences proofAsstPreferences, VerifyProofs verifyProofs, Cnst provableLogicStmtTyp, java.util.List<Assrt> unifySearchList)
proofAsstPreferences
- the ProofAsstPreferences objectverifyProofs
- the VerifyProofs objectprovableLogicStmtTyp
- a Provable Logic Stmt Type CodeunifySearchList
- the unification search listpublic void mergeListOfAssrtAddsSortedBySeq(java.util.List<Theorem> listOfAssrtAddsSortedBySeq)
public StepSelectorResults loadStepSelectorResults(DerivationStep derivStep) throws VerifyException
Always returns at least one StepSelectorResult item, "***END***" with Assrt = null (or n items + "***MORE***").
derivStep
- DerivationStep from ProofWorksheetVerifyException
- if not enough allocatable WorkVars.public java.util.List<Assrt> getSortedAssrtSearchList()