Term.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 TERM_HPP
#define TERM_HPP
 
#include<iostream>
#include<sstream>
#include<string>
#include<vector>
#include<set>
#include<unordered_map>
 
#include "VariableIndex.hpp"
 
using std::vector;
using std::pair;
using std::unordered_map;
using std::ostream;
using std::ostringstream;
using std::to_string;
using std::set;
 
using VarMapType = pair<Variable*,Term*>;
 
class TermIndex;
 
class Term {
private:
    Variable* v;
    Function* f;
    vector<Term*> args;
    Term() : v(nullptr), f(nullptr), args() {}
    Term(Variable* new_v) : v(new_v), f(nullptr), args() {}
    Term(Function*, const vector<Term*>&);
public:
    inline Variable* get_v() const { return v; }
    inline Function* get_f() const { return f; }
    inline bool is_variable() const { return v != nullptr; }
    inline bool is_function() const { return f != nullptr; }
    inline Arity arity() const { return args.size(); }
    Term* operator[](size_t) const;
    bool is_ground() const;
    string to_string(bool = false, bool = false) const;
    string to_prolog_string() const;
    string make_LaTeX(bool = false) const;
    bool operator==(const Term&) const;
    bool is_subbed() const;
    bool subbed_equal(Term*) const;
    bool is_unsubbed_variable() const;
    //----------------------------------------------------------------------
    // The next block of methods are exactly analogous to those in
    // Variable.
    //----------------------------------------------------------------------
    bool subbed_is_function() const;
    bool subbed_is_variable() const;
    bool contains_variable(Variable*) const;
    Variable* subbed_variable() const;
    Function* get_subbed_f() const;
    Arity get_subbed_arity() const;
    Term* skip_leading_variables() const;
    Term* skip_leading_variables_for_unification(bool&, Variable*&, Function*&, size_t&) const;
    void find_subbed_vars(set<Variable*>&) const;
    Term* make_copy_with_new_vars(VariableIndex&, TermIndex&) const;
    Term* make_copy_with_new_vars_helper(VariableIndex&,
                                         TermIndex&,
                                         unordered_map<Variable*,Term*>&) const;
    set<Term*> all_variables() const;
 
    friend class TermIndex;
    friend ostream& operator<<(ostream&, const Term&);
};
 
#endif