Stack.hpp

/*
 
Copyright © 2023-25 Sean Holden. All rights reserved.
 
*/
/*
 
This file is part of Connect++.
 
Connect++ is free software: you can redistribute it and/or modify it 
under the terms of the GNU General Public License as published by the 
Free Software Foundation, either version 3 of the License, or (at your 
option) any later version.
 
Connect++ is distributed in the hope that it will be useful, but WITHOUT 
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 
FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for 
more details.
 
You should have received a copy of the GNU General Public License along 
with Connect++. If not, see <https://www.gnu.org/licenses/>. 
 
*/
 
#pragma once
 
#include "StackItem.hpp"
 
class Stack {
private:
    StackItem* stack;
    size_t next_item_index;
    size_t capacity;
    void extend(size_t _n) {
        size_t old_capacity = capacity;
        // _n == 0 is interpreted as "double the capacity".
        _n == 0 ? capacity *= 2 : capacity += _n;
        StackItem* old_stack = stack;
        stack = new StackItem [capacity];
        for (size_t i = 0; i < old_capacity; i++) {
            stack[i] = old_stack[i];
        }
        delete [] old_stack;
    }
public:
    Stack() : stack(), next_item_index(0), capacity(params::stack_start_size) { 
        stack = new StackItem [params::stack_start_size];
    };
    ~Stack() { delete [] stack; }
    inline void clear() {
        next_item_index = 0;
    }
    inline bool empty() const {
        return next_item_index == 0;
    }
    inline size_t size() const {
        return next_item_index;
    }
    inline void push_back(const StackItem& _item) {
        if (next_item_index == capacity) {
            extend(params::stack_increment);
        }
        stack[next_item_index++] = _item;
    }
    inline StackItem& back() {
        return stack[next_item_index - 1];
    }
    inline void pop_back() {
        next_item_index--;
    }
    inline StackItem& operator[](size_t _i) {
        return stack[_i];
    }
    inline void emplace_back(StackItemType sit,
                      const Clause& _c,
                      const SimplePath& _p,
                      const Lemmata& _l,
                      uint32_t _d) {
        if (next_item_index == capacity) {
            extend(params::stack_increment);
        }
        StackItem* si = stack + next_item_index;
        si->item_type = sit;
        si->c = _c;
        si->p = _p;
        si->l = _l;
        si->sub.clear();
        si->depth = _d;
        si->bt_restriction_index = 0;
        si->stack_item_setup();
        next_item_index++;
    }
    inline void emplace_back(StackItemType sit, 
                      const Clause& _c, 
                      const SimplePath& _p, 
                      const Lemmata& _l,
                      const Substitution& _sub, 
                      uint32_t _d) {
        if (next_item_index == capacity) {
            extend(params::stack_increment);
        }
        StackItem* si = stack + next_item_index;
        si->item_type = sit;
        si->c = _c;
        si->p = _p;
        si->l = _l;
        si->sub = _sub;
        si->depth = _d;
        si->bt_restriction_index = 0;
        si->stack_item_setup();
        next_item_index++;
    }
    friend ostream& operator<<(ostream&, Stack&);
};