InferenceItem.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 INFERENCEITEM_HPP
#define INFERENCEITEM_HPP
 
#include <iostream>
 
#include "Literal.hpp"
#include "Substitution.hpp"
 
using std::ostream;
using std::endl;
 
enum class InferenceItemType { 
          None, 
          Start, 
          Reduction, 
          Extension, 
          Axiom, 
          Lemma 
};
 
ostream& operator<<(ostream&, const InferenceItemType&);
 
struct InferenceItem {
  InferenceItemType T;
  Literal L;
  LitNum Lindex;
  ClauseNum C_2;
  LitNum Lprime;
  Substitution sigma;
  size_t index_in_path;
  size_t index_in_lemmata;
 
  InferenceItem();
  InferenceItem(InferenceItemType);
  InferenceItem(InferenceItemType, ClauseNum);
  InferenceItem(InferenceItemType, const Literal&, LitNum);
  InferenceItem(InferenceItemType, const Literal&, LitNum, size_t);
  InferenceItem(InferenceItemType, const Literal&, LitNum, 
      ClauseNum, LitNum, const Substitution&);
  InferenceItem(InferenceItemType, const Literal&, LitNum, 
      ClauseNum, LitNum, const Substitution&, size_t);
};
 
ostream& operator<<(ostream&, const InferenceItem&);
 
#endif