Class/Object

ap.theories

Heap

Related Docs: object Heap | package theories

Permalink

class Heap extends Theory

Linear Supertypes
Theory, AnyRef, Any
Ordering
  1. Alphabetic
  2. By inheritance
Inherited
  1. Heap
  2. Theory
  3. AnyRef
  4. Any
  1. Hide All
  2. Show all
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Heap(heapSortName: String, addressSortName: String, objectSort: ADTSort, sortNames: Seq[String], ctorSignatures: Seq[(String, CtorSignature)], defaultObjectCtor: (Seq[MonoSortedIFunction], ADT) ⇒ ITerm)

    Permalink

Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. val AddressSort: AddressSort

    Permalink
  5. object HeapADTSortId extends Enumeration

    Permalink
  6. implicit def HeapADTSortIdToInt(id: HeapADTSortId): Int

    Permalink
  7. val HeapSort: HeapSort

    Permalink
  8. val ObjectSort: Sort

    Permalink
  9. val _defObj: ITerm

    Permalink
  10. val addrRangeSize: MonoSortedIFunction

    Permalink
  11. val addrRangeStart: MonoSortedIFunction

    Permalink
  12. val addressRangeCtor: MonoSortedIFunction

    Permalink
  13. val addressRangeSort: ADTProxySort

    Permalink
  14. val alloc: MonoSortedIFunction

    Permalink

    Functions and predicates of the theory Assuming Address as address sort name, Heap as heap sort name, and Obj as the selected object sort.

    Functions and predicates of the theory Assuming Address as address sort name, Heap as heap sort name, and Obj as the selected object sort. Some function / predicate names incorporate the defined / selected names. *************************************************************************** Public functions and predicates *************************************************************************** emptyHeap : () --> Heap alloc : Heap x Obj --> Heap x Address (allocResHeap) read : Heap x Address --> Obj write : Heap x Address x Obj --> Heap valid (isAlloc) : Heap x Address --> Bool deAlloc : Heap --> Heap nthAddress : Nat --> Address

    batchAlloc : Heap x Obj x Nat --> Heap x AddressRange (batchAllocResHeap) batchWrite : Heap x AddressRange x Obj --> Heap nth : AddressRange x Nat --> Address within : AddressRange x Address --> Bool

    0 1 writeADT : Obj x Obj --> Heap * Updates the ADT's field (described by a read to 0) using value (1) *************************************************************************** Private functions and predicates *************************************************************************** counter : Heap --> Nat

    * Below two functions are shorthand functions to get rid of allocRes ADT. * They return a single value instead of the pair <Heap x Addr>. * This also removes some quantifiers related to the ADT in the generated * interpolants. alloc<heapSortName> : Heap x Obj --> Heap alloc<addressSortName> : Heap x Obj --> Address

    * Below two functions are shorthand functions to get rid of batchAllocRes ADT. * They return a single value instead of the pair <Heap x AddressRange>. * This also removes some quantifiers related to the ADT in the generated * interpolants. batchAlloc<heapSortName> : Heap x Obj x Nat --> Heap batchAlloc<addressSortName>Range : Heap x Obj x Nat --> AddressRange * ***************************************************************************

  15. val allocAddr: MonoSortedIFunction

    Permalink
  16. val allocHeap: MonoSortedIFunction

    Permalink
  17. val allocResCtor: MonoSortedIFunction

    Permalink
  18. val allocResSort: ADTProxySort

    Permalink
  19. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  20. val axioms: Conjunction

    Permalink

    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).

    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).

    Definition Classes
    HeapTheory
  21. val axioms1: Formula

    Permalink
  22. val axioms2: Formula

    Permalink
  23. val batchAlloc: MonoSortedIFunction

    Permalink
  24. val batchAllocAddrRange: MonoSortedIFunction

    Permalink
  25. val batchAllocHeap: MonoSortedIFunction

    Permalink
  26. val batchAllocResCtor: MonoSortedIFunction

    Permalink
  27. val batchAllocResSort: ADTProxySort

    Permalink
  28. val batchWrite: MonoSortedIFunction

    Permalink
  29. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  30. def containsADTSort(sort: Sort): Boolean

    Permalink

    Returns whether (an ADT) sort is declared as part of this theory.

  31. val counter: MonoSortedIFunction

    Permalink
  32. val deAlloc: MonoSortedIFunction

    Permalink
  33. val dependencies: Iterable[Theory]

    Permalink

    Optionally, other theories that this theory depends on.

    Optionally, other theories that this theory depends on.

    Definition Classes
    HeapTheory
  34. val emptyHeap: MonoSortedIFunction

    Permalink
  35. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  36. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  37. def evalFun(f: IFunApp): Option[ITerm]

    Permalink

    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
  38. def evalPred(p: IAtom): Option[Boolean]

    Permalink

    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
  39. def extend(order: TermOrder): TermOrder

    Permalink

    Add the symbols defined by this theory to the order

    Add the symbols defined by this theory to the order

    Definition Classes
    Theory
  40. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  41. val funPredicates: Seq[Predicate]

    Permalink
  42. val functionPredicateMapping: List[(MonoSortedIFunction, Predicate)]

    Permalink

    Mapping of interpreted functions to interpreted predicates, used translating input ASTs to internal ASTs (the latter only containing predicates).

    Mapping of interpreted functions to interpreted predicates, used translating input ASTs to internal ASTs (the latter only containing predicates).

    Definition Classes
    HeapTheory
  43. val functionTranslation: Map[IFunction, Predicate]

    Permalink
  44. val functionalPredicates: Set[Predicate]

    Permalink

    Information which of the predicates satisfy the functionality axiom; at some internal points, such predicates can be handled more efficiently

    Information which of the predicates satisfy the functionality axiom; at some internal points, such predicates can be handled more efficiently

    Definition Classes
    HeapTheory
  45. val functions: List[MonoSortedIFunction]

    Permalink

    Interpreted functions of the theory

    Interpreted functions of the theory

    Definition Classes
    HeapTheory
  46. def generateDecoderData(model: Conjunction): Option[TheoryDecoderData]

    Permalink

    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
  47. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  48. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  49. val heapADTDefinitions: Map[HeapADTSortId, (String, CtorSignature)]

    Permalink
  50. val heapADTs: ADT

    Permalink
  51. def iPostprocess(f: IFormula, signature: Signature): IFormula

    Permalink

    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 formula after calling Internal2Inputabsy.

    Definition Classes
    Theory
  52. def iPreprocess(f: IFormula, signature: Signature): (IFormula, Signature)

    Permalink

    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. This method will be applied very early in the translation process.

    Definition Classes
    HeapTheory
  53. val inductionAxioms: IFormula

    Permalink
  54. val isAlloc: MonoSortedPredicate

    Permalink
  55. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  56. def isSoundForSat(theories: Seq[Theory], config: Theory.SatSoundnessConfig.Value): Boolean

    Permalink

    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.

    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.

    Definition Classes
    HeapTheory
  57. val modelGenPredicates: Set[Predicate]

    Permalink

    Optionally, a set of predicates used by the theory to tell the PresburgerModelFinder about terms that will be handled exclusively by this theory.

    Optionally, a set of predicates used by the theory to tell the PresburgerModelFinder about terms that will be handled exclusively by this theory. If a proof goal in model generation mode contains an atom p(x), for p in this set, then the PresburgerModelFinder will ignore x when assigning concrete values to symbols.

    Definition Classes
    Theory
  58. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  59. val newAddr: MonoSortedIFunction

    Permalink
  60. val newAddrRange: MonoSortedIFunction

    Permalink
  61. val newBatchHeap: MonoSortedIFunction

    Permalink
  62. val newHeap: MonoSortedIFunction

    Permalink
  63. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  64. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  65. val nth: MonoSortedIFunction

    Permalink
  66. val nthAddr: MonoSortedIFunction

    Permalink
  67. val nullAddr: MonoSortedIFunction

    Permalink
  68. val order: TermOrder

    Permalink
  69. def plugin: Option[Plugin]

    Permalink

    Optionally, a plug-in implementing reasoning in this theory

    Optionally, a plug-in implementing reasoning in this theory

    Definition Classes
    HeapTheory
  70. val postSimplifiers: Seq[(IExpression) ⇒ IExpression]

    Permalink

    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 with ap.parser.Simplifier.

    Definition Classes
    HeapTheory
  71. def postprocess(f: Conjunction, order: TermOrder): Conjunction

    Permalink

    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
  72. val predefPredicates: List[MonoSortedPredicate]

    Permalink
  73. val predicateMatchConfig: PredicateMatchConfig

    Permalink

    Information how interpreted predicates should be handled for e-matching.

    Information how interpreted predicates should be handled for e-matching.

    Definition Classes
    HeapTheory
  74. val predicates: List[Predicate]

    Permalink

    Interpreted predicates of the theory

    Interpreted predicates of the theory

    Definition Classes
    HeapTheory
  75. def preprocess(f: Conjunction, order: TermOrder): Conjunction

    Permalink

    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
  76. val read: MonoSortedIFunction

    Permalink
  77. val reducerPlugin: ReducerPluginFactory

    Permalink

    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
  78. def rewriter(expr: IExpression): IExpression

    Permalink
  79. val singleInstantiationPredicates: Set[Predicate]

    Permalink

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

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

    Definition Classes
    Theory
  80. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  81. val theoryAxioms: IFormula

    Permalink
  82. def toString(): String

    Permalink
    Definition Classes
    Heap → AnyRef → Any
  83. val totalityAxioms: Conjunction

    Permalink

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

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

    Definition Classes
    HeapTheory
  84. val triggerRelevantFunctions: Set[IFunction]

    Permalink

    A list of functions that should be considered in automatic trigger generation

    A list of functions that should be considered in automatic trigger generation

    Definition Classes
    HeapTheory
  85. val triggeredAxioms: IFormula

    Permalink
  86. val userADTCtors: Seq[MonoSortedIFunction]

    Permalink
  87. val userADTSels: Seq[Seq[MonoSortedIFunction]]

    Permalink
  88. val userADTSorts: IndexedSeq[ADTProxySort]

    Permalink
  89. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  90. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  91. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  92. val within: MonoSortedPredicate

    Permalink
  93. val write: MonoSortedIFunction

    Permalink
  94. def writeADT(lhs: IFunApp, rhs: ITerm): ITerm

    Permalink

    Helper function to write to ADT fields.

    Helper function to write to ADT fields.

    lhs

    : the ADT field term to be written to. This should be an IFunApp, where the outermost function is a selector of the ADT, the innermost function is a heap read to the ADT on the heap, the innermost+1 function is the getter of the ADT, and any intermediate functions are other selectors e.g. x(getS(read(h, p))) or (in C: p->x) x(s(getS(read(h, p)))) (in C: p->s.x) note that this method works for writing to non-ADTs as well, if lhs is provided as a read Object (e.g. getInt(read(h,p))).

    rhs

    : the new value for the field, e.g. 42 this would return a new term, such as: S(42, y(s))

    returns

    : the new ADT term

Inherited from Theory

Inherited from AnyRef

Inherited from Any

Ungrouped