SimplePath.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 SIMPLEPATH_HPP
#define SIMPLEPATH_HPP
 
#include<iostream>
#include<vector>
 
#include "InferenceItem.hpp"
#include "Unifier.hpp"
#include "Clause.hpp"
 
using std::vector;
using std::ostream;
using std::endl;
using std::cout;
 
class SimplePath {
private:
    vector<Literal> path;
    uint32_t num_preds;
    uint32_t len;
    void find_reductions(Unifier&, vector<InferenceItem>&, const Literal&,
                         LitNum);
public:
    SimplePath() : path(), num_preds(0), len(0) {}
    SimplePath(uint32_t);
    inline uint32_t length() const { return len; }
    void clear();
    inline void set_num_preds(size_t num_predicates) { num_preds = num_predicates; }
    void push(const Literal&);
    Literal back() const;
    void pop();
    bool test_for_regularity(Clause&) const;
    void find_limited_reductions(Unifier&, vector<InferenceItem>&,
                         Clause&);
    void find_all_reductions(Unifier&, vector<InferenceItem>&,
                         Clause&);
    void show_path_only(ostream&);
    string to_string(bool = false) const;
    string make_LaTeX(bool = false) const;
    vector<Literal>::const_iterator cbegin() const { return path.cbegin(); }
    vector<Literal>::const_iterator cend() const { return path.cend(); }
    vector<Literal>::iterator begin() { return path.begin(); }
    vector<Literal>::iterator end() { return path.end(); }
 
    friend ostream& operator<<(ostream&, const SimplePath&);
};
 
#endif