heaps

Type Members

1. class ArrayHeap extends Heap

   

   A theory of heaps implemented using arrays.

   A theory of heaps implemented using arrays.

   At the moment, extensionality and the range operations are not fully implemented yet.

2. trait Heap extends Theory with SMTLinearisableTheory

   

   Trait implemented by the different heap theories.

3. class NativeHeap extends Heap

   

   defaultObjectCtor is called from the theory (before it is completely initialised), and it passes back the theory ADTs for adding to environment (e.g.

   defaultObjectCtor is called from the theory (before it is completely initialised), and it passes back the theory ADTs for adding to environment (e.g. as done in SMTParser2InputAbsy), and also the actual constructors for the ctorSignatures, so the defObj term can be built using those.