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
Rationals
rationals
ReducableModelElement
arithconj
ReduceInference
certificates
ReducePredInference
certificates
ReduceWithAC
arithconj
ReduceWithConjunction
conjunctions
ReduceWithEmptyInEqs
inequalities
ReduceWithEqs
equations
ReduceWithInEqs
inequalities
ReduceWithInEqsImpl
inequalities
ReduceWithNegEqs
equations
ReduceWithPredLits
preds
Reducer
ModReducer
ReducerFactory
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
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
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_eps
AbstractStringTheory StringTheory
re_from_str
AbstractStringTheory StringTheory
re_inter
AbstractStringTheory StringTheory
re_loop
AbstractStringTheory StringTheory
re_none
AbstractStringTheory StringTheory
re_opt
AbstractStringTheory StringTheory
re_range
AbstractStringTheory StringTheory
re_union
AbstractStringTheory StringTheory
read
JavaWrapper CRRemover2 SMTCommandTerminator
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
IdentityReducerPlugin ReducerPlugin SeqReducerPlugin 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
reduceWithFacts
Goal
reduceWithLeadingCoeff
LinearCombination
reducerPlugin
Theory ModuloArithmetic GroebnerMultiplication
reducerSettings
Goal AddReducableModelElement ReducableModelElement
reductionPossible
ReduceWithPredLits
regexAsTerm
RegexExtractor
register
TheoryRegistry 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
removeAll
EmptyHeap LeftistHeap Node
removeDuplicates
Seqs
removeFirst
TaskManager
removePartName
IExpression
rename
ConstantSubstVisitor
res
ShortCutResult VisitorRes FilteredSorted
resSort
MonoSortedIFunction
resTerm
VisitorRes
resType
Rank
reset
SimpleAPI Parser2InputAbsy SMTParser2InputAbsy TheoryCollector Timer
resetPredicates
TermOrder
restrict
TermOrder
result
IntelliFileProver ParallelFileProver Prover SMTArray SMTFunctionType AntiSymmetryInference CombineEquationsInference CombineInequalitiesInference DirectStrengthenInference DivRightInference GroundInstInference PredUnifyInference QuantifierInference ReduceInference ReducePredInference SimpInference SubsumptionRemover ColumnSolver LCBlender CtorSignature
resultSort
IndexedBVOp ShiftFunction MonoSortedIFunction SortedIFunction
reverseAtomOrdering
TermOrder
reverseConjOrdering
Conjunction
reverseLCOrdering
TermOrder
reversePredOrdering
TermOrder
reverseTermOrdering
TermOrder
rewrite
Rewriter
rewriteADTFormula
ADT
rewritePredAtom
InterpolationContext
rewritePreds
ReducerPlugin Theory
rewritePredsHelp
Theory
rhs
Assignment
right
Node IFormulaITE IInterpolantSpec ITermITE AndTree AndLazyConjunction
rightActions
SplitDisequality
rightAtom
PredUnifyInference
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 APTestCase
runTest
TestIdealInt TestLeftistHeap TestInputAbsyVisitor TestEquationSystems TestRandomProving TestPropConnectives TestTermOrder TestEquationSet TestInequalities TestLinearCombination TestSubst APTestCase