POGraph
util
PORTFOLIO
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
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
SimpleAPI
PartitionOrdering
nia
PeekIterator
util
PeekIteratorTrafo
util
PlainIdentifier
SMTParser2InputAbsy
PlainRange
util
PlainSymbol
SMTParser2InputAbsy
Plugin
theoryPlugins
PluginSequence
theoryPlugins
PluginTask
theoryPlugins
Polynomial
nia
PortfolioOptions
Param
Positive
PredicateMatchStatus NegSolvingOptions
PreVisitResult
CollectingVisitor
PredApplier
IExpression
PredConj
preds
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
ProofTree
tree
ProofTreeFactory
tree
ProofTreeOneChild
tree
ProofWithModel
Prover
Prover
ap
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
pairs
Monomial
paramMap
Settings
parameters
InterpolationContext ap
parikhSizeConstraints
ADT
parseAndSimplify
SoftwareInterpolationFramework
parseExpression
ApParser2InputAbsy SMTParser2InputAbsy
parseIgnoreCommand
SMTParser2InputAbsy
parseParameter
TheoryBuilder
parseParameters
TheoryBuilder
parseProblem
SoftwareInterpolationFramework
parser
ap
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
path1
NIInterpolation NIInterpolation
path2
NIInterpolation NIInterpolation
patternType
ConstantWeight NonCoeffWeight OneWeight VariableWeight
patterns
ITrigger
peekNext
LCBlender PeekIterator PeekIteratorTrafo PriorityQueueWithIterators
plainReduce
ReduceWithAC
plugin
ADT BitShiftMultiplication FunctionalConsistency SimpleArray Theory ModuloArithmetic GroebnerMultiplication Fractions 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
popState
Parser2InputAbsy
popVar
Environment
posTranslation
AbstractFileProver
positiveEqs
ArithConj
positiveLits
PredConj
positiveLitsAsSet
PredConj
positiveLitsWithPred
PredConj
postVisit
AllExVisitor BitvectorSimplifier SelectStoreCollector PredicateCollector PredicateReplace WolverineInterpolantLineariser CollectingVisitor ConstantSubstVisitor ContainsSymbol EquivExpander FunctionCollector IsUniversalFormulaVisitor PartExtractor PartNameEliminator PartialEvaluator PredicateSubstVisitor QuantifierCollectingVisitor QuantifierCountVisitor SelectiveQuantifierCountVisitor SimplifyingConstantSubstVisitor SimplifyingVariableSubstVisitor SymbolCollector DepthCountingVisitor SimpleSubstVisitor Transform2NNF Transform2Prenex TriggerGenerator UniformSubstVisitor VariableIndexCollector VariablePermVisitor VariableShiftVisitor VariableSubstVisitor TheoryCollector Preproc IntToTermTranslator
pow
IdealInt MulTheory
pow2
ModuloArithmetic
pow2MinusOne
ModuloArithmetic
pow2Mod
ModuloArithmetic
powMod
IdealInt
pp
SimpleAPI
preAxioms
ModuloArithmetic
preVisit
AllExVisitor BitvectorSimplifier WolverineInterpolantLineariser CollectingVisitor ConstantSubstVisitor ContainsSymbol ContextAwareVisitor EquivExpander IsUniversalFormulaVisitor PartExtractor PredicateSubstVisitor QuantifierCollectingVisitor SelectiveQuantifierCountVisitor SimplifyingConstantSubstVisitor SimplifyingVariableSubstVisitor SymbolCollector Transform2NNF Transform2Prenex TriggerGenerator VariableIndexCollector VariablePermVisitor VariableShiftVisitor VariableSubstVisitor 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
predefPredicates
AbstractStringTheory
predicateMatchConfig
Signature Environment ADT BitShiftMultiplication FunctionalConsistency SimpleArray Theory ModuloArithmetic GroebnerMultiplication Fractions SeqStringTheory TypeTheory UninterpretedSortTheory
predicates
PredicateCollector CertFormula CompoundFormulas SortedWithOrder TerFor Term ArithConj Conjunction NegatedConjunctions EquationSet InEqConj Atom PredConj ADT BitShiftMultiplication FunctionalConsistency SimpleArray Theory ModuloArithmetic GroebnerMultiplication Fractions SeqStringTheory TypeTheory UninterpretedSortTheory
preds
ModelElement terfor
prefix
IVarShiftList IVarShiftMap
prefixLength
IVarShiftMap IVarShiftMapEmptyPrefix
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
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 ScheduleTask PrioritisedPluginTask
proc
ScheduleTask
processIncrementally
SMTParser2InputAbsy
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
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
push
SimpleAPI SymbolRangeEnvironment Context IVarShift IVarShiftList IVarShiftMap IVarShiftMapEmptyPrefix SMTParser2InputAbsy LemmaBase
pushEmptyFrame
SimpleAPI
pushState
Parser2InputAbsy
pushVar
Environment VisitorArg
pwd
InputDialog