ABBREV_LABELS
Param
AC
IExpression IVarShift QuantifierCountVisitor ConstraintSimplifier BetaCertificate PartialCertificate BoundStrengthenTask EliminateFactsTask FactsNormalisationTask Plugin VariableTerm ArithConj ModelElement ConjunctEliminator LazyConjunction NegatedConjunctions EquationConj NegEquationConj InEqConj IntervalProp ReduceWithInEqs ExtArray
AC_ADT
Debug
AC_ALGEBRA
Debug
AC_ALIAS_ANALYSER
Debug
AC_ARRAY
Debug
AC_BASE_TYPE
Debug
AC_BLOCKED_FORMULAS_TASK
Debug
AC_CERTIFICATES
Debug
AC_CERTIFICATE_LINEARISER
Debug
AC_CLAUSE_MATCHER
Debug
AC_COMPLEX_FORMULAS_TASK
Debug
AC_COMPUTATION_LOGGER
Debug
AC_CONSTANT_FREEDOM
Debug
AC_CONSTRAINT_SIMPLIFIER
Debug
AC_ELIM_CONJUNCTS
Debug
AC_ELIM_FACTS_TASK
Debug
AC_ENVIRONMENT
Debug
AC_EQUATIONS
Debug
AC_FACTS_TASK
Debug
AC_GOAL
Debug
AC_INEQUALITIES
Debug
AC_INPUT_ABSY
Debug
AC_INTERPOLATION
Debug
AC_INTERPOLATION_IMPLICATION_CHECKS
Debug
AC_LINEAR_COMB
Debug
AC_MAIN
Debug
AC_MAP_UTILS
Debug
AC_MODEL_FINDER
Debug
AC_MODULO_ARITHMETIC
Debug
AC_NIA
Debug
AC_OMEGA
Debug
AC_PARAMETERS
Debug
AC_PARSER
Debug
AC_PLUGIN
Debug
AC_PO_GRAPH
Debug
AC_PREDICATES
Debug
AC_PRESBURGER_TOOLS
Debug
AC_PROOF_TREE
Debug
AC_PROPAGATION
Debug
AC_PROP_CONNECTIVES
Debug
AC_PROVER
Debug
AC_QUEUE_WITH_ITERATORS
Debug
AC_SEQUENCE
Debug
AC_SEQ_UTILS
Debug
AC_SET_UTILS
Debug
AC_SIGNATURE
Debug
AC_SIMPLE_API
Debug
AC_STRING
Debug
AC_SUBSTITUTIONS
Debug
AC_TERM_ORDER
Debug
AC_THEORY
Debug
AC_TYPES
Debug
AC_VALUE_ENUMERATOR
Debug
AC_VARIABLES
Debug
AC_VAR_TYPES
Debug
ADT
theories
ADTException
ADT
ADTProxySort
ADT
ADTSort
ADT Heap
ADT_MEASURE
Param
ALL
Context Quantifier
APIStack
api
APPLY_BLOCKED_TASKS
Param
APTestCase
util
ASSERTIONS
Param
ASSERTION_CATEGORY
Debug
ASSERTION_TYPE
Debug
ASTConnective
Parser2InputAbsy
AT_METHOD_INTERNAL
Debug
AT_METHOD_POST
Debug
AT_METHOD_PRE
Debug
AT_OBJECT_CONSTRUCTION
Debug
Abelian
algebra
AbstractCompleteFunctionPreproc
parser
AbstractFileProver
ap
AbstractStringSort
AbstractStringTheoryWithSort
AbstractStringTheory
strings
AbstractStringTheoryWithSort
strings
AbstractVariableSubstVisitor
parser
AcceptModelDir
ModelSearchProver
Action
Plugin
AddAxiom
Plugin
AddFactsTask
goal
AddFormula
Plugin
AddFormulaCommand
ProofThreadRunnable
AddFormulaDir
ModelSearchProver
AddReducableModelElement
Plugin
AddressCtor
Heap
AddressRangeCtor
Heap
AddressSort
Heap Heap
AliasAnalyser
goal
AliasChecker
terfor
AliasStatus
terfor
All
FunctionGCOptions TriggerGenerationOptions
AllExVisitor
AbstractFileProver
AllMaximal
TriggerStrategyOptions
AllMinimal
TriggerStrategyOptions
AllMinimalAndEmpty
TriggerStrategyOptions
AllModels
Prover
AllQuantifierTask
goal
AllTests
ap
AllUni
TriggerStrategyOptions
AlphaInference
certificates
Always
ProofConstructionOptions
And
IBinJunctor BoolADT
AndLazyConjunction
conjunctions
AndTree
tree
AntiSymmetryInference
certificates
AnyBool
Sort
AnySort
Sort
ApParser2InputAbsy
parser
ArithConj
arithconj
ArrayLinearCombination
linearcombination
ArraySeqTheory
sequences
ArraySeqTheoryBuilder
sequences
ArraySimplifier
interpolants
ArraySort
ExtArray SimpleArray
Assertion
StructuredPrograms
Assignment
StructuredPrograms
Assumption
StructuredPrograms
Atom
preds
AtomicLazyConjunction
conjunctions
Auto
InputFormat NegSolvingOptions
AxiomSplit
Plugin
a
Choice Sequence Context
abbrev
SimpleAPI
abbrevCounter
TaskAggregator
abbrevFunctions
APIStack
abbrevPredicates
APIStack
abbrevSharedExpressions
SimpleAPI
abbrevSharedExpressionsWithMap
SimpleAPI
abbrevWeight
SymbolWeights
abs
IdealInt IdealRat IExpression
ac
InNegEqModelElement
accepting
SymTransducer
add
Basis
addAbbrev
SimpleAPI
addActionListener
DialogUtil
addAndContract
BindingContext
addAssertion
SimpleAPI
addAssumptions
IdentityReducerPlugin ReducerPlugin SeqReducerPlugin Reducer Reducer
addAxiom
Parser2InputAbsy SMTParser2InputAbsy
addBasis
Basis
addBooleanVariable
SimpleAPI
addBooleanVariables
SimpleAPI
addCertificate
LemmaBase
addClauses
IterativeClauseMatcher
addCommon
InterpolationContext
addConclusion
SimpleAPI
addConst
NonInterferenceChecker NonInterferenceChecker2 SigTracker
addConstant
SimpleAPI Environment
addConstantRaw
SimpleAPI
addConstants
SimpleAPI InterpolationContext
addConstantsRaw
SimpleAPI
addCounts
CountingTaskAggregator
addDisjuncts
SubsumptionRemover
addDivisibility
ConjunctEliminator
addDoubleConstant
InterpolationContext
addDoubleConstants
InterpolationContext
addEquations
ReduceWithEqs ReduceWithNegEqs
addExConstraints
TypeTheory
addFunction
SimpleAPI Environment FunctionEncoder
addInEqs
ReduceWithEmptyInEqs ReduceWithInEqs ReduceWithInEqsImpl
addLeft
InterpolationContext
addLits
ReduceWithPredLits
addMod
VisitorArg
addObsoleteConstants
LemmaBase
addOverloadedFunction
Environment
addOverloadedPredicate
Environment
addParameter
InterpolationContext
addPart
PartExtractor
addPartialInterpolant
InterpolationContext
addPortfolio
ParallelFileProver
addPred
SigTracker
addPredicate
Environment
addPredicateTasks
MatchTasks
addRange
SymbolRangeEnvironment
addRelation
SimpleAPI
addRelations
SimpleAPI
addRight
InterpolationContext
addSigned
FrameworkVocabulary
addSort
Environment
addTask
LazyMatchTask IntermediatePluginTask
addTasksFor
Goal
addTest
AllTests
addTheories
Signature SimpleAPI
addTheoriesFor
SimpleAPI
addTheory
SimpleAPI FunctionEncoder Parser2InputAbsy SMTParser2InputAbsy TheoryCollector
addTheoryFront
TheoryCollector
addToQFClauses
BetaFormulaTask
addTopStatus
ConstantFreedom
addTransducer
SeqStringTheoryBuilder StringTheoryBuilder
addUnsigned
FrameworkVocabulary
addWithDefaultInfs
BranchInferenceCollection
additionalConstants
ReferenceCertificate
additiveGroup
PseudoRing
addrRangeSize
Heap
addrRangeStart
Heap
addressRangeCtor
Heap
addressRangeSort
Heap
addressRangeSortId
HeapADTSortId
addressRangeSuffix
Heap
adt
SMTADT
adtTheory
ADTProxySort
after
PartialCertificate PartialCompositionCertificate PartialIdentityCertificate
afterTask
EagerTaskManager
age
FormulaTask Goal
aggregators
VectorTaskAggregator
algebra
ap
all
IExpression Sort
allAxioms
ExtArray ArraySeqTheory SeqStringTheory
allConstants
InterpolationContext
allGVars
NonInterferenceChecker2
allGeqZero
InEqConj
allGeqZeroInfs
InEqConj
allKnown
LemmaBase
allKnownWitness
LemmaBase
allLVars
NonInterferenceChecker2
allNonNegative
Interval
allNonPositive
Interval
allParams
GlobalSettings GoalSettings ParserSettings PreprocessingSettings ReducerSettings Settings
allPredicates
InterpolationContext
allTriggeredFunctions
FunctionPreproc
allVariablesAtLeast
ContainsSymbol
alloc
Heap
allocAddr
Heap
allocHeap
Heap
allocResCtor
Heap
allocResSort
Heap
allocResSortId
HeapADTSortId
alphabetSize
SeqStringTheory StringTheory
and
IExpression ProofTreeFactory SimpleProofTreeFactory
andInOrder
ProofTreeFactory SimpleProofTreeFactory
andSimplify
IFormula
andThen
PartialCertificate
antiSymmetry
LoggingBranchInferenceCollector ComputationLogger NonLoggingLogger
anyDivideAndRemainder
IdealInt
ap
root
api
ap
apply
AllExVisitor ParallelFileProver Signature Evaluator SimpleAPI IdealInt IdealRat Leaf MultiSet UnionFind InterpolationContext Interpolator InterpolatorQE Interval PartialInterpolant PredicateCollector PredicateReplace ProofSimplifier Assignment RichTerm SymbolRangeEnvironment Param Settings AbstractVariableSubstVisitor ApParser2InputAbsy BooleanCompactifier CSIsatLineariser ConstantSubstVisitor ContainsPredicate ContainsSymbol ContainsVariable Context EquivExpander EquivInliner ExMaxiscoper ExpressionReplacingVisitor FunctionCollector FunctionEncoder IAtom IBinFormula IEpsilon IEquation IExpression BooleanFunApplier Conj Disj Divisibility Eq EqLit EqZ FunApplier Geq GeqZ NonDivisibility PredApplier IFormulaITE IFunApp IIntFormula INamedPart INot IPlus IQuantified ISortedEpsilon ISortedQuantified ITermITE ITimes ITrigger IVarShift IVarShiftList IVarShiftMap IVarShiftMapEmptyPrefix IVariable ImplicationCompressor InputAbsy2Internal Internal2InputAbsy IsUniversalFormulaVisitor LineariseVisitor Parser2InputAbsy PartExtractor PartialEvaluator Postprocessing PredPartNameEliminator PredicateSubstVisitor Preprocessing PrettyScalaLineariser PrincessLineariser QuantifierCollectingVisitor QuantifierCountVisitor SMTLineariser SMTParser2InputAbsy SimpleClausifier SimpleMiniscoper Simplifier SimplifyingConstantSubstVisitor SizeVisitor SubExprAbbreviator TPTPLineariser TPTPTParser Transform2NNF Transform2Prenex TriggerGenerator UniformSubstVisitor VariableIndexCollector VariablePermVisitor VariableShiftVisitor VariableSortChecker VariableSortInferenceVisitor ConstraintSimplifier ExhaustiveProver ModelSearchProver QuantifierElimProver SimpleSimplifier Vocabulary AntiSymmetryInference BetaCertificate BinaryCertificate BranchInferenceCollection CertFormula Certificate CertificateOneChild CertificatePrettyPrinter CloseCertificate DagCertificateConverter ReferenceCertificate DotLineariser LoggingBranchInferenceCollector OmegaCertificate PartialCertificate PartialCombCertificate PartialCompositionCertificate PartialFixedCertificate PartialIdentityCertificate PartialInferenceCertificate ReduceInference StrengthenCertificate AddFactsTask AliasAnalyser AllQuantifierTask BetaFormulaTask BlockedFormulaTask BoundStrengthenTask DivisibilityTask EagerMatchTask EliminateFactsTask ExQuantifierTask FactsNormalisationTask Goal LazyMatchTask NegLitClauseTask OmegaTask SymbolWeights Task UpdateConstantFreedomTask UpdateTasksTask WrappedFormulaTask PluginSequence PluginTask AndTree QuantifiedTree StrengthenTree WeakenTree AliasChecker RichPredicate ArithConj InNegEqModelElement ReduceWithAC Conjunction IdentityReducerPluginFactory LazyConjunction NegatedConjunctions Quantifier ReduceWithConjunction ReducerPluginFactory SeqReducerPluginFactory EquationConj EquationSet NegEquationConj ReduceWithEqs ReduceWithNegEqs InEqConj ReduceWithEmptyInEqs ReduceWithInEqs ReduceWithInEqsImpl LinearCombination ScalingIterator Atom PredConj ReduceWithPredLits ComposeSubsts ConstantSubst IdentitySubst PseudoDivSubstitution SimpleSubstitution Substitution VariableShiftSubst VariableSubst ExtArray Lambda ReducerFactory SimpleArray Decoder TheoryBuilder TheoryCollector ModPostprocessor VisitorRes ReducerFactory ModRing SignedBVSort UnsignedBVSort Gaussian IntervalPropagator Fraction ArraySeqTheory SeqTheoryBuilder RegexExtractor WordExtractor SeqStringTheory StringTheoryBuilder IntToTermTranslator MonoSortedIFunction MonoSortedPredicate FastImmutableMap FilterIt IdealRange IntervalIdealRange IntervalPlainRange LRUCache LazyIndexedSeqConcat LazyIndexedSeqSlice PeekIterator PlainRange PredicatedIdealRange PredicatedPlainRange Tarjan UnionMap UnionSet
applyCert
BranchInferenceCollection
applyNoPrettyBitvectors
SMTLineariser
applyToConstant
ConstantSubst PseudoConstantSubst PseudoDivSubstitution SimpleSubstitution VariableShiftSubst VariableSubst
applyToVariable
ConstantSubst PseudoConstantSubst PseudoDivSubstitution SimpleSubstitution VariableShiftSubst VariableSubst
arg
UniSubArgs
argSorts
MonoSortedIFunction MonoSortedPredicate
args
SubArgs IAtom IFunApp
argsTypes
Rank
argumentSorts
BVOrder ShiftPredicate MonoSortedPredicate SortedIFunction SortedPredicate
arguments
SMTArray SMTFunctionType CtorSignature CtorSignature
arithConj
TerForConvenience Conjunction ChangedConjResult
arithConj2Conj
TerForConvenience
arithconj
terfor
arity
IFunction PartialCertificate PartialCombCertificate PartialCompositionCertificate PartialFixedCertificate PartialIdentityCertificate PartialInferenceCertificate Predicate ExtArray ArraySort
arrayAsMap
SimpleAPI
arrayAxioms
Parser2InputAbsy
arrayConstant
ExtArray
arrayCopy
ArraySeqTheory
arrayMaps
DecoderData
arrayTheory
ArraySeqTheory
asConcreteWord
SymWord
asConjunction
SimpleAPI
asFormula
SMTParser2InputAbsy
asIFormula
SimpleAPI
asMap
SimpleArray
asString
DialogUtil PrincessLineariser SMTLineariser SMTParser2InputAbsy SeqStringTheory StringTheory
asStringPartial
SeqStringTheory StringTheory
asTerm
SMTParser2InputAbsy Sort
assert
IncProver
assertCtor
LinearCombination Debug
assertEquals
APTestCase
assertInt
Debug
assertIntFast
Debug
assertNormalisedTree
TestProofTree
assertPost
Debug
assertPostFast
Debug
assertPre
Debug
assertPreFast
Debug
assertTrue
APTestCase Debug
assertion
NICheck NIInterpolation NICheck NIInterpolation
assertionProver
Interpolator
assignReadWriteTrackers
NonInterferenceChecker2
assignStringValues
AbstractStringTheory
assignTrackers
NonInterferenceChecker2
assignedVars
StructuredPrograms
assumeFormula
LemmaBase
assumeFormulas
LemmaBase
assumedFormulas
AlphaInference AntiSymmetryInference BranchInference Certificate ColumnReduceInference CombineEquationsInference CombineInequalitiesInference DirectStrengthenInference DivRightInference GroundInstInference MacroInference PartialCertificateInference PredUnifyInference QuantifierInference ReduceInference ReducePredInference ReusedProofMarker SimpInference TheoryAxiomInference
assumptions
AddAxiom AxiomSplit CloseByAxiom
atFinal
EagerTaskManager
atom
CertPredLiteral
atom2Conj
TerForConvenience
atom2PredConj
TerForConvenience
atomOrdering
TermOrder
augmentModelTermSet
ADTProxySort ArraySort HeapSort FractionSort SeqSort AbstractStringSort ProxySort Sort Integer Interval MultipleValueBool UninterpretedSort
axiom
TheoryAxiomInference AddAxiom
axiom1
ExtArray
axiom2
ExtArray
axiom3
ExtArray
axiom4
ExtArray
axiom5
ExtArray
axiom6
ExtArray
axiom7
ExtArray
axiom8
ExtArray
axiomInferences
PluginTask
axioms
FunctionEncoder ADT BitShiftMultiplication DivZero ExtArray FunctionalConsistency Heap IntValueEnumTheory SimpleArray Theory ModuloArithmetic GroebnerMultiplication Fractions ArraySeqTheory SeqStringTheory TypeTheory UninterpretedSortTheory
axioms1
Heap SeqStringTheory
axioms2
Heap