Literal.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 LITERAL_HPP
#define LITERAL_HPP
 
#include<iostream>
#include<iomanip>
#include<string>
#include<vector>
#include<set>
#include<unordered_map>
 
#include "TermIndex.hpp"
#include "Predicate.hpp"
 
using std::vector;
using std::string;
using std::set;
using std::unordered_map;
using std::ostream;
using std::endl;
 
class Literal {
private:
    Predicate* pred;
    vector<Term*> args;
    Arity arity;
    bool polarity;
public:
    Literal() : pred(nullptr), args(), arity(0), polarity(true) {}
    Literal(Predicate*, const vector<Term*>&, Arity, bool);
    inline Predicate* get_pred() const { return pred; }
    inline Arity get_arity() const { return arity; }
    inline bool get_polarity() const { return polarity; }
    inline const vector<Term*>& get_args() const { return args; }
    inline Term* operator[](size_t i) const { return args[i]; }
    inline bool is_positive() const { return polarity; }
    inline bool is_negative() const { return !polarity; }
    inline void make_positive() { polarity = true; }
    inline void make_negative() { polarity = false; }
    inline void invert() { polarity = !polarity; }
    inline void make_empty() { pred = nullptr; }
    inline bool is_empty() const { return (pred == nullptr); }
    void clear() { pred = nullptr; args.clear(), arity = 0; polarity = true; } 
    inline size_t get_pred_as_index() const {
        size_t index = pred->get_ID() << 1;
        if (!polarity)
            index |= 0x00000001;
        return index;
    };
    bool is_ground() const;
    bool is_true() const;
    bool is_false() const;
    bool contains_variable(Variable*) const;
    bool is_compatible_with(const Literal*) const;
    bool is_complement_of(const Literal&) const;
    string get_small_lit() const;
    string to_string(bool = false) const;
    string to_prolog_string() const;
    string to_tptp_string() const;
    string make_LaTeX(bool = false) const;
    bool operator==(const Literal&) const;
    bool subbed_equal(Literal*) const;
    Literal make_copy_with_new_vars(VariableIndex&, TermIndex&) const;
    Literal make_copy_with_new_vars_helper(VariableIndex&,
                                           TermIndex&,
                                           unordered_map<Variable*,Term*>&) const;
    void make_copy_with_new_vars_replace_helper(VariableIndex&,
                                           TermIndex&,
                                           unordered_map<Variable*,Term*>&);
    void replace_variable(Variable*, Variable*, TermIndex*);
    void replace_variable_with_term(Term*, Variable*, TermIndex*);
 
    friend ostream& operator<<(ostream&, const Literal&);
};
 
#endif