1 2 /* 3 * File LaTeX.hpp. 4 * 5 * This file is part of the source code of the software program 6 * Vampire. It is protected by applicable 7 * copyright laws. 8 * 9 * This source code is distributed under the licence found here 10 * https://vprover.github.io/license.html 11 * and in the source directory 12 * 13 * In summary, you are allowed to use Vampire for non-commercial 14 * purposes but not allowed to distribute, modify, copy, create derivatives, 15 * or use in competitions. 16 * For other uses of Vampire please contact developers for a different 17 * licence, which we will make an effort to provide. 18 */ 19 /** 20 * @file LaTeX.hpp 21 * Defines a class LaTeX translating Vampire data structures 22 * into LaTeX. 23 * 24 * @since 04/01/2004 Manchester 25 */ 26 27 #ifndef __LaTeX__ 28 #define __LaTeX__ 29 30 #include "Forwards.hpp" 31 32 #include "Lib/DHMap.hpp" 33 #include "Lib/Stack.hpp" 34 #include "Lib/VString.hpp" 35 36 #include "Kernel/Connective.hpp" 37 #include "Kernel/InferenceStore.hpp" 38 39 // #include "VS/Connective.hpp" 40 // #include "Var.hpp" 41 42 // namespace VS { 43 // class Symbol; 44 // class SymbolMap; 45 // } 46 47 // using namespace VS; 48 49 namespace Shell { 50 51 using namespace Kernel; 52 53 /** 54 * Translates Vampire refutations into LaTeX. 55 * @since 04/01/2004 Manchester 56 */ 57 class LaTeX 58 { 59 public: LaTeX()60 LaTeX() {} 61 62 vstring header(); 63 vstring footer(); 64 vstring refutationToString(Unit* ref); 65 66 // LaTeX(const Options& options,const SymbolMap* map); 67 // void output (const Refutation&) const; 68 vstring toString(const Term&) const; 69 vstring toString(const vstring& funOrPred,const TermList& args) const; 70 vstring toString(Unit*); 71 private: 72 // /** options used for output */ 73 // const Options& _options; 74 // /** symbol map for printing atoms, functions and variables */ 75 // const SymbolMap* _map; 76 vstring varToString(unsigned num) const; 77 vstring toString(TermList*,bool single=false) const; 78 vstring toString(Literal*) const; 79 vstring toString(Clause*); 80 vstring toString(Formula*) const; 81 vstring toString(Formula*, Connective c) const; 82 83 vstring getClauseLatexId(Unit* cs); 84 85 //vstring splittingToString(InferenceStore::SplittingRecord*); 86 vstring toStringAsInference(Unit*); 87 vstring toStringAsInference(Unit* cs, InferenceStore::FullInference* inf); 88 89 vstring symbolToString (unsigned num, bool pred) const; 90 91 92 }; // class LaTeX 93 94 95 } 96 97 #endif // _LaTeX__ 98 99