TPTPParser.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 TPTPPARSER_HPP
#define TPTPPARSER_HPP
 
#include <iostream>
#include <fstream>
 
#include <boost/spirit/include/qi.hpp>
 
#include "Exceptions.hpp"
#include "PredicateIndex.hpp"
#include "FunctionIndex.hpp"
#include "Matrix.hpp"
#include "FOF.hpp"
#include "vic_strings.hpp"
 
using std::string;
using std::vector;
using std::set;
using std::ifstream;
using std::cout;
namespace fs = std::filesystem;
 
using namespace boost::spirit;
 
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
namespace tptp_parser {
  using Iter = string::const_iterator;
  struct fof_plain_term_struct;
  using fof_arguments_struct =
    boost::variant<
      string,
      boost::recursive_wrapper<fof_plain_term_struct>
    >;
  struct fof_plain_term_struct {
    string functor;
    std::vector<fof_arguments_struct> args;
  };
  struct infix_struct {
    fof_arguments_struct left;
    string connective;
    fof_arguments_struct right;
  };
  using fof_atomic_formula_type = boost::variant<
    fof_plain_term_struct,
    infix_struct
  >;
  struct cnf_annotated_struct {
    string name;
    string role;
    std::vector<fof_atomic_formula_type> f;
  };
} // tptp_parser namespace ends.
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
BOOST_FUSION_ADAPT_STRUCT(
    tptp_parser::fof_plain_term_struct,
    (string, functor)
    (std::vector<tptp_parser::fof_arguments_struct>, args)
)
BOOST_FUSION_ADAPT_STRUCT(
    tptp_parser::infix_struct,
    (tptp_parser::fof_arguments_struct, left)
    (string, connective)
    (tptp_parser::fof_arguments_struct, right)
)
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
// Back to the tptp_parser namespace.
//---------------------------------------------------------------------
namespace tptp_parser {
  struct fof_unitary_formula_struct;
  struct fof_negation_struct;
  struct fof_quantifier_struct;
  struct fof_binary_struct;
  struct fof_andor_struct;
  using fof_formula_type = boost::variant<
    fof_plain_term_struct,
    infix_struct,
    boost::recursive_wrapper<fof_unitary_formula_struct>,
    boost::recursive_wrapper<fof_negation_struct>,
    boost::recursive_wrapper<fof_quantifier_struct>,
    boost::recursive_wrapper<fof_binary_struct>,
    boost::recursive_wrapper<fof_andor_struct>
  >;
  struct fof_unitary_formula_struct {
    fof_formula_type arg;
  };
  struct fof_negation_struct {
    string type;
    fof_formula_type arg;
  };
  struct fof_quantifier_struct {
    string type;
    std::vector<string> vars;
    fof_formula_type arg;
  };
  struct fof_binary_struct {
    fof_formula_type lhs;
    string type;
    fof_formula_type rhs;
  };
  struct fof_andor_struct {
    fof_formula_type lhs;
    string type;
    vector<fof_formula_type> rhs;
  };
} // tptp_parser namespace ends.
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
BOOST_FUSION_ADAPT_STRUCT(
  tptp_parser::fof_unitary_formula_struct,
  (tptp_parser::fof_formula_type, arg)
)
BOOST_FUSION_ADAPT_STRUCT(
  tptp_parser::fof_negation_struct,
  (string, type)
  (tptp_parser::fof_formula_type, arg)
)
BOOST_FUSION_ADAPT_STRUCT(
  tptp_parser::fof_quantifier_struct,
  (string, type)
  (std::vector<string>, vars)
  (tptp_parser::fof_formula_type, arg)
)
BOOST_FUSION_ADAPT_STRUCT(
  tptp_parser::fof_binary_struct,
  (tptp_parser::fof_formula_type, lhs)
  (string, type)
  (tptp_parser::fof_formula_type, rhs)
)
BOOST_FUSION_ADAPT_STRUCT(
  tptp_parser::fof_andor_struct,
  (tptp_parser::fof_formula_type, lhs)
  (string, type)
  (std::vector<tptp_parser::fof_formula_type>, rhs)
)
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
// Back to the tptp_parser namespace.
//---------------------------------------------------------------------
namespace tptp_parser {
  struct show_fof_plain_term {
    void operator()(const fof_plain_term_struct&);
  };
  struct show_fof_arguments : boost::static_visitor<> {
    void operator()(const string& s) {
      cout << s;
    }
    void operator()(const fof_plain_term_struct& t) {
      show_fof_plain_term spt;
      spt(t);
    }
  };
  struct show_fof_atomic_formula : boost::static_visitor<> {
    void operator()(const fof_plain_term_struct& s) {
      show_fof_plain_term st;
      st(s);
    }
    void operator()(const infix_struct& s) {
      show_fof_arguments sa;
      boost::apply_visitor(sa, s.left);
      cout << " " << s.connective << " ";
      boost::apply_visitor(sa, s.right);
    }
  };
  struct show_clause {
    void operator()(const vector<fof_atomic_formula_type>& v) const {
      show_fof_atomic_formula st;
      cout << "Clause = {" << endl;
      for (fof_atomic_formula_type f : v) {
          cout << "    ";
          boost::apply_visitor(st, f);
          cout << endl;
      }
      cout << '}' << endl;
    }
  };
  struct show_fof_formula_type : boost::static_visitor<> {
    void operator()(const fof_plain_term_struct& t) {
      show_fof_atomic_formula saf;
      saf(t);
    }
    void operator()(const infix_struct& s) {
      show_fof_atomic_formula saf;
      saf(s);
    }
    void operator()(const fof_unitary_formula_struct& f) {
      show_fof_formula_type sf;
      boost::apply_visitor(sf, f.arg);
    }
    void operator()(const fof_negation_struct& f) {
      cout << f.type << "(";
      show_fof_formula_type sf;
      boost::apply_visitor(sf, f.arg);
      cout << ")";
    }
    void operator()(const fof_quantifier_struct& f) {
      cout << f.type << " [";
      for (const string& s : f.vars)
        cout << s << " ";
      cout << "] (";
      show_fof_formula_type sf;
      boost::apply_visitor(sf, f.arg);
      cout << ")";
    }
    void operator()(const fof_binary_struct& f) {
      show_fof_formula_type sf;
      boost::apply_visitor(sf, f.lhs);
      cout << " " << f.type << " ";
      boost::apply_visitor(sf, f.rhs);
    }
    void operator()(const fof_andor_struct& f) {
      show_fof_formula_type sf;
      boost::apply_visitor(sf, f.lhs);
      for (const fof_formula_type& g : f.rhs) {
        cout << " " << f.type << " ";
        boost::apply_visitor(sf, g);
      }
    }
  };
  struct show_fof_formula {
    void operator()(const fof_formula_type& f) const {
    show_fof_formula_type sf;
    boost::apply_visitor(sf, f);
    cout << endl;
  }
};
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
struct FileIncludeAdder {
  void operator()(const vector<string>&, qi::unused_type, qi::unused_type) const;
};
struct CommentStatus {
  void operator()(const string&, qi::unused_type, qi::unused_type) const;
};
struct DefinedAdder {
  void operator()(const string&, qi::unused_type, qi::unused_type) const;
};
struct SystemAdder {
  void operator()(const string&, qi::unused_type, qi::unused_type) const;
};
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
struct to_lit {
  void operator()(const fof_atomic_formula_type&,  qi::unused_type,qi::unused_type) const;
};
struct show_lit {
  void operator()(const fof_atomic_formula_type&,  qi::unused_type,  qi::unused_type) const;
};
struct set_neg_lit {
  void operator()(qi::unused_type,  qi::unused_type,  qi::unused_type) const;
};
struct unset_neg_lit {
  void operator()(qi::unused_type,  qi::unused_type,  qi::unused_type) const;
};
struct clear_current_clause {
  void operator()(qi::unused_type,  qi::unused_type,  qi::unused_type) const;
};
struct add_current_clause {
  void operator()(qi::unused_type,  qi::unused_type,  qi::unused_type) const;
};
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
struct convert_fof_atomic_formula : boost::static_visitor<Literal> {
  Literal operator()(const fof_plain_term_struct&) const;
  Literal operator()(const infix_struct&) const;
};
struct convert_fof_arguments_struct : boost::static_visitor<Term*> {
  Term* operator()(const string&) const;
  Term* operator()(const fof_plain_term_struct&) const;
};
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
struct print_cnf_formula_name {
  void operator()(const string&,
    qi::unused_type,
    qi::unused_type) const;
};
struct print_cnf_formula_role {
  void operator()(const string&,
    qi::unused_type,
    qi::unused_type) const;
};
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
struct print_fof_formula_name {
  void operator()(const string&,
    qi::unused_type,
    qi::unused_type) const;
};
struct print_fof_formula_role {
  void operator()(const string&,
    qi::unused_type,
    qi::unused_type) const;
};
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
struct convert_fof_formula : boost::static_visitor<FOF> {
  FOF operator()(const fof_plain_term_struct&) const;
  FOF operator()(const infix_struct&) const;
  FOF operator()(const fof_unitary_formula_struct&) const;
  FOF operator()(const fof_negation_struct&) const;
  FOF operator()(const fof_quantifier_struct&) const;
  FOF operator()(const fof_binary_struct&) const;
  FOF operator()(const fof_andor_struct&) const;
};
struct make_fof_formula {
  void operator()(const fof_formula_type&, qi::unused_type,  qi::unused_type) const;
};
struct add_fof_formula {
  void operator()(qi::unused_type,  qi::unused_type,  qi::unused_type) const;
};
//---------------------------------------------------------------------
void read_tptp_from_file_simple(const string&, string&);
//---------------------------------------------------------------------
using FileIncludeItem = pair<string, vector<string>>;
 
void recursive_tptp_include(const FileIncludeItem&);
//---------------------------------------------------------------------
//---------------------------------------------------------------------
//---------------------------------------------------------------------
class TPTPParser {
private:
    string file_contents;
    vector<string> comment_blocks;
    VariableIndex* vip;
    FunctionIndex* fip;
    TermIndex* tip;
    PredicateIndex* pip;
    Matrix* matrix;
    void read_tptp_from_file(const string&);
public:
    TPTPParser() = delete;
    TPTPParser(VariableIndex*,
      FunctionIndex*,
      TermIndex*,
      PredicateIndex*,
      Matrix*);
    bool parse_tptp_from_file(const string&);
    void show_file_includes();
    void clear();
    vector<string> get_defined_items();
    vector<string> get_system_items();
    bool equality_used();
    bool conjecture_present() const;
    size_t number_of_fof_formulas() const;
    string get_problem_status();
    Predicate* get_equals_predicate() const;
};
 
};
 
#endif