/******************************************************************************

 * Top contributors (to current version):

 *   Morgan Deters, Tim King, Clark Barrett

 *

 * This file is part of the cvc5 project.

 *

 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS

 * in the top-level source directory and their institutional affiliations.

 * All rights reserved.  See the file COPYING in the top-level source

 * directory for licensing information.

 * ****************************************************************************

 * Context-dependent list class (only supports append).

 *

 * This list only supports appending to the list; on backtrack, the list is

 * simply shortened.

 */

#include "cvc5_private.h"

#ifndef CVC5__CONTEXT__CDLIST_H

#define CVC5__CONTEXT__CDLIST_H

#include <cstring>

#include <iterator>

#include <memory>

#include <string>

#include "base/check.h"

#include "context/cdlist_forward.h"

#include "context/context.h"

#include "context/context_mm.h"

namespace cvc5 {

namespace context {

/**

 * Generic context-dependent dynamic array.  Note that for efficiency,

 * this implementation makes the following assumptions:

 *

 * 1. Over time, objects are only added to the list.  Objects are only

 *    removed when a pop restores the list to a previous state.

 *

 * 2. T objects can safely be copied using their copy constructor,

 *    operator=, and memcpy.

 */

template <class T, class CleanUpT, class AllocatorT>

class CDList : public ContextObj {

public:

  /** The value type with which this CDList<> was instantiated. */

  typedef T value_type;

  /** The cleanup type with which this CDList<> was instantiated. */

  typedef CleanUpT CleanUp;

  /** The allocator type with which this CDList<> was instantiated. */

  typedef AllocatorT Allocator;

protected:

  /**

   * d_list is a dynamic array of objects of type T.

   */

  T* d_list;

  /**

   * Number of objects in d_list

   */

  size_t d_size;

private:

  static const size_t INITIAL_SIZE = 10;

  static const size_t GROWTH_FACTOR = 2;

  /**

   * Whether to call the destructor when items are popped from the

   * list.  True by default, but can be set to false by setting the

   * second argument in the constructor to false.

   */

  bool d_callDestructor;

  /**

   * Allocated size of d_list.

   */

  size_t d_sizeAlloc;

  /**

   * The CleanUp functor.

   */

  CleanUp d_cleanUp;

  /**

   * Our allocator.

   */

  Allocator d_allocator;

protected:

  /**

   * Private copy constructor used only by save().  d_list and

   * d_sizeAlloc are not copied: only the base class information and

   * d_size are needed in restore.

   */

    ContextObj(l),

    d_list(NULL),

    d_callDestructor(false),

    d_sizeAlloc(0),

    d_cleanUp(l.d_cleanUp),

  CDList& operator=(const CDList& l) = delete;

 private:

  /**

   * Reallocate the array with more space. Throws bad_alloc if memory

   * allocation fails. Does not perform any action if there is still unused

   * allocated space.

   */

    {

      // If there is still unused allocated space

    }

      // Allocate an initial list if one does not yet exist

      }

      }

    } else {

      // Allocate a new array with double the size

      }

      }

    }

  }

  /**

   * Implementation of mandatory ContextObj method save: simply copies

   * the current size to a copy using the copy constructor (the

   * pointer and the allocated size are *not* copied as they are not

   * restored on a pop).  The saved information is allocated using the

   * ContextMemoryManager.

   */

  {

  }

protected:

  /**

   * Implementation of mandatory ContextObj method restore: simply

   * restores the previous size.  Note that the list pointer and the

   * allocated size are not changed.

   */

 {

                   << std::endl;

  /**

   * Given a size parameter smaller than d_size, truncateList()

   * removes the elements from the end of the list until d_size equals size.

   *

   * WARNING! You should only use this function when you know what you are doing.

   * This is a primitive operation with strange context dependent behavior!

   * It is up to the user of the function to ensure that the saved d_size values

   * at lower context levels are less than or equal to size.

   */

      }

    } else {

    }

 public:

  /**

   * Main constructor: d_list starts as NULL, size is 0

   */

         bool callDestructor = true,

         const CleanUp& cleanup = CleanUp(),

         const Allocator& alloc = Allocator()) :

    ContextObj(context),

    d_list(NULL),

    d_size(0),

    d_callDestructor(callDestructor),

    d_sizeAlloc(0),

    d_cleanUp(cleanup),

  /**

   * Destructor: delete the list

   */

    }

  /**

   * Return the current size of (i.e. valid number of objects in) the

   * list.

   */

  }

  /**

   * Return true iff there are no valid objects in the list.

   */

  }

  /**

   * Add an item to the end of the list. This method uses the copy constructor

   * of T, so the type has to support it. As a result, this method cannot be

   * used with types that do not have a copy constructor such as

   * std::unique_ptr. Use CDList::emplace_back() instead of CDList::push_back()

   * to avoid this issue.

   */

                    << std::endl;

  /**

   * Construct an item to the end of the list. This method constructs the item

   * in-place (similar to std::vector::emplace_back()), so it can be used for

   * types that do not have a copy constructor such as std::unique_ptr.

   */

  template <typename... Args>

  {

                    << std::endl;

  /**

   * Access to the ith item in the list.

   */

  }

  /**

   * Returns the most recent item added to the list.

   */

  }

  /**

   * Iterator for CDList class.  It has to be const because we don't

   * allow items in the list to be changed.  It's a straightforward

   * wrapper around a pointer.  Note that for efficiency, we implement

   * only prefix increment and decrement.  Also note that it's OK to

   * create an iterator from an empty, uninitialized list, as begin()

   * and end() will have the same value (NULL).

   */

  class const_iterator {

    T const* d_it;

    friend class CDList<T, CleanUp, Allocator>;

  public:

    // FIXME we support operator--, but do we satisfy all the

    // requirements of a bidirectional iterator ?

    typedef std::input_iterator_tag iterator_category;

    typedef T value_type;

    typedef std::ptrdiff_t difference_type;

    typedef const T* pointer;

    typedef const T& reference;

    }

    }

    }

    inline const T* operator->() const { return d_it; }

    /** Prefix increment */

    }

    /** Prefix decrement */

    const_iterator& operator--() { --d_it; return *this; }

    /** operator+ */

    }

    // Postfix operations on iterators: requires a Proxy object to

    // hold the intermediate value for dereferencing

    class Proxy {

      const T* d_t;

    public:

      Proxy(const T& p): d_t(&p) {}

      T& operator*() {

        return *d_t;

      }

    };/* class CDList<>::const_iterator::Proxy */

    /** Postfix increment: returns Proxy with the old value. */

    Proxy operator++(int) {

      Proxy e(*(*this));

      ++(*this);

      return e;

    }

    /** Postfix decrement: returns Proxy with the old value. */

    Proxy operator--(int) {

      Proxy e(*(*this));

      --(*this);

      return e;

    }

  };/* class CDList<>::const_iterator */

  typedef const_iterator iterator;

  /**

   * Returns an iterator pointing to the first item in the list.

   */

  }

  /**

   * Returns an iterator pointing one past the last item in the list.

   */

  }

};/* class CDList<> */

template <class T, class CleanUp>

class CDList<T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {

  /* CDList is incompatible for use with a ContextMemoryAllocator.

   *

   * Explanation:

   * If ContextMemoryAllocator is used and d_list grows at a deeper context

   * level the reallocated will be reallocated in a context memory region that

   * can be destroyed on pop. To support this, a full copy of d_list would have

   * to be made. As this is unacceptable for performance in other situations, we

   * do not do this.

   */

  static_assert(sizeof(T) == 0,

                "Cannot create a CDList with a ContextMemoryAllocator.");

};

}  // namespace context

}  // namespace cvc5

#endif /* CVC5__CONTEXT__CDLIST_H */