Clause.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 CLAUSE_HPP
#define CLAUSE_HPP
 
#include<iostream>
#include<string>
#include<vector>
#include<random>
#include<algorithm>
 
#include "Literal.hpp"
 
using std::vector;
using std::string;
using std::ostream;
using std::endl;
 
enum class SimplificationResult {OK, Tautology, Contradiction};
 
class Clause {
private:
    vector<Literal> c;
    static std::mt19937 d;
public:
    Clause() : c() {}
    Clause(const vector<Literal>& new_lits) : c(new_lits) {
    #ifdef DEBUGMESSAGES
        if (new_lits.size() == 0)
            cerr << "Why are you constructing an empty clause?" << endl;
    #endif
    }
    inline size_t size() const { return c.size(); }
    inline bool empty() const { return c.empty(); }
    inline void clear() { c.clear(); }
    bool is_positive() const;
    bool is_negative() const;
    void remove_duplicates();
    bool has_complementary_literals() const;
    void add_lit(const Literal&);
    void drop_literal(LitNum);
    Literal extract_literal(LitNum);
    Literal& operator[](size_t);
    Clause make_copy_with_new_vars(VariableIndex&, TermIndex&) const;
    SimplificationResult simplify(); 
    void random_reorder();
    string to_string(bool = false) const;
    string to_prolog_string() const;
    string to_tptp_string() const;
    string make_LaTeX(bool = false) const;
 
    vector<Literal>::const_iterator cbegin() const { return c.cbegin(); }
    vector<Literal>::const_iterator cend() const { return c.cend(); }
    vector<Literal>::iterator begin() { return c.begin(); }
    vector<Literal>::iterator end() { return c.end(); }
 
    friend ostream& operator<<(ostream&, const Clause&);
};
 
#endif