Class StratDefVector

java.lang.Object
es.ucm.maude.bindings.StratDefVector
public class StratDefVector extends Object
Internal Maude vector.

  • Constructor Details

    • StratDefVector

      public StratDefVector(long length)
      Construct a vector.

      Parameters:
      length - The initial length.

    • StratDefVector

      public StratDefVector()
      Construct a vector.

  • Method Details

    • delete

      public void delete()

    • empty

      public boolean empty()
      Is the vector empty?

    • size

      public long size()
      Size of the vector.

    • capacity

      public long capacity()
      Reserved capacity of the vector.

    • swap

      public void swap(StratDefVector other)
      Swap this vector's contents with another.

      Parameters:
      other - The other vector.

    • get

      public StrategyDefinition get(long n)
      Get a vector position value.

      Parameters:
      n - Vector position from zero.

    • set

      public void set(long n, StrategyDefinition value)
      Set a vector position value.

      Parameters:
      n - Vector position from zero.
      value - Value to be set.

    • append

      public void append(StrategyDefinition value)
      Append a new element to the vector.

    • clear

      public void clear()
      Set the vector length to zero.

    • resize

      public void resize(long new_size)
      Resize the vector.

      Parameters:
      new_size - New size.