T
TheoryBuilder SeqTheoryBuilder StringTheoryBuilder
THEORY_AXIOMS
PartName
THEORY_PLUGIN
Param
THROTTLED_INF_NUM
InEqConj
TIGHT_FUNCTION_SCOPES
Param
TIMEOUT
Param
TIMEOUT_PER
Param
TPTP
InputFormat
TPTPFormulaPrinter
CertificatePrettyPrinter
TPTPLineariser
parser
TPTPTParser
parser
TRACE_CONSTRAINT_SIMPLIFIER
Param
TRIGGERS_IN_CONJECTURE
Param
TRIGGER_GENERATION
Param
TRIGGER_STRATEGY
Param
TRUE
Goal ArithConj Conjunction LazyConjunction NegatedConjunctions EquationConj NegEquationConj InEqConj PredConj
Tarjan
util
Task
goal
TaskAggregator
goal
TaskApplications
OpCounters
TaskHeap
TaskManager
TaskManager
goal
TaskSummary
CountingTaskAggregator PairCountingTaskAggregator TaskAggregator VectorTaskAggregator
TerFor
terfor
TerForConvenience
terfor
Term
terfor
TermMeasure
ADT
TermOrder
terfor
TermSize
ADT
TestProofTree
tree
Theory
theories
TheoryAxiomInference
certificates
TheoryBuilder
theories
TheoryBuilderException
TheoryBuilder
TheoryCollector
theories
TheoryDecoderData
Theory
TheoryProcedure
theoryPlugins
TheoryRegistry
theories
TheorySort
Theory
Timeout
util
TimeoutCondition
AbstractFileProver
TimeoutCounterModel
Prover
TimeoutException
SimpleAPI
TimeoutModel
Prover
TimeoutProof
Prover
TimeoutResult
Prover
Timer
util
Total
FunctionGCOptions TriggerGenerationOptions
TransducerTransition
StringTheoryBuilder
Transform2NNF
parser
Transform2Prenex
parser
Translation
AbstractFileProver
TranslationException
Parser2InputAbsy
Tree
basetypes
TriggerGenerationOptions
Param
TriggerGenerator
parser
TriggerStrategyOptions
Param
True
BoolADT MultipleValueBool
TryAgain
CollectingVisitor
Type
TPTPTParser
TypeTheory
types
t
ExceptionResult IIntFormula SubstExpression
t1
IPlus
t2
IPlus
tDiv
MulTheory RichMulTerm
tMod
MulTheory RichMulTerm
tail
SymWord
targetLit
ReduceInference ReducePredInference SimpInference
taskAggregator
TaskManager
taskConstants
TaskManager
taskSummary
TaskManager
taskSummaryFor
TaskManager
tasks
Goal
tentativeReduce
ReduceWithConjunction
terfor
ap
term0
LinearCombination1 LinearCombination2
term1
LinearCombination2
term2List
StringTheory
term2RichLC
TerForConvenience
term2RichWord
StringTheory
term2String
FormulaPrinter PrincessFormulaPrinter SMTLIBFormulaPrinter TPTPFormulaPrinter StringTheory
termDepth
ADT
termDepthPreds
ADT
termIterator
ArrayLinearCombination LinearCombination LinearCombination0 LinearCombination1 LinearCombination2
termOrdering
TermOrder MonomialOrdering
termSeq
LinearCombination
termSeq2RichLCSeq
TerForConvenience
termSize
ADT
termSizePreds
ADT
terms
Polynomial
theories
Translation Signature SimpleAPI FunctionPreprocArgs ap TheoryCollector
theory
SMTArray SMTSeq TheoryAxiomInference AddAxiom AxiomSplit CloseByAxiom ADTProxySort AddressSort HeapSort TheorySort TheoryBuilder ArraySort ModSort FractionSort ArraySeqTheoryBuilder AbstractStringSort SeqStringTheoryBuilder UninterpretedSort
theoryAxioms
Certificate Heap
theoryCollector
APIStack
theoryPlugin
APIStack
theoryPlugins
proof
theoryTriggerFunctions
FunctionPreproc
threadNum
ProverArguments
timeout
Configuration ProverArguments
timeoutFromSettings
AbstractFileProver
times
Group Monoid PseudoRing Semigroup SymbolicTimes IdealIntIsIntegral IdealRatIsNumeric Fractions
toArray
Basis Seqs
toBinder
Context
toCoeffWeight
CoeffWeight NonCoeffWeight Weight
toConj
CertCompoundFormula CertEquation CertFormula CertInequality CertNegEquation CertPredLiteral
toConjunction
AndLazyConjunction AtomicLazyConjunction LazyConjunction NegLazyConjunction
toDNF
PresburgerTools
toDouble
IdealIntIsIntegral IdealRatIsNumeric
toEqs
ModelElement
toFloat
IdealIntIsIntegral IdealRatIsNumeric
toFormula
PartialInterpolant CertCompoundFormula CertEquation CertFormula CertInequality CertNegEquation CertPredLiteral AndLazyConjunction AtomicLazyConjunction LazyConjunction NegLazyConjunction
toFunApplier
IExpression
toGoalSettings
Settings
toIndexedSeq
LazyIndexedSeqConcat LazyIndexedSeqSlice
toInputAbsyAndSimplify
SoftwareInterpolationFramework
toInt
IdealIntIsIntegral IdealRatIsNumeric
toInternal
SoftwareInterpolationFramework
toList
Tree Basis
toLong
IdealIntIsIntegral IdealRatIsNumeric
toMap
EquationConj
toNamedParts
SoftwareInterpolationFramework
toNormalBool
SMTParser2InputAbsy
toOptionList
ParallelFileProver
toParserSettings
Settings
toPredApplier
IExpression
toPredConj
ModelElement
toPredicate
IndexedBVOp ShiftFunction MonoSortedIFunction SortedIFunction
toPrenex
PresburgerTools
toPreprocessingSettings
Settings
toQuantifier
ALL Binder EX
toReducerSettings
Settings
toRichTerm
StructuredPrograms
toSMTExpr
SMTLineariser
toSMTLIBString
SMTADT SMTArray SMTBitVec SMTBool SMTChar SMTFF SMTHeap SMTHeapAddress SMTInteger SMTReal SMTRegLan SMTSeq SMTString SMTType SMTUnint
toSeq
Tree
toSet
Tree EquationSet InEqConj Basis
toSetting
ParallelFileProver
toSignature
Environment
toSort
SMTADT SMTArray SMTBitVec SMTBool SMTChar SMTFF SMTHeap SMTHeapAddress SMTInteger SMTReal SMTRegLan SMTSeq SMTString SMTType SMTUnint Type
toState
BlockedTransition TransducerTransition
toStream
Seqs
toString
PseudoRing Semigroup PartialModel IdealInt IdealRat LeftistHeap MultiSet UnionFind PartialInterpolant Assignment Choice Sequence Skip Settings IAtom IBinFormula IBoolLit IConstant IEquation IFormulaITE IFunApp IFunction IIntFormula IIntLit INamedPart INot IPlus ISortedEpsilon ISortedQuantified ISortedVariable ITermITE ITimes ITrigger PartName SMTADT SMTChar SMTHeap SMTHeapAddress SMTRegLan SMTSeq SMTString SMTUnint Rank Type ConstantFreedom AlphaInference AntiSymmetryInference BetaCertificate BranchInferenceCertificate BranchInferenceCollection CertCompoundFormula CertEquation CertInequality CertNegEquation CertPredLiteral CloseCertificate ColumnReduceInference CombineEquationsInference CombineInequalitiesInference CutCertificate ReferenceCertificate DirectStrengthenInference DivRightInference GroundInstInference LoggingBranchInferenceCollector MacroInference OmegaCertificate PartialCertificateInference PredUnifyInference QuantifierInference ReduceInference ReducePredInference ReusedProofMarker SimpInference SplitEqCertificate StrengthenCertificate TheoryAxiomInference BoundStrengthenTask CompoundFormulas FormulaTask Goal LazyMatchTask TaskManager UpdateConstantFreedomTask WrappedFormulaTask EagerPluginTask IntermediatePluginTask PluginSequence PrioritisedPluginTask AndTree QuantifiedTree StrengthenTree WeakenTree ConstantTerm OneTerm TermOrder VariableTerm ArithConj Conjunction IterativeClauseMatcher NegatedConjunctions EquationSet InEqConj LinearCombination Atom PredConj Predicate ComposeSubsts ConstantSubst IdentitySubst PseudoConstantSubst VariableSubst ADT BitShiftMultiplication DivZero FunctionalConsistency Heap PointHandler CombArray ExtArray SetTheory SimpleArray ModuloArithmetic Basis CoeffMonomial Gaussian GrevlexOrdering GroebnerMultiplication Interval IntervalSet IntervalVal ListOrdering Monomial PartitionOrdering Polynomial Fractions Sort TypeTheory UninterpretedSortTheory LRUCache Timer
toTermSeq
IExpression
togglePolarity
Context
totalFunctions
AbstractCompleteFunctionPreproc
totalityAxioms
ADT BitShiftMultiplication DivZero FunctionalConsistency Heap IntValueEnumTheory SaturationProcedure Theory CombArray ExtArray SimpleArray ModuloArithmetic GroebnerMultiplication Fractions ArraySeqTheory SeqStringTheory TypeTheory UninterpretedSortTheory
track
Incompleteness
trackingProgram
NonInterferenceChecker2
transSignature
Translation
transitions
SymTransducer
transitiveDependencies
Theory
translate
FormulaPrinter
translateExtraTheorySort
SMTParser2InputAbsy
translateHeapFun
SMTParser2InputAbsy
translateInterpolantSpecs
ApParser2InputAbsy
translateProblem
ApParser2InputAbsy
translateSMTOperatorAST
SMTParseableTheory
translateSMTSortAST
SMTParseableTheory
translateSort
SMTParser2InputAbsy
translateSpecConstant
SMTParser2InputAbsy
translateTerm
SMTParser2InputAbsy
tree
Proof ProofWithModel proof
trig
IExpression
triggerRelevantFunctions
ADT BitShiftMultiplication DivZero FunctionalConsistency Heap IntValueEnumTheory SaturationProcedure Theory CombArray ExtArray SimpleArray ModuloArithmetic GroebnerMultiplication Fractions ArraySeqTheory SeqStringTheory TypeTheory UninterpretedSortTheory
triggeredAxioms
Heap
tripleIterator
Seqs
trueFun
BoolADT
tryCompare
BindingContext ValueOrdering
tryCompareTo
ConstantFreedom ConstantStatus
typ
Constant Function Predicate Variable
types
ap