Unifier.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 UNIFIER_HPP
#define UNIFIER_HPP
 
#include<iostream>
#include<string>
#include<deque>
 
#include "Substitution.hpp"
#include "Literal.hpp"
 
using std::deque;
using std::pair;
using std::ostream;
using std::endl;
using std::string;
 
using UPair = pair<Term* ,Term*>;
enum class UnificationOutcome {Succeed, ConflictFail, OccursFail};
ostream& operator<<(ostream&, const UnificationOutcome&);
class Unifier {
private:
    Substitution s;
    vector<UPair> to_do;
    UnificationOutcome complete_unification();
public:
    Unifier() : s(), to_do() {}
    Unifier(const Unifier&) = delete;
    Unifier(const Unifier&&) = delete;
    Unifier& operator=(const Unifier&) = delete;
    Unifier& operator=(const Unifier&&) = delete;
    Substitution get_substitution() const { return s; }
    UnificationOutcome operator()(Term*, Term*);
    UnificationOutcome unify(Term*, Term*);
    UnificationOutcome unify_terms(Term*, Term*);
    UnificationOutcome operator()(const vector<Term*>&,
                                  const vector<Term*>&);
    UnificationOutcome operator()(Literal*, Literal*);
    inline UnificationOutcome operator()(const Literal& l1, const Literal& l2) {
        if (params::poly_unification) {
            to_do.clear();
            size_t s = l1.get_arity();
            for (size_t i = 0; i < s; i++) {
                to_do.push_back(UPair(l1[i], l2[i]));
            }
            return complete_unification();
        }
        else {
            auto i = l1.get_args().begin();
            for (Term* term1 : l2.get_args()) {
                UnificationOutcome outcome = unify_terms(term1, *i);
                if (outcome != UnificationOutcome::Succeed) {
                    backtrack();
                    return outcome;
                }
                i++;
            }   
            return UnificationOutcome::Succeed;
        }
    }
    void backtrack();
    string to_string(bool subbed = false) const {
        return s.to_string(subbed);
    }
 
    friend ostream& operator<<(ostream&, const Unifier&);
};
 
#endif