Connect++ 0.1
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
ProofPrinter.hpp
1/*
2
3Copyright © 2023-24 Sean Holden. All rights reserved.
4
5*/
6/*
7
8This file is part of Connect++.
9
10Connect++ is free software: you can redistribute it and/or modify it
11under the terms of the GNU General Public License as published by the
12Free Software Foundation, either version 3 of the License, or (at your
13option) any later version.
14
15Connect++ is distributed in the hope that it will be useful, but WITHOUT
16ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
17FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
18more details.
19
20You should have received a copy of the GNU General Public License along
21with Connect++. If not, see <https://www.gnu.org/licenses/>.
22
23*/
24
25#ifndef PROOFPRINTER_HPP
26#define PROOFPRINTER_HPP
27
28#include<iostream>
29#include<fstream>
30#include<filesystem>
31
32#include "StackItem.hpp"
33
34using std::filesystem::path;
35
51private:
55 vector<StackItem>* p;
64 string make_LaTeX_state(StackItem*) const;
76 string make_LaTeX_subtree(StackItem*) const;
77public:
81 ProofPrinter() : p(nullptr) {};
87 ProofPrinter(vector<StackItem>* _p) : p(_p) {};
93 inline void set_proof(vector<StackItem>* _p) { p = _p; }
97 inline void clear() { p = nullptr; }
105 void make_LaTeX(const path&, const path&, const string&);
112 void make_Prolog(const path&);
113};
114
115#endif
Class for rendering a proof in various formats.
Definition ProofPrinter.hpp:50
void make_Prolog(const path &)
Convert to a form suitable for use by the Prolog proof checker and write to a file.
Definition ProofPrinter.cpp:165
ProofPrinter(vector< StackItem > *_p)
The constructor yuo want.
Definition ProofPrinter.hpp:87
void set_proof(vector< StackItem > *_p)
Basic set method.
Definition ProofPrinter.hpp:93
void make_LaTeX(const path &, const path &, const string &)
Convert to LaTeX and store in the specified file.
Definition ProofPrinter.cpp:104
ProofPrinter()
Basic constructor.
Definition ProofPrinter.hpp:81
void clear()
Basic set method.
Definition ProofPrinter.hpp:97
Stack items: each contains its own stack of possible next inferences.
Definition StackItem.hpp:51