StackItem.hpp

/*
 
Copyright © 2023-24 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/>. 
 
*/
 
#ifndef STACKITEM_HPP
#define STACKITEM_HPP
 
#include<iostream>
 
#include "SimplePath.hpp"
#include "Lemmata.hpp"
 
using std::ostream;
 
enum class StackItemType {
  Start, Axiom, Reduction, LeftBranch, RightBranch, Lemmata
};
 
ostream& operator<<(ostream&, const StackItemType&);
 
struct StackItem {
  StackItemType item_type;
  Clause c;
  SimplePath p;
  Lemmata l;
  Substitution sub;
  vector<InferenceItem> actions;
  uint32_t depth;
  InferenceItem this_action;
  size_t bt_restriction_index;
  //----------------------------------------------------------------------
  // Many constructors - mostly you're just using StackItems as 
  // storage and there isn't much to do with the contents.
  //----------------------------------------------------------------------
  StackItem() = delete;
  StackItem(StackItemType sit)
  : item_type(sit)
  , c()
  , p()
  , l()
  , sub()
  , actions()
  , depth(0)
  , this_action()
  , bt_restriction_index(0)
  {};
  StackItem(StackItemType sit, const Clause& _c, const SimplePath& _p)
  : item_type(sit)
  , c(_c)
  , p(_p)
  , l()
  , sub()
  , actions()
  , depth(0)
  , this_action()
  , bt_restriction_index(0)
  {};
  StackItem(StackItemType sit, const Clause& _c, const SimplePath& _p, const Lemmata& _l)
  : item_type(sit)
  , c(_c)
  , p(_p)
  , l(_l)
  , sub()
  , actions()
  , depth(0)
  , this_action()
  , bt_restriction_index(0)
  {};
  StackItem(StackItemType sit, const Clause& _c, const SimplePath& _p, uint32_t _d)
  : item_type(sit)
  , c(_c)
  , p(_p)
  , l()
  , sub()
  , actions()
  , depth(_d)
  , this_action()
  , bt_restriction_index(0)
  {};
  StackItem(StackItemType sit,
    const Clause& _c,
    const SimplePath& _p,
    const Lemmata& _l,
    uint32_t _d)
  : item_type(sit)
  , c(_c)
  , p(_p)
  , l(_l)
  , sub()
  , actions()
  , depth(_d)
  , this_action()
  , bt_restriction_index(0)
  {};
  StackItem(StackItemType sit, const Clause& _c, const SimplePath& _p,
            const Substitution& _sub , uint32_t _d)
  : item_type(sit)
  , c(_c)
  , p(_p)
  , l()
  , sub(_sub)
  , actions()
  , depth(_d)
  , this_action()
  , bt_restriction_index(0)
  {};
  StackItem(StackItemType sit, const Clause& _c, const SimplePath& _p, const Lemmata& _l,
            const Substitution& _sub , uint32_t _d)
  : item_type(sit)
  , c(_c)
  , p(_p)
  , l(_l)
  , sub(_sub)
  , actions()
  , depth(_d)
  , this_action()
  , bt_restriction_index(0)
  {};
  void restrict_backtrack();
  string to_string_unsubbed() const;
  void clear() { actions.clear(); }
  inline void set_this_action(const InferenceItem& inf_i) {
    this_action = inf_i;
  }
  inline void set_bt_restriction_index(size_t i) {
    bt_restriction_index = i;
  }
};
 
ostream& operator<<(ostream&, const StackItem&);
 
#endif