#
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
focus
hide
ap.terfor.equations
ColumnSolver
EquationConj
EquationSet
NegEquationConj
ReduceWithEqs
ReduceWithNegEqs
TestEquationSet
focus
hide
ap.terfor.inequalities
FMInfsComputer
InEqConj
IntervalProp
ReduceWithEmptyInEqs
ReduceWithInEqs
ReduceWithInEqsImpl
TestInequalities
focus
hide
ap.terfor.linearcombination
ArrayLinearCombination
LCBlender
LinearCombination
LinearCombination0
LinearCombination1
LinearCombination2
ScalingIterator
TestLinearCombination
focus
hide
ap.terfor.preds
Atom
PredConj
Predicate
ReduceWithPredLits
focus
hide
ap.terfor.substitutions
ComposeSubsts
ConstantSubst
IdentitySubst
PseudoConstantSubst
PseudoDivSubstitution
SimpleSubstitution
Substitution
TestSubst
VariableShiftSubst
VariableSubst
focus
hide
ap.theories
ADT
BitShiftMultiplication
DivZero
ExtArray
FunctionalConsistency
Heap
Incompleteness
IntValueEnumTheory
MulTheory
SimpleArray
Theory
TheoryBuilder
TheoryCollector
TheoryRegistry
focus
hide
ap.theories.bitvectors
ExtractArithEncoder
GaloisField
LShiftCastSplitter
ModCastSplitter
ModPlugin
ModPostprocessor
ModPreprocessor
ModReducer
ModRing
ModuloArithmetic
RShiftCastSplitter
SignedBVRing
UnsignedBVRing
focus
hide
ap.theories.nia
Basis
CoeffMonomial
Gaussian
GlexOrdering
GrevlexOrdering
GroebnerMultiplication
InconsistentIntervalsException
Interval
IntervalException
IntervalInt
IntervalNegInf
IntervalPosInf
IntervalPropagator
IntervalSet
IntervalVal
LexOrdering
ListOrdering
Monomial
MonomialOrdering
PartitionOrdering
Polynomial
StringOrdering
focus
hide
ap.theories.rationals
Fractions
Rationals
focus
hide
ap.theories.sequences
ArraySeqTheory
ArraySeqTheoryBuilder
SeqMonoid
SeqTheory
SeqTheoryBuilder
focus
hide
ap.theories.strings
AbstractStringTheory
AbstractStringTheoryWithSort
SeqStringTheory
SeqStringTheoryBuilder
StringMonoid
StringTheory
StringTheoryBuilder
focus
hide
ap.types
IntToTermTranslator
MonoSortedIFunction
MonoSortedPredicate
ProxySort
Sort
SortedConstantTerm
SortedIFunction
SortedPredicate
TypeTheory
UninterpretedSortTheory
focus
hide
ap.util
APTestCase
CmdlParser
Combinatorics
CountIt
Debug
Dijkstra
FastImmutableMap
FilterIt
IdealRange
IntervalIdealRange
IntervalPlainRange
LazyIndexedSeqConcat
LazyIndexedSeqSlice
LazyMappedMap
LazyMappedSet
Logic
LRUCache
PeekIterator
PeekIteratorTrafo
PlainRange
POGraph
PredicatedIdealRange
PredicatedPlainRange
PriorityQueueWithIterators
RuntimeStatistics
Seqs
Tarjan
Timeout
Timer
UnionMap
UnionSet