RANDOMISE_CASES
GroebnerMultiplication
RANDOMISE_VARIABLE_ORDER
GroebnerMultiplication
RANDOM_DATA_SOURCE
Param
RANDOM_SEED
Param
READ
ConcurrentProgram
READ_REC
ConcurrentProgram
REAL_RAT_SATURATION_ROUNDS
Param
REDUCER_PLUGIN
Param
REDUCER_SETTINGS
Param
REVERSE_FUNCTIONALITY_PROPAGATION
Param
RShiftCastSplitter
bitvectors
RandomDataSource
tree
Range2Interval
IExpression
Rank
TPTPTParser
RatDivZero
Rationals
RatDivZeroTheory
Rationals
Rationals
rationals
RecheckCommand
ProofThreadRunnable
ReducableModelElement
arithconj
ReduceInference
certificates
ReducePredInference
certificates
ReduceWithAC
arithconj
ReduceWithConjunction
conjunctions
ReduceWithEmptyInEqs
inequalities
ReduceWithEqs
equations
ReduceWithInEqs
inequalities
ReduceWithInEqsImpl
inequalities
ReduceWithNegEqs
equations
ReduceWithPredLits
preds
Reducer
ExtArray ModReducer
ReducerFactory
ExtArray ModReducer
ReducerPlugin
conjunctions
ReducerPluginFactory
conjunctions
ReducerSettings
parameters
ReductionMode
ReducerPlugin
ReductionResult
ReducerPlugin
ReferenceCertificate
DagCertificateConverter
RegexExtractor
AbstractStringTheory
RegexSort
SeqStringTheory StringTheory
RegularityBlockedTask
goal
RelDepth
TermMeasure
RemoveFacts
Plugin
Renaming
NonInterferenceChecker2 StructuredPrograms
ReplMap
ProofSimplifier
ResourceFiles
interpolants
Result
Prover
ReturnSatDir
ModelSearchProver
ReusedProofMarker
certificates
Rewriter
parser
RichActionSeq
TheoryProcedure
RichITerm
IExpression
RichITermSeq
IExpression
RichLinearCombination
terfor
RichLinearCombinationSeq
terfor
RichMulTerm
MulTheory
RichPredicate
terfor
RichTerm
StructuredPrograms
RichWord
StringTheory
Ring
algebra
RingWithDivision
algebra
RingWithIntConversions
algebra
RingWithOrder
algebra
Running
ProverStatus
RuntimeStatistics
util
r
AllTests
r_shift_cast
ModuloArithmetic
raise
Timeout
random
Debug
randomAC
TestGenConjunctions
randomConj
TestGenConjunctions
randomEqAC
TestGenConjunctions
randomEqConj
TestGenConjunctions
randomInput
TestGenConjunctions
randomLC
TestGenConjunctions
randoms
Debug
rank
Rank
rationals
theories
rawConstants
AbstractFileProver
rawInputFormula
AbstractFileProver
rawInterpolantSpecs
AbstractFileProver
rawQuantifiers
AbstractFileProver
rawSignature
AbstractFileProver
reDerivativeAxioms
SeqStringTheory
reDerivativeAxioms2
SeqStringTheory
reMatchingAxioms
SeqStringTheory
reMatchingAxioms2
SeqStringTheory
reNullableAxioms
SeqStringTheory
reSimpAxioms
SeqStringTheory
re_*
AbstractStringTheory StringTheory
re_+
AbstractStringTheory StringTheory
re_++
AbstractStringTheory StringTheory
re_all
AbstractStringTheory StringTheory
re_allchar
AbstractStringTheory StringTheory
re_charrange
AbstractStringTheory StringTheory
re_comp
AbstractStringTheory StringTheory
re_derivative_help
SeqStringTheory
re_diff
AbstractStringTheory StringTheory
re_eps
AbstractStringTheory StringTheory
re_from_str
AbstractStringTheory StringTheory
re_inter
AbstractStringTheory StringTheory
re_loop
AbstractStringTheory StringTheory
re_matches_str_help
SeqStringTheory
re_none
AbstractStringTheory StringTheory
re_nullable_help
SeqStringTheory
re_opt
AbstractStringTheory StringTheory
re_range
AbstractStringTheory StringTheory
re_union
AbstractStringTheory StringTheory
read
JavaWrapper CRRemover2 SMTCommandTerminator Heap
read1
NonInterferenceChecker2
read2
NonInterferenceChecker2
readFile
InputDialog
readFromFile
JavaWrapper
readFromReader
JavaWrapper
readFromString
JavaWrapper
readRec
NonInterferenceChecker2
ready
SMTCommandTerminator
realTask
WrappedFormulaTask
recommend
EagerTaskManager
recommendInitialProofRuntime
RuntimeStatistics
recordInitialProofRuntime
RuntimeStatistics
recordProofRuntime
RuntimeStatistics
reduce
SimpleAPI IdentityReducerPlugin ReducerPlugin SeqReducerPlugin Reducer Reducer
reduceAbs
IdealInt
reduceAndAdd
ReduceWithAC
reduceAndCreateGoal
Goal
reduceBy
Basis Polynomial
reduceClauses
IterativeClauseMatcher
reduceInequality
LoggingBranchInferenceCollector ComputationLogger NonLoggingLogger
reduceLeft
Seqs
reduceNegEquation
LoggingBranchInferenceCollector ComputationLogger NonLoggingLogger
reduceNoEqualityInfs
ReduceWithEmptyInEqs ReduceWithInEqs ReduceWithInEqsImpl
reducePolynomial
Basis
reducePredFormula
LoggingBranchInferenceCollector ComputationLogger NonLoggingLogger
reduceSelects
Reducer
reduceStores
Reducer
reduceWithFacts
Goal
reduceWithFormula
SimpleAPI
reduceWithLeadingCoeff
LinearCombination
reducerPlugin
ExtArray Theory ModuloArithmetic GroebnerMultiplication
reducerSettings
Goal AddReducableModelElement ReducableModelElement
reductionPossible
ReduceWithPredLits
regexAsTerm
RegexExtractor
register
TheoryRegistry SeqTheory StringTheory
registerRecFunctions
SMTParser2InputAbsy
rel
IIntFormula
relationString
EquationConj EquationSet NegEquationConj InEqConj
relational
IFunction
relations
FunctionEncoder
releaseFormula
BlockedFormulaTask RegularityBlockedTask
reload
PrincessPanel
rem
IdealIntIsIntegral
remainder
SortedIterator
remove
ArithConj Conjunction IterativeClauseMatcher InEqConj Basis
removeAdd
CountingTaskAggregator PairCountingTaskAggregator TaskAggregator VectorTaskAggregator
removeAll
EmptyHeap LeftistHeap Node
removeCounts
CountingTaskAggregator
removeDuplicates
Seqs
removeFirst
TaskManager
removePartName
IExpression
rename
ConstantSubstVisitor
representatives
UnionFind
res
ShortCutResult VisitorRes FilteredSorted
resSort
MonoSortedIFunction
resTerm
VisitorRes
resType
Rank
reset
SimpleAPI Parser2InputAbsy SMTParser2InputAbsy TheoryCollector Timer
resetAPIConfig
APIStack
resetAPIFormulas
APIStack
resetAPIOptions
APIStack
resetPredicates
TermOrder
resetStopProofTask
ProofThreadRunnable
restrict
TermOrder
result
IntelliFileProver ParallelFileProver Prover SMTArray SMTFunctionType AntiSymmetryInference CombineEquationsInference CombineInequalitiesInference DirectStrengthenInference DivRightInference GroundInstInference PredUnifyInference QuantifierInference ReduceInference ReducePredInference SimpInference SubsumptionRemover ColumnSolver LCBlender CtorSignature CtorSignature
resultSort
IndexedBVOp ShiftFunction MonoSortedIFunction SortedIFunction
reuseLemmaBase
CheckSatCommand
reverseAtomOrdering
TermOrder
reverseConjOrdering
Conjunction
reverseLCOrdering
TermOrder
reversePredOrdering
TermOrder
reverseTermOrdering
TermOrder
rewrite
Rewriter
rewriteADTFormula
ADT
rewritePredAtom
InterpolationContext
rewritePreds
ReducerPlugin Theory
rewritePredsHelp
Theory
rewriter
Heap
rewritings
ArraySimplifier ExtArraySimplifier
rhs
Assignment
richActionSeq
TheoryProcedure
right
Node IEquation IFormulaITE IInterpolantSpec ITermITE AndTree AndLazyConjunction
rightActions
SplitDisequality
rightAtom
PredUnifyInference
rightCase
CutSplit
rightChild
BinaryCertificate
rightCoeff
CombineInequalitiesInference
rightConstants
InterpolationContext
rightFormula
BetaCertificate
rightFormulae
InterpolationContext
rightHeight
EmptyHeap LeftistHeap Node
rightInEq
AntiSymmetryInference CombineInequalitiesInference SplitEqCertificate
rightLocalConstants
InterpolationContext
rightParts
NIInterpolation NIInterpolation
rightPredicates
InterpolationContext
ring2int
RingWithIntConversions ModRing Rationals
risingEdge
Seqs
risingEdgeBwd
Seqs
risingEdgeBwdFull
Seqs
risingEdgeFull
Seqs
risingEdgeFwd
Seqs
risingEdgeFwdFull
Seqs
rows
Gaussian
ruleApplicationYield
ExhaustiveProver
run
AllTests ProofThreadRunnable APTestCase
runTest
TestIdealInt TestLeftistHeap TestInputAbsyVisitor TestEquationSystems TestRandomProving TestPropConnectives TestTermOrder TestEquationSet TestInequalities TestLinearCombination TestSubst APTestCase
runUntilProof
ProverArguments