POGraph
util
POLY_PREFIX
SMTADT
PORTFOLIO
Param
PORTFOLIO_THREAD_NUM
Param
POS_UNIT_RESOLUTION
Param
PREDICATE_MATCH_CONFIG
Param
PRINT_CERTIFICATE
Param
PRINT_DOT_CERTIFICATE_FILE
Param
PRINT_SMT_FILE
Param
PRINT_TPTP_FILE
Param
PRINT_TREE
Param
PROOF_CONSTRUCTION
Param
PROOF_CONSTRUCTION_GLOBAL
Param
PROOF_SIMPLIFICATION
Param
PairCountingTaskAggregator
goal
PairList
Monomial
ParallelFileProver
ap
Param
parameters
ParseException
Parser2InputAbsy
Parser2InputAbsy
parser
ParserSettings
parameters
PartExtractor
parser
PartName
parser
PartNameEliminator
parser
PartialCertificate
certificates
PartialCertificateInference
certificates
PartialCombCertificate
certificates
PartialCompositionCertificate
certificates
PartialEvaluator
parser
PartialFixedCertificate
certificates
PartialIdentityCertificate
certificates
PartialInferenceCertificate
certificates
PartialInterpolant
interpolants
PartialModel
api
PartitionOrdering
nia
PeekIterator
util
PeekIteratorTrafo
util
PlainIdentifier
SMTParser2InputAbsy
PlainRange
util
PlainSymbol
SMTParser2InputAbsy
Plugin
theoryPlugins
PluginSequence
theoryPlugins
PluginTask
theoryPlugins
Polynomial
nia
Positive
PredicateMatchStatus NegSolvingOptions
Postprocessing
parser
PreVisitResult
CollectingVisitor
PredApplier
IExpression
PredConj
preds
PredPartNameEliminator
parser
PredUnifyInference
certificates
Predicate
Environment IExpression preds
PredicateCollector
interpolants
PredicateMatchConfig
Signature
PredicateMatchStatus
Signature
PredicateReplace
interpolants
PredicateSubstVisitor
parser
PredicatedIdealRange
util
PredicatedPlainRange
util
Preproc
ModPreprocessor
Preprocessing
parser
PreprocessingException
Preprocessing
PreprocessingSettings
parameters
PresburgerTools
ap
PrettyScalaLineariser
parser
Princess
InputFormat
PrincessFormulaPrinter
CertificatePrettyPrinter
PrincessLineariser
parser
PrincessPanel
ap
PrioritisedPluginTask
theoryPlugins
PrioritisedTask
goal
PriorityQueueWithIterators
util
ProducesLits
Matchable
Proof
Prover
ProofConstructionOptions
Param
ProofResult
Prover
ProofSimplifier
interpolants
ProofThreadRunnable
api
ProofTree
tree
ProofTreeFactory
tree
ProofTreeOneChild
tree
ProofWithModel
Prover
Prover
ap
ProverArguments
ParallelFileProver
ProverCommand
ProofThreadRunnable
ProverResult
ProofThreadRunnable
ProverStatus
SimpleAPI
ProxySort
types
PseudoConstantSubst
substitutions
PseudoDivSubstitution
substitutions
PseudoRing
algebra
p
GaloisField
pCert
PartialCertificateInference
pair
FrameworkVocabulary
pairIterator
ArrayLinearCombination LinearCombination LinearCombination0
pairSeq
ArrayLinearCombination LinearCombination LinearCombination0 LinearCombination1 LinearCombination2
pairSort
ArraySeqTheory
pairTheory
ArraySeqTheory
pairs
Monomial
paramMap
Settings
parameters
InterpolationContext ap
parikhSizeConstraints
ADT
parseAndSimplify
SoftwareInterpolationFramework
parseExpression
ApParser2InputAbsy SMTParser2InputAbsy
parseIgnoreCommand
SMTParser2InputAbsy
parseParameter
TheoryBuilder
parseParameters
TheoryBuilder
parseProblem
SoftwareInterpolationFramework
parser
ap
partName2String
FormulaPrinter PrincessFormulaPrinter SMTLIBFormulaPrinter TPTPFormulaPrinter
partial
IFunction
partialCertificate
AndTree
partialInterpolants
InterpolationContext
partialMinBy
Seqs
partialModel
SimpleAPI
partialModelAsFormula
SimpleAPI
partition
PredConj
passQuantifiers
ReduceWithAC IdentityReducerPlugin ReduceWithConjunction ReducerPlugin SeqReducerPlugin ReduceWithEqs ReduceWithNegEqs ReduceWithEmptyInEqs ReduceWithInEqs ReduceWithInEqsImpl ReduceWithPredLits ComposeSubsts ConstantSubst IdentitySubst PseudoConstantSubst Substitution VariableShiftSubst VariableSubst Reducer Reducer
path1
NIInterpolation NIInterpolation
path2
NIInterpolation NIInterpolation
patternType
ConstantWeight NonCoeffWeight OneWeight VariableWeight
patterns
ITrigger
peekNext
LCBlender PeekIterator PeekIteratorTrafo PriorityQueueWithIterators
pick
RandomDataSource
plainReduce
ReduceWithAC
plugin
PluginTask ADT BitShiftMultiplication DivZero ExtArray FunctionalConsistency Heap IntValueEnumTheory SimpleArray Theory ModuloArithmetic GroebnerMultiplication Fractions ArraySeqTheory SeqStringTheory TypeTheory UninterpretedSortTheory
plugins
PluginSequence SeqReducerPluginFactory
plus
IntegerRing PseudoRing IdealIntIsIntegral IdealRatIsNumeric ModRing Fractions
polarity
Context
polyIterator
Basis
polyMap
Basis
polyQueue
Basis
pop
SimpleAPI SymbolRangeEnvironment IVarShift IVarShiftList IVarShiftMap IVarShiftMapEmptyPrefix SMTParser2InputAbsy LemmaBase
popAPIFrame
APIStack
popState
Parser2InputAbsy
popVar
Environment
posTranslation
AbstractFileProver
positiveEqs
ArithConj
positiveLits
PredConj
positiveLitsAsSet
PredConj
positiveLitsWithPred
PredConj
postSimplifiers
ExtArray Heap SimpleArray Theory
postVisit
AllExVisitor BitvectorSimplifier SelectStoreCollector PredicateCollector PredicateReplace WolverineInterpolantLineariser CollectingVisitor ConstantSubstVisitor ContainsSymbol EquivExpander ExpressionReplacingVisitor FunctionCollector IsUniversalFormulaVisitor PartExtractor PartialEvaluator PredPartNameEliminator PredicateSubstVisitor QuantifierCollectingVisitor QuantifierCountVisitor SelectiveQuantifierCountVisitor SimplifyingConstantSubstVisitor SimplifyingVariableSubstVisitor SymbolCollector DepthCountingVisitor SimpleSubstVisitor Transform2NNF Transform2Prenex TriggerGenerator UniformSubstVisitor VariableIndexCollector VariablePermVisitor VariableShiftVisitor VariableSortChecker VariableSortInferenceVisitor VariableSubstVisitor CtorIdRewriter TheoryCollector ModPostprocessor Preproc IntToTermTranslator
postprocess
Theory TypeTheory
pow
IdealInt MulTheory
pow2
IdealInt ModuloArithmetic
pow2MinusOne
IdealInt ModuloArithmetic
pow2Mod
IdealInt ModuloArithmetic
powMod
IdealInt
pp
SimpleAPI
preAxioms
ModuloArithmetic
preVisit
AllExVisitor BitvectorSimplifier WolverineInterpolantLineariser AbstractVariableSubstVisitor CollectingVisitor ConstantSubstVisitor ContainsSymbol ContextAwareVisitor EquivExpander ExpressionReplacingVisitor IsUniversalFormulaVisitor PartExtractor PredicateSubstVisitor QuantifierCollectingVisitor SelectiveQuantifierCountVisitor SimplifyingConstantSubstVisitor SymbolCollector Transform2NNF Transform2Prenex TriggerGenerator VariableIndexCollector VariablePermVisitor VariableShiftVisitor VariableSortInferenceVisitor CtorIdRewriter ModPostprocessor Preproc
pred
Predicate IAtom Atom
pred2Conj
TerForConvenience
pred2PredConj
TerForConvenience
pred2RichPred
TerForConvenience
predConj
Conjunction ChangedConjResult
predConj2Conj
TerForConvenience
predOrdering
TermOrder
predTranslation
FunctionEncoder
predTypeFromSort
SMTLineariser
predefFunctions
AbstractStringTheory AbstractStringTheoryWithSort
predefNames
PartName
predefNamesSet
PartName
predefPredicates
Heap ArraySeqTheory AbstractStringTheory
predicateMatchConfig
Signature APIStack Environment ADT BitShiftMultiplication DivZero ExtArray FunctionalConsistency Heap IntValueEnumTheory SimpleArray Theory ModuloArithmetic GroebnerMultiplication Fractions ArraySeqTheory SeqStringTheory TypeTheory UninterpretedSortTheory
predicateTypeMap
SMTParser2InputAbsy
predicates
PredicateCollector CertFormula CompoundFormulas SortedWithOrder TerFor Term ArithConj Conjunction NegatedConjunctions EquationSet InEqConj Atom PredConj ADT BitShiftMultiplication DivZero ExtArray FunctionalConsistency Heap IntValueEnumTheory SimpleArray Theory ModuloArithmetic GroebnerMultiplication Fractions ArraySeqTheory SeqStringTheory TypeTheory UninterpretedSortTheory
preds
ModelElement terfor
prefix
IVarShiftList IVarShiftMap
prefixLength
IVarShiftMap IVarShiftMapEmptyPrefix
prelResultPrinter
ProverArguments
preludeReader
ResourceFiles
preludeSignature
SoftwareInterpolationFramework
prepareAssumptions
PluginTask
prepareCert
LemmaBase
prepend
BranchInferenceCertificate SymWord Seqs
preprocInterpolantSpecs
Translation
preprocess
ADT Theory ModPreprocessor ModuloArithmetic SeqStringTheory TypeTheory
prettyPrint
Tree
printADTDeclaration
SMTLineariser
printADTDeclarations
SMTLineariser
printArguments
SMTLineariser
printConjecture
TPTPLineariser
printDefineFun
SMTLineariser
printExoticOptions
CmdlMain
printExpression
PrincessLineariser
printFormula
SMTLineariser TPTPLineariser
printGreeting
CmdlMain
printHeapDeclaration
SMTLineariser
printHeapDeclarations
SMTLineariser
printModel
SMTLineariser
printOptions
CmdlMain
printResult
CmdlMain
printSMTType
SMTLineariser
printSort
PrettyScalaLineariser
printTerm
SMTLineariser TPTPLineariser
printUsage
CmdlMain
println
AbstractFileProver
prioritisedTasks
TaskManager
priority
AddFactsTask AllQuantifierTask BetaFormulaTask BlockedFormulaTask BoundStrengthenTask DivisibilityTask ExQuantifierTask LazyMatchTask NegLitClauseTask PrioritisedTask UpdateConstantFreedomTask WrappedFormulaTask IntermediatePluginTask ScheduleTask PrioritisedPluginTask
problemFunctions
FunctionPreproc
proc
ScheduleTask
processConstraint
Translation Postprocessing
processFormula
Postprocessing
processIncrementally
SMTParser2InputAbsy
processInterpolant
Translation Postprocessing
processModel
Translation Postprocessing
product
PseudoRing
program
NonInterferenceChecker NonInterferenceChecker2
programRelation
NonInterferenceChecker2
proj1
FrameworkVocabulary
proj2
FrameworkVocabulary
projectAll
SimpleAPI
projectEx
SimpleAPI
proof
ap
proofResult
IntelliFileProver
proofTree
IntelliFileProver
propagateConstraint
AlphaInference AntiSymmetryInference BranchInference ColumnReduceInference CombineEquationsInference CombineInequalitiesInference DirectStrengthenInference DivRightInference GroundInstInference MacroInference PartialCertificateInference PredUnifyInference QuantifierInference ReduceInference ReducePredInference ReusedProofMarker SimpInference TheoryAxiomInference
propagateGreaterThan
IntervalSet
propagateIneq
IntervalSet
propagateLessThan
IntervalSet
propagateSpecials
IntervalSet
proveMultiSMT
CmdlMain
proveProblem
CmdlMain
proveProblems
CmdlMain
proveSimpleAssumptions
PluginTask
prover
CheckSatCommand
providedFormulas
AlphaInference AntiSymmetryInference BetaCertificate BetaCertificateHelper BranchInference ColumnReduceInference CombineEquationsInference CombineInequalitiesInference DirectStrengthenInference DivRightInference GroundInstInference MacroInference OmegaCertificate PartialCertificateInference PartialCombCertificate PredUnifyInference QuantifierInference ReduceInference ReducePredInference ReusedProofMarker SimpInference StrengthenCertificate StrengthenCertificateHelper TheoryAxiomInference
pseudoApply
ComposeSubsts IdentitySubst PseudoDivSubstitution SimpleSubstitution Substitution
pseudoReduce
EquationConj ReduceWithEqs
pullOutTriggers
IterativeClauseMatcher
purifyFormula
ModPostprocessor
push
SimpleAPI SymbolRangeEnvironment Context IVarShift IVarShiftList IVarShiftMap IVarShiftMapEmptyPrefix SMTParser2InputAbsy LemmaBase
pushAPIFrame
APIStack
pushEmptyFrame
SimpleAPI
pushState
Parser2InputAbsy
pushVar
Environment
pwd
InputDialog