From 45b2a477cfdf4e0cb5121151f1863b22c6a482e3 Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Fri, 20 Sep 2024 09:47:54 +0100 Subject: [PATCH 1/3] proof extra data, rather than strings --- CMakeLists.txt | 3 ++ Inferences/ProofExtra.cpp | 42 ++++++++++++++++++++ Inferences/ProofExtra.hpp | 75 ++++++++++++++++++++++++++++++++++++ Inferences/SubVarSup.cpp | 6 --- Inferences/Superposition.cpp | 33 ++++------------ Inferences/Superposition.hpp | 2 + Kernel/Clause.cpp | 6 +-- Kernel/Unit.cpp | 11 ++++-- Lib/Environment.hpp | 3 +- Lib/ProofExtra.hpp | 74 +++++++++++++++++++++++++++++++++++ Makefile | 1 + Shell/Options.cpp | 9 ++--- Shell/Options.hpp | 9 +---- 13 files changed, 221 insertions(+), 53 deletions(-) create mode 100644 Inferences/ProofExtra.cpp create mode 100644 Inferences/ProofExtra.hpp create mode 100644 Lib/ProofExtra.hpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 66d5173c5..5e266ac41 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -170,6 +170,7 @@ set(VAMPIRE_LIB_SOURCES Lib/Numbering.hpp Lib/PairUtils.hpp Lib/Portability.hpp + Lib/ProofExtra.hpp Lib/Random.hpp Lib/RatioKeeper.hpp Lib/Recycled.hpp @@ -333,6 +334,8 @@ set(VAMPIRE_KERNEL_SOURCES Inferences/CasesSimp.hpp Inferences/Cases.cpp Inferences/Cases.hpp + Inferences/ProofExtra.hpp + Inferences/ProofExtra.cpp Shell/LambdaElimination.cpp Shell/LambdaElimination.hpp ) diff --git a/Inferences/ProofExtra.cpp b/Inferences/ProofExtra.cpp new file mode 100644 index 000000000..baaaa5cbc --- /dev/null +++ b/Inferences/ProofExtra.cpp @@ -0,0 +1,42 @@ +/* + * 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 ProofExtra.cpp + * Various objects that include "extra information" about an inference, + * e.g. selected literals, unifier, etc. + * + * @since 09/09/2024 Oxford + */ + +#include "ProofExtra.hpp" + +namespace Inferences { + +void LiteralInferenceExtra::output(std::ostream &out) const { + out << "selected=(" << selectedLiteral->toString() << ')'; +} + +void TwoLiteralInferenceExtra::output(std::ostream &out) const { + LiteralInferenceExtra::output(out); + out << ",other=(" << otherLiteral->toString() << ')'; +} + +void RewriteInferenceExtra::output(std::ostream &out) const { + out << "side=" << reversed; +} + +void RewriteIntoInferenceExtra::output(std::ostream &out) const { + TwoLiteralInferenceExtra::output(out); + out << ','; + RewriteInferenceExtra::output(out); + out << ",rewritten=" << rewritten; +} + +} // namespace Inferences diff --git a/Inferences/ProofExtra.hpp b/Inferences/ProofExtra.hpp new file mode 100644 index 000000000..b443c4310 --- /dev/null +++ b/Inferences/ProofExtra.hpp @@ -0,0 +1,75 @@ +/* + * 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 ProofExtra.hpp + * Various objects that include "extra information" about an inference, + * e.g. selected literals, unifier, etc. + * + * @since 09/09/2024 Oxford + */ + +#ifndef __Inferences_ProofExtra__ +#define __Inferences_ProofExtra__ + +#include "Kernel/Term.hpp" +#include "Lib/ProofExtra.hpp" + +namespace Inferences { + +// inferences that use one literal from their main premise +struct LiteralInferenceExtra : virtual public InferenceExtra { + LiteralInferenceExtra(Kernel::Literal *selected) : selectedLiteral(selected) {} + + virtual void output(std::ostream &out) const override; + + // the literal from the main premise + Kernel::Literal *selectedLiteral; +}; + +// inferences that use one literal from their side premise +struct TwoLiteralInferenceExtra : public LiteralInferenceExtra { + TwoLiteralInferenceExtra(Kernel::Literal *selected, Kernel::Literal *other) + : LiteralInferenceExtra(selected), otherLiteral(other) {} + + virtual void output(std::ostream &out) const override; + + // the literal from the side premise + Kernel::Literal *otherLiteral; +}; + +struct RewriteInferenceExtra : virtual public InferenceExtra { + RewriteInferenceExtra(bool reversed) : reversed(reversed) {} + + virtual void output(std::ostream &out) const override; + + // if true, rewrite RHS to LHS + bool reversed; +}; + +struct RewriteIntoInferenceExtra : public TwoLiteralInferenceExtra, public RewriteInferenceExtra { + RewriteIntoInferenceExtra( + Kernel::Literal *selected, + Kernel::Literal *other, + bool reversed, + Kernel::TermList rewritten + ) : + TwoLiteralInferenceExtra(selected, other), + RewriteInferenceExtra(reversed), + rewritten(rewritten) {} + + virtual void output(std::ostream &out) const override; + + // the rewritten term + Kernel::TermList rewritten; +}; + +} + +#endif diff --git a/Inferences/SubVarSup.cpp b/Inferences/SubVarSup.cpp index 61d9d99df..037e7eecc 100644 --- a/Inferences/SubVarSup.cpp +++ b/Inferences/SubVarSup.cpp @@ -261,12 +261,6 @@ Clause* SubVarSup::performSubVarSup( return 0; } - // If proof extra is on let's compute the positions we have performed - // SubVarSup on - if(env.options->proofExtra()==Options::ProofExtra::FULL){ - //TODO update for proof extra - } - bool afterCheck = getOptions().literalMaximalityAftercheck() && _salg->getLiteralSelector().isBGComplete(); Inference inf(GeneratingInference2(InferenceRule::SUB_VAR_SUP, rwClause, eqClause)); diff --git a/Inferences/Superposition.cpp b/Inferences/Superposition.cpp index b5a03a23f..866935717 100644 --- a/Inferences/Superposition.cpp +++ b/Inferences/Superposition.cpp @@ -529,32 +529,13 @@ Clause* Superposition::performSuperposition( inf_destroyer.disable(); // ownership passed to the the clause below auto clause = Clause::fromStack(*res, inf); - // If proof extra is on let's compute the positions we have performed - // superposition on - if(env.options->proofExtra()==Options::ProofExtra::FULL){ - - // First find which literal it is in the clause, as selection has occured already - // this should remain the same...? - std::string rwPlace = Lib::Int::toString(rwClause->getLiteralPosition(rwLit)); - std::string eqPlace = Lib::Int::toString(eqClause->getLiteralPosition(eqLit)); - - std::string rwPos="_"; - ALWAYS(Kernel::positionIn(rwTerm,rwLit,rwPos)); - std::string eqPos = "("+eqPlace+").2"; - rwPos = "("+rwPlace+")."+rwPos; - - std::string eqClauseNum = Lib::Int::toString(eqClause->number()); - std::string rwClauseNum = Lib::Int::toString(rwClause->number()); - - std::string extra = eqClauseNum + " into " + rwClauseNum+", unify on "+ - eqPos+" in "+eqClauseNum+" and "+ - rwPos+" in "+rwClauseNum; - - if (!env.proofExtra) { - env.proofExtra = new DHMap(); - } - env.proofExtra->insert(clause,extra); - } + if(env.options->proofExtra()) + env.proofExtra.insert(clause, std::unique_ptr(new SuperpositionExtra( + rwLit, + eqLit, + eqLHS == (*eqLit)[1], + rwTerm + ))); return clause; } diff --git a/Inferences/Superposition.hpp b/Inferences/Superposition.hpp index 2b22e578f..bf62b5b92 100644 --- a/Inferences/Superposition.hpp +++ b/Inferences/Superposition.hpp @@ -20,6 +20,7 @@ #include "Indexing/TermIndex.hpp" #include "InferenceEngine.hpp" +#include "Inferences/ProofExtra.hpp" #include "Kernel/RobSubstitution.hpp" namespace Inferences { @@ -61,6 +62,7 @@ class Superposition SuperpositionLHSIndex* _lhsIndex; }; +using SuperpositionExtra = RewriteIntoInferenceExtra; }; diff --git a/Kernel/Clause.cpp b/Kernel/Clause.cpp index e25127a0a..3c96541be 100644 --- a/Kernel/Clause.cpp +++ b/Kernel/Clause.cpp @@ -219,8 +219,8 @@ void Clause::destroy() static Stack toDestroy(32); Clause* cl = this; for(;;) { - if ((env.options->proofExtra()==Options::ProofExtra::FULL) && env.proofExtra) { - env.proofExtra->remove(cl); + if (env.options->proofExtra()) { + env.proofExtra.remove(cl); } Inference::Iterator it = cl->_inference.iterator(); while (cl->_inference.hasNext(it)) { @@ -383,7 +383,7 @@ std::string Clause::toString() const // print inference and ids of parent clauses result += " " + inferenceAsString(); - if(env.options->proofExtra()!=Options::ProofExtra::OFF){ + if(env.options->proofExtra()){ // print statistics: each entry should have the form key:value result += std::string(" {"); diff --git a/Kernel/Unit.cpp b/Kernel/Unit.cpp index f76faadf7..42848f69b 100644 --- a/Kernel/Unit.cpp +++ b/Kernel/Unit.cpp @@ -166,10 +166,13 @@ std::string Unit::inferenceAsString() const first = false; result += Int::toString(parent->number()); } - // print Extra - std::string extra; - if (env.proofExtra && env.proofExtra->find(this,extra) && extra != "") { - result += ", " + extra; + + // print extra if present + auto *extra = env.proofExtra.find(this); + if(extra) { + if(!first) + result += ','; + result += extra->toString(); } return result + ']'; diff --git a/Lib/Environment.hpp b/Lib/Environment.hpp index 2d4122585..9824b4c74 100644 --- a/Lib/Environment.hpp +++ b/Lib/Environment.hpp @@ -23,6 +23,7 @@ #include "Exception.hpp" #include "DHMap.hpp" #include "Kernel/Problem.hpp" +#include "Lib/ProofExtra.hpp" namespace Lib { @@ -51,7 +52,7 @@ class Environment DHMap* predicateSineLevels; - DHMap* proofExtra; // maps Unit* pointers to the associated proof extra string, if available + ProofExtra proofExtra; /** Time remaining until the end of the time-limit in miliseconds */ int remainingTime() const; diff --git a/Lib/ProofExtra.hpp b/Lib/ProofExtra.hpp new file mode 100644 index 000000000..5865d2123 --- /dev/null +++ b/Lib/ProofExtra.hpp @@ -0,0 +1,74 @@ +/* + * 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 ProofExtra.hpp + * + * Include "extra information" about an inference, e.g. selected literals, unifier, etc. + * + * @since 09/09/2024 Oxford + */ + +#ifndef __Lib_ProofExtra__ +#define __Lib_ProofExtra__ + +#include "Lib/DHMap.hpp" + +namespace Lib { + +// base for extra inference information +struct InferenceExtra { + virtual ~InferenceExtra() {}; + + // for debug printing only, specific output formats should downcast and handle individually + virtual void output(std::ostream &out) const = 0; + + std::string toString() const { + std::stringstream ss; + this->output(ss); + return ss.str(); + } +}; + +inline std::ostream &operator<<(std::ostream &out, const InferenceExtra &extra) { + extra.output(out); + return out; +} + +// container for extras +class ProofExtra { + DHMap> extras; + +public: + // associate `extra` with `unit` + void insert(Kernel::Unit *unit, std::unique_ptr extra) { + extras.insert(unit, std::move(extra)); + } + + // remove the extra information for this unit + void remove(Kernel::Unit *unit) { + extras.remove(unit); + } + + // associated InferenceExtra if present, nullptr otherwise + const InferenceExtra *find(const Kernel::Unit *unit) { + auto *found = extras.findPtr(const_cast(unit)); + if(!found) + return nullptr; + return found->get(); + } + + // associated InferenceExtra: must be present + const InferenceExtra &get(const Kernel::Unit *unit) { + return *extras.get(const_cast(unit)); + } +}; +} + +#endif diff --git a/Makefile b/Makefile index 60c699044..0f7f78eff 100644 --- a/Makefile +++ b/Makefile @@ -290,6 +290,7 @@ VINF_OBJ=Inferences/BackwardDemodulation.o\ Inferences/InterpretedEvaluation.o\ Inferences/InvalidAnswerLiteralRemovals.o\ Inferences/TheoryInstAndSimp.o\ + Inferences/ProofExtra.o\ SATSubsumption/SATSubsumptionAndResolution.o\ SATSubsumption/subsat/constraint.o\ SATSubsumption/subsat/log.o\ diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 26311f8a0..e7cd74683 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -317,12 +317,9 @@ void Options::init() _lookup.insert(&_printProofToFile); _printProofToFile.tag(OptionTag::OUTPUT); - _proofExtra = ChoiceOptionValue("proof_extra","",ProofExtra::OFF,{"off","free","full"}); - _proofExtra.description="Add extra detail to proofs:\n " - "- free uses known information only\n" - "- full may perform expensive operations to achieve this so may" - " significantly impact on performance.\n" - " The option is still under development and the format of extra information (mainly from full) may change between minor releases"; + _proofExtra = BoolOptionValue("proof_extra","",false); + _proofExtra.description="Add extra detail to proofs in exchange for performance.\n" + "This option is still under development and the format of information may change."; _lookup.insert(&_proofExtra); _proofExtra.tag(OptionTag::OUTPUT); diff --git a/Shell/Options.hpp b/Shell/Options.hpp index 809d6958a..c6a9c9843 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -298,11 +298,6 @@ class Options CHEAP }; - enum class ProofExtra : unsigned int { - OFF, - FREE, - FULL - }; enum class FMBWidgetOrders : unsigned int { FUNCTION_FIRST, // f(1) f(2) f(3) ... g(1) g(2) ... ARGUMENT_FIRST, // f(1) g(1) h(1) ... f(2) g(2) ... @@ -1949,7 +1944,7 @@ bool _hard; void setStatistics(Statistics newVal) { _statistics.actualValue=newVal; } Proof proof() const { return _proof.actualValue; } bool minimizeSatProofs() const { return _minimizeSatProofs.actualValue; } - ProofExtra proofExtra() const { return _proofExtra.actualValue; } + bool proofExtra() const { return _proofExtra.actualValue; } bool traceback() const { return _traceback.actualValue; } void setTraceback(bool traceback) { _traceback.actualValue = traceback; } std::string printProofToFile() const { return _printProofToFile.actualValue; } @@ -2586,7 +2581,7 @@ bool _hard; StringOptionValue _problemName; ChoiceOptionValue _proof; BoolOptionValue _minimizeSatProofs; - ChoiceOptionValue _proofExtra; + BoolOptionValue _proofExtra; BoolOptionValue _traceback; StringOptionValue _protectedPrefix; From 619127915612af00c7d8724f2351c1e8444548ab Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Fri, 20 Sep 2024 13:16:40 +0100 Subject: [PATCH 2/3] add resolution, demodulation, equality resolution --- Inferences/BackwardDemodulation.cpp | 11 +++++++---- Inferences/BackwardDemodulation.hpp | 3 ++- Inferences/BinaryResolution.cpp | 9 +++++++-- Inferences/BinaryResolution.hpp | 3 +++ Inferences/EqualityResolution.cpp | 5 ++++- Inferences/EqualityResolution.hpp | 2 ++ Inferences/ForwardDemodulation.cpp | 2 ++ Inferences/ForwardDemodulation.hpp | 3 +++ Inferences/ProofExtra.cpp | 5 ++--- Inferences/ProofExtra.hpp | 23 ++++++++++------------- Inferences/Superposition.cpp | 6 +++--- Inferences/Superposition.hpp | 2 +- Lib/ProofExtra.hpp | 6 +++--- 13 files changed, 49 insertions(+), 31 deletions(-) diff --git a/Inferences/BackwardDemodulation.cpp b/Inferences/BackwardDemodulation.cpp index bc06298bd..f3474e12b 100644 --- a/Inferences/BackwardDemodulation.cpp +++ b/Inferences/BackwardDemodulation.cpp @@ -176,10 +176,13 @@ struct BackwardDemodulation::ResultFn env.statistics->backwardDemodulations++; _removed->insert(qr.data->clause); - - return BwSimplificationRecord( - qr.data->clause, - Clause::fromStack(*resLits, SimplifyingInference2(InferenceRule::BACKWARD_DEMODULATION, qr.data->clause, _cl))); + Clause *replacement = Clause::fromStack( + *resLits, + SimplifyingInference2(InferenceRule::BACKWARD_DEMODULATION, qr.data->clause, _cl) + ); + if(env.options->proofExtra()) + env.proofExtra.insert(replacement, new BackwardDemodulationExtra(lhs, lhsS)); + return BwSimplificationRecord(qr.data->clause, replacement); } private: Literal* _eqLit; diff --git a/Inferences/BackwardDemodulation.hpp b/Inferences/BackwardDemodulation.hpp index 61872a4be..0ffa6b8db 100644 --- a/Inferences/BackwardDemodulation.hpp +++ b/Inferences/BackwardDemodulation.hpp @@ -20,8 +20,8 @@ #include "Indexing/TermIndex.hpp" #include "DemodulationHelper.hpp" - #include "InferenceEngine.hpp" +#include "ProofExtra.hpp" namespace Inferences { @@ -45,6 +45,7 @@ class BackwardDemodulation DemodulationHelper _helper; }; +using BackwardDemodulationExtra = RewriteInferenceExtra; }; #endif /* __BackwardDemodulation__ */ diff --git a/Inferences/BinaryResolution.cpp b/Inferences/BinaryResolution.cpp index 0a886b2cb..18a7d66b9 100644 --- a/Inferences/BinaryResolution.cpp +++ b/Inferences/BinaryResolution.cpp @@ -235,12 +235,17 @@ Clause* BinaryResolution::generateClause( if(nConstraints != 0){ env.statistics->cResolution++; } - else{ + else{ env.statistics->resolution++; } inf_destroyer.disable(); // ownership passed to the the clause below - return Clause::fromStack(*resLits, inf); + Clause *cl = Clause::fromStack(*resLits, inf); + if(env.options->proofExtra()) + env.proofExtra.insert(cl, new BinaryResolutionExtra(queryLit, resultLit)); + + return cl; + } ClauseIterator BinaryResolution::generateClauses(Clause* premise) diff --git a/Inferences/BinaryResolution.hpp b/Inferences/BinaryResolution.hpp index e5b095048..3931abeb2 100644 --- a/Inferences/BinaryResolution.hpp +++ b/Inferences/BinaryResolution.hpp @@ -19,6 +19,7 @@ #include "Forwards.hpp" #include "InferenceEngine.hpp" +#include "ProofExtra.hpp" #include "Kernel/Ordering.hpp" #include "Kernel/RobSubstitution.hpp" @@ -50,6 +51,8 @@ class BinaryResolution BinaryResolutionIndex* _index; }; +using BinaryResolutionExtra = TwoLiteralInferenceExtra; + }; #endif /*__BinaryResolution__*/ diff --git a/Inferences/EqualityResolution.cpp b/Inferences/EqualityResolution.cpp index 6b4642422..e9c84b450 100644 --- a/Inferences/EqualityResolution.cpp +++ b/Inferences/EqualityResolution.cpp @@ -127,7 +127,10 @@ struct EqualityResolution::ResultFn env.statistics->equalityResolution++; - return Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::EQUALITY_RESOLUTION, _cl)); + Clause *cl = Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::EQUALITY_RESOLUTION, _cl)); + if(env.options->proofExtra()) + env.proofExtra.insert(cl, new EqualityResolutionExtra(lit)); + return cl; } private: bool _afterCheck; diff --git a/Inferences/EqualityResolution.hpp b/Inferences/EqualityResolution.hpp index a6c579885..949e2c4c4 100644 --- a/Inferences/EqualityResolution.hpp +++ b/Inferences/EqualityResolution.hpp @@ -19,6 +19,7 @@ #include "Forwards.hpp" #include "InferenceEngine.hpp" +#include "Inferences/ProofExtra.hpp" #include "Shell/Options.hpp" namespace Inferences { @@ -38,6 +39,7 @@ class EqualityResolution struct IsNegativeEqualityFn; }; +using EqualityResolutionExtra = LiteralInferenceExtra; }; diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp index ae9af4c39..ed988cc2c 100644 --- a/Inferences/ForwardDemodulation.cpp +++ b/Inferences/ForwardDemodulation.cpp @@ -224,6 +224,8 @@ bool ForwardDemodulationImpl::perform(Clause* cl, Clause* premises = pvi( getSingletonIterator(qr.data->clause)); replacement = Clause::fromStack(*resLits, SimplifyingInference2(InferenceRule::FORWARD_DEMODULATION, cl, qr.data->clause)); + if(env.options->proofExtra()) + env.proofExtra.insert(replacement, new ForwardDemodulationExtra(lhs, trm)); return true; } } diff --git a/Inferences/ForwardDemodulation.hpp b/Inferences/ForwardDemodulation.hpp index 81210fbc8..27d650545 100644 --- a/Inferences/ForwardDemodulation.hpp +++ b/Inferences/ForwardDemodulation.hpp @@ -19,7 +19,9 @@ #include "Forwards.hpp" #include "Indexing/TermIndex.hpp" +#include "DemodulationHelper.hpp" #include "InferenceEngine.hpp" +#include "ProofExtra.hpp" namespace Inferences { @@ -53,6 +55,7 @@ class ForwardDemodulationImpl private: }; +using ForwardDemodulationExtra = RewriteInferenceExtra; }; diff --git a/Inferences/ProofExtra.cpp b/Inferences/ProofExtra.cpp index baaaa5cbc..b088f8f2f 100644 --- a/Inferences/ProofExtra.cpp +++ b/Inferences/ProofExtra.cpp @@ -29,14 +29,13 @@ void TwoLiteralInferenceExtra::output(std::ostream &out) const { } void RewriteInferenceExtra::output(std::ostream &out) const { - out << "side=" << reversed; + out << "lhs=" << lhs << ",target=" << target; } -void RewriteIntoInferenceExtra::output(std::ostream &out) const { +void TwoLiteralRewriteInferenceExtra::output(std::ostream &out) const { TwoLiteralInferenceExtra::output(out); out << ','; RewriteInferenceExtra::output(out); - out << ",rewritten=" << rewritten; } } // namespace Inferences diff --git a/Inferences/ProofExtra.hpp b/Inferences/ProofExtra.hpp index b443c4310..a5cf7abf6 100644 --- a/Inferences/ProofExtra.hpp +++ b/Inferences/ProofExtra.hpp @@ -45,29 +45,26 @@ struct TwoLiteralInferenceExtra : public LiteralInferenceExtra { }; struct RewriteInferenceExtra : virtual public InferenceExtra { - RewriteInferenceExtra(bool reversed) : reversed(reversed) {} + RewriteInferenceExtra(Kernel::TermList lhs, Kernel::TermList target) + : lhs(lhs), target(target) {} virtual void output(std::ostream &out) const override; - // if true, rewrite RHS to LHS - bool reversed; + // the LHS used to rewrite with + Kernel::TermList lhs; + // the rewritten term + Kernel::TermList target; }; -struct RewriteIntoInferenceExtra : public TwoLiteralInferenceExtra, public RewriteInferenceExtra { - RewriteIntoInferenceExtra( +struct TwoLiteralRewriteInferenceExtra : public TwoLiteralInferenceExtra, public RewriteInferenceExtra { + TwoLiteralRewriteInferenceExtra( Kernel::Literal *selected, Kernel::Literal *other, - bool reversed, + Kernel::TermList target, Kernel::TermList rewritten - ) : - TwoLiteralInferenceExtra(selected, other), - RewriteInferenceExtra(reversed), - rewritten(rewritten) {} + ) : TwoLiteralInferenceExtra(selected, other), RewriteInferenceExtra(target, rewritten) {} virtual void output(std::ostream &out) const override; - - // the rewritten term - Kernel::TermList rewritten; }; } diff --git a/Inferences/Superposition.cpp b/Inferences/Superposition.cpp index 866935717..9a4451b50 100644 --- a/Inferences/Superposition.cpp +++ b/Inferences/Superposition.cpp @@ -530,12 +530,12 @@ Clause* Superposition::performSuperposition( auto clause = Clause::fromStack(*res, inf); if(env.options->proofExtra()) - env.proofExtra.insert(clause, std::unique_ptr(new SuperpositionExtra( + env.proofExtra.insert(clause, new SuperpositionExtra( rwLit, eqLit, - eqLHS == (*eqLit)[1], + eqLHS, rwTerm - ))); + )); return clause; } diff --git a/Inferences/Superposition.hpp b/Inferences/Superposition.hpp index bf62b5b92..f9ff1434c 100644 --- a/Inferences/Superposition.hpp +++ b/Inferences/Superposition.hpp @@ -62,7 +62,7 @@ class Superposition SuperpositionLHSIndex* _lhsIndex; }; -using SuperpositionExtra = RewriteIntoInferenceExtra; +using SuperpositionExtra = TwoLiteralRewriteInferenceExtra; }; diff --git a/Lib/ProofExtra.hpp b/Lib/ProofExtra.hpp index 5865d2123..75c1402c1 100644 --- a/Lib/ProofExtra.hpp +++ b/Lib/ProofExtra.hpp @@ -46,9 +46,9 @@ class ProofExtra { DHMap> extras; public: - // associate `extra` with `unit` - void insert(Kernel::Unit *unit, std::unique_ptr extra) { - extras.insert(unit, std::move(extra)); + // associate `extra` with `unit`, taking ownership of `extra` + void insert(Kernel::Unit *unit, InferenceExtra *extra) { + extras.insert(unit, std::unique_ptr(extra)); } // remove the extra information for this unit From 305297131e88153c50d495e69d311fd75b602e4e Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Mon, 23 Sep 2024 11:04:01 +0100 Subject: [PATCH 3/3] keep the free class of proof_extra --- Inferences/BackwardDemodulation.cpp | 2 +- Inferences/BinaryResolution.cpp | 2 +- Inferences/EqualityResolution.cpp | 2 +- Inferences/ForwardDemodulation.cpp | 2 +- Inferences/Superposition.cpp | 2 +- Kernel/Clause.cpp | 4 ++-- Kernel/Unit.cpp | 12 +++++++----- Shell/Options.cpp | 9 ++++++--- Shell/Options.hpp | 9 +++++++-- 9 files changed, 27 insertions(+), 17 deletions(-) diff --git a/Inferences/BackwardDemodulation.cpp b/Inferences/BackwardDemodulation.cpp index f3474e12b..ebd00a31c 100644 --- a/Inferences/BackwardDemodulation.cpp +++ b/Inferences/BackwardDemodulation.cpp @@ -180,7 +180,7 @@ struct BackwardDemodulation::ResultFn *resLits, SimplifyingInference2(InferenceRule::BACKWARD_DEMODULATION, qr.data->clause, _cl) ); - if(env.options->proofExtra()) + if(env.options->proofExtra() == Options::ProofExtra::FULL) env.proofExtra.insert(replacement, new BackwardDemodulationExtra(lhs, lhsS)); return BwSimplificationRecord(qr.data->clause, replacement); } diff --git a/Inferences/BinaryResolution.cpp b/Inferences/BinaryResolution.cpp index 18a7d66b9..b80dae276 100644 --- a/Inferences/BinaryResolution.cpp +++ b/Inferences/BinaryResolution.cpp @@ -241,7 +241,7 @@ Clause* BinaryResolution::generateClause( inf_destroyer.disable(); // ownership passed to the the clause below Clause *cl = Clause::fromStack(*resLits, inf); - if(env.options->proofExtra()) + if(env.options->proofExtra() == Options::ProofExtra::FULL) env.proofExtra.insert(cl, new BinaryResolutionExtra(queryLit, resultLit)); return cl; diff --git a/Inferences/EqualityResolution.cpp b/Inferences/EqualityResolution.cpp index e9c84b450..5a1ca2aae 100644 --- a/Inferences/EqualityResolution.cpp +++ b/Inferences/EqualityResolution.cpp @@ -128,7 +128,7 @@ struct EqualityResolution::ResultFn env.statistics->equalityResolution++; Clause *cl = Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::EQUALITY_RESOLUTION, _cl)); - if(env.options->proofExtra()) + if(env.options->proofExtra() == Options::ProofExtra::FULL) env.proofExtra.insert(cl, new EqualityResolutionExtra(lit)); return cl; } diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp index ed988cc2c..9f2f0878d 100644 --- a/Inferences/ForwardDemodulation.cpp +++ b/Inferences/ForwardDemodulation.cpp @@ -224,7 +224,7 @@ bool ForwardDemodulationImpl::perform(Clause* cl, Clause* premises = pvi( getSingletonIterator(qr.data->clause)); replacement = Clause::fromStack(*resLits, SimplifyingInference2(InferenceRule::FORWARD_DEMODULATION, cl, qr.data->clause)); - if(env.options->proofExtra()) + if(env.options->proofExtra() == Options::ProofExtra::FULL) env.proofExtra.insert(replacement, new ForwardDemodulationExtra(lhs, trm)); return true; } diff --git a/Inferences/Superposition.cpp b/Inferences/Superposition.cpp index 9a4451b50..7cc844bb0 100644 --- a/Inferences/Superposition.cpp +++ b/Inferences/Superposition.cpp @@ -529,7 +529,7 @@ Clause* Superposition::performSuperposition( inf_destroyer.disable(); // ownership passed to the the clause below auto clause = Clause::fromStack(*res, inf); - if(env.options->proofExtra()) + if(env.options->proofExtra() == Options::ProofExtra::FULL) env.proofExtra.insert(clause, new SuperpositionExtra( rwLit, eqLit, diff --git a/Kernel/Clause.cpp b/Kernel/Clause.cpp index 3c96541be..ff5fcbe6e 100644 --- a/Kernel/Clause.cpp +++ b/Kernel/Clause.cpp @@ -219,7 +219,7 @@ void Clause::destroy() static Stack toDestroy(32); Clause* cl = this; for(;;) { - if (env.options->proofExtra()) { + if (env.options->proofExtra() == Options::ProofExtra::FULL) { env.proofExtra.remove(cl); } Inference::Iterator it = cl->_inference.iterator(); @@ -383,7 +383,7 @@ std::string Clause::toString() const // print inference and ids of parent clauses result += " " + inferenceAsString(); - if(env.options->proofExtra()){ + if(env.options->proofExtra() != Options::ProofExtra::OFF){ // print statistics: each entry should have the form key:value result += std::string(" {"); diff --git a/Kernel/Unit.cpp b/Kernel/Unit.cpp index 42848f69b..8c5165af4 100644 --- a/Kernel/Unit.cpp +++ b/Kernel/Unit.cpp @@ -168,11 +168,13 @@ std::string Unit::inferenceAsString() const } // print extra if present - auto *extra = env.proofExtra.find(this); - if(extra) { - if(!first) - result += ','; - result += extra->toString(); + if(env.options->proofExtra() == Options::ProofExtra::FULL) { + auto *extra = env.proofExtra.find(this); + if(extra) { + if(!first) + result += ','; + result += extra->toString(); + } } return result + ']'; diff --git a/Shell/Options.cpp b/Shell/Options.cpp index e7cd74683..26311f8a0 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -317,9 +317,12 @@ void Options::init() _lookup.insert(&_printProofToFile); _printProofToFile.tag(OptionTag::OUTPUT); - _proofExtra = BoolOptionValue("proof_extra","",false); - _proofExtra.description="Add extra detail to proofs in exchange for performance.\n" - "This option is still under development and the format of information may change."; + _proofExtra = ChoiceOptionValue("proof_extra","",ProofExtra::OFF,{"off","free","full"}); + _proofExtra.description="Add extra detail to proofs:\n " + "- free uses known information only\n" + "- full may perform expensive operations to achieve this so may" + " significantly impact on performance.\n" + " The option is still under development and the format of extra information (mainly from full) may change between minor releases"; _lookup.insert(&_proofExtra); _proofExtra.tag(OptionTag::OUTPUT); diff --git a/Shell/Options.hpp b/Shell/Options.hpp index c6a9c9843..809d6958a 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -298,6 +298,11 @@ class Options CHEAP }; + enum class ProofExtra : unsigned int { + OFF, + FREE, + FULL + }; enum class FMBWidgetOrders : unsigned int { FUNCTION_FIRST, // f(1) f(2) f(3) ... g(1) g(2) ... ARGUMENT_FIRST, // f(1) g(1) h(1) ... f(2) g(2) ... @@ -1944,7 +1949,7 @@ bool _hard; void setStatistics(Statistics newVal) { _statistics.actualValue=newVal; } Proof proof() const { return _proof.actualValue; } bool minimizeSatProofs() const { return _minimizeSatProofs.actualValue; } - bool proofExtra() const { return _proofExtra.actualValue; } + ProofExtra proofExtra() const { return _proofExtra.actualValue; } bool traceback() const { return _traceback.actualValue; } void setTraceback(bool traceback) { _traceback.actualValue = traceback; } std::string printProofToFile() const { return _printProofToFile.actualValue; } @@ -2581,7 +2586,7 @@ bool _hard; StringOptionValue _problemName; ChoiceOptionValue _proof; BoolOptionValue _minimizeSatProofs; - BoolOptionValue _proofExtra; + ChoiceOptionValue _proofExtra; BoolOptionValue _traceback; StringOptionValue _protectedPrefix;