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"
#include "Matrix.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;
size_t path_length;
Lemmata l;
Substitution sub;
vector<InferenceItem> actions;
uint32_t depth;
InferenceItem this_action;
size_t bt_restriction_index;
//----------------------------------------------------------------------
// Generation of reductions.
//----------------------------------------------------------------------
Literal reduction_lit;
Literal reduction_neg_lit;
LitNum reduction_ind;
size_t reduction_current_path_index;
bool reduction_backtrack_restricted;
InferenceItem reduction_next_result;
bool reduction_no_more_results;
//----------------------------------------------------------------------
// Generation of extensions.
//----------------------------------------------------------------------
Literal extension_lit;
Literal extension_neg_lit;
LitNum extension_ind;
size_t extension_i;
size_t extension_index_entry_size;
size_t extension_current_index_entry;
bool extension_backtrack_restricted;
InferenceItem extension_next_result;
bool extension_no_more_results;
void stack_item_setup(); 
void reduction_initialize(Unifier&); 
void reduction_move_to_next_result(Unifier&);
inline bool reduction_is_empty() const { 
    return (reduction_backtrack_restricted || reduction_no_more_results); 
}
inline void reduction_restrict_backtrack() { 
    reduction_backtrack_restricted = true; 
}
InferenceItem next_reduction(Unifier&);
void all_reductions(vector<InferenceItem>&, Unifier&);
void extension_initialize(Matrix&, Unifier&);
void extension_move_to_next_result(Matrix&, Unifier&);
inline bool extension_is_empty() const { 
    return (extension_backtrack_restricted || extension_no_more_results); 
}
inline void extension_restrict_backtrack() { 
    extension_backtrack_restricted = true; 
}
InferenceItem next_extension(Matrix&, Unifier&);
void all_extensions(vector<InferenceItem>&, Matrix&, Unifier&);
  //----------------------------------------------------------------------
  // 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)
  { stack_item_setup(); }
 
  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)
  { stack_item_setup(); }
 
  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)
  { stack_item_setup(); }
 
  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)
  { stack_item_setup(); }
 
  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)
  { stack_item_setup(); }
 
  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)
  { stack_item_setup(); }
  
  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)
  { stack_item_setup(); }
  void initialize(Matrix&, Unifier&);
  void restrict_backtrack();
  void add_all_extensions_to_actions(Matrix&, Unifier&);
  void add_all_reductions_to_actions(Unifier&);
  bool no_more_inferences(); 
  InferenceItem get_next_inference(Matrix&, Unifier&); 
  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