class ArrayHeap extends Heap
A theory of heaps implemented using arrays.
At the moment, extensionality and the range operations are not fully implemented yet.
- Alphabetic
- By Inheritance
- ArrayHeap
- Heap
- SMTLinearisableTheory
- Theory
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new ArrayHeap(heapSortName: String, addressSortName: String, rangeSortName: String, objectSort: ADTSort, userSortNames: Seq[String], ctorSignatures: Seq[(String, CtorSignature)], defaultObjectCtor: (Seq[MonoSortedIFunction]) => ITerm)
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val AddressSort: ADTProxySort
Sort of addresses in this heap theory.
- val ArraySort: ArraySort
- val HeapAddressPairSort: ADTProxySort
Result sort of the allocation function.
- val HeapRangePairSort: ADTProxySort
Result sort of the range allocation function.
- val ObjectSort: ADTProxySort
Sort of objects stored on the heap.
- val RangeSort: ADTProxySort
Sort of address ranges in this heap theory.
- def SMTDeclarationSideEffects: Seq[Theory]
A list of (other) theories that are implicitly declared as a side-effect of declaring this theory.
A list of (other) theories that are implicitly declared as a side-effect of declaring this theory. We assume that theories can implicitly define some of their dependencies, but not vice versa.
- Definition Classes
- Heap → SMTLinearisableTheory
- val addr: MonoSortedIFunction
A function to enumerate the addresses that can be used on this heap.
- val addrCtorId: Int
- val addrOrd: MonoSortedIFunction
- val addressSortId: Int
- val allAxioms: IFormula
- val alloc: MonoSortedIFunction
Function to allocate new objects on the heap.
- val allocRange: MonoSortedIFunction
Function to allocate a sequence of objects on the heap.
- val arrayTheory: ExtArray
Arrays used to represent heap contents.
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- val axioms: Formula
Axioms defining the theory; such axioms are simply added as formulae to the problem to be proven, and thus handled using the standard reasoning techniques (including e-matching).
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- val defaultObject: ITerm
The object stored on the heap at not yet allocated locations.
- val dependencies: List[Theory { val totalityAxioms: ap.terfor.conjunctions.Conjunction }]
Optionally, other theories that this theory depends on.
- val distinctHeaps: MonoSortedPredicate
- val emptyHeap: MonoSortedIFunction
Constant representing empty heaps.
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- def evalFun(f: IFunApp): Option[ITerm]
Optionally, a function evaluating theory functions applied to concrete arguments, represented as constructor terms.
Optionally, a function evaluating theory functions applied to concrete arguments, represented as constructor terms.
- Definition Classes
- Theory
- def evalPred(p: IAtom): Option[Boolean]
Optionally, a function evaluating theory predicates applied to concrete arguments, represented as constructor terms.
Optionally, a function evaluating theory predicates applied to concrete arguments, represented as constructor terms.
- Definition Classes
- Theory
- def evaluatingSimplifier(t: IExpression): IExpression
A simplification function that applies the methods
evalFunandevalPredto some given expression (but not recursively).A simplification function that applies the methods
evalFunandevalPredto some given expression (but not recursively). This is used in theTheory.postSimplifiersmethods.- Definition Classes
- Theory
- def expandFormula(f: IFormula): IFormula
Translate a formula to its internal presentation in terms of arrays and ADTs.
- def expandTerm(f: ITerm): ITerm
Translate a term to its internal presentation in terms of arrays and ADTs.
- def extend(order: TermOrder): TermOrder
Add the symbols defined by this theory to the
orderAdd the symbols defined by this theory to the
order- Definition Classes
- Theory
- def fun2SMTString(f: IFunction): Option[String]
Translate a function belonging to this theory to an SMT-LIB identifier.
Translate a function belonging to this theory to an SMT-LIB identifier.
- Definition Classes
- SMTLinearisableTheory
- val funPredMap: Map[IFunction, Predicate]
- val functionPredicateMapping: List[(MonoSortedIFunction, Predicate)]
Mapping of interpreted functions to interpreted predicates, used translating input ASTs to internal ASTs (the latter only containing predicates).
- val functionalPredicates: Set[Predicate]
Information which of the predicates satisfy the functionality axiom; at some internal points, such predicates can be handled more efficiently
- val functions: List[MonoSortedIFunction]
Interpreted functions of the theory
- def generateDecoderData(model: Conjunction): Option[TheoryDecoderData]
If this theory defines any
Theory.Decoder, which can translate model data into some theory-specific representation, this function can be overridden to pre-compute required data from a model.If this theory defines any
Theory.Decoder, which can translate model data into some theory-specific representation, this function can be overridden to pre-compute required data from a model.- Definition Classes
- Theory
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hasUserHeapCtor(t: ITerm, id: Int): IFormula
Tester for the user-declared heap constructors.
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- val heapAddrPair: MonoSortedIFunction
- val heapAddrPair_1: MonoSortedIFunction
Function to obtain the new heap after allocation.
- val heapAddrPair_2: MonoSortedIFunction
Function to obtain the new address after allocation.
- val heapConstant: Predicate
- val heapContents: MonoSortedIFunction
- val heapPair: MonoSortedIFunction
- val heapRangePair: MonoSortedIFunction
- val heapRangePair_1: MonoSortedIFunction
Function to obtain the new heap after range allocation.
- val heapRangePair_2: MonoSortedIFunction
Function to obtain the new address range after range allocation.
- lazy val heapRelatedSymbols: (Set[IFunction], Set[Predicate])
Method to query all functions and predicates of the theory, including API, internal symbols, and symbols of the constituent theories.
- val heapSize: MonoSortedIFunction
- val heapSizeADT: ADT
ADT for the heap contents array and its size.
- def iPostprocess(f: IFormula, signature: Signature): IFormula
Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination.
- def iPreprocess(f: IFormula, signature: Signature): (IFormula, Signature)
Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover.
- def isAlloc: Predicate
Predicate to test whether an address is valid (allocated and non-null) in a given heap.
Predicate to test whether an address is valid (allocated and non-null) in a given heap. Synonym for
valid.- Definition Classes
- Heap
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def isSoundForSat(theories: Seq[Theory], config: Theory.SatSoundnessConfig.Value): Boolean
Check whether we can tell that the given combination of theories is sound for checking satisfiability of a problem, i.e., if proof construction ends up in a dead end, can it be concluded that a problem is satisfiable.
- val modelGenPredicates: Set[Predicate]
Optionally, a set of predicates used by the theory to tell the
PresburgerModelFinderabout terms that will be handled exclusively by this theory.Optionally, a set of predicates used by the theory to tell the
PresburgerModelFinderabout terms that will be handled exclusively by this theory. If a proof goal in model generation mode contains an atomp(x), forpin this set, then thePresburgerModelFinderwill ignorexwhen assigning concrete values to symbols. - val name: String
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- val nextAddr: MonoSortedIFunction
A function to enumerate the next addresses that will be returned by the
allocfunction.A function to enumerate the next addresses that will be returned by the
allocfunction. The next address that can be allocated isnextAddr(h, 0), thennextAddr(h, 1), etc. Applying the function to negative integers returns the last addresses that have been allocated:nextAddr(h, -1)is the last address that has been allocated onh,nextAddr(h, -2)the address before that, etc. Since a heap only has finitely many allocated addresses, for two smalln, the result ofnextAddr(h, n)isnullAddr.addr(k)is a synonym fornextAddr(emptyHeap, k - 1). - final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- val nullAddr: MonoSortedIFunction
Constant representing the null address.
- val nullAddrCtorId: Int
- lazy val objectSortIndex: Int
The index of the
ObjectSortamong theuserHeapSorts.The index of the
ObjectSortamong theuserHeapSorts.- Definition Classes
- Heap
- val offHeapADT: ADT
ADT for all things that cannot be on the heap.
- val onHeapADT: ADT
ADT for all objects that can potentially be stored on the heap.
- def plugin: Some[Plugin]
Optionally, a plug-in implementing reasoning in this theory
- def postSimplifiers: Seq[(IExpression) => IExpression]
Optionally, simplifiers that are applied to formulas output by the prover, for instance to interpolants or the result of quantifier.
Optionally, simplifiers that are applied to formulas output by the prover, for instance to interpolants or the result of quantifier. Such simplifiers are invoked by
ap.parser.Simplifier. By default, this list will only include theevaluatingSimplifier.- Definition Classes
- Theory
- def postprocess(f: Conjunction, signature: Signature): Conjunction
Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination.
Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination. This method will be applied to the raw formulas, before calling
Internal2Inputabsy.- Definition Classes
- Theory
- def pred2SMTString(p: Predicate): Option[String]
Translate a predicate belonging to this theory to an SMT-LIB identifier.
Translate a predicate belonging to this theory to an SMT-LIB identifier.
- Definition Classes
- SMTLinearisableTheory
- val predefPredicates: List[Predicate]
- val predicateMatchConfig: PredicateMatchConfig
Information how interpreted predicates should be handled for e-matching.
- val predicates: Seq[Predicate]
Interpreted predicates of the theory
- def preprocess(f: Conjunction, signature: Signature): Conjunction
Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover.
Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover.
- Definition Classes
- Theory
- def printSMTDeclaration: Unit
Overrides to make Heap SMT-linearisable
Overrides to make Heap SMT-linearisable
- Definition Classes
- Heap → SMTLinearisableTheory
- val range: MonoSortedIFunction
A function to enumerate range of the addresses that can be used on this heap.
A function to enumerate range of the addresses that can be used on this heap.
range(1, n)is a range of addresses starting at the addressaddr(1)of sizen. Applying the function to a start address that is not positive or size that is not non-negative should be interpreted as an empty address range. - val rangeCtorId: Int
- val rangeNth: MonoSortedIFunction
Function to obtain the n'th address in an address range.
- val rangeSize: MonoSortedIFunction
Function to obtain the number of addresses in an address range.
- val rangeSortId: Int
- val rangeStart: MonoSortedIFunction
- val rangeWithin: MonoSortedPredicate
Predicate to test whether an address belongs to an address range.
- val rawHeapSort: ADTProxySort
- val read: MonoSortedIFunction
Function to read from the heap.
- val readUnsafe: MonoSortedIFunction
- val reducerPlugin: ReducerPluginFactory
Optionally, a plugin for the reducer applied to formulas both before and during proving.
Optionally, a plugin for the reducer applied to formulas both before and during proving.
- Definition Classes
- Theory
- val singleInstantiationPredicates: Set[Predicate]
When instantiating existentially quantifier formulas,
EX phi, at most one instantiation is necessary provided that all predicates inphiare contained in this set.When instantiating existentially quantifier formulas,
EX phi, at most one instantiation is necessary provided that all predicates inphiare contained in this set.- Definition Classes
- Theory
- def sort2SMTType(s: Sort): Option[SMTType]
Translate a sort belonging to this theory to an SMT type.
Translate a sort belonging to this theory to an SMT type.
- Definition Classes
- SMTLinearisableTheory
- val storeRange: MonoSortedIFunction
- val storeRange2: MonoSortedIFunction
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- ArrayHeap → AnyRef → Any
- val totalityAxioms: Conjunction
Additional axioms that are included if the option
+genTotalityAxiomsis given to Princess. - lazy val transitiveDependencies: Iterable[Theory]
Dependencies closed under transitivity, i.e., also including the dependencies of dependencies.
Dependencies closed under transitivity, i.e., also including the dependencies of dependencies.
- Definition Classes
- Theory
- val triggerRelevantFunctions: Set[IFunction]
A list of functions that should be considered in automatic trigger generation
- val userHeapConstructors: IndexedSeq[MonoSortedIFunction]
Constructors declared as part of the heap ADT.
- val userHeapCtorSignatures: Seq[(String, CtorSignature)]
User-specified constructor declarations.
- val userHeapSelectors: IndexedSeq[Seq[MonoSortedIFunction]]
Selectors declared as part of the heap ADT.
- val userHeapSorts: IndexedSeq[ADTProxySort]
Sorts declared as part of the heap ADT.
- val userHeapUpdators: IndexedSeq[Seq[MonoSortedIFunction]]
Updators declared as part of the heap ADT.
- val userSortNum: Int
- val valid: MonoSortedPredicate
Predicate to test whether an address is valid (allocated and non-null) in a given heap.
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- val write: MonoSortedIFunction
Function to write to the heap.
- val writeRange: MonoSortedIFunction
Function to overwrite objects within an address range.
- object HeapSort extends ProxySort with TheorySort
The sort of heaps.
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)