ArrayHeap

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

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.

object HeapSort extends ProxySort with TheorySort

The sort of heaps.

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.

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

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

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

def equals(arg0: Any): Boolean

def evalFun(f: IFunApp): Option[ITerm]

Optionally, a function evaluating theory functions applied to concrete arguments, represented as constructor terms.

def evalPred(p: IAtom): Option[Boolean]

Optionally, a function evaluating theory predicates applied to concrete arguments, represented as constructor terms.

def evaluatingSimplifier(t: IExpression): IExpression

A simplification function that applies the methods evalFun and evalPred to some given expression (but not recursively).

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 order

def fun2SMTString(f: IFunction): Option[String]

Translate a function belonging to this theory to an SMT-LIB identifier.

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.

final def getClass(): Class[_]

def hasUserHeapCtor(t: ITerm, id: Int): IFormula

Tester for the user-declared heap constructors.

def hashCode(): Int

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.

final def isInstanceOf[T0]: Boolean

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 PresburgerModelFinder about terms that will be handled exclusively by this theory.

val name: String

final def ne(arg0: AnyRef): Boolean

val nextAddr: MonoSortedIFunction

A function to enumerate the next addresses that will be returned by the alloc function.

final def notify(): Unit

final def notifyAll(): Unit

val nullAddr: MonoSortedIFunction

Constant representing the null address.

val nullAddrCtorId: Int

lazy val objectSortIndex: Int

The index of the ObjectSort among the userHeapSorts.

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.

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.

def pred2SMTString(p: Predicate): Option[String]

Translate a predicate belonging to this theory to an SMT-LIB identifier.

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.

def printSMTDeclaration: Unit

Overrides to make Heap SMT-linearisable

val range: MonoSortedIFunction

A function to enumerate range of the addresses that can be used on this heap.

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.

val singleInstantiationPredicates: Set[Predicate]

When instantiating existentially quantifier formulas, EX phi, at most one instantiation is necessary provided that all predicates in phi are contained in this set.

def sort2SMTType(s: Sort): Option[SMTType]

Translate a sort belonging to this theory to an SMT type.

val storeRange: MonoSortedIFunction

val storeRange2: MonoSortedIFunction

final def synchronized[T0](arg0: ⇒ T0): T0

def toString(): String

val totalityAxioms: Conjunction

Additional axioms that are included if the option +genTotalityAxioms is given to Princess.

lazy val transitiveDependencies: Iterable[Theory]

Dependencies closed under transitivity, i.e., also including the dependencies of dependencies.

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

final def wait(arg0: Long): Unit

final def wait(): Unit

val write: MonoSortedIFunction

Function to write to the heap.

val writeRange: MonoSortedIFunction

Function to overwrite objects within an address range.

def finalize(): Unit