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
TaskHeap
TaskManager
TaskManager
goal
TaskSummary
CountingTaskAggregator PairCountingTaskAggregator TaskAggregator VectorTaskAggregator
TerFor
terfor
TerForConvenience
terfor
Term
terfor
TermMeasure
ADT
TermOrder
terfor
TermSize
ADT
TestEquationSet
equations
TestEquationSystems
proof
TestException
APTestCase
TestGenConjunctions
terfor
TestIdealInt
basetypes
TestInequalities
inequalities
TestInputAbsyVisitor
parser
TestLeftistHeap
basetypes
TestLinearCombination
linearcombination
TestProofTree
tree
TestPropConnectives
terfor
TestRandomProving
proof
TestResult
APTestCase
TestSubst
substitutions
TestTermOrder
terfor
Theory
theories
TheoryAxiomInference
certificates
TheoryBuilder
theories
TheoryBuilderException
TheoryBuilder
TheoryCollector
theories
TheoryDecoderData
Theory
TheoryProcedure
theoryPlugins
TheoryRegistry
theories
Timeout
util
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
tearDown
APTestCase
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
testArithConj1
TestPropConnectives
testArithConj2
TestPropConnectives
testArithConj3
TestPropConnectives
testConditionalExtension
TestTermOrder
testConj1
TestPropConnectives TestEquationSet TestInequalities
testConj2
TestInequalities
testDepthVisitor
TestInputAbsyVisitor
testDivisibility1
TestEquationSystems
testEqs1
TestEquationSystems
testEqs2
TestEquationSystems
testFlatMap
TestLeftistHeap
testFlatMap2
TestLeftistHeap
testHeapCollector
TestLeftistHeap
testInputAbsy2Internal
TestInputAbsyVisitor
testInsertElements
TestLeftistHeap
testInsertHeap
TestLeftistHeap
testInsertIterator
TestLeftistHeap
testLC1
TestLinearCombination
testLCAddition1
TestLinearCombination
testLCAddition2
TestLinearCombination
testLCAddition3
TestLinearCombination
testLCFlatten
TestLinearCombination
testLargeHeap
TestLeftistHeap
testLinearCombinationComparison
TestTermOrder
testNegConj1
TestEquationSet
testPseudoSubst
TestSubst
testQuantifiedEqs1
TestEquationSystems
testReduceDisj
TestEquationSet
testReduceWithConjunction1
TestPropConnectives
testReduceWithConjunction2
TestPropConnectives
testReduceWithEqs1
TestEquationSet
testReduceWithEqs2
TestEquationSet
testReduceWithEqs3
TestEquationSet
testReduceWithInEqs1
TestInequalities
testReduceWithInEqs2
TestInequalities
testRemoveAll
TestLeftistHeap
testSimpleExtension
TestTermOrder
testSubstVisitor
TestInputAbsyVisitor
tests
AllTests
theories
Translation Signature SimpleAPI FunctionPreprocArgs ap TheoryCollector
theory
SMTArray SMTSeq TheoryAxiomInference AddAxiom AxiomSplit CloseByAxiom ArraySort TheoryBuilder ArraySeqTheoryBuilder SeqStringTheoryBuilder UninterpretedSort
theoryAxioms
Certificate Heap
theoryCollector
APIStack
theoryPlugin
APIStack
theoryPlugins
proof
theoryTriggerFunctions
FunctionPreproc
threadNum
ProverArguments
timeAfter
AllTests
timeBefore
AllTests
timeout
Configuration ProverArguments
times
Group Monoid PseudoRing Semigroup SymbolicTimes IdealIntIsIntegral IdealRatIsNumeric Fractions
to
TestGenConjunctions
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
toOptionList
ParallelFileProver
toParserSettings
Settings
toPredApplier
IExpression
toPredConj
ModelElement
toPredicate
IndexedBVOp ShiftFunction MonoSortedIFunction SortedIFunction
toPrenex
PresburgerTools
toPreprocessingSettings
Settings
toQuantifier
ALL Binder EX
toReducerSettings
Settings
toRev
TestGenConjunctions
toRichTerm
StructuredPrograms
toSMTExpr
SMTLineariser
toSeq
Tree
toSet
Tree EquationSet InEqConj Basis
toSetting
ParallelFileProver
toSignature
Environment
toSort
SMTADT SMTArray SMTBitVec SMTBool SMTChar 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 ExtArray FunctionalConsistency Heap 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 ExtArray FunctionalConsistency Heap IntValueEnumTheory SimpleArray Theory ModuloArithmetic GroebnerMultiplication Fractions ArraySeqTheory SeqStringTheory TypeTheory UninterpretedSortTheory
track
Incompleteness
trackingProgram
NonInterferenceChecker2
transSignature
Translation
transitions
SymTransducer
translate
FormulaPrinter
translateHeapFun
SMTParser2InputAbsy
translateInterpolantSpecs
ApParser2InputAbsy
translateProblem
ApParser2InputAbsy
translateSort
SMTParser2InputAbsy
translateSpecConstant
SMTParser2InputAbsy
translateTerm
SMTParser2InputAbsy
tree
Proof ProofWithModel proof
trig
IExpression
triggerRelevantFunctions
ADT BitShiftMultiplication DivZero ExtArray FunctionalConsistency Heap IntValueEnumTheory SimpleArray Theory 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