From 29eb62fb872eb4ce4d701fe1f9521799c6143b29 Mon Sep 17 00:00:00 2001 From: Jonas Date: Thu, 8 Oct 2026 11:55:31 +0200 Subject: [PATCH] Refactor and extract TPTP proof printing --- Kernel/InferenceStore.cpp | 751 +++++------------------------------- Kernel/InferenceStore.hpp | 34 +- Kernel/TPTPProofPrinter.cpp | 593 ++++++++++++++++++++++++++++ Kernel/TPTPProofPrinter.hpp | 56 +++ Makefile | 3 + cmake/sources.cmake | 1 + 6 files changed, 786 insertions(+), 652 deletions(-) create mode 100644 Kernel/TPTPProofPrinter.cpp create mode 100644 Kernel/TPTPProofPrinter.hpp diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index ed89c116b..c073f9581 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -18,9 +18,8 @@ #include "Lib/Int.hpp" #include "Lib/Metaiterators.hpp" #include "Lib/ScopedPtr.hpp" -#include "Lib/SharedSet.hpp" +#include "Lib/Set.hpp" #include "Lib/Stack.hpp" -#include "Lib/StringUtils.hpp" #include "Lib/ScopedPtr.hpp" #include "Shell/Options.hpp" @@ -28,6 +27,7 @@ #include "Shell/SMTCheck.hpp" #include "Parse/TPTP.hpp" +#include "SAT/SATInference.hpp" #include "Saturation/Splitter.hpp" @@ -42,14 +42,15 @@ #include "SortHelper.hpp" #include "InferenceStore.hpp" +#include "TPTPProofPrinter.hpp" #include "Term.hpp" #include "TermIterators.hpp" #include "Theory.hpp" #include "Unit.hpp" #include -#include -#include +#include +#include //TODO: when we delete clause, we should also delete all its records from the inference store namespace Kernel @@ -58,6 +59,7 @@ namespace Kernel using namespace std; using namespace Lib; using namespace Shell; +using namespace SAT; /** * Records information needed for outputting proofs of general splitting @@ -100,146 +102,51 @@ void InferenceStore::recordIntroducedSplitName(Unit* u, std::string name) ALWAYS(_introducedSplitNames.insert(u->number(),name)); } -/** - * Return @b inner quantified over variables in @b vars - * - * It is caller's responsibility to ensure that variables in @b vars are unique. - */ -template -std::string getQuantifiedStr(VarIter vit, std::string inner, DHMap& t_map, bool innerParentheses=true){ - std::string varStr; - bool first=true; - while(vit.hasNext()) { - unsigned var =vit.next(); - std::string ty=""; - TermList t; - - if(t_map.find(var,t)){ - //a variable of a sort other than $i must always be annotated, and - //preprocessing is not expected to introduce such a sort into an - //initially untyped problem. Same predicate as Formula::toString. - ASS(t == AtomicSort::defaultSort() || env.initiallyHasNonDefaultSorts()); - if(env.initiallyHasNonDefaultSorts()){ - ty=" : " + t.toString(); - } - } - if(ty == " : $tType"){ - if (!first) { varStr = "," + varStr; } - varStr=std::string("X")+Int::toString(var)+ty + varStr; - } else { - if (!first) { varStr+=","; } - varStr+=std::string("X")+Int::toString(var)+ty; - } - first=false; - } - - if (first) { - //we didn't quantify any variable - return inner; - } - - if (innerParentheses) { - return "( ! ["+varStr+"] : ("+inner+") )"; - } - else { - return "( ! ["+varStr+"] : "+inner+" )"; - } +bool InferenceStore::AbstractProofPrinter::CompareUnits::operator()(Unit* left, Unit* right) const +{ + return left->number() < right->number(); } -/** - * Return std::string containing quantified unit @b u. - */ -std::string getQuantifiedStr(Unit* u, List* nonQuantified=0) +// compute closure of `us`' ancestors for printing and insert into `proof` +void InferenceStore::AbstractProofPrinter::scheduleForPrinting(Unit* us) { - Set vars; - std::string res; - DHMap t_map; - SortHelper::collectVariableSorts(u,t_map, /*ignoreBound=*/true); - if (u->isClause()) { - Clause* cl=static_cast(u); - unsigned clen=cl->length(); - for(unsigned i=0;i::member(var, nonQuantified)) { - continue; - } - vars.insert(var); - } - } - res=cl->literalsOnlyToString(); - } else { - Formula* formula=static_cast(u)->formula(); - FormulaVarIterator fvit( formula ); - while(fvit.hasNext()) { - unsigned var=fvit.next(); - if (List::member(var, nonQuantified)) { + std::vector todo = { us }; + while(!todo.empty()) { + Unit *next = todo.back(); + todo.pop_back(); + + // check if this step should be printed + InferenceRule rule = next->inference().rule(); + if(!hideProofStep(rule)) { + // check if already processed (proofs are DAGs, not trees) + auto [_, inserted] = proof.insert(next); + if(!inserted) continue; - } - vars.insert(var); } - res=formula->toString(); - } - - return getQuantifiedStr(decltype(vars)::Iterator(vars), res, t_map); -} + // NB step may be hidden, but its parents are not + // TODO not sure this is desirable, but it was the old behaviour -struct InferenceStore::ProofPrinter -{ - ProofPrinter(std::ostream& out, InferenceStore* is) - : _is(is), out(out) {} - - // compute closure of `us`' ancestors for printing and insert into `proof` - void scheduleForPrinting(Unit* us) - { - std::vector todo = { us }; - while(!todo.empty()) { - Unit *next = todo.back(); - todo.pop_back(); - - // check if this step should be printed - InferenceRule rule = next->inference().rule(); - if(!hideProofStep(rule)) { - // check if already processed (proofs are DAGs, not trees) - auto [_, inserted] = proof.insert(next); - if(!inserted) - continue; - } - // NB step may be hidden, but its parents are not - // TODO not sure this is desirable, but it was the old behaviour - - // process premise parents - UnitIterator parents = next->getParents(); - while(parents.hasNext()) { - Unit* prem = parents.next(); - ASS_NEQ(prem, next) - todo.push_back(prem); - } + // process premise parents + UnitIterator parents = next->getParents(); + while(parents.hasNext()) { + Unit* prem = parents.next(); + ASS_NEQ(prem, next) + todo.push_back(prem); } } +} - virtual ~ProofPrinter() {} - - virtual void print() - { - for(Unit *u : proof) { - SATClause *sat = u->inference().satPremise(); - if(sat) - for(SATClause *scl : topological_sort(sat)) - printSATStep(scl); +void InferenceStore::AbstractProofPrinter::print() +{ + for (Unit* unit : proof) { printStep(unit); } +} - printStep(u); - } - } +struct InferenceStore::ProofPrinter : public InferenceStore::AbstractSATProofPrinter +{ + using AbstractSATProofPrinter::AbstractSATProofPrinter; protected: - virtual bool hideProofStep(InferenceRule rule) - { - return false; - } - - virtual void printStep(Unit* cs) + void printStep(Unit* cs) override { if (cs->isClause()) { Clause* cl=cs->asClause(); @@ -286,59 +193,63 @@ struct InferenceStore::ProofPrinter } } - virtual void printSATStep(SATClause *cl) { + void printSATStep(SATClause *cl) override { out << *cl << '\n'; } - InferenceStore *_is = nullptr; - ostream &out; - -private: - struct CompareSATClauses { - bool operator()(SATClause *l, SATClause *r) const { return l->number < r->number; } - }; +}; - struct CompareUnits { - bool operator()(Unit *l, Unit *r) const { return l->number() < r->number(); } - }; +namespace { - // produce a topological sort of the SAT proof starting at `root` - std::set topological_sort(SATClause *root) { - // things inserted in here will be topologically sorted, - // because it's an ordered set and the clauses are numbered - std::set topological; +struct CompareSATClauses { + bool operator()(SATClause *l, SATClause *r) const { return l->number < r->number; } +}; - // compute closure of root and insert into `topological` - std::vector todo = { root }; - while(!todo.empty()) { - SATClause *next = todo.back(); - todo.pop_back(); +// produce a topological sort of the SAT proof starting at `root` +std::set topological_sort(SATClause *root) { + // things inserted in here will be topologically sorted, + // because it's an ordered set and the clauses are numbered + std::set topological; + + // compute closure of root and insert into `topological` + std::vector todo = { root }; + while(!todo.empty()) { + SATClause *next = todo.back(); + todo.pop_back(); + + // check if already processed (proofs are DAGs, not trees) + auto [_, inserted] = topological.insert(next); + if(!inserted) + continue; + + // process premise parents + SATInference *inference = next->inference(); + if(inference->getType() != SATInference::InfType::PROP_INF) + continue; + SATClauseList *parents = + static_cast(inference)->getPremises(); + for(SATClause *parent : iterTraits(parents->iter())) + todo.push_back(parent); + } - // check if already processed (proofs are DAGs, not trees) - auto [_, inserted] = topological.insert(next); - if(!inserted) - continue; + return topological; +} +} // namespace - // process premise parents - SATInference *inference = next->inference(); - if(inference->getType() != SATInference::InfType::PROP_INF) - continue; - SATClauseList *parents = - static_cast(inference)->getPremises(); - for(SATClause *parent : iterTraits(parents->iter())) - todo.push_back(parent); +void InferenceStore::AbstractSATProofPrinter::print() +{ + for (Unit* unit : proof) { + if (SATClause* sat = unit->inference().satPremise()) { + for (SATClause* clause : topological_sort(sat)) { printSATStep(clause); } } - - return topological; + printStep(unit); } - - std::set proof; -}; +} struct InferenceStore::ProofPropertyPrinter -: public InferenceStore::ProofPrinter +: public InferenceStore::AbstractProofPrinter { - ProofPropertyPrinter(std::ostream& out, InferenceStore* is) : ProofPrinter(out,is) + ProofPropertyPrinter(std::ostream& out, InferenceStore* is) : AbstractProofPrinter(out,is) { max_theory_clause_depth = 0; for(unsigned i=0;i<11;i++){ buckets.push(0); } @@ -347,7 +258,7 @@ struct InferenceStore::ProofPropertyPrinter void print() override { - ProofPrinter::print(); + AbstractProofPrinter::print(); for(unsigned i=0;i<11;i++){ out << buckets[i] << " ";} out << endl; if(last_one){ out << "yes" << endl; } @@ -418,473 +329,11 @@ struct InferenceStore::ProofPropertyPrinter }; -struct InferenceStore::TPTPProofPrinter -: public InferenceStore::ProofPrinter -{ - TPTPProofPrinter(std::ostream& out, InferenceStore* is) - : ProofPrinter(out, is) { - splitPrefix = Saturation::Splitter::splPrefix; - } - - void print() override - { - //an fof proof needs no type declarations, and the signature can hold a - //typed symbol no unit ever used, whose declaration would put a tff line - //into an otherwise fof proof - if(env.initiallyHasNonDefaultSorts() || env.initiallyHigherOrder()){ - //outputSymbolDeclarations also deals with sorts for now - //UIHelper::outputSortDeclarations(out); - UIHelper::outputSymbolDeclarations(out); - } - ProofPrinter::print(); - } - -protected: - std::string splitPrefix; - - std::string getRole(InferenceRule rule, UnitInputType origin) - { - if (isTheoryAxiomRule(rule)) { - return "axiom"; - } - switch(rule) { - case InferenceRule::INPUT: - if (origin==UnitInputType::CONJECTURE) { - return "conjecture"; - } else if (origin==UnitInputType::NEGATED_CONJECTURE) { - return "negated_conjecture"; - } else { - return "axiom"; - } - case InferenceRule::NEGATED_CONJECTURE: - return "negated_conjecture"; - case InferenceRule::AVATAR_DEFINITION: - case InferenceRule::FUNCTION_DEFINITION: - case InferenceRule::PREDICATE_DEFINITION: - case InferenceRule::FOOL_ITE_DEFINITION: - case InferenceRule::FOOL_LET_DEFINITION: - case InferenceRule::FOOL_FORMULA_DEFINITION: - case InferenceRule::FOOL_MATCH_DEFINITION: - case InferenceRule::GENERAL_SPLITTING_COMPONENT: - case InferenceRule::INEQUALITY_SPLITTING_NAME_INTRODUCTION: - case InferenceRule::EQUALITY_PROXY_DEFINITION: - return "definition"; - case InferenceRule::THEORY_TAUTOLOGY_SAT_CONFLICT: - case InferenceRule::HILBERTS_CHOICE_INSTANCE: - case InferenceRule::DISTINCTNESS_AXIOM: - return "axiom"; - default: - return "plain"; - } - } - - std::string tptpRuleName(InferenceRule rule) - { - return StringUtils::replaceChar(ruleName(rule), ' ', '_'); - } - - std::string unitIdToTptp(std::string unitId) - { - return "f"+unitId; - } - - std::string tptpUnitId(Unit* us) - { - return unitIdToTptp(Int::toString(us->number())); - } - - std::string tptpDefId(Unit* us) - { - return unitIdToTptp(Int::toString(us->number())+"_D"); - } - - std::string splitsToString(SplitSet* splits) - { - ASS_G(splits->size(),0); - - if (splits->size()==1) { - return Saturation::Splitter::getFormulaStringFromName(splits->sval(),true /*negated*/); - } - auto sit = splits->iter(); - std::string res("("); - while(sit.hasNext()) { - res+= Saturation::Splitter::getFormulaStringFromName(sit.next(),true /*negated*/); - if (sit.hasNext()) { - res+=" | "; - } - } - res+=")"; - return res; - } - - std::string getFofString(std::string id, std::string formula, std::string inference, InferenceRule rule, UnitInputType origin=UnitInputType::AXIOM) - { - // use the fragment of the unpreprocessed input: the problem's own - // hasNonDefaultSorts() and isHigherOrder() are recomputed from the current - // unit list, so they forget sorts that preprocessing removed, and TPTP - // conventions allow a proof in a weaker fragment than the input but not in - // a stronger one - std::string kind = "fof"; - if(env.initiallyHasNonDefaultSorts()){ kind="tff"; } - if(env.initiallyHigherOrder()){ kind="thf"; } - - return kind+"("+id+","+getRole(rule,origin)+",("+"\n" - +" "+formula+"),\n" - +" "+inference+")."; - } - - std::string getFormulaString(Unit* us) - { - std::string formulaStr; - if (us->isClause()) { - Clause* cl=us->asClause(); - formulaStr=getQuantifiedStr(cl); - if (cl->splits() && !cl->splits()->isEmpty()) { - formulaStr+=" | "+splitsToString(cl->splits()); - } - } - else { - FormulaUnit* fu=static_cast(us); - formulaStr=getQuantifiedStr(fu); - } - return formulaStr; - } - - bool hasNewSymbols(Unit* u) { - bool res = _is->_introducedSymbols.find(u->number()); - ASS(!res || _is->_introducedSymbols.get(u->number()).isNonEmpty()); - if(!res){ - res = _is->_introducedSplitNames.find(u->number()); - } - return res; - } - std::string getNewSymbols(std::string origin, std::string symStr) { - return "new_symbols(" + origin + ",[" +symStr + "])"; - } - - /** It is an iterator over SymbolId */ - template - std::string getNewSymbols(std::string origin, It symIt) { - std::ostringstream symsStr; - while(symIt.hasNext()) { - auto sym = symIt.next(); - symsStr << sym->name(); - if (symIt.hasNext()) { - symsStr << ','; - } - } - return getNewSymbols(origin, symsStr.str()); - } - std::string getNewSymbols(std::string origin, Unit* u) { - ASS(hasNewSymbols(u)); - - if(_is->_introducedSplitNames.find(u->number())){ - return getNewSymbols(origin,_is->_introducedSplitNames.get(u->number())); - } - - SymbolStack& syms = _is->_introducedSymbols.get(u->number()); - return getNewSymbols(origin, SymbolStack::ConstIterator(syms)); - } - -std::string getSkolemizeMap(Unit* u){ - ASS(hasNewSymbols(u)); - SymbolStack& syms = _is->_introducedSymbols.get(u->number()); - return getSkolemizeMap(u->number(), SymbolStack::ConstIterator(syms)); -} - -template -std::string getSkolemizeMap(unsigned unitNumber, It symIt){ - std::ostringstream symsStr; - bool hasNext = symIt.hasNext(); - while (hasNext) { - symsStr << "skolemize("; - auto symbol = symIt.next(); - auto skolemTerm = _is->_introducedSkolemSymTerms.find(symbol); - NEVER(skolemTerm.isNone()); - auto skolemizedVariable = _is->_introducedSymbolReplacedVars.find(symbol); - NEVER(skolemizedVariable.isNone()); - - // for now we have to output standard prolog, i.e. f(X1,...,Xn) even in THF - // TODO: change this once GDV is updated - std::string skolemStr; - if (env.higherOrder()) { - // we require non-lambda terms - ASS(!TermList(*skolemTerm).isLambdaTerm()); - auto [head, args] = HOL::getHeadAndArgs(TermList(*skolemTerm)); - ASS(head.isTerm() && !head.isLambdaTerm()); - - auto h = head.term(); - if(h->isLiteral()) { - skolemStr = static_cast(h)->predicateName(); - } else if (h->isSort()) { - skolemStr = static_cast(h)->typeConName(); - } else { - skolemStr = h->functionName(); - } - - if (h->arity() || args.size()) { - skolemStr += "("; - bool first = true; - for (unsigned i = 0; i < h->arity(); i++) { - auto v = *h->nthArgument(i); - ASS(v.isVar()); - if (!first) { - skolemStr += ","; - } - skolemStr += v.toString(); - first = false; - } - for (unsigned i = 0; i < args.size(); i++) { - ASS(args[i].isVar()); - if (!first) { - skolemStr += ","; - } - skolemStr += args[i].toString(); - first = false; - } - skolemStr += ")"; - } - - } else { - skolemStr = (*skolemTerm)->toString(); - } - - symsStr << "X" << *skolemizedVariable << "," << skolemStr << ")"; - hasNext = symIt.hasNext(); - if(hasNext) { - symsStr << ","; - } - } - return symsStr.str(); -} - - void printStep(Unit* us) override - { - InferenceRule rule = us->inference().rule(); - UnitIterator parents= us->getParents(); - - switch(rule) { - case InferenceRule::GENERAL_SPLITTING_COMPONENT: - printGeneralSplittingComponent(us); - return; - case InferenceRule::GENERAL_SPLITTING: - printSplitting(us); - return; - default: ; - } - - //get std::string representing the formula - - std::string formulaStr=getFormulaString(us); - - //get inference std::string - - std::string inferenceStr; - if (rule==InferenceRule::INPUT) { - std::string axiomName; - std::filesystem::path axiomPath; - if (!Parse::TPTP::findAxiomName(us, axiomName, axiomPath)) { - // Giles' ucore extraction code parses labels from smtlib files, let's try printing these too - if (!us->isClause() && us->getFormula()->hasLabel()) { - axiomName = us->getFormula()->getLabel(); - axiomPath = "unknown"; - } else { - axiomName="unknown"; - axiomPath = "unknown"; - } - } - inferenceStr="file('"+std::string(axiomPath)+"','"+axiomName+"')"; - } - else if (!parents.hasNext()) { - std::string newSymbolInfo; - if (hasNewSymbols(us)) { - newSymbolInfo = getNewSymbols("definition",us); - inferenceStr="introduced(definition,["+newSymbolInfo+"],["+tptpRuleName(rule)+"])"; - } else { - // without introduced symbols we have to claim that the axiom comes from a theory - inferenceStr="introduced(theory,["+tptpRuleName(rule)+"],[])"; - } - } - else { - ASS(parents.hasNext()); - std::string statusStr; - if (rule==InferenceRule::SKOLEMIZE) { - statusStr="status(esa),"+getNewSymbols("skolem",us) + "," + getSkolemizeMap(us); - } - else if(rule==InferenceRule::NEGATED_CONJECTURE) { - statusStr="status(cth)"; - } - - inferenceStr="inference("+tptpRuleName(rule); - - inferenceStr+=",["+statusStr+"],["; - if(rule==InferenceRule::AVATAR_REFUTATION) { - SATClause *premise = us->inference().satPremise(); - ASS(premise) - inferenceStr += "s" + Int::toString(premise->number); - } - else { - bool first=true; - while(parents.hasNext()) { - Unit* prem=parents.next(); - if (!first) { - inferenceStr+=','; - } - inferenceStr+=tptpUnitId(prem); - first=false; - } - } - inferenceStr+="])"; - } - - out<inputType())<number << ", plain, "; - if(cl->isEmpty()) - out << "$false"; - else { - bool first = true; - for(SATLiteral l : iterTraits(cl->iter())) { - if(!first) - out << " | "; - first = false; - out << Saturation::Splitter::getFormulaStringFromLiteral(l); - } - } - - out << ", inference("; - auto inference = cl->inference(); - switch(inference->getType()) { - case SAT::SATInference::PROP_INF: { - out << "rat,[],["; - bool first = true; - SATClauseList *parents = - static_cast(inference)->getPremises(); - for(SATClause *parent : iterTraits(parents->iter())) { - if(!first) - out << ","; - first = false; - out << 's' << parent->number; - } - break; - } - case SAT::SATInference::FO_CONVERSION: - out - << "sat_conversion,[],[f" - << static_cast(inference)->getOrigin()->number(); - break; - } - out << "])).\n"; - } - - void printSplitting(Unit* us) - { - ASS(us->isClause()); - - InferenceRule rule = us->inference().rule(); - UnitIterator parents= us->getParents(); - ASS(rule==InferenceRule::GENERAL_SPLITTING); - - std::string inferenceStr="inference("+tptpRuleName(rule)+",[],["; - - //here we rely on the fact that the base premise is always put as the first premise in - //GeneralSplitting::apply - - ALWAYS(parents.hasNext()); - Unit* base=parents.next(); - inferenceStr+=tptpUnitId(base); - - ASS(parents.hasNext()); //we always split off at least one component - while(parents.hasNext()) { - Unit* comp=parents.next(); - ASS(_is->_splittingNameLiterals.find(comp->number())); - inferenceStr+=","+tptpDefId(comp); - } - inferenceStr+="])"; - - out<isClause()); - - InferenceRule rule = us->inference().rule(); - UnitIterator parents= us->getParents(); - ASS(!parents.hasNext()); - - Literal* nameLit=_is->_splittingNameLiterals.get(us->number()); //the name literal must always be stored - - //sorts of the clause's variables, so the quantifiers of the definition - //below are annotated like every other formula in the proof - DHMap t_map; - SortHelper::collectVariableSorts(us, t_map); - - std::string defId=tptpDefId(us); - - out<* nameVars=0; - VariableIterator vit(nameLit); - while(vit.hasNext()) { - unsigned var=vit.next().var(); - ASS(!List::member(var, nameVars)); //each variable appears only once in the naming literal - List::push(var,nameVars); - } - - std::string compStr; - List* compOnlyVars=0; - bool first=true; - bool multiple=false; - for (Literal* lit : us->asClause()->iterLits()) { - if (lit==nameLit) { - continue; - } - if (first) { - first=false; - } - else { - multiple=true; - compStr+=" | "; - } - compStr+=lit->toString(); - - VariableIterator lvit(lit); - while(lvit.hasNext()) { - unsigned var=lvit.next().var(); - if (!List::member(var, nameVars) && !List::member(var, compOnlyVars)) { - List::push(var,compOnlyVars); - } - } - } - ASS(!first); - - compStr=getQuantifiedStr(VList::Iterator(compOnlyVars), compStr, t_map, multiple); - List::destroy(compOnlyVars); - - std::string defStr=compStr+" <=> "+Literal::complementaryLiteral(nameLit)->toString(); - defStr=getQuantifiedStr(VList::Iterator(nameVars), defStr, t_map); - List::destroy(nameVars); - - auto nameSymbol = env.signature->getPredicate(nameLit->functor()); - std::ostringstream originStm; - originStm << "introduced(definition,[" - << getNewSymbols("definition",getSingletonIterator(nameSymbol)) - << "],[" << tptpRuleName(rule) << "])"; - - out<number() << ",conjecture, " - << getQuantifiedStr(cs) + << getQuantifiedStr(cs) << " ). %"<number() << ",axiom, " - << getQuantifiedStr(prem); + << getQuantifiedStr(prem); out << " ).\n"; } out << "%#\n"; @@ -955,17 +404,17 @@ struct InferenceStore::ProofCheckPrinter void print() override { - ProofPrinter::print(); + AbstractProofPrinter::print(); out << "%#\n"; } }; struct InferenceStore::Smt2ProofCheckPrinter -: public InferenceStore::ProofPrinter +: public InferenceStore::AbstractProofPrinter { USE_ALLOCATOR(InferenceStore::Smt2ProofCheckPrinter); Smt2ProofCheckPrinter(std::ostream& out, InferenceStore* is) - : ProofPrinter(out, is) {} + : AbstractProofPrinter(out, is) {} protected: @@ -1622,21 +1071,21 @@ struct InferenceStore::Smt2ProofCheckPrinter void print() override { - ProofPrinter::print(); + AbstractProofPrinter::print(); out << "%#\n"; } }; struct InferenceStore::SMTCheckPrinter -: public InferenceStore::ProofPrinter +: public InferenceStore::AbstractProofPrinter { SMTCheckPrinter(ostream& out, InferenceStore* is) - : ProofPrinter(out, is) {} + : AbstractProofPrinter(out, is) {} void print() override { SMTCheck::outputSignature(out); - ProofPrinter::print(); + AbstractProofPrinter::print(); } void printStep(Unit* u) override @@ -1645,7 +1094,7 @@ struct InferenceStore::SMTCheckPrinter } }; -InferenceStore::ProofPrinter* InferenceStore::createProofPrinter(std::ostream& out) +InferenceStore::AbstractProofPrinter* InferenceStore::createProofPrinter(std::ostream& out) { switch(env.options->proof()) { case Options::Proof::ON: @@ -1727,11 +1176,11 @@ void InferenceStore::outputUnsatCore(std::ostream& out, Unit* refutation) */ void InferenceStore::outputProof(std::ostream& out, Unit* refutation) { - ProofPrinter* p = createProofPrinter(out); + AbstractProofPrinter* p = createProofPrinter(out); if (!p) { return; } - ScopedPtr pp(p); + ScopedPtr pp(p); pp->scheduleForPrinting(refutation); pp->print(); } @@ -1742,11 +1191,11 @@ void InferenceStore::outputProof(std::ostream& out, Unit* refutation) */ void InferenceStore::outputProof(std::ostream& out, UnitList* units) { - ProofPrinter* p = createProofPrinter(out); + AbstractProofPrinter* p = createProofPrinter(out); if (!p) { return; } - ScopedPtr pp(p); + ScopedPtr pp(p); UnitList::Iterator uit(units); while(uit.hasNext()) { Unit* u = uit.next(); diff --git a/Kernel/InferenceStore.hpp b/Kernel/InferenceStore.hpp index 435459669..69e50c6f2 100644 --- a/Kernel/InferenceStore.hpp +++ b/Kernel/InferenceStore.hpp @@ -17,6 +17,8 @@ #define __InferenceStore__ #include +#include +#include #include "Forwards.hpp" @@ -45,16 +47,46 @@ class InferenceStore void outputUnsatCore(std::ostream& out, Unit* refutation); void outputProof(std::ostream& out, Unit* refutation); void outputProof(std::ostream& out, UnitList* units); + /** Common proof scheduling, independent of any output format. */ + struct AbstractProofPrinter { + AbstractProofPrinter(std::ostream& out, InferenceStore* is) : _is(is), out(out) {} + virtual ~AbstractProofPrinter() = default; + + void scheduleForPrinting(Unit* us); + virtual void print(); + + protected: + virtual bool hideProofStep(InferenceRule rule) { return false; } + virtual void printStep(Unit* unit) = 0; + + struct CompareUnits { + bool operator()(Unit* left, Unit* right) const; + }; + + InferenceStore* _is; + std::ostream& out; + std::set proof; + + }; + struct ProofPrinter; private: + /** Shared SAT traversal; concrete printers choose their own SAT syntax. */ + struct AbstractSATProofPrinter : AbstractProofPrinter { + using AbstractProofPrinter::AbstractProofPrinter; + void print() override; + + protected: + virtual void printSATStep(SAT::SATClause* clause) = 0; + }; struct TPTPProofPrinter; struct Smt2ProofCheckPrinter; struct ProofCheckPrinter; struct ProofPropertyPrinter; struct SMTCheckPrinter; - ProofPrinter* createProofPrinter(std::ostream& out); + AbstractProofPrinter* createProofPrinter(std::ostream& out); DHMultiset _nextClIds; diff --git a/Kernel/TPTPProofPrinter.cpp b/Kernel/TPTPProofPrinter.cpp new file mode 100644 index 000000000..2090ad6b0 --- /dev/null +++ b/Kernel/TPTPProofPrinter.cpp @@ -0,0 +1,593 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ +/** + * @file TPTPProofPrinter.cpp + * TPTP proof formatting and inference output. + */ + +#include "InferenceStore.hpp" +#include "TPTPProofPrinter.hpp" + +#include "Clause.hpp" +#include "Formula.hpp" +#include "FormulaUnit.hpp" +#include "FormulaVarIterator.hpp" +#include "SortHelper.hpp" +#include "TermIterators.hpp" +#include "Unit.hpp" +#include "HOL/HOL.hpp" +#include "Lib/Environment.hpp" +#include "Lib/Int.hpp" +#include "Lib/Metaiterators.hpp" +#include "Lib/Set.hpp" +#include "Lib/SharedSet.hpp" +#include "Lib/StringUtils.hpp" +#include "Parse/TPTP.hpp" +#include "SAT/SATInference.hpp" +#include "Saturation/Splitter.hpp" +#include "Shell/Options.hpp" +#include "Shell/UIHelper.hpp" + +#include + +namespace Kernel { + +using namespace std; +using namespace Lib; +using namespace Shell; +using namespace SAT; + +/** + * Return @b inner quantified over variables in @b vars + * + * It is caller's responsibility to ensure that variables in @b vars are unique. + */ +template +std::string getQuantifiedStr(VarIter vit, std::string inner, DHMap& t_map, bool innerParentheses=true){ + std::string varStr; + bool first=true; + while(vit.hasNext()) { + unsigned var =vit.next(); + std::string ty=""; + TermList t; + + if(t_map.find(var,t)){ + //a variable of a sort other than $i must always be annotated, and + //preprocessing is not expected to introduce such a sort into an + //initially untyped problem. Same predicate as Formula::toString. + ASS(t == AtomicSort::defaultSort() || env.initiallyHasNonDefaultSorts()); + if(env.initiallyHasNonDefaultSorts()){ + ty=" : " + t.toString(); + } + } + if(ty == " : $tType"){ + if (!first) { varStr = "," + varStr; } + varStr=std::string("X")+Int::toString(var)+ty + varStr; + } else { + if (!first) { varStr+=","; } + varStr+=std::string("X")+Int::toString(var)+ty; + } + first=false; + } + + if (first) { + //we didn't quantify any variable + return inner; + } + + if (innerParentheses) { + return "( ! ["+varStr+"] : ("+inner+") )"; + } + else { + return "( ! ["+varStr+"] : "+inner+" )"; + } +} + +std::string getQuantifiedStr(VirtualIterator variables, std::string inner, + DHMap& sorts, bool innerParentheses) +{ + return getQuantifiedStr>(std::move(variables), inner, sorts, innerParentheses); +} + +std::string getQuantifiedStr(Unit* u, List* nonQuantified) +{ + Set vars; + std::string res; + DHMap t_map; + SortHelper::collectVariableSorts(u,t_map, /*ignoreBound=*/true); + if (u->isClause()) { + Clause* cl=static_cast(u); + unsigned clen=cl->length(); + for(unsigned i=0;i::member(var, nonQuantified)) { + continue; + } + vars.insert(var); + } + } + res=cl->literalsOnlyToString(); + } else { + Formula* formula=static_cast(u)->formula(); + FormulaVarIterator fvit( formula ); + while(fvit.hasNext()) { + unsigned var=fvit.next(); + if (List::member(var, nonQuantified)) { + continue; + } + vars.insert(var); + } + res=formula->toString(); + } + + return getQuantifiedStr(decltype(vars)::Iterator(vars), res, t_map); +} + +InferenceStore::TPTPProofPrinter::TPTPProofPrinter(std::ostream& out, InferenceStore* is) + : AbstractSATProofPrinter(out, is), splitPrefix(Saturation::Splitter::splPrefix) +{} + +void InferenceStore::TPTPProofPrinter::print() +{ + //an fof proof needs no type declarations, and the signature can hold a + //typed symbol no unit ever used, whose declaration would put a tff line + //into an otherwise fof proof + if(env.initiallyHasNonDefaultSorts() || env.initiallyHigherOrder()){ + //outputSymbolDeclarations also deals with sorts for now + //UIHelper::outputSortDeclarations(out); + UIHelper::outputSymbolDeclarations(out); + } + AbstractSATProofPrinter::print(); + } + +std::string InferenceStore::TPTPProofPrinter::getRole(InferenceRule rule, UnitInputType origin) +{ + if (isTheoryAxiomRule(rule)) { + return "axiom"; + } + switch(rule) { + case InferenceRule::INPUT: + if (origin==UnitInputType::CONJECTURE) { + return "conjecture"; + } else if (origin==UnitInputType::NEGATED_CONJECTURE) { + return "negated_conjecture"; + } else { + return "axiom"; + } + case InferenceRule::NEGATED_CONJECTURE: + return "negated_conjecture"; + case InferenceRule::AVATAR_DEFINITION: + case InferenceRule::FUNCTION_DEFINITION: + case InferenceRule::PREDICATE_DEFINITION: + case InferenceRule::FOOL_ITE_DEFINITION: + case InferenceRule::FOOL_LET_DEFINITION: + case InferenceRule::FOOL_FORMULA_DEFINITION: + case InferenceRule::FOOL_MATCH_DEFINITION: + case InferenceRule::GENERAL_SPLITTING_COMPONENT: + case InferenceRule::INEQUALITY_SPLITTING_NAME_INTRODUCTION: + case InferenceRule::EQUALITY_PROXY_DEFINITION: + return "definition"; + case InferenceRule::THEORY_TAUTOLOGY_SAT_CONFLICT: + case InferenceRule::HILBERTS_CHOICE_INSTANCE: + case InferenceRule::DISTINCTNESS_AXIOM: + return "axiom"; + default: + return "plain"; + } + } + +std::string InferenceStore::TPTPProofPrinter::tptpRuleName(InferenceRule rule) +{ + return StringUtils::replaceChar(ruleName(rule), ' ', '_'); + } + +std::string InferenceStore::TPTPProofPrinter::unitIdToTptp(std::string unitId) +{ + return "f"+unitId; + } + +std::string InferenceStore::TPTPProofPrinter::tptpUnitId(Unit* us) +{ + return unitIdToTptp(Int::toString(us->number())); + } + +std::string InferenceStore::TPTPProofPrinter::tptpDefId(Unit* us) +{ + return unitIdToTptp(Int::toString(us->number())+"_D"); + } + +std::string InferenceStore::TPTPProofPrinter::splitsToString(SplitSet* splits) +{ + ASS_G(splits->size(),0); + + if (splits->size()==1) { + return Saturation::Splitter::getFormulaStringFromName(splits->sval(),true /*negated*/); + } + auto sit = splits->iter(); + std::string res("("); + while(sit.hasNext()) { + res+= Saturation::Splitter::getFormulaStringFromName(sit.next(),true /*negated*/); + if (sit.hasNext()) { + res+=" | "; + } + } + res+=")"; + return res; + } + +std::string InferenceStore::TPTPProofPrinter::getFofString(std::string id, std::string formula, std::string inference, InferenceRule rule, UnitInputType origin) +{ + // use the fragment of the unpreprocessed input: the problem's own + // hasNonDefaultSorts() and isHigherOrder() are recomputed from the current + // unit list, so they forget sorts that preprocessing removed, and TPTP + // conventions allow a proof in a weaker fragment than the input but not in + // a stronger one + std::string kind = "fof"; + if(env.initiallyHasNonDefaultSorts()){ kind="tff"; } + if(env.initiallyHigherOrder()){ kind="thf"; } + + return kind+"("+id+","+getRole(rule,origin)+",("+"\n" + +" "+formula+"),\n" + +" "+inference+")."; + } + +std::string InferenceStore::TPTPProofPrinter::getFormulaString(Unit* us) +{ + std::string formulaStr; + if (us->isClause()) { + Clause* cl=us->asClause(); + formulaStr=getQuantifiedStr(cl); + if (cl->splits() && !cl->splits()->isEmpty()) { + formulaStr+=" | "+splitsToString(cl->splits()); + } + } + else { + FormulaUnit* fu=static_cast(us); + formulaStr=getQuantifiedStr(fu); + } + return formulaStr; + } + +bool InferenceStore::TPTPProofPrinter::hasNewSymbols(Unit* u) +{ + bool res = _is->_introducedSymbols.find(u->number()); + ASS(!res || _is->_introducedSymbols.get(u->number()).isNonEmpty()); + if(!res){ + res = _is->_introducedSplitNames.find(u->number()); + } + return res; + } + +std::string InferenceStore::TPTPProofPrinter::getNewSymbols(std::string origin, std::string symStr) +{ + return "new_symbols(" + origin + ",[" +symStr + "])"; + } + +std::string InferenceStore::TPTPProofPrinter::getNewSymbols(std::string origin, SymbolStack::ConstIterator symIt) +{ + std::ostringstream symsStr; + while(symIt.hasNext()) { + auto sym = symIt.next(); + symsStr << sym->name(); + if (symIt.hasNext()) { symsStr << ','; } + } + return getNewSymbols(origin, symsStr.str()); + } + +std::string InferenceStore::TPTPProofPrinter::getNewSymbols(std::string origin, Unit* u) +{ + ASS(hasNewSymbols(u)); + + if(_is->_introducedSplitNames.find(u->number())){ + return getNewSymbols(origin,_is->_introducedSplitNames.get(u->number())); + } + + SymbolStack& syms = _is->_introducedSymbols.get(u->number()); + return getNewSymbols(origin, SymbolStack::ConstIterator(syms)); + } + +std::string InferenceStore::TPTPProofPrinter::getSkolemizeMap(Unit* u) +{ + ASS(hasNewSymbols(u)); + SymbolStack& syms = _is->_introducedSymbols.get(u->number()); + return getSkolemizeMap(SymbolStack::ConstIterator(syms)); +} + +std::string InferenceStore::TPTPProofPrinter::getSkolemizeMap(SymbolStack::ConstIterator symIt) +{ + std::ostringstream symsStr; + bool hasNext = symIt.hasNext(); + while (hasNext) { + symsStr << "skolemize("; + auto symbol = symIt.next(); + auto skolemTerm = _is->_introducedSkolemSymTerms.find(symbol); + NEVER(skolemTerm.isNone()); + auto skolemizedVariable = _is->_introducedSymbolReplacedVars.find(symbol); + NEVER(skolemizedVariable.isNone()); + + // for now we have to output standard prolog, i.e. f(X1,...,Xn) even in THF + // TODO: change this once GDV is updated + std::string skolemStr; + if (env.higherOrder()) { + // we require non-lambda terms + ASS(!TermList(*skolemTerm).isLambdaTerm()); + auto [head, args] = HOL::getHeadAndArgs(TermList(*skolemTerm)); + ASS(head.isTerm() && !head.isLambdaTerm()); + + auto h = head.term(); + if(h->isLiteral()) { + skolemStr = static_cast(h)->predicateName(); + } else if (h->isSort()) { + skolemStr = static_cast(h)->typeConName(); + } else { + skolemStr = h->functionName(); + } + + if (h->arity() || args.size()) { + skolemStr += "("; + bool first = true; + for (unsigned i = 0; i < h->arity(); i++) { + auto v = *h->nthArgument(i); + ASS(v.isVar()); + if (!first) { + skolemStr += ","; + } + skolemStr += v.toString(); + first = false; + } + for (unsigned i = 0; i < args.size(); i++) { + ASS(args[i].isVar()); + if (!first) { + skolemStr += ","; + } + skolemStr += args[i].toString(); + first = false; + } + skolemStr += ")"; + } + + } else { + skolemStr = (*skolemTerm)->toString(); + } + + symsStr << "X" << *skolemizedVariable << "," << skolemStr << ")"; + hasNext = symIt.hasNext(); + if(hasNext) { + symsStr << ","; + } + } + return symsStr.str(); +} + +void InferenceStore::TPTPProofPrinter::printStep(Unit* us) +{ + InferenceRule rule = us->inference().rule(); + UnitIterator parents= us->getParents(); + + switch(rule) { + case InferenceRule::GENERAL_SPLITTING_COMPONENT: + printGeneralSplittingComponent(us); + return; + case InferenceRule::GENERAL_SPLITTING: + printSplitting(us); + return; + default: ; + } + + //get std::string representing the formula + + std::string formulaStr=getFormulaString(us); + + //get inference std::string + + std::string inferenceStr; + if (rule==InferenceRule::INPUT) { + std::string axiomName; + std::filesystem::path axiomPath; + if (!Parse::TPTP::findAxiomName(us, axiomName, axiomPath)) { + // Giles' ucore extraction code parses labels from smtlib files, let's try printing these too + if (!us->isClause() && us->getFormula()->hasLabel()) { + axiomName = us->getFormula()->getLabel(); + axiomPath = "unknown"; + } else { + axiomName="unknown"; + axiomPath="unknown"; + } + } + inferenceStr="file('"+std::string(axiomPath)+"','"+axiomName+"')"; + } + else if (!parents.hasNext()) { + std::string newSymbolInfo; + if (hasNewSymbols(us)) { + newSymbolInfo = getNewSymbols("definition",us); + inferenceStr="introduced(definition,["+newSymbolInfo+"],["+tptpRuleName(rule)+"])"; + } else { + // without introduced symbols we have to claim that the axiom comes from a theory + inferenceStr="introduced(theory,["+tptpRuleName(rule)+"],[])"; + } + } + else { + ASS(parents.hasNext()); + std::string statusStr; + if (rule==InferenceRule::SKOLEMIZE) { + statusStr="status(esa),"+getNewSymbols("skolem",us) + "," + getSkolemizeMap(us); + } + else if(rule==InferenceRule::NEGATED_CONJECTURE) { + statusStr="status(cth)"; + } + + inferenceStr="inference("+tptpRuleName(rule); + + inferenceStr+=",["+statusStr+"],["; + if(rule==InferenceRule::AVATAR_REFUTATION) { + SATClause *premise = us->inference().satPremise(); + ASS(premise) + inferenceStr += "s" + Int::toString(premise->number); + } + else { + bool first=true; + while(parents.hasNext()) { + Unit* prem=parents.next(); + if (!first) { + inferenceStr+=','; + } + inferenceStr+=tptpUnitId(prem); + first=false; + } + } + inferenceStr+="])"; + } + + out<inputType())<number << ", plain, "; + if(cl->isEmpty()) + out << "$false"; + else { + bool first = true; + for(SATLiteral l : iterTraits(cl->iter())) { + if(!first) + out << " | "; + first = false; + out << Saturation::Splitter::getFormulaStringFromLiteral(l); + } + } + + out << ", inference("; + auto inference = cl->inference(); + switch(inference->getType()) { + case SAT::SATInference::PROP_INF: { + out << "rat,[],["; + bool first = true; + SATClauseList *parents = + static_cast(inference)->getPremises(); + for(SATClause *parent : iterTraits(parents->iter())) { + if(!first) + out << ","; + first = false; + out << 's' << parent->number; + } + break; + } + case SAT::SATInference::FO_CONVERSION: + out + << "sat_conversion,[],[f" + << static_cast(inference)->getOrigin()->number(); + break; + } + out << "])).\n"; + } + +void InferenceStore::TPTPProofPrinter::printSplitting(Unit* us) +{ + ASS(us->isClause()); + + InferenceRule rule = us->inference().rule(); + UnitIterator parents= us->getParents(); + ASS(rule==InferenceRule::GENERAL_SPLITTING); + + std::string inferenceStr="inference("+tptpRuleName(rule)+",[],["; + + //here we rely on the fact that the base premise is always put as the first premise in + //GeneralSplitting::apply + + ALWAYS(parents.hasNext()); + Unit* base=parents.next(); + inferenceStr+=tptpUnitId(base); + + ASS(parents.hasNext()); //we always split off at least one component + while(parents.hasNext()) { + Unit* comp=parents.next(); + ASS(_is->_splittingNameLiterals.find(comp->number())); + inferenceStr+=","+tptpDefId(comp); + } + inferenceStr+="])"; + + out<isClause()); + + InferenceRule rule = us->inference().rule(); + UnitIterator parents= us->getParents(); + ASS(!parents.hasNext()); + + Literal* nameLit=_is->_splittingNameLiterals.get(us->number()); //the name literal must always be stored + + //sorts of the clause's variables, so the quantifiers of the definition + //below are annotated like every other formula in the proof + DHMap t_map; + SortHelper::collectVariableSorts(us, t_map); + + std::string defId=tptpDefId(us); + + out<* nameVars=0; + VariableIterator vit(nameLit); + while(vit.hasNext()) { + unsigned var=vit.next().var(); + ASS(!List::member(var, nameVars)); //each variable appears only once in the naming literal + List::push(var,nameVars); + } + + std::string compStr; + List* compOnlyVars=0; + bool first=true; + bool multiple=false; + for (Literal* lit : us->asClause()->iterLits()) { + if (lit==nameLit) { + continue; + } + if (first) { + first=false; + } + else { + multiple=true; + compStr+=" | "; + } + compStr+=lit->toString(); + + VariableIterator lvit(lit); + while(lvit.hasNext()) { + unsigned var=lvit.next().var(); + if (!List::member(var, nameVars) && !List::member(var, compOnlyVars)) { + List::push(var,compOnlyVars); + } + } + } + ASS(!first); + + compStr=getQuantifiedStr(pvi(VList::Iterator(compOnlyVars)), compStr, t_map, multiple); + List::destroy(compOnlyVars); + + std::string defStr=compStr+" <=> "+Literal::complementaryLiteral(nameLit)->toString(); + defStr=getQuantifiedStr(pvi(VList::Iterator(nameVars)), defStr, t_map); + List::destroy(nameVars); + + auto nameSymbol = env.signature->getPredicate(nameLit->functor()); + std::ostringstream originStm; + originStm << "introduced(definition,[" + << getNewSymbols("definition",nameSymbol->name()) + << "],[" << tptpRuleName(rule) << "])"; + + out< +#include + +namespace Kernel { + +using namespace Lib; + +/** Quantify a proof body over unique variables, preserving their iteration order. */ +std::string getQuantifiedStr(VirtualIterator variables, std::string inner, + DHMap& sorts, bool innerParentheses = true); + +/** Return the universally closed unit, excluding the supplied variables. */ +std::string getQuantifiedStr(Unit* unit, List* nonQuantified = nullptr); + +struct InferenceStore::TPTPProofPrinter : InferenceStore::AbstractSATProofPrinter +{ + TPTPProofPrinter(std::ostream& out, InferenceStore* is); + void print() override; + +protected: + void printStep(Unit* unit) override; + void printSATStep(SAT::SATClause* clause) override; + std::string getRole(InferenceRule rule, UnitInputType origin); + std::string tptpRuleName(InferenceRule rule); + std::string unitIdToTptp(std::string unitId); + std::string tptpUnitId(Unit* unit); + std::string tptpDefId(Unit* unit); + std::string splitsToString(SplitSet* splits); + std::string getFofString(std::string id, std::string formula, std::string inference, + InferenceRule rule, UnitInputType origin = UnitInputType::AXIOM); + std::string getFormulaString(Unit* unit); + bool hasNewSymbols(Unit* unit); + std::string getNewSymbols(std::string origin, std::string symbols); + std::string getNewSymbols(std::string origin, SymbolStack::ConstIterator symbols); + std::string getNewSymbols(std::string origin, Unit* unit); + std::string getSkolemizeMap(Unit* unit); + std::string getSkolemizeMap(SymbolStack::ConstIterator symbols); + void printSplitting(Unit* unit); + void printGeneralSplittingComponent(Unit* unit); + + std::string splitPrefix; +}; + +} // namespace Kernel + +#endif diff --git a/Makefile b/Makefile index 9696fd865..5d90c00d5 100644 --- a/Makefile +++ b/Makefile @@ -173,6 +173,7 @@ VK_OBJ= Kernel/Clause.o\ Kernel/Grounder.o\ Kernel/Inference.o\ Kernel/InferenceStore.o\ + Kernel/TPTPProofPrinter.o\ Kernel/KBO.o\ Kernel/QKbo.o\ Kernel/ALASCA/Signature.o\ @@ -435,6 +436,7 @@ LIB_DEP = Indexing/TermSharing.o\ Kernel/NumTraits.o\ Kernel/Inference.o\ Kernel/InferenceStore.o\ + Kernel/TPTPProofPrinter.o\ Kernel/Problem.o\ Kernel/SortHelper.o\ Kernel/OperatorType.o\ @@ -466,6 +468,7 @@ OTHER_CL_DEP = Indexing/ResultSubstitution.o\ Kernel/FormulaTransformer.o\ Kernel/Grounder.o\ Kernel/InferenceStore.o\ + Kernel/TPTPProofPrinter.o\ Kernel/Matcher.o\ Kernel/KBO.o\ Kernel/SKIKBO.o\ diff --git a/cmake/sources.cmake b/cmake/sources.cmake index 8cbd6dec1..335274358 100644 --- a/cmake/sources.cmake +++ b/cmake/sources.cmake @@ -406,6 +406,7 @@ set(SOURCES Kernel/Inference.cpp Kernel/Inference.hpp Kernel/InferenceStore.cpp + Kernel/TPTPProofPrinter.cpp Kernel/InferenceStore.hpp Kernel/InterpretedLiteralEvaluator.cpp Kernel/InterpretedLiteralEvaluator.hpp