ProofPrinter Class Reference

Class for rendering a proof in various formats. More...

#include <ProofPrinter.hpp>

Collaboration diagram for ProofPrinter:

Public Member Functions
	ProofPrinter ()
	Basic constructor.
	ProofPrinter (Stack *_p)
	The constructor you want.
void	set_proof (Stack *_p)
	Basic set method.
void	clear ()
	Basic set method.
void	make_LaTeX (const path &, const path &, const string &)
	Convert to LaTeX and store in the specified file.
void	make_LaTeX_connection_tableau (const path &, const path &, const string &)
	Convert to LaTeX in the connection tableau calculus and store in the specified file.
void	make_Prolog (const path &)
	Convert to a form suitable for use by the Prolog proof checker and write to a file.
void	show_Prolog ()
	Show the proof in Prolog format.
void	show_tptp ()
	Show the proof in a TPTP-friendly format.
vector< pair< string, vector< size_t > > >	make_internal () const
	Make a simple data structure representing the proof stack.

Private Member Functions
string	make_LaTeX_state (StackItem *) const
	Helper for producing LaTeX output.
string	make_LaTeX_subtree (StackItem *) const
	Helper for producing LaTeX output.

Private Attributes
Stack *	p
	Pointer to the output of StackProver.

Detailed Description

Class for rendering a proof in various formats.

A proof is supplied as a stack of StackItem produced by StackProver.

At present, this class will render a proof as LaTeX, or in a Prolog-readable certificate format that can be passed through the Connect++ certificate checker.

It will be extended later if a standard format for connection calculus proof certificates is agreed – this discussion is ongoing.

Definition at line 61 of file ProofPrinter.hpp.

Constructor & Destructor Documentation

ProofPrinter() [1/2]

ProofPrinter::ProofPrinter ( )

inline

Basic constructor.

Definition at line 92 of file ProofPrinter.hpp.

: p(nullptr) {};

ProofPrinter() [2/2]

ProofPrinter::ProofPrinter ( Stack * _p )

inline

The constructor you want.

Parameters

_p	Pointer to the output of StackProver.

Definition at line 98 of file ProofPrinter.hpp.

: p(_p) {};

Member Function Documentation

clear()

void ProofPrinter::clear ( )

inline

Basic set method.

Definition at line 108 of file ProofPrinter.hpp.

{ p = nullptr; }

make_internal()

vector< pair< string, vector< size_t > > > ProofPrinter::make_internal

(

)

const

Make a simple data structure representing the proof stack.

The first part each element of the output is a string naming the proof rules. The second contains the associated numbers.

Definition at line 402 of file ProofPrinter.cpp.

                                                                         {
  vector<pair<string, vector<size_t>>> out;
 
  size_t s = p->size() - 1;
  size_t i = 0;
  pair<string, vector<size_t>> next_out;
  for (size_t si_index = 0; si_index < p->size(); si_index++) {
    StackItem si((*p)[si_index]);
    next_out.second.clear();
    switch (si.item_type) {
      case StackItemType::Start:
        next_out.first = "start";
        next_out.second.push_back(si.this_action.C_2);
        out.push_back(next_out);
        break;
      case StackItemType::Axiom:
        next_out.first = "axiom";
        out.push_back(next_out);
        break;
      case StackItemType::Reduction:
        next_out.first = "reduction";
        next_out.second.push_back(si.this_action.Lindex);
        next_out.second.push_back(si.this_action.index_in_path);
        out.push_back(next_out);
        break;
      case StackItemType::LeftBranch:
        next_out.first = "left_branch";
        next_out.second.push_back(si.this_action.Lindex);
        next_out.second.push_back(si.this_action.C_2);
        next_out.second.push_back(si.this_action.Lprime);
        next_out.second.push_back(si.depth);
        out.push_back(next_out);
        break;
      case StackItemType::RightBranch:
        next_out.first = "right_branch";
        next_out.second.push_back(si.depth);
        out.push_back(next_out);
        break;
      case StackItemType::Lemmata:
        next_out.first = "lemmata";
        next_out.second.push_back(si.this_action.Lindex);
        next_out.second.push_back(si.this_action.index_in_lemmata);
        out.push_back(next_out);
        break;
      default:
        cerr << "Something is really wrong..." << endl;
        break;
    }
  }
  return out;
}

make_LaTeX()

void ProofPrinter::make_LaTeX	(	const path &	path_to_file,
		const path &	path_to_input_file,
		const string &	matrix_as_latex )

Convert to LaTeX and store in the specified file.

Parameters

path_to_file	Path of file to store to
path_to_input_file	File for the problem being solved
matrix_as_latex	LaTeX formatted matrix

Definition at line 118 of file ProofPrinter.cpp.

                                                      {
  std::ofstream file(path_to_file);
 
  file << "\\documentclass[10pt]{article}" << '\n';
  file << "\\usepackage{libertine}" << '\n';
  file << "\\usepackage{amsmath,amsfonts,amssymb}" << '\n';
  file << "\\usepackage{prftree}" << '\n';
  file << "\\usepackage{color}" << '\n';
  file << "\\usepackage[paperwidth = 5000mm, paperheight = 5000mm,landscape]{geometry}" << '\n' << '\n';
  file << "\\begin{document}" << '\n';
 
  // Add details of the problem.
  file << "\\noindent\\begin{LARGE}\\textsc{Connect++}\\end{LARGE} \\\\" << endl << endl;
  file << "\\noindent Attempting to prove problem from file: ";
  file << "$\\mathtt{";
  file << latex_escape_characters(path_to_input_file.filename());
  file << "}$ \\\\" << endl << endl;
  if (params::latex_include_matrix) {
    file << "\\noindent Problem has matrix: " << endl << endl;
    file << matrix_as_latex << endl;
  }
  file << "\\noindent\\textsc{Proof}: \\\\" << endl << endl;
 
  if (params::latex_tiny_proof)
    file << "\\begin{tiny}" << endl;
 
  file << "\\[";
 
  /*
  *  Build a LaTeX representation of the Proof.
  */
  if (p != nullptr) {
    /*
    * Start move.
    */
    file << "\\prftree[r]{Start}{";
    file << make_LaTeX_subtree(&((*p)[0]));
    file << "}{\\epsilon, \\textcolor{magenta}{M}, \\epsilon, \\epsilon}\n";
  }
 
  file << "\\]";
 
  if (params::latex_tiny_proof)
    file << "\\end{tiny}" << endl;
 
  file << '\n' << '\n' << "\\end{document}" << '\n';
 
  file.close();
}

make_LaTeX_connection_tableau()

void ProofPrinter::make_LaTeX_connection_tableau	(	const path &	path_to_file,
		const path &	path_to_input_file,
		const string &	matrix_as_latex )

Convert to LaTeX in the connection tableau calculus and store in the specified file.

Parameters

path_to_file	Path of file to store to
path_to_input_file	File for the problem being solved
matrix_as_latex	LaTeX formatted matrix

Definition at line 170 of file ProofPrinter.cpp.

                                                      {
  std::ofstream file(path_to_file);
 
  file << "\\documentclass[10pt]{article}" << '\n';
  file << "\\usepackage{libertine}" << '\n';
  file << "\\usepackage{amsmath,amsfonts,amssymb}" << '\n';
  file << "\\usepackage{forest}" << '\n';
  file << "\\usepackage{color}" << '\n';
  file << "\\usepackage[paperwidth = 5000mm, paperheight = 5000mm,landscape]{geometry}" << '\n' << '\n';
  file << "\\begin{document}" << '\n';
 
  // Add details of the problem.
  file << "\\noindent\\begin{LARGE}\\textsc{Connect++}\\end{LARGE} \\\\" << endl << endl;
  file << "\\noindent Attempting to prove problem from file: ";
  file << "$\\mathtt{";
  file << latex_escape_characters(path_to_input_file.filename());
  file << "}$ \\\\" << endl << endl;
  if (params::latex_include_matrix) {
    file << "\\noindent Problem has matrix: " << endl << endl;
    file << matrix_as_latex << endl;
  }
  file << "\\noindent\\textsc{Proof}: \\\\" << endl << endl;
 
  if (params::latex_tiny_proof)
    file << "\\begin{tiny}" << endl;
 
  /*
  *  Build a LaTeX representation of the Proof.
  */
  if (p != nullptr) {
    /*
    * Start move.
    */
    file << "\\begin{forest}[Start";
    file << '\n';
    Clause start_clause((*p)[0].c);
    for (const Literal& lit : start_clause) {
      file << "[{$";
      file << lit.make_LaTeX(params::sub_LaTeX_proof);
      file << "$}]";
      file << '\n';
    }
    file << "]\\end{forest}";
    //file << "\\prftree[r]{Start}{";
    //file << make_LaTeX_subtree(&((*p)[0]));
    //file << "}{\\epsilon, \\textcolor{magenta}{M}, \\epsilon, \\epsilon}\n";
  }
 
  if (params::latex_tiny_proof)
    file << "\\end{tiny}" << endl;
 
  file << '\n' << '\n' << "\\end{document}" << '\n';
 
  file.close();
}

make_LaTeX_state()

string ProofPrinter::make_LaTeX_state ( StackItem * item_p ) const

private

Helper for producing LaTeX output.

Make a string with the LaTeX reprresentation of the clause, path and lemmata list.

Parameters

item_p

Pointer to StackItem to render

Definition at line 40 of file ProofPrinter.cpp.

                                                             {
  string s("{\\begin{aligned}");
  s += "C &= ";
  s += (item_p->c).make_LaTeX(params::sub_LaTeX_proof);
  s += "\\\\ P &= ";
  s += (item_p->p).make_LaTeX(params::sub_LaTeX_proof);
  s += "\\\\ L &= ";
  s += (item_p->l).make_LaTeX(params::sub_LaTeX_proof);
  s += "\\end{aligned}}";
  return s;
}

make_LaTeX_subtree()

string ProofPrinter::make_LaTeX_subtree ( StackItem * item_p ) const

private

Helper for producing LaTeX output.

A bit tricky. This should produce \prf???{axioms1}{axioms2} with the {conclusion} being added by the caller. The exception is right branches, which can include the conclusion themselves.

Parameters

item_p

Pointer to StackItem to render

Definition at line 52 of file ProofPrinter.cpp.

                                                               {
  string s;
  string axiom_s("\\prfbyaxiom{Axiom}");
  StackItem* next_p = item_p + 1;
  StackItem* right_item_p;
  switch (item_p->item_type) {
    case StackItemType::Start:
      s += make_LaTeX_subtree(next_p);
      s += make_LaTeX_state(item_p);
      break;
    case StackItemType::Lemmata:
      s += "\\prftree[r]{Lem}{";
      if ((item_p->c).size() == 0)
        s += axiom_s;
      else
        s += make_LaTeX_subtree(next_p);
      s += make_LaTeX_state(item_p);
      s += "}";
      break;
    case StackItemType::Reduction:
      s += "\\prftree[r,l]{Red}{$";
      s += (item_p->sub).make_LaTeX(params::sub_LaTeX_proof);
      s += "$}{";
      if ((item_p->c).size() == 0)
        s += axiom_s;
      else
        s += make_LaTeX_subtree(next_p);
      s += make_LaTeX_state(item_p);
      s += "}";
      break;
    case StackItemType::LeftBranch:
      s += "\\prftree[r,l]{Ext[";
      s += std::to_string(item_p->this_action.C_2);
      s += "]}{$";
      s += (item_p->sub).make_LaTeX(params::sub_LaTeX_proof);
      s += "$}{";
      if ((item_p->c).size() == 0)
        s += axiom_s;
      else
        s += make_LaTeX_subtree(next_p);
      s += make_LaTeX_state(item_p);
      s += "}{";
      /*
      * You need to find the right subtree, which is the only thing at
      * the same depth as you currently are.
      */
      right_item_p = item_p + 1;
      while (right_item_p->depth != item_p->depth)
        right_item_p++;
      s += make_LaTeX_subtree(right_item_p);
      s += "}";
      break;
    case StackItemType::RightBranch:
      if ((item_p->c).size() == 0)
        s += axiom_s;
      else
        s += make_LaTeX_subtree(next_p);
      s += make_LaTeX_state(item_p);
      break;
    default:
      cerr << "Something is really wrong..." << endl;
      break;
  }
  return s;
}

make_Prolog()

void ProofPrinter::make_Prolog

(

const path &

path_to_file

)

Convert to a form suitable for use by the Prolog proof checker and write to a file.

Parameters

path_to_file

Path for output file

Definition at line 228 of file ProofPrinter.cpp.

                                                       {
  std::ofstream file(path_to_file);
  file << "proof_stack([" << std::endl;
  size_t s = p->size() - 1;
  size_t i = 0;
  for (size_t si_index = 0; si_index < p->size(); si_index++) {
    StackItem si((*p)[si_index]);
    switch (si.item_type) {
      case StackItemType::Start:
        file << "start(";
        file << std::to_string(si.this_action.C_2);
        file << ")";
        break;
      case StackItemType::Axiom:
        file << "axiom()";
        break;
      case StackItemType::Reduction:
        file << "reduction(";
        file << std::to_string(si.this_action.Lindex);
        file << ", ";
        file << std::to_string(si.this_action.index_in_path);
        file << ")";
        break;
      case StackItemType::LeftBranch:
        file << "left_branch(";
        file << std::to_string(si.this_action.Lindex);
        file << ", ";
        file << std::to_string(si.this_action.C_2);
        file << ", ";
        file << std::to_string(si.this_action.Lprime);
        file << ", ";
        file << std::to_string(si.depth);
        file << ")";
        break;
      case StackItemType::RightBranch:
        file << "right_branch(";
        file << std::to_string(si.depth);
        file << ")";
        break;
      case StackItemType::Lemmata:
        file << "lemmata(";
        file << std::to_string(si.this_action.Lindex);
        file << ", ";
        file << std::to_string(si.this_action.index_in_lemmata);
        file << ")";
        break;
      default:
        cerr << "Something is really wrong..." << endl;
        break;
    }
    if (i < s)
      file << ", ";
    file << std::endl;
    i++;
  }
  file << "])." << std::endl;
  file.close();
}

set_proof()

void ProofPrinter::set_proof ( Stack * _p )

inline

Basic set method.

Parameters

_p	Pointer to the output of StackProver.

Definition at line 104 of file ProofPrinter.hpp.

{ p = _p; }

show_Prolog()

void ProofPrinter::show_Prolog

(

)

Show the proof in Prolog format.

Definition at line 287 of file ProofPrinter.cpp.

                               {
  cout << "proof_stack([" << std::endl;
  size_t s = p->size() - 1;
  size_t i = 0;
  for (size_t si_index = 0; si_index < p->size(); si_index++) {
    StackItem si((*p)[si_index]);
    switch (si.item_type) {
      case StackItemType::Start:
        cout<< "start(";
        cout << std::to_string(si.this_action.C_2);
        cout << ")";
        break;
      case StackItemType::Axiom:
        cout << "axiom()";
        break;
      case StackItemType::Reduction:
        cout << "reduction(";
        cout << std::to_string(si.this_action.Lindex);
        cout << ", ";
        cout << std::to_string(si.this_action.index_in_path);
        cout << ")";
        break;
      case StackItemType::LeftBranch:
        cout << "left_branch(";
        cout << std::to_string(si.this_action.Lindex);
        cout << ", ";
        cout << std::to_string(si.this_action.C_2);
        cout << ", ";
        cout << std::to_string(si.this_action.Lprime);
        cout << ", ";
        cout << std::to_string(si.depth);
        cout << ")";
        break;
      case StackItemType::RightBranch:
        cout << "right_branch(";
        cout << std::to_string(si.depth);
        cout << ")";
        break;
      case StackItemType::Lemmata:
        cout << "lemmata(";
        cout << std::to_string(si.this_action.Lindex);
        cout << ", ";
        cout << std::to_string(si.this_action.index_in_lemmata);
        cout << ")";
        break;
      default:
        cerr << "Something is really wrong..." << endl;
        break;
    }
    if (i < s)
      cout << ", ";
    cout << std::endl;
    i++;
  }
  cout << "])." << std::endl;
}

show_tptp()

void ProofPrinter::show_tptp

(

)

Show the proof in a TPTP-friendly format.

Definition at line 344 of file ProofPrinter.cpp.

                             {
  cout << "cnf(proof-stack, plain, " << std::endl;
  cout << "proof_stack(" << std::endl;
  size_t s = p->size() - 1;
  size_t i = 0;
  for (size_t si_index = 0; si_index < p->size(); si_index++) {
    StackItem si((*p)[si_index]);
    switch (si.item_type) {
      case StackItemType::Start:
        cout<< "start(";
        cout << std::to_string(si.this_action.C_2);
        cout << ")";
        break;
      case StackItemType::Axiom:
        cout << "axiom()";
        break;
      case StackItemType::Reduction:
        cout << "reduction(";
        cout << std::to_string(si.this_action.Lindex);
        cout << ", ";
        cout << std::to_string(si.this_action.index_in_path);
        cout << ")";
        break;
      case StackItemType::LeftBranch:
        cout << "left_branch(";
        cout << std::to_string(si.this_action.Lindex);
        cout << ", ";
        cout << std::to_string(si.this_action.C_2);
        cout << ", ";
        cout << std::to_string(si.this_action.Lprime);
        cout << ", ";
        cout << std::to_string(si.depth);
        cout << ")";
        break;
      case StackItemType::RightBranch:
        cout << "right_branch(";
        cout << std::to_string(si.depth);
        cout << ")";
        break;
      case StackItemType::Lemmata:
        cout << "lemmata(";
        cout << std::to_string(si.this_action.Lindex);
        cout << ", ";
        cout << std::to_string(si.this_action.index_in_lemmata);
        cout << ")";
        break;
      default:
        cerr << "Something is really wrong..." << endl;
        break;
    }
    if (i < s)
      cout << ", ";
    cout << std::endl;
    i++;
  }
  cout << "))." << std::endl;
}

Member Data Documentation

p

Stack* ProofPrinter::p

private

Pointer to the output of StackProver.

Definition at line 66 of file ProofPrinter.hpp.

---

The documentation for this class was generated from the following files:

• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/misc/ProofPrinter.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/misc/ProofPrinter.cpp