StackItem.cpp

/*
 
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/>. 
 
*/
 
#include "StackItem.hpp"
 
//----------------------------------------------------------------------
ostream& operator<<(ostream& out, const StackItemType& si) {
  switch (si) {
    case StackItemType::Start:
      out << "Start";
      break;
    case StackItemType::Axiom:
      out << "Axiom";
      break;
    case StackItemType::Reduction:
      out << "Reduction";
      break;
    case StackItemType::LeftBranch:
      out << "Left Branch";
      break;
    case StackItemType::RightBranch:
      out << "Right Branch";
      break;
    default:
      break;
  }
  return out;
}
//----------------------------------------------------------------------
void StackItem::stack_item_setup() {
  path_length = p.length();
  reduction_lit = c.get_literal(0);
  reduction_neg_lit = reduction_lit;
  reduction_neg_lit.invert();
  reduction_ind = 0;
  reduction_current_path_index = 0;
  reduction_backtrack_restricted = false;
  reduction_no_more_results = true;
 
  extension_lit = c.get_literal(0);
  extension_neg_lit = extension_lit;
  extension_neg_lit.invert();
  extension_ind = 0;extension_i = 0;
  extension_index_entry_size = 0;
  extension_current_index_entry = 0;
  extension_backtrack_restricted = false;
  extension_no_more_results = true;
}
//----------------------------------------------------------------------
void StackItem::reduction_initialize(Unifier& _u) {
    reduction_no_more_results = false; 
    reduction_move_to_next_result(_u);
}
//----------------------------------------------------------------------
void StackItem::reduction_move_to_next_result(Unifier& _u) {
    // Default constructor makes InferenceItemType::None.
    if (reduction_no_more_results)
        return;
    UnificationOutcome outcome = UnificationOutcome::ConflictFail;
    while (outcome != UnificationOutcome::Succeed && 
           reduction_current_path_index < path_length) {
        const Literal& lit2 = p.examine_literal(path_length - 1 - reduction_current_path_index++);
        if (!reduction_neg_lit.is_compatible_with(&lit2)) {
            continue;
        }
        outcome = _u(reduction_neg_lit, lit2);
        if (outcome == UnificationOutcome::Succeed) {
            reduction_next_result = InferenceItem(InferenceItemType::Reduction, reduction_lit, reduction_ind,
                        0, 0, _u.get_substitution(), path_length - reduction_current_path_index);
            _u.backtrack();
            return;
        }   
        _u.backtrack();
    }
    reduction_no_more_results = true;
}
//----------------------------------------------------------------------
InferenceItem StackItem::next_reduction(Unifier& _u) {
    // Default constructor makes InferenceItemType::None.
    InferenceItem result;
    if (reduction_backtrack_restricted || reduction_no_more_results) 
        return result;
    result = reduction_next_result;
    reduction_move_to_next_result(_u);
    return result;
}
//----------------------------------------------------------------------
void StackItem::all_reductions(vector<InferenceItem>& reductions, 
                                         Unifier& _u) {
    while (!reduction_no_more_results) {
        reductions.push_back(reduction_next_result);
        reduction_move_to_next_result(_u);
    }
}
//----------------------------------------------------------------------
void StackItem::extension_initialize(Matrix& _m, Unifier& _u) {
    extension_no_more_results = false;
    extension_i = extension_neg_lit.get_pred_as_index();  
    extension_index_entry_size = _m.get_index_entry_size(extension_i);
    extension_move_to_next_result(_m, _u);
}
//----------------------------------------------------------------------
void StackItem::extension_move_to_next_result(Matrix& _m, Unifier& _u) {
    if (extension_no_more_results) {
        return;
    }
    UnificationOutcome outcome = UnificationOutcome::ConflictFail;
    while (outcome != UnificationOutcome::Succeed && 
           extension_current_index_entry < extension_index_entry_size) {
        size_t new_index = extension_index_entry_size - 1 - extension_current_index_entry++;
        outcome = _u(extension_neg_lit, _m.inspect_index_literal(extension_i, new_index));
        if (outcome == UnificationOutcome::Succeed) {
            const MatrixPairType p = _m.get_index_entry(extension_i, new_index); 
            extension_next_result = InferenceItem(InferenceItemType::Extension, 
                        extension_lit, extension_ind,
                        p.first, p.second, extension_i, new_index);
            _u.backtrack();
            return;
        }   
        _u.backtrack();
    }
    extension_no_more_results = true;
}
//----------------------------------------------------------------------
InferenceItem StackItem::next_extension(Matrix& _m, Unifier& _u) {
    // Default constructor makes InferenceItemType::None.
    InferenceItem result;
    if (extension_backtrack_restricted || extension_no_more_results) 
        return result;
    result = extension_next_result;
    extension_move_to_next_result(_m, _u);
    return result;
}
//----------------------------------------------------------------------
void StackItem::all_extensions(vector<InferenceItem>& extensions, 
                                         Matrix& _m, Unifier& _u) {
    while (!extension_no_more_results) {
        extensions.push_back(extension_next_result);
        extension_move_to_next_result(_m, _u);
    }
}
//----------------------------------------------------------------------
void StackItem::initialize(Matrix& _m, Unifier& _u) {
  reduction_initialize(_u);
  extension_initialize(_m, _u);
}
//----------------------------------------------------------------------
void StackItem::restrict_backtrack() {
  /*
  * Implement the leanCop style restriction on backtracking.
  */
  actions.clear();
  reduction_restrict_backtrack();
  extension_restrict_backtrack();
}
//----------------------------------------------------------------------
void StackItem::add_all_extensions_to_actions(Matrix& _m, Unifier& _u) {
  all_extensions(actions, _m, _u);
}
//----------------------------------------------------------------------
void StackItem::add_all_reductions_to_actions(Unifier& _u) {
  all_reductions(actions, _u);
}
//----------------------------------------------------------------------
bool StackItem::no_more_inferences() { 
    return actions.empty() && reduction_is_empty() && extension_is_empty();
}
//----------------------------------------------------------------------
 InferenceItem StackItem::get_next_inference(Matrix& _m, Unifier& _u) {
  InferenceItem result;
  if (actions.size() > 0) { 
    result = actions.back();
    actions.pop_back();
    return result;
  }
  if (!reduction_is_empty()) {
    return next_reduction(_u);
  }
  if (!extension_is_empty()) {
    return next_extension(_m, _u);
  }
  return result;
}
//----------------------------------------------------------------------
string StackItem::to_string_unsubbed() const {
  string result;
  result += "Stack item: ";
  switch (item_type) {
    case StackItemType::Start:
      result += "Start";
      break;
    case StackItemType::Axiom:
      result += "Axiom";
      break;
    case StackItemType::Reduction:
      result += "Reduction";
      break;
    case StackItemType::LeftBranch:
      result += "Left Branch";
      break;
    case StackItemType::RightBranch:
      result += "Right Branch";
      break;
    default:
      break;
  }
  result += " with ";
  result  += to_string(actions.size()) += " options\n";
  result += "C = ";
  result += c.to_string() += "\n";
  result += "P = ";
  result += p.to_string() += "\n";
  result += "L = ";
  result += l.to_string() += "\n";
  result += "Sub = ";
  result += sub.to_string() += "\n";
  result += "Depth: ";
  result += std::to_string(depth);
  return result;
}
//----------------------------------------------------------------------
ostream& operator<<(ostream& out, const StackItem& si) {
  out << si.to_string_unsubbed() << endl;
  for (const InferenceItem& i : si.actions) {
    out << i << endl;
  }
  return out;
}