Lemmata.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/>. 
 
*/
 
#ifndef LEMMATA_HPP
#define LEMMATA_HPP
 
#include <iostream>
#include <vector>
 
#include "Clause.hpp"
#include "InferenceItem.hpp"
 
using std::vector;
using std::ostream;
using std::endl;
using std::cout;
 
class Lemmata {
private:
  vector<Literal> ls;
  size_t len;
public:
  Lemmata() : ls(), len(0) {}
  inline size_t size() { return len; }
  void push_back(const Literal&);
  void clear() { ls.clear(); len = 0; }
  inline Literal& examine_literal(size_t i) { return ls[i]; }
  void find_all_lemmata(vector<InferenceItem>&, Clause&);
  void find_initial_lemmata(vector<InferenceItem>&, Clause&);
  string to_string(bool = false) const;
  string make_LaTeX(bool = false) const;
 
  friend ostream& operator<<(ostream&, const Lemmata&);
};
 
#endif