FOF.hpp

/*
 
Copyright © 2023-26 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 FOF_HPP
#define FOF_HPP
 
#include<iostream>
#include<string>
 
#include "PredicateIndex.hpp"
#include "FunctionIndex.hpp"
#include "Literal.hpp"
#include "Clause.hpp"
#include "TPTPRecords.hpp"
 
using std::string;
using std::cout;
using std::endl;
 
enum class FOFType {Empty, Atom, Neg, And, Or, Imp, Iff, A, E};
 
class FOF {
private:
  static TPTPRecords* recs_p;
  FOFType type;
  Literal pred;
  vector<FOF> sub_formulas;
  Variable* var;
  static VariableIndex* var_index;
  static FunctionIndex* fun_index;
  static TermIndex* term_index;
  static PredicateIndex* pred_index;
  //---------------------------------------------------------------------------
  // Simple methods for Variables.
  //---------------------------------------------------------------------------
  bool has_free_variable(Variable*);
  void replace_variable(Variable*, Variable*);
  //---------------------------------------------------------------------------
  // Skolemization.
  //---------------------------------------------------------------------------
  Term* make_skolem_function(const vector<Term*>&);
  void replace_variable_with_term(Term*, Variable*);
  void skolemize_main(vector<Term*>, FOF*, bool=false);
  void skolemize_universals_main(vector<Term*>, FOF*, bool=false);
  //---------------------------------------------------------------------------
  // Miniscoping.
  //---------------------------------------------------------------------------
  void miniscope_split(Variable*, vector<FOF>&, vector<FOF>&);
  void miniscope_all();
  //---------------------------------------------------------------------------
  // Definitional clause translation.
  //---------------------------------------------------------------------------
  FOF make_definitional_predicate() const;
  //---------------------------------------------------------------------------
  // Distribution of Or/And.
  //---------------------------------------------------------------------------
  bool distribute_or_once();
  bool distribute_and_once();
public:
  //---------------------------------------------------------------------------
  // Constructors.
  //---------------------------------------------------------------------------
  FOF() = delete;
   FOF(FOFType t)
  : type(t), pred(), sub_formulas(), var(nullptr) {}
  FOF(const Literal&);
  FOF(FOFType, const vector<FOF>&, Variable*);
  //---------------------------------------------------------------------------
  // Straightforward methods for getting, setting etc.
  //---------------------------------------------------------------------------
  static void set_indexes(std::tuple<VariableIndex*, 
                          FunctionIndex*, 
                          PredicateIndex*, 
                          TermIndex*> is) {
    var_index = std::get<0>(is);
    fun_index = std::get<1>(is);
    pred_index = std::get<2>(is);
    term_index = std::get<3>(is);
  }
  static void set_recs_p(TPTPRecords* _p) {
    recs_p = _p;
  }
  void show_indexes() const {
    cout << var_index << " " << fun_index 
                      << " " << pred_index 
                      << " " << term_index 
                      << endl;
  }
  FOFType fof_type() { return type; }
  void add_formula(const FOF& f) { sub_formulas.push_back(f); }
  void clear() { 
    type = FOFType::Empty; 
    pred.clear(); 
    sub_formulas.clear();
     var = nullptr; 
  }
  //---------------------------------------------------------------------------
  // Straightforward methods for making FOFs.
  //---------------------------------------------------------------------------
  static FOF make_literal(const Literal& lit) {
    FOF result(lit);
    return result;
  }
  static FOF make_neg(const FOF& f) {
    vector<FOF> fs;
    fs.push_back(f);
    FOF result(FOFType::Neg, fs, nullptr);
    return result;
  }
  static FOF make_and(const vector<FOF>& fs) {
    FOF result(FOFType::And, fs, nullptr);
    return result;
  }
  static FOF make_or(const vector<FOF>& fs) {
    FOF result(FOFType::Or, fs, nullptr);
    return result;
  }
  static FOF make_imp(const FOF& lhs, const FOF& rhs) {
    vector<FOF> fs;
    fs.push_back(lhs);
    fs.push_back(rhs);
    FOF result(FOFType::Imp, fs, nullptr);
    return result;
  }
  static FOF make_iff(const FOF& lhs, const FOF& rhs) {
    vector<FOF> fs;
    fs.push_back(lhs);
    fs.push_back(rhs);
    FOF result(FOFType::Iff, fs, nullptr);
    return result;
  }
  static FOF make_forall(const FOF& f, Variable* v) {
    vector<FOF> fs;
    fs.push_back(f);
    FOF result(FOFType::A, fs, v);
    return result;
  }
  static FOF make_exists(const FOF& f, Variable* v) {
    vector<FOF> fs;
    fs.push_back(f);
    FOF result(FOFType::E, fs, v);
    return result;
  }
  //---------------------------------------------------------------------------
  // Basic tests.
  //---------------------------------------------------------------------------
  bool is_literal() const;
  bool is_clause() const;
  //---------------------------------------------------------------------------
  // Standard simplifications.
  //---------------------------------------------------------------------------
  void remove_negation();
  void negate();
  void simple_negate();
  void invert_literal();
  void remove_iff();
  void remove_imp();
  void make_unique_bound_variables();
  void remove_redundant_quantifiers();
  void push_negs();
  void convert_to_nnf();
  void miniscope();
  void convert_to_cnf_clauses(vector<Clause>&, vector<string>&, const string&);
  void split_sub_formulas(vector<FOF>&, vector<FOF>&);
  void find_definitional_tuple(FOF&, vector<FOF>&, vector<FOF>&, bool);
  void definitional_convert_to_cnf_clauses(vector<Clause>&, vector<string>&, const string&);
  void skolemize();
  void remove_universal_quantifiers();
  void skolemize_universals();
  void remove_existential_quantifiers();
  void to_Literal(Literal&) const;
  void convert_to_clauses(vector<Clause>&) const;
  void dnf_invert_and_convert_to_clauses(vector<Clause>&) const;
  size_t find_and() const;
  size_t find_or() const;
  void distribute_or();
  void distribute_and();
  string to_string() const;
  string to_tptp_string(bool=false) const;
  string predicate_to_tptp_string() const;
  static SimplificationResult simplify_cnf(vector<Clause>&);
  static SimplificationResult simplify_cnf(vector<Clause>&, 
                                           vector<string>&,
                                           vector<string>&);
  set<Term*> find_free_variables() const;
 
  friend ostream& operator<<(ostream&, const FOF&);
};
 
 
#endif