#
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
–
deprecated
display packages only
focused on
focus
hide
ap
AbstractFileProver
AllTests
CmdlMain
DialogMain
DialogUtil
InputDialog
IntelliFileProver
JavaWrapper
ParallelFileProver
PresburgerTools
PrincessPanel
Prover
ServerMain
Signature
focus
hide
ap.algebra
Abelian
CommutativePseudoRing
CommutativeRing
EuclidianRing
Field
Group
IntegerRing
Monoid
OrderedRing
PseudoRing
Ring
RingWithDivision
RingWithIntConversions
RingWithOrder
Semigroup
SymbolicTimes
focus
hide
ap.api
APIStack
Evaluator
PartialModel
ProofThreadRunnable
SimpleAPI
focus
hide
ap.basetypes
EmptyHeap
HeapCollector
IdealInt
IdealRat
Leaf
LeftistHeap
MultiSet
Node
SortedIterator
TestIdealInt
TestLeftistHeap
Tree
UnionFind
UnsortedIterator
focus
hide
ap.interpolants
ArraySimplifier
BitvectorSimplifier
ConcurrentProgram
ExtArraySimplifier
FrameworkVocabulary
InterpolantSimplifier
InterpolationContext
Interpolator
InterpolatorQE
Interval
NonInterferenceChecker
NonInterferenceChecker2
PartialInterpolant
PredicateCollector
PredicateReplace
ProofSimplifier
ResourceFiles
SigTracker
SoftwareInterpolationFramework
StructuredPrograms
SymbolRangeEnvironment
WolverineInterfaceMain
WolverineInterpolantLineariser
focus
hide
ap.parameters
GlobalSettings
GoalSettings
Param
ParserSettings
PreprocessingSettings
ReducerSettings
Settings
focus
hide
ap.parser
AbstractCompleteFunctionPreproc
AbstractVariableSubstVisitor
ApParser2InputAbsy
BooleanCompactifier
CollectingVisitor
CompleteFrugalFunctionPreproc
CompleteFunctionPreproc
ConstantSubstVisitor
ContainsPredicate
ContainsSymbol
ContainsVariable
Context
ContextAwareVisitor
CSIsatLineariser
DNFConverter
Environment
EquivExpander
EquivInliner
ExMaxiscoper
ExpressionReplacingVisitor
FunctionCollector
FunctionEncoder
FunctionPreproc
IAtom
IBinFormula
IBinJunctor
IBoolLit
IConstant
IEpsilon
IEquation
IExpression
IFormula
IFormulaITE
IFunApp
IFunction
IInterpolantSpec
IIntFormula
IIntLit
IIntRelation
ImplicationCompressor
INamedPart
INot
InputAbsy2Internal
Internal2InputAbsy
IPlus
IQuantified
ISortedEpsilon
ISortedQuantified
ISortedVariable
IsUniversalFormulaVisitor
ITerm
ITermITE
ITimes
ITrigger
IVariable
IVariableBinder
IVarShift
IVarShiftList
IVarShiftMap
IVarShiftMapEmptyPrefix
KBO
LineariseVisitor
Parser2InputAbsy
PartExtractor
PartialEvaluator
PartName
PartNameEliminator
Postprocessing
PredicateSubstVisitor
PredPartNameEliminator
Preprocessing
PrettyScalaLineariser
PrincessLineariser
QuantifierCollectingVisitor
QuantifierCountVisitor
Rewriter
SelectiveQuantifierCountVisitor
SimpleClausifier
SimpleMiniscoper
Simplifier
SimplifyingConstantSubstVisitor
SimplifyingVariableSubstVisitor
SizeVisitor
SMTLineariser
SMTParser2InputAbsy
StdFunctionPreproc
SubExprAbbreviator
SymbolCollector
TestInputAbsyVisitor
TPTPLineariser
TPTPTParser
Transform2NNF
Transform2Prenex
TriggerGenerator
UniformSubstVisitor
VariableIndexCollector
VariablePermVisitor
VariableShiftVisitor
VariableSortChecker
VariableSortInferenceVisitor
VariableSubstVisitor
focus
hide
ap.proof
BindingContext
ConstantFreedom
ConstraintSimplifier
ExhaustiveProver
ModelSearchProver
QuantifierElimProver
SimpleSimplifier
TestEquationSystems
TestRandomProving
Vocabulary
focus
hide
ap.proof.certificates
AlphaInference
AntiSymmetryInference
BetaCertificate
BetaCertificateHelper
BinaryCertificate
BranchInference
BranchInferenceCertificate
BranchInferenceCollection
BranchInferenceCollector
CertArithLiteral
CertCompoundFormula
CertEquation
CertFormula
Certificate
CertificateOneChild
CertificatePrettyPrinter
CertInequality
CertNegEquation
CertPredLiteral
CloseCertificate
ColumnReduceInference
CombineEquationsInference
CombineInequalitiesInference
CutCertificate
DagCertificateConverter
DirectStrengthenInference
DivRightInference
DotLineariser
GroundInstInference
LemmaBase
LoggingBranchInferenceCollector
MacroInference
NonLoggingBranchInferenceCollector
OmegaCertificate
PartialCertificate
PartialCertificateInference
PartialCombCertificate
PartialCompositionCertificate
PartialFixedCertificate
PartialIdentityCertificate
PartialInferenceCertificate
PredUnifyInference
QuantifierInference
ReduceInference
ReducePredInference
ReusedProofMarker
SimpInference
SplitEqCertificate
StrengthenCertificate
StrengthenCertificateHelper
TheoryAxiomInference
focus
hide
ap.proof.goal
AddFactsTask
AliasAnalyser
AllQuantifierTask
BetaFormulaTask
BlockedFormulaTask
BoundStrengthenTask
CompoundFormulas
CountingTaskAggregator
DivisibilityTask
EagerMatchTask
EagerTask
EagerTaskAutomaton
EagerTaskManager
EliminateFactsTask
ExQuantifierTask
FactsNormalisationTask
FormulaTask
Goal
LazyMatchTask
MatchTasks
NegLitClauseTask
OmegaTask
PairCountingTaskAggregator
PrioritisedTask
QuantifierTask
RegularityBlockedTask
SymbolWeights
Task
TaskAggregator
TaskManager
UpdateConstantFreedomTask
UpdateTasksTask
VectorTaskAggregator
WrappedFormulaTask
focus
hide
ap.proof.theoryPlugins
EagerPluginTask
IntermediatePluginTask
Plugin
PluginSequence
PluginTask
PrioritisedPluginTask
TheoryProcedure
focus
hide
ap.proof.tree
AndTree
IteratingProofTreeFactory
NonRandomDataSource
ProofTree
ProofTreeFactory
ProofTreeOneChild
QuantifiedTree
RandomDataSource
SeededRandomDataSource
SimpleProofTreeFactory
StrengthenTree
TestProofTree
WeakenTree
focus
hide
ap.terfor
AliasChecker
AliasStatus
ComputationLogger
ConstantTerm
Formula
OneTerm
RichLinearCombination
RichLinearCombinationSeq
RichPredicate
Sorted
SortedWithOrder
TerFor
TerForConvenience
Term
TermOrder
TestGenConjunctions
TestPropConnectives
TestTermOrder
VariableTerm
focus
hide
ap.terfor.arithconj
ArithConj
ElimPredModelElement
EqModelElement
EquivModelElement
InNegEqModelElement
ModelElement
ReducableModelElement
ReduceWithAC
focus
hide
ap.terfor.conjunctions
AndLazyConjunction
AtomicLazyConjunction
ConjunctEliminator
Conjunction
IdentityReducerPlugin
IdentityReducerPluginFactory
IterativeClauseMatcher
LazyConjunction
NegatedConjunctions
NegLazyConjunction
Quantifier
ReducerPlugin
ReducerPluginFactory
ReduceWithConjunction
SeqReducerPlugin
SeqReducerPluginFactory
SubsumptionRemover